Commit 4a2b5e8b authored by MARCHE Claude's avatar MARCHE Claude Committed by Guillaume Melquiond

Alt-Ergo: addd option -no-rm-eq-existential to prevent an Alt-Ergo bug

parent 5fcf22a9
...@@ -2,13 +2,9 @@ ...@@ -2,13 +2,9 @@
name = "Alt-Ergo" name = "Alt-Ergo"
exec = "alt-ergo" exec = "alt-ergo"
exec = "alt-ergo-1.00.prv" exec = "alt-ergo-1.00.prv"
exec = "alt-ergo-0.99.1"
exec = "alt-ergo-0.95.2"
version_switch = "-version" version_switch = "-version"
version_regexp = "^\\([0-9.]+\\(-dev\\|prv\\)?\\)$" version_regexp = "^\\([0-9.]+\\(-dev\\|prv\\)?\\)$"
version_ok = "1.00.prv" version_ok = "1.00.prv"
version_ok = "0.99.1"
version_ok = "0.95.2"
# %T means timelimit+1 # %T means timelimit+1
command = "%l/why3-cpulimit %T %m -s %e -timelimit %t %f" command = "%l/why3-cpulimit %T %m -s %e -timelimit %t %f"
# %U means 2*timelimit+1 # %U means 2*timelimit+1
...@@ -16,6 +12,22 @@ command_steps = "%l/why3-cpulimit %U %m -s %e -steps-bound %S %f" ...@@ -16,6 +12,22 @@ command_steps = "%l/why3-cpulimit %U %m -s %e -steps-bound %S %f"
driver = "drivers/alt_ergo.drv" driver = "drivers/alt_ergo.drv"
editor = "altgr-ergo" editor = "altgr-ergo"
[ATP alt-ergo]
name = "Alt-Ergo"
exec = "alt-ergo"
exec = "alt-ergo-0.99.1"
exec = "alt-ergo-0.95.2"
version_switch = "-version"
version_regexp = "^\\([0-9.]+\\)$"
version_ok = "0.99.1"
version_ok = "0.95.2"
# %T means timelimit+1
command = "%l/why3-cpulimit %T %m -s %e -no-rm-eq-existential -timelimit %t %f"
# %U means 2*timelimit+1
command_steps = "%l/why3-cpulimit %U %m -s %e -no-rm-eq-existential -steps-bound %S %f"
driver = "drivers/alt_ergo.drv"
editor = "altgr-ergo"
[ATP alt-ergo] [ATP alt-ergo]
name = "Alt-Ergo" name = "Alt-Ergo"
exec = "alt-ergo" exec = "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