Workaround for division bug in CVC3

drivers/cvc3_bare.drv

@@ -74,15 +74,23 @@ 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))));
+"
+
   syntax function zero "0"
   syntax function one  "1"
 
   syntax function (+)  "(%1 + %2)"
   syntax function (-)  "(%1 - %2)"
   syntax function (*)  "(%1 * %2)"
-  syntax function (/)  "(%1 / %2)"
+  syntax function (/)  "div_partial(%1,%2)"
   syntax function (-_) "(- %1)"
-  syntax function inv  "(1 / %1)"
+  syntax function inv  "inv_partial(%1)"
 
   syntax predicate (<=) "(%1 <= %2)"
   syntax predicate (<)  "(%1 < %2)"

examples/check-builtin/real/why3session.xml

 <?xml version="1.0" encoding="UTF-8"?>
-<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
+<!DOCTYPE why3session SYSTEM "/home/cmarche/recherche/why3/share/why3session.dtd">
 <why3session
- name="check-builtin/real/why3session.xml">
+ name="real/why3session.xml">
  <prover
   id="0"
   name="Alt-Ergo"
@@ -33,20 +33,20 @@
  <file
   name="../real.why"
   verified="false"
-  expanded="false">
+  expanded="true">
   <theory
    name="Test"
-   locfile="check-builtin/real/../real.why"
+   locfile="real/../real.why"
    loclnum="1" loccnumb="7" loccnume="11"
    verified="true"
-   expanded="false">
+   expanded="true">
    <goal
     name="G1"
-    locfile="check-builtin/real/../real.why"
+    locfile="real/../real.why"
     loclnum="3" loccnumb="7" loccnume="9"
     sum="7961c96b42f34e5cb3280ce85643dffb"
     proved="true"
-    expanded="false"
+    expanded="true"
     shape="ainfix =ainfix *c5.5c10.c55.">
     <proof
      prover="5"
@@ -58,7 +58,7 @@
     </proof>
     <proof
      prover="1"
-     timelimit="3"
+     timelimit="10"
      memlimit="0"
      obsolete="false"
      archived="false">
@@ -74,7 +74,7 @@
     </proof>
     <proof
      prover="2"
-     timelimit="3"
+     timelimit="10"
      memlimit="0"
      obsolete="false"
      archived="false">
@@ -107,11 +107,11 @@
    </goal>
    <goal
     name="G2"
-    locfile="check-builtin/real/../real.why"
+    locfile="real/../real.why"
     loclnum="4" loccnumb="7" loccnume="9"
     sum="b18a4b0fb8e663468863ba1c86a7cc64"
     proved="true"
-    expanded="false"
+    expanded="true"
     shape="ainfix =ainfix /c9.c3.c3.">
     <proof
      prover="5"
@@ -123,11 +123,11 @@
     </proof>
     <proof
      prover="1"
-     timelimit="3"
+     timelimit="10"
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.00"/>
+     <result status="valid" time="0.01"/>
     </proof>
     <proof
      prover="0"
@@ -139,7 +139,7 @@
     </proof>
     <proof
      prover="2"
-     timelimit="3"
+     timelimit="10"
      memlimit="0"
      obsolete="false"
      archived="false">
@@ -164,11 +164,11 @@
    </goal>
    <goal
     name="G3"
-    locfile="check-builtin/real/../real.why"
+    locfile="real/../real.why"
     loclnum="5" loccnumb="7" loccnume="9"
     sum="297dff92907d47bda80a8ffe2d186396"
     proved="true"
-    expanded="false"
+    expanded="true"
     shape="ainfix =ainvc5.c0.2">
     <proof
      prover="5"
@@ -180,7 +180,7 @@
     </proof>
     <proof
      prover="1"
-     timelimit="3"
+     timelimit="10"
      memlimit="0"
      obsolete="false"
      archived="false">
@@ -196,11 +196,11 @@
     </proof>
     <proof
      prover="2"
-     timelimit="3"
+     timelimit="10"
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.00"/>
+     <result status="valid" time="0.01"/>
     </proof>
     <proof
      prover="3"
@@ -222,17 +222,17 @@
   </theory>
   <theory
    name="TestInfix"
-   locfile="check-builtin/real/../real.why"
+   locfile="real/../real.why"
    loclnum="8" loccnumb="7" loccnume="16"
    verified="true"
