Commit 3b375dd5 authored by MARCHE Claude's avatar MARCHE Claude

slight improvements of CVC4 driver, preparing the support for the "steps"...

slight improvements of CVC4 driver, preparing the support for the "steps" feature and the counter-examples
parent 714c4d8f
......@@ -8,6 +8,14 @@ prelude "(set-logic AUFNIRA)" (* how come bv is supported by cvc4 in this logi
import "smt-libv2.drv"
(* regexp for steps should match things like
smt::SmtEngine::resourceUnitsUsed, 1041
but not in the same line as the "valid" answer
*)
(* CVC4 division seems to be neither the Euclidean one, nor the Computer one *)
(*
theory int.EuclideanDivision
......
......@@ -86,18 +86,30 @@ version_old = "0.8"
command = "%l/why3-cpulimit %t %m -s %e %f"
driver = "drivers/alt_ergo_0.92.drv"
# CVC4 version 1.x
# CVC4 version 1.4 and 1.5-prerelease
[ATP cvc4]
name = "CVC4"
exec = "cvc4"
exec = "cvc4-1.5-prerelease"
exec = "cvc4-1.4"
version_switch = "--version"
version_regexp = "This is CVC4 version \\([^ \n\r]+\\)"
version_ok = "1.5-prerelease"
version_ok = "1.4"
driver = "drivers/cvc4.drv"
# --random-seed=42 is not needed as soon as --random-freq=0.0 by default
command = "%l/why3-cpulimit %T %m -s %e --tlimit-per=%t000 --lang=smt2 %f"
# CVC4 version 1.0 to 1.3
[ATP cvc4]
name = "CVC4"
exec = "cvc4"
exec = "cvc4-1.3"
exec = "cvc4-1.2"
exec = "cvc4-1.1"
exec = "cvc4-1.0"
version_switch = "--version"
version_regexp = "This is CVC4 version \\([^ \n\r]+\\)"
version_ok = "1.4"
version_old = "1.3"
version_old = "1.2"
version_old = "1.1"
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment