Commit 6aecd3ff authored by MARCHE Claude's avatar MARCHE Claude

Workaround for the Alt-Ergo-0.94 bug on modulo which can become negative

parent 2bfff3b8
......@@ -5,6 +5,17 @@ theory BuiltIn
meta "eliminate_algebraic" "keep_recs"
end
theory int.EuclideanDivision
(* workaround for the "-1 % 32 = -1" bug *)
prelude "logic safe_modulo: int, int -> int"
prelude "axiom safe_modulo_def: forall x, y:int. x >= 0 and y > 0 -> safe_modulo(x,y) = x % y"
syntax function div "(%1 / %2)"
syntax function mod "safe_modulo(%1,%2)"
end
theory map.Map
syntax type map "(%1,%2) farray"
......
......@@ -69,13 +69,6 @@ theory int.Int
end
theory int.EuclideanDivision
syntax function div "(%1 / %2)"
syntax function mod "(%1 % %2)"
end
theory real.Real
......
import "alt_ergo.drv"
import "alt_ergo_bare.drv"
theory BuiltIn
meta "printer_option" "show_labels"
meta "eliminate_algebraic" "keep_enums"
meta "eliminate_algebraic" "keep_recs"
end
theory int.EuclideanDivision
syntax function div "(%1 / %2)"
syntax function mod "(%1 % %2)"
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
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<why3session
name="check-builtin/euclideandivision/why3session.xml">
name="euclideandivision/why3session.xml">
<prover
id="0"
name="Alt-Ergo"
version="0.94"/>
<prover
id="1"
name="Alt-Ergo"
version="0.95-dev"/>
<prover
id="2"
name="CVC3"
version="2.2"/>
<prover
id="2"
id="3"
name="Spass"
version="3.7"/>
<prover
id="3"
id="4"
name="Z3"
version="2.19"/>
<file
name="../euclideandivision.why"
verified="true"
expanded="false">
expanded="true">
<theory
name="Test"
locfile="check-builtin/euclideandivision/../euclideandivision.why"
locfile="euclideandivision/../euclideandivision.why"
loclnum="1" loccnumb="7" loccnume="11"
verified="true"
expanded="true">
<goal
name="G1"
locfile="check-builtin/euclideandivision/../euclideandivision.why"
locfile="euclideandivision/../euclideandivision.why"
loclnum="3" loccnumb="12" loccnume="14"
sum="73c47861b347211a7dc97e723e8ebc83"
proved="true"
expanded="true"
shape="ainfix =amodc10c3c1">
<proof
prover="3"
prover="4"
timelimit="10"
memlimit="0"
obsolete="false"
......@@ -45,7 +49,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="2"
prover="3"
timelimit="10"
memlimit="0"
obsolete="false"
......@@ -53,7 +57,7 @@
<result status="timeout" time="10.09"/>
</proof>
<proof
prover="1"
prover="2"
timelimit="10"
memlimit="0"
obsolete="false"
......@@ -62,8 +66,17 @@
</proof>
<proof
prover="0"
timelimit="10"
memlimit="0"
timelimit="3"
memlimit="1000"
edited="euclideandivision-Test-G1_1.why"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="1"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
......@@ -71,14 +84,14 @@
</goal>
<goal
name="G2"
locfile="check-builtin/euclideandivision/../euclideandivision.why"
locfile="euclideandivision/../euclideandivision.why"
loclnum="4" loccnumb="12" loccnume="14"
sum="eeac5b4c0d8433540bfca1c4d506ff93"
proved="true"
expanded="true"
shape="ainfix =adivc10c3c3">
<proof
prover="3"
prover="4"
timelimit="10"
memlimit="0"
obsolete="false"
......@@ -86,7 +99,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="2"
prover="3"
timelimit="10"
memlimit="0"
obsolete="false"
......@@ -94,7 +107,7 @@
<result status="timeout" time="10.12"/>
</proof>
<proof
prover="1"
prover="2"
timelimit="10"
memlimit="0"
obsolete="false"
......@@ -103,8 +116,16 @@
</proof>
<proof
prover="0"
timelimit="10"
memlimit="0"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="1"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
......
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