-   expanded="false">
+   expanded="true">
    <goal
     name="Add"
-    locfile="check-builtin/real/../real.why"
+    locfile="real/../real.why"
     loclnum="10" loccnumb="7" loccnume="10"
     sum="43afbf3638f15444ec33376879694c6b"
     proved="true"
-    expanded="false"
+    expanded="true"
     shape="ainfix =ainfix +.c5.5c10.c15.5">
     <proof
      prover="5"
@@ -244,7 +244,7 @@
     </proof>
     <proof
      prover="1"
-     timelimit="3"
+     timelimit="10"
      memlimit="0"
      obsolete="false"
      archived="false">
@@ -260,7 +260,7 @@
     </proof>
     <proof
      prover="2"
-     timelimit="3"
+     timelimit="10"
      memlimit="0"
      obsolete="false"
      archived="false">
@@ -285,11 +285,11 @@
    </goal>
    <goal
     name="Sub"
-    locfile="check-builtin/real/../real.why"
+    locfile="real/../real.why"
     loclnum="11" loccnumb="7" loccnume="10"
     sum="9e26dca43231665f3c20276262e0e4ef"
     proved="true"
-    expanded="false"
+    expanded="true"
     shape="ainfix =ainfix -.c9.c3.c6.">
     <proof
      prover="5"
@@ -301,7 +301,7 @@
     </proof>
     <proof
      prover="1"
-     timelimit="3"
+     timelimit="10"
      memlimit="0"
      obsolete="false"
      archived="false">
@@ -317,7 +317,7 @@
     </proof>
     <proof
      prover="2"
-     timelimit="3"
+     timelimit="10"
      memlimit="0"
      obsolete="false"
      archived="false">
@@ -342,11 +342,11 @@
    </goal>
    <goal
     name="Neg"
-    locfile="check-builtin/real/../real.why"
+    locfile="real/../real.why"
     loclnum="12" loccnumb="7" loccnume="10"
     sum="4f3a94d0b96c33ec0276c6802921cd6a"
     proved="true"
-    expanded="false"
+    expanded="true"
     shape="ainfix =ainfix +.aprefix -.c5.c3.5aprefix -.c1.5">
     <proof
      prover="5"
@@ -358,7 +358,7 @@
     </proof>
     <proof
      prover="1"
-     timelimit="3"
+     timelimit="10"
      memlimit="0"
      obsolete="false"
      archived="false">
@@ -374,7 +374,7 @@
     </proof>
     <proof
      prover="2"
-     timelimit="3"
+     timelimit="10"
      memlimit="0"
      obsolete="false"
      archived="false">
@@ -399,11 +399,11 @@
    </goal>
    <goal
     name="Mul"
-    locfile="check-builtin/real/../real.why"
+    locfile="real/../real.why"
     loclnum="13" loccnumb="7" loccnume="10"
     sum="547a086bd1da4bd6a329f80d539f9e4f"
     proved="true"
-    expanded="false"
+    expanded="true"
     shape="ainfix =ainfix *.c5.5c10.c55.">
     <proof
      prover="5"
@@ -415,7 +415,7 @@
     </proof>
     <proof
      prover="1"
-     timelimit="3"
+     timelimit="10"
      memlimit="0"
      obsolete="false"
      archived="false">
@@ -431,7 +431,7 @@
     </proof>
     <proof
      prover="2"
-     timelimit="3"
+     timelimit="10"
      memlimit="0"
      obsolete="false"
      archived="false">
@@ -456,11 +456,11 @@
    </goal>
    <goal
     name="Div"
-    locfile="check-builtin/real/../real.why"
+    locfile="real/../real.why"
     loclnum="14" loccnumb="7" loccnume="10"
     sum="11f3cf0fd8346c98624030a58cf9940a"
     proved="true"
-    expanded="false"
+    expanded="true"
     shape="ainfix =ainfix /.c9.c2.c4.5">
     <proof
      prover="5"
@@ -472,7 +472,7 @@
     </proof>
     <proof
      prover="1"
-     timelimit="3"
+     timelimit="10"
      memlimit="0"
      obsolete="false"
      archived="false">
@@ -488,11 +488,11 @@
     </proof>
     <proof
      prover="2"
-     timelimit="3"
+     timelimit="10"
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.00"/>
+     <result status="valid" time="0.01"/>
     </proof>
     <proof
      prover="3"
