Commit dc022e22 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Update Gappa driver.

parent f5690a9d
...@@ -70,25 +70,11 @@ theory int.Abs ...@@ -70,25 +70,11 @@ theory int.Abs
end end
(* wrong: Euclidean division is NOT division round down
e.g : div (-1) (-2) is 1, not 0 *)
(*
theory int.EuclideanDivision
syntax function div "int<dn>(%1 / %2)"
end
*)
(* Gappa <- 0.16.4 has a bug,
it says that div (-1) 2 can have any value *)
(*
theory int.ComputerDivision theory int.ComputerDivision
syntax function div "int<zr>(%1 / %2)" syntax function div "int<zr>(%1 / %2)"
end end
*)
theory real.Real theory real.Real
......
...@@ -158,16 +158,15 @@ driver = "drivers/eprover.drv" ...@@ -158,16 +158,15 @@ driver = "drivers/eprover.drv"
[ATP gappa] [ATP gappa]
name = "Gappa" name = "Gappa"
exec = "gappa" exec = "gappa"
exec = "gappa-0.16.4"
exec = "gappa-0.16.1"
exec = "gappa-0.16.0"
exec = "gappa-0.15.1" exec = "gappa-0.15.1"
exec = "gappa-0.14.1" exec = "gappa-0.14.1"
exec = "gappa-0.13.0"
exec = "gappa-0.12.3"
version_switch = "--version" version_switch = "--version"
version_regexp = "Gappa \\([^ \n]*\\)" version_regexp = "Gappa \\([^ \n]*\\)"
version_ok = "^0\.16\.[0-4]$" version_ok = "^0\.16\.[0-6]$"
version_ok = "^0\.1[4-5]\..+$" version_ok = "^0\.1[4-5]\..+$"
version_old = "^0\.1[1-2]\..+$" version_old = "^0\.1[1-3]\..+$"
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e -Eprecision=70" command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e -Eprecision=70"
driver = "drivers/gappa.drv" driver = "drivers/gappa.drv"
......
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