Skip to content

Commit 37e3adb

Browse files
committed
Revert back to default timeout of 0 for all provers.
1 parent 56e4539 commit 37e3adb

1 file changed

Lines changed: 3 additions & 14 deletions

File tree

src/main/scala/Config.scala

Lines changed: 3 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -186,24 +186,13 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
186186
valueName = "level"
187187
)
188188

189-
// cvc5 uses a different default timeout since per check timeouts are not supported.
190-
private val rawTimeout: ScallopOption[Int] = opt[Int]("timeout",
189+
val timeout: ScallopOption[Int] = opt[Int]("timeout",
191190
descr = ( "Time out after approx. n seconds. The timeout is for the whole verification, "
192-
+ s"not per method or proof obligation (default for ${Cvc5ProverStdIO.name} prover: 180"
193-
+"; default for all other provers: 0, i.e. no timeout."),
194-
default = None,
191+
+ "not per method or proof obligation (default: 0, i.e. no timeout)."),
192+
default = Some(0),
195193
noshort = true
196194
)
197195

198-
lazy val timeout: Int = rawTimeout.toOption match {
199-
case Some(t) => t
200-
// Not set, so compute default value based on prover selected.
201-
case _ => prover.toOption match {
202-
case Some(Cvc5ProverStdIO.name) => 180
203-
case _ => 0
204-
}
205-
}
206-
207196
val assertTimeout: ScallopOption[Int] = opt[Int]("assertTimeout",
208197
descr = ("Timeout (in ms) per SMT solver assertion (default: 0, i.e. no timeout)."
209198
+ s"Ignored when using the ${Cvc5ProverStdIO.name} prover."),

0 commit comments

Comments
 (0)