@@ -513,11 +513,11 @@
    </goal>
    <goal
     name="Inv"
-    locfile="check-builtin/real/../real.why"
+    locfile="real/../real.why"
     loclnum="15" loccnumb="7" loccnume="10"
     sum="70900cabfcc887614c28215d0ac16b18"
     proved="true"
-    expanded="false"
+    expanded="true"
     shape="ainfix =ainvc5.c0.2">
     <proof
      prover="5"
@@ -529,7 +529,7 @@
     </proof>
     <proof
      prover="1"
-     timelimit="3"
+     timelimit="10"
      memlimit="0"
      obsolete="false"
      archived="false">
@@ -545,11 +545,11 @@
     </proof>
     <proof
      prover="2"
-     timelimit="3"
+     timelimit="10"
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.00"/>
+     <result status="valid" time="0.01"/>
     </proof>
     <proof
      prover="3"
@@ -571,17 +571,17 @@
   </theory>
   <theory
    name="SquareTest"
-   locfile="check-builtin/real/../real.why"
+   locfile="real/../real.why"
    loclnum="19" loccnumb="7" loccnume="17"
    verified="true"
-   expanded="false">
+   expanded="true">
    <goal
     name="Sqrt_zero"
-    locfile="check-builtin/real/../real.why"
+    locfile="real/../real.why"
     loclnum="23" loccnumb="8" loccnume="17"
     sum="07d931db2f76f36bb664b47c010a0842"
     proved="true"
-    expanded="false"
+    expanded="true"
     shape="ainfix =asqrtc0.0c0.0">
     <proof
      prover="5"
@@ -593,7 +593,7 @@
     </proof>
     <proof
      prover="1"
-     timelimit="3"
+     timelimit="10"
      memlimit="0"
      obsolete="false"
      archived="false">
@@ -609,11 +609,11 @@
     </proof>
     <proof
      prover="2"
-     timelimit="3"
+     timelimit="10"
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.00"/>
+     <result status="valid" time="0.01"/>
     </proof>
     <proof
      prover="6"
@@ -626,11 +626,11 @@
    </goal>
    <goal
     name="Sqrt_one"
-    locfile="check-builtin/real/../real.why"
+    locfile="real/../real.why"
     loclnum="24" loccnumb="8" loccnume="16"
     sum="7e296fe9986bd1fdabe51ad79f9d0769"
     proved="true"
-    expanded="false"
+    expanded="true"
     shape="ainfix =asqrtc1.0c1.0">
     <proof
      prover="5"
@@ -642,7 +642,7 @@
     </proof>
     <proof
      prover="1"
-     timelimit="3"
+     timelimit="10"
      memlimit="0"
      obsolete="false"
      archived="false">
@@ -658,7 +658,7 @@
     </proof>
     <proof
      prover="2"
-     timelimit="3"
+     timelimit="10"
      memlimit="0"
      obsolete="false"
      archived="false">
@@ -675,11 +675,11 @@
    </goal>
    <goal
     name="Sqrt_four"
-    locfile="check-builtin/real/../real.why"
+    locfile="real/../real.why"
     loclnum="25" loccnumb="8" loccnume="17"
     sum="d5f5001e27c8787c3384ab4f365ba3c3"
     proved="true"
-    expanded="false"
+    expanded="true"
     shape="ainfix =asqrtc4.0c2.0">
     <proof
      prover="5"
@@ -691,11 +691,11 @@
     </proof>
     <proof
      prover="1"
-     timelimit="3"
+     timelimit="10"
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.00"/>
+     <result status="valid" time="0.01"/>
     </proof>
     <proof
      prover="0"
@@ -707,7 +707,7 @@
     </proof>
     <proof
      prover="2"
-     timelimit="3"
+     timelimit="10"
      memlimit="0"
      obsolete="false"
      archived="false">
@@ -725,13 +725,13 @@
   </theory>
   <theory
    name="ExpLogTest"
-   locfile="check-builtin/real/../real.why"
+   locfile="real/../real.why"
    loclnum="29" loccnumb="7" loccnume="17"
    verified="true"
    expanded="true">
    <goal
     name="Log_e"
-    locfile="check-builtin/real/../real.why"
+    locfile="real/../real.why"
     loclnum="33" loccnumb="8" loccnume="13"
     sum="5d5559f827756f1d565d4171bbd37c0a"
     proved="true"
