Commit 86869647 authored by Jean-Christophe's avatar Jean-Christophe

support for Yices2

parent 16a37e9f
......@@ -31,6 +31,9 @@ theory BuiltIn
syntax predicate (=) "(= %1 %2)"
meta "encoding : kept" type int
(* could we do this? *)
(* meta "eliminate_algebraic" "keep_enums" *)
end
theory int.Int
......
......@@ -91,6 +91,16 @@ version_old = "^1\.0\.1\.*$"
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e"
driver = "drivers/yices.drv"
[ATP yices2]
name = "Yices2"
exec = "yices"
exec = "yices-2.0.4"
version_switch = "--version"
version_regexp = "[Yices ]*\\([^ \n]+\\)\."
version_ok = "^2\.0\.4"
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e"
driver = "drivers/yices.drv"
[ATP eprover]
name = "Eprover"
exec = "eprover"
......
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