Commit 95fe29c7 authored by Andrei Paskevich's avatar Andrei Paskevich

records are not supported in Alt-Ergo 0.93

parent f4994e1d
import "alt_ergo_bare.drv"
theory BuiltIn
meta "eliminate_algebraic" "keep_enums"
end
theory map.Map
syntax type map "(%1,%2) farray"
syntax function get "(%1[%2])"
syntax function set "(%1[%2 <- %3])"
remove prop Select_eq
remove prop Select_neq
end
(*
Local Variables:
mode: why
compile-command: "make -C .. bench"
End:
*)
......@@ -2,11 +2,28 @@
name = "Alt-Ergo"
exec = "alt-ergo"
exec = "alt-ergo-0.94"
version_switch = "-version"
version_regexp = "\\([0-9.]+\\)"
version_ok = "0.94"
version_bad = "0.93.1"
version_bad = "0.93"
version_bad = "0.92.3"
version_bad = "0.92.2"
version_bad = "0.92.1"
version_bad = "0.92"
version_bad = "0.91"
version_bad = "0.9"
version_bad = "0.8"
command = "@LOCALBIN@why3-cpulimit %t %m -s %e %f"
driver = "drivers/alt_ergo.drv"
[ATP alt-ergo]
name = "Alt-Ergo"
exec = "alt-ergo"
exec = "alt-ergo-0.93.1"
exec = "alt-ergo-0.93"
version_switch = "-version"
version_regexp = "\\([0-9.]+\\)"
version_ok = "0.94"
version_ok = "0.93.1"
version_ok = "0.93"
version_bad = "0.92.3"
......@@ -17,7 +34,7 @@ version_bad = "0.91"
version_bad = "0.9"
version_bad = "0.8"
command = "@LOCALBIN@why3-cpulimit %t %m -s %e %f"
driver = "drivers/alt_ergo.drv"
driver = "drivers/alt_ergo_0.93.drv"
[ATP alt-ergo]
name = "Alt-Ergo"
......
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