Commit 9381e853 authored by David Hauzar's avatar David Hauzar

Parsing step limit for CVC4.

parent 42143e80
......@@ -14,7 +14,7 @@ prelude ";; Enable model construction"
prelude "(set-option :produce-models true)"
(* Counterexamples: makes it possible to get rid of more quantifiers while introducing premises *)
(* transformation "split_intro" *)
(* transformation "split_goal_wp" *)
(* Counterexamples: get rid of some quantifiers - makes it possible to query model values of the variables in premises *)
transformation "introduce_premises"
......@@ -24,7 +24,6 @@ import "smt-libv2.drv"
(* regexp for steps *)
steps "smt::SmtEngine::resourceUnitsUsed, \\([0-9]+.?[0-9]*\\)" 1
(* CVC4 division seems to be neither the Euclidean one, nor the Computer one *)
(*
theory int.EuclideanDivision
......
......@@ -91,6 +91,7 @@ driver = "drivers/alt_ergo_0.92.drv"
name = "CVC4"
exec = "cvc4"
exec = "cvc4-1.5-prerelease"
exec = "cvc4-1.5"
version_switch = "--version"
version_regexp = "This is CVC4 version \\([^ \n\r]+\\)"
version_ok = "1.5-prerelease"
......@@ -114,6 +115,7 @@ driver = "drivers/cvc4.drv"
# cvc4 .14 does not print steps used in --stats anyway
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"
......
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