Commit c11e26d5 authored by MARCHE Claude's avatar MARCHE Claude

Support for Alt-Ergo 1.00~beta (academia only)

detect it with

why3 config --add-prover alt-ergo /usr/local/bin/alt-ergo-1.00~beta.prv
parent 5030e3ae
......@@ -10,6 +10,7 @@ provers
o support for Coq 8.4pl5 (released Nov 7, 2014)
o support for Z3 4.3.2 (released Oct 25, 2014)
o support for MetiTarski 2.4 (released Oct 21, 2014)
o support for Alt-Ergo 0.99.1 (released Dec 30, 2014)
version 0.85, September 17, 2014
================================
......
......@@ -14,6 +14,7 @@ outofmemory "Fatal error: out of memory"
outofmemory "Fatal error: exception Stack_overflow"
fail "typing error:\\(.*\\)$" "Failure : File generation error : \\1"
time "Valid (%s) (%S)"
time "Valid (%s) (%S steps)"
time "why3cpulimit time : %s s"
(* À discuter *)
......
......@@ -4,7 +4,7 @@ exec = "alt-ergo"
exec = "alt-ergo-0.99.1"
exec = "alt-ergo-0.95.2"
version_switch = "-version"
version_regexp = "\\([0-9.]+\\(-dev\\)?\\)"
version_regexp = "\\([0-9.]+\\(-dev\\|~beta.prv\\)?\\)"
version_ok = "0.99.1"
version_ok = "0.95.2"
command = "%l/why3-cpulimit %t %m -s %e -timelimit %t -steps-bound %S %f"
......
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