@@ -745,6 +745,14 @@
      archived="false">
      <result status="valid" time="0.00"/>
     </proof>
+    <proof
+     prover="1"
+     timelimit="10"
+     memlimit="0"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.00"/>
+    </proof>
     <proof
      prover="0"
      timelimit="3"
@@ -753,6 +761,14 @@
      archived="false">
      <result status="valid" time="0.00"/>
     </proof>
+    <proof
+     prover="2"
+     timelimit="10"
+     memlimit="0"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.01"/>
+    </proof>
     <proof
      prover="6"
      timelimit="3"
@@ -765,17 +781,17 @@
   </theory>
   <theory
    name="PowerIntTest"
-   locfile="check-builtin/real/../real.why"
+   locfile="real/../real.why"
    loclnum="38" loccnumb="7" loccnume="19"
    verified="true"
-   expanded="false">
+   expanded="true">
    <goal
     name="Pow_2_2"
-    locfile="check-builtin/real/../real.why"
+    locfile="real/../real.why"
     loclnum="42" loccnumb="8" loccnume="15"
     sum="445233a777aa7b9782354cc55191daf9"
     proved="true"
-    expanded="false"
+    expanded="true"
     shape="ainfix =apowerc2.0c2c4.0">
     <proof
      prover="5"
@@ -787,11 +803,11 @@
     </proof>
     <proof
      prover="1"
-     timelimit="3"
+     timelimit="10"
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="unknown" time="0.02"/>
+     <result status="unknown" time="0.05"/>
     </proof>
     <proof
      prover="0"
@@ -803,11 +819,11 @@
     </proof>
     <proof
      prover="2"
-     timelimit="3"
+     timelimit="10"
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="unknown" time="0.15"/>
+     <result status="unknown" time="0.25"/>
     </proof>
     <proof
      prover="6"
@@ -821,13 +837,13 @@
   </theory>
   <theory
    name="PowerRealTest"
-   locfile="check-builtin/real/../real.why"
+   locfile="real/../real.why"
    loclnum="47" loccnumb="7" loccnume="20"
    verified="true"
    expanded="true">
    <goal
     name="Pow_2_2"
-    locfile="check-builtin/real/../real.why"
+    locfile="real/../real.why"
     loclnum="51" loccnumb="8" loccnume="15"
     sum="49c4f6c2eab59fb473e72ca70d4774d9"
     proved="true"
@@ -841,6 +857,14 @@
      archived="false">
      <result status="valid" time="0.00"/>
     </proof>
+    <proof
+     prover="1"
+     timelimit="10"
+     memlimit="0"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.02"/>
+    </proof>
     <proof
      prover="0"
      timelimit="3"
@@ -849,6 +873,14 @@
      archived="false">
      <result status="valid" time="0.00"/>
     </proof>
+    <proof
+     prover="2"
+     timelimit="10"
+     memlimit="0"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.01"/>
+    </proof>
     <proof
      prover="6"
      timelimit="3"
@@ -861,13 +893,13 @@
   </theory>
   <theory
    name="TrigonometryTest"
-   locfile="check-builtin/real/../real.why"
+   locfile="real/../real.why"
    loclnum="56" loccnumb="7" loccnume="23"
    verified="false"
    expanded="true">
    <goal
     name="Cos_2_pi"
-    locfile="check-builtin/real/../real.why"
+    locfile="real/../real.why"
     loclnum="62" loccnumb="8" loccnume="16"
     sum="b933acc073bf2cd19bc7444f5fe7a44b"
     proved="true"
@@ -891,19 +923,19 @@
     </proof>
     <proof
      prover="1"
-     timelimit="3"
+     timelimit="10"
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.00"/>
+     <result status="valid" time="0.02"/>
     </proof>
     <proof
      prover="2"
-     timelimit="3"
+     timelimit="10"
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.00"/>
+     <result status="valid" time="0.01"/>
     </proof>
     <proof
      prover="6"
@@ -916,7 +948,7 @@
    </goal>
    <goal
     name="Sin_2_pi"
-    locfile="check-builtin/real/../real.why"
+    locfile="real/../real.why"
     loclnum="63" loccnumb="8" loccnume="16"
     sum="f9b7c2446bfea7d86251892545c2c7d3"
     proved="true"
@@ -940,19 +972,19 @@