Commit 7c9ab69f authored by MARCHE Claude's avatar MARCHE Claude

fix division bug with CVC3

parent 813b6414
......@@ -74,13 +74,7 @@ theory real.Real
prelude "%%% this is a prelude for CVC3 real arithmetic"
prelude "inv_partial: (REAL) -> REAL;
ASSERT (FORALL (x : REAL): ((NOT (x = 0)) => (inv_partial(x) = (1 / x))));
div_partial: (REAL, REAL) -> REAL;
ASSERT
(FORALL (x : REAL, y : REAL):
((NOT (y = 0)) => (div_partial(x, y) = (x / y))));
"
prelude "div_by_zero: (REAL) -> REAL;"
syntax function zero "0"
syntax function one "1"
......@@ -88,9 +82,9 @@ theory real.Real
syntax function (+) "(%1 + %2)"
syntax function (-) "(%1 - %2)"
syntax function (*) "(%1 * %2)"
syntax function (/) "div_partial(%1,%2)"
syntax function (/) "(IF (%2 = 0) THEN (div_by_zero(%1)) ELSE (%1 / %2) ENDIF)"
syntax function (-_) "(- %1)"
syntax function inv "inv_partial(%1)"
syntax function inv "(IF (%1 = 0) THEN (div_by_zero(1)) ELSE (1 / %1) ENDIF)"
syntax predicate (<=) "(%1 <= %2)"
syntax predicate (<) "(%1 < %2)"
......
......@@ -30,7 +30,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.42"/>
<result status="valid" time="0.49"/>
</proof>
</goal>
</theory>
......
......@@ -31,7 +31,7 @@
edited="13849_T_x_2.v"
obsolete="false"
archived="false">
<result status="valid" time="0.43"/>
<result status="valid" time="0.49"/>
</proof>
</goal>
</theory>
......
......@@ -31,7 +31,7 @@
edited="13854_T_g_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.43"/>
<result status="valid" time="0.49"/>
</proof>
</goal>
<goal
......@@ -49,7 +49,7 @@
edited="13854_T_x_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.42"/>
<result status="valid" time="0.50"/>
</proof>
</goal>
</theory>
......
......@@ -119,7 +119,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="4"
......@@ -192,7 +192,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.14"/>
<result status="valid" time="0.15"/>
</proof>
<proof
prover="1"
......@@ -257,7 +257,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.21"/>
<result status="valid" time="0.23"/>
</proof>
<proof
prover="1"
......
......@@ -66,7 +66,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
......@@ -132,7 +132,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="1"
......
......@@ -50,7 +50,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="10.29"/>
<result status="timeout" time="9.98"/>
</proof>
<proof
prover="1"
......@@ -91,7 +91,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="10.12"/>
<result status="timeout" time="10.05"/>
</proof>
<proof
prover="1"
......
......@@ -76,7 +76,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="1"
......
......@@ -58,7 +58,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="10.78"/>
<result status="timeout" time="10.15"/>
</proof>
<proof
prover="1"
......@@ -115,7 +115,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="10.23"/>
<result status="timeout" time="10.16"/>
</proof>
<proof
prover="1"
......@@ -245,7 +245,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="5"
......@@ -286,7 +286,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="10.32"/>
<result status="timeout" time="10.13"/>
</proof>
<proof
prover="1"
......@@ -302,7 +302,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="5"
......@@ -343,7 +343,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="10.29"/>
<result status="timeout" time="10.03"/>
</proof>
<proof
prover="1"
......@@ -400,7 +400,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="10.35"/>
<result status="timeout" time="10.01"/>
</proof>
<proof
prover="1"
......@@ -457,7 +457,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="10.00"/>
<result status="timeout" time="10.07"/>
</proof>
<proof
prover="1"
......@@ -473,7 +473,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="5"
......@@ -514,7 +514,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="10.02"/>
<result status="timeout" time="9.99"/>
</proof>
<proof
prover="1"
......@@ -635,7 +635,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="10.05"/>
<result status="timeout" time="10.03"/>
</proof>
<proof
prover="1"
......@@ -651,7 +651,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="5"
......@@ -659,7 +659,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="2"
......
......@@ -70,7 +70,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="10.20"/>
<result status="timeout" time="10.02"/>
</proof>
<proof
prover="0"
......@@ -135,7 +135,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="10.74"/>
<result status="timeout" time="10.32"/>
</proof>
<proof
prover="0"
......@@ -143,7 +143,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="3.14"/>
<result status="valid" time="3.47"/>
</proof>
<proof
prover="3"
......@@ -159,7 +159,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
......@@ -184,7 +184,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="10.05"/>
<result status="timeout" time="10.11"/>
</proof>
<proof
prover="0"
......@@ -192,7 +192,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="3.86"/>
<result status="valid" time="4.28"/>
</proof>
<proof
prover="3"
......@@ -208,7 +208,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
......@@ -233,7 +233,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="10.03"/>
<result status="timeout" time="10.02"/>
</proof>
<proof
prover="3"
......@@ -249,7 +249,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="10.03"/>
<result status="timeout" time="10.02"/>
</proof>
<proof
prover="8"
......@@ -257,7 +257,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="6"
......@@ -282,7 +282,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="5"
......@@ -290,7 +290,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="10.17"/>
<result status="timeout" time="10.05"/>
</proof>
<proof
prover="0"
......@@ -339,7 +339,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.26"/>
<result status="valid" time="0.31"/>
</proof>
<proof
prover="0"
......@@ -379,7 +379,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
......@@ -404,7 +404,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="10.64"/>
<result status="timeout" time="10.09"/>
</proof>
<proof
prover="0"
......
......@@ -66,7 +66,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
......@@ -83,7 +83,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="2"
......@@ -91,7 +91,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="1"
......@@ -107,7 +107,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
</theory>
......
This diff is collapsed.
......@@ -56,7 +56,7 @@
verified="true"
expanded="true">
<label
name="Einstein's problem"/>
name="Einstein&apos;s problem"/>
</theory>
<theory
name="EinsteinClues"
......@@ -74,7 +74,7 @@
verified="false"
expanded="true">
<label
name="Goals about Einstein's problem"/>
name="Goals about Einstein&apos;s problem"/>
<goal
name="G1"
locfile="./einstein/../einstein.why"
......@@ -97,15 +97,15 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="3.00"/>
<result status="timeout" time="3.01"/>
</proof>
<proof
prover="0"
timelimit="17"
timelimit="19"
memlimit="0"
obsolete="false"
archived="false">
<result status="unknown" time="9.05"/>
<result status="unknown" time="9.83"/>
</proof>
<proof
prover="1"
......@@ -113,7 +113,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="2.40"/>
<result status="valid" time="3.19"/>
</proof>
<proof
prover="2"
......@@ -121,7 +121,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="2.00"/>
<result status="valid" time="2.69"/>
</proof>
<proof
prover="8"
......@@ -133,11 +133,11 @@
</proof>
<proof
prover="5"
timelimit="7"
timelimit="29"
memlimit="0"
obsolete="false"
archived="false">
<result status="unknown" time="6.98"/>
<result status="unknown" time="28.90"/>
</proof>
<proof
prover="6"
......@@ -153,7 +153,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="2.99"/>
<result status="timeout" time="2.98"/>
</proof>
</goal>
<goal
......@@ -170,7 +170,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="10.03"/>
<result status="timeout" time="10.02"/>
</proof>
<proof
prover="4"
......@@ -182,11 +182,11 @@
</proof>
<proof
prover="0"
timelimit="14"
timelimit="15"
memlimit="0"
obsolete="false"
archived="false">
<result status="unknown" time="6.70"/>
<result status="unknown" time="7.33"/>
</proof>
<proof
prover="1"
......@@ -194,7 +194,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="10.13"/>
<result status="timeout" time="10.12"/>
</proof>
<proof
prover="2"
......@@ -202,7 +202,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="10.13"/>
<result status="timeout" time="10.12"/>
</proof>
<proof
prover="8"
......@@ -214,11 +214,11 @@
</proof>
<proof
prover="5"
timelimit="7"
timelimit="29"
memlimit="0"
obsolete="false"
archived="false">
<result status="unknown" time="6.98"/>
<result status="unknown" time="28.93"/>
</proof>
<proof
prover="6"
......@@ -234,7 +234,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="2.98"/>
<result status="timeout" time="2.99"/>
</proof>
</goal>
<goal
......@@ -267,7 +267,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="unknown" time="6.70"/>
<result status="unknown" time="7.36"/>
</proof>
<proof
prover="1"
......@@ -275,7 +275,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="1.87"/>
<result status="valid" time="2.47"/>
</proof>
<proof
prover="2"
......@@ -283,7 +283,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="1.98"/>
<result status="valid" time="2.75"/>
</proof>
<proof
prover="8"
......@@ -291,15 +291,15 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.05"/>
<result status="valid" time="0.06"/>
</proof>
<proof
prover="5"
timelimit="7"
timelimit="29"
memlimit="0"
obsolete="false"
archived="false">
<result status="unknown" time="6.99"/>
<result status="unknown" time="28.91"/>
</proof>
<proof
prover="6"
......
......@@ -65,7 +65,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="4"
......@@ -81,7 +81,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="1"
......@@ -89,7 +89,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="2"
......@@ -97,7 +97,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="7"
......@@ -146,7 +146,7 @@
memlimit="0"
obsolete="false"
archived="false">