Commit bff9fb1e authored by MARCHE Claude's avatar MARCHE Claude
Browse files

fix errors in test file for built-in reals

parent 64d0b83f
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session
name="intreal/why3session.xml">
name="check-builtin/intreal/why3session.xml">
<prover
id="0"
name="Alt-Ergo"
......@@ -41,18 +41,18 @@
<file
name="../intreal.why"
verified="true"
expanded="true">
expanded="false">
<theory
name="IntReal"
locfile="intreal/../intreal.why"
loclnum="1" loccnumb="7" loccnume="14"
locfile="check-builtin/intreal/../intreal.why"
loclnum="2" loccnumb="7" loccnume="14"
verified="true"
expanded="true">
<goal
name="G1"
locfile="intreal/../intreal.why"
loclnum="7" loccnumb="7" loccnume="9"
sum="f471c6c924b564aee8f4934746236ec5"
locfile="check-builtin/intreal/../intreal.why"
loclnum="8" loccnumb="7" loccnume="9"
sum="a3dff87b8d8fedb505c6359dde79722f"
proved="true"
expanded="true"
shape="ainfix =afrom_intc2c2.0">
......@@ -68,7 +68,7 @@
timelimit="10"
obsolete="false"
archived="false">
<result status="timeout" time="10.39"/>
<result status="timeout" time="10.06"/>
</proof>
<proof
prover="0"
......@@ -103,14 +103,14 @@
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="0.08"/>
<result status="valid" time="0.07"/>
</proof>
</goal>
<goal
name="G2"
locfile="intreal/../intreal.why"
loclnum="8" loccnumb="7" loccnume="9"
sum="a03422ffac4ca142a1a0e2945b8150b1"
locfile="check-builtin/intreal/../intreal.why"
loclnum="9" loccnumb="7" loccnume="9"
sum="d4b897b0551e058df4a9a889d20d247c"
proved="true"
expanded="true"
shape="ainfix =afloorc1.5c1">
......@@ -126,14 +126,14 @@
timelimit="10"
obsolete="false"
archived="false">
<result status="timeout" time="10.04"/>
<result status="timeout" time="10.10"/>
</proof>
<proof
prover="0"
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="3.42"/>
<result status="valid" time="3.19"/>
</proof>
<proof
prover="3"
......@@ -147,14 +147,14 @@
timelimit="10"
obsolete="false"
archived="false">
<result status="timeout" time="10.13"/>
<result status="timeout" time="10.12"/>
</proof>
</goal>
<goal
name="G3"
locfile="intreal/../intreal.why"
loclnum="9" loccnumb="7" loccnume="9"
sum="5a0b387c12f9700c3e3c3646efbd68aa"
locfile="check-builtin/intreal/../intreal.why"
loclnum="10" loccnumb="7" loccnume="9"
sum="92820ed54136bf4354490d405f16c848"
proved="true"
expanded="true"
shape="ainfix =aceilc1.5c2">
......@@ -163,21 +163,21 @@
timelimit="10"
obsolete="false"
archived="false">
<result status="timeout" time="10.13"/>
<result status="timeout" time="10.12"/>
</proof>
<proof
prover="5"
timelimit="10"
obsolete="false"
archived="false">
<result status="timeout" time="10.22"/>
<result status="timeout" time="10.05"/>
</proof>
<proof
prover="0"
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="3.94"/>
<result status="valid" time="4.03"/>
</proof>
<proof
prover="3"
......@@ -191,14 +191,14 @@
timelimit="10"
obsolete="false"
archived="false">
<result status="timeout" time="10.13"/>
<result status="timeout" time="10.12"/>
</proof>
</goal>
<goal
name="G4"
locfile="intreal/../intreal.why"
loclnum="10" loccnumb="7" loccnume="9"
sum="350db14fcb4c074460205c9f3bdfb7d7"
locfile="check-builtin/intreal/../intreal.why"
loclnum="11" loccnumb="7" loccnume="9"
sum="b7c53145c92254d781ba372f7a4a128b"
proved="true"
expanded="true"
shape="ainfix =aflooraprefix -.c1.5aprefix -c2">
......@@ -207,14 +207,14 @@
timelimit="10"
obsolete="false"
archived="false">
<result status="timeout" time="10.08"/>
<result status="timeout" time="10.12"/>
</proof>
<proof
prover="0"
timelimit="10"
obsolete="false"
archived="false">
<result status="timeout" time="10.01"/>
<result status="timeout" time="10.02"/>
</proof>
<proof
prover="3"
......@@ -228,14 +228,14 @@
timelimit="10"
obsolete="false"
archived="false">
<result status="timeout" time="10.04"/>
<result status="timeout" time="10.03"/>
</proof>
<proof
prover="8"
timelimit="10"
obsolete="false"
archived="false">
<result status="timeout" time="10.08"/>
<result status="timeout" time="10.13"/>
</proof>
<proof
prover="6"
......@@ -247,9 +247,9 @@
</goal>
<goal
name="G5"
locfile="intreal/../intreal.why"
loclnum="11" loccnumb="7" loccnume="9"
sum="fe76735f57427088f9dc7c492260de1d"
locfile="check-builtin/intreal/../intreal.why"
loclnum="12" loccnumb="7" loccnume="9"
sum="87b623f4677e9fef5a35fc06bd420bc8"
proved="true"
expanded="true"
shape="ainfix =aceilaprefix -.c1.5aprefix -c1">
......@@ -265,14 +265,14 @@
timelimit="10"
obsolete="false"
archived="false">
<result status="timeout" time="10.38"/>
<result status="timeout" time="10.56"/>
</proof>
<proof
prover="0"
timelimit="10"
obsolete="false"
archived="false">
<result status="timeout" time="10.02"/>
<result status="timeout" time="10.03"/>
</proof>
<proof
prover="3"
......@@ -291,9 +291,9 @@
</goal>
<goal
name="G6"
locfile="intreal/../intreal.why"
loclnum="12" loccnumb="7" loccnume="9"
sum="35b4ccc44d873f0925f27ecf4bc7ebe1"
locfile="check-builtin/intreal/../intreal.why"
loclnum="13" loccnumb="7" loccnume="9"
sum="d3a0d063178687050ff7243e9938885c"
proved="true"
expanded="true"
shape="ainfix <=afloorV0aceilV0F">
......@@ -302,14 +302,14 @@
timelimit="10"
obsolete="false"
archived="false">
<result status="timeout" time="10.13"/>
<result status="timeout" time="10.03"/>
</proof>
<proof
prover="5"
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="0.28"/>
<result status="valid" time="0.29"/>
</proof>
<proof
prover="0"
......@@ -349,9 +349,9 @@
</goal>
<goal
name="G7"
locfile="intreal/../intreal.why"
loclnum="13" loccnumb="7" loccnume="9"
sum="ef9cf6577bfe5fa811d8cab87076ba52"
locfile="check-builtin/intreal/../intreal.why"
loclnum="14" loccnumb="7" loccnume="9"
sum="9fcfef9104182d119649f34b0174b552"
proved="true"
expanded="true"
shape="ainfix =afrom_intafloorV0V0NIainfix <afloorV0aceilV0F">
......@@ -367,7 +367,7 @@
timelimit="10"
obsolete="false"
archived="false">
<result status="timeout" time="10.03"/>
<result status="timeout" time="10.35"/>
</proof>
<proof
prover="0"
......
......@@ -55,9 +55,9 @@ end
theory TrigonometryTest
use import Real
use import Trigonometry
use import Square
use import real.Real
use import real.Trigonometry
use import real.Square
lemma Cos_2_pi : cos (2.0 * pi) = 1.0
lemma Sin_2_pi : sin (2.0 * pi) = 0.
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session
name="real/why3session.xml">
name="examples/check-builtin/real/why3session.xml">
<prover
id="0"
name="Alt-Ergo"
......@@ -32,21 +32,21 @@
version="3.2"/>
<file
name="../real.why"
verified="true"
verified="false"
expanded="true">
<theory
name="Test"
locfile="real/../real.why"
locfile="examples/check-builtin/real/../real.why"
loclnum="1" loccnumb="7" loccnume="11"
verified="true"
expanded="true">
expanded="false">
<goal
name="G1"
locfile="real/../real.why"
locfile="examples/check-builtin/real/../real.why"
loclnum="3" loccnumb="7" loccnume="9"
sum="7961c96b42f34e5cb3280ce85643dffb"
proved="true"
expanded="true"
expanded="false"
shape="ainfix =ainfix *c5.5c10.c55.">
<proof
prover="5"
......@@ -100,11 +100,11 @@
</goal>
<goal
name="G2"
locfile="real/../real.why"
locfile="examples/check-builtin/real/../real.why"
loclnum="4" loccnumb="7" loccnume="9"
sum="b18a4b0fb8e663468863ba1c86a7cc64"
proved="true"
expanded="true"
expanded="false"
shape="ainfix =ainfix /c9.c3.c3.">
<proof
prover="5"
......@@ -151,11 +151,11 @@
</goal>
<goal
name="G3"
locfile="real/../real.why"
locfile="examples/check-builtin/real/../real.why"
loclnum="5" loccnumb="7" loccnume="9"
sum="297dff92907d47bda80a8ffe2d186396"
proved="true"
expanded="true"
expanded="false"
shape="ainfix =ainvc5.c0.2">
<proof
prover="5"
......@@ -203,17 +203,17 @@
</theory>
<theory
name="TestInfix"
locfile="real/../real.why"
locfile="examples/check-builtin/real/../real.why"
loclnum="8" loccnumb="7" loccnume="16"
verified="true"
expanded="true">
expanded="false">
<goal
name="Add"
locfile="real/../real.why"
locfile="examples/check-builtin/real/../real.why"
loclnum="10" loccnumb="7" loccnume="10"
sum="43afbf3638f15444ec33376879694c6b"
proved="true"
expanded="true"
expanded="false"
shape="ainfix =ainfix +.c5.5c10.c15.5">
<proof
prover="5"
......@@ -260,11 +260,11 @@
</goal>
<goal
name="Sub"
locfile="real/../real.why"
locfile="examples/check-builtin/real/../real.why"
loclnum="11" loccnumb="7" loccnume="10"
sum="9e26dca43231665f3c20276262e0e4ef"
proved="true"
expanded="true"
expanded="false"
shape="ainfix =ainfix -.c9.c3.c6.">
<proof
prover="5"
......@@ -311,11 +311,11 @@
</goal>
<goal
name="Neg"
locfile="real/../real.why"
locfile="examples/check-builtin/real/../real.why"
loclnum="12" loccnumb="7" loccnume="10"
sum="4f3a94d0b96c33ec0276c6802921cd6a"
proved="true"
expanded="true"
expanded="false"
shape="ainfix =ainfix +.aprefix -.c5.c3.5aprefix -.c1.5">
<proof
prover="5"
......@@ -362,11 +362,11 @@
</goal>
<goal
name="Mul"
locfile="real/../real.why"
locfile="examples/check-builtin/real/../real.why"
loclnum="13" loccnumb="7" loccnume="10"
sum="547a086bd1da4bd6a329f80d539f9e4f"
proved="true"
expanded="true"
expanded="false"
shape="ainfix =ainfix *.c5.5c10.c55.">
<proof
prover="5"
......@@ -413,11 +413,11 @@
</goal>
<goal
name="Div"
locfile="real/../real.why"
locfile="examples/check-builtin/real/../real.why"
loclnum="14" loccnumb="7" loccnume="10"
sum="11f3cf0fd8346c98624030a58cf9940a"
proved="true"
expanded="true"
expanded="false"
shape="ainfix =ainfix /.c9.c2.c4.5">
<proof
prover="5"
......@@ -464,11 +464,11 @@
</goal>
<goal
name="Inv"
locfile="real/../real.why"
locfile="examples/check-builtin/real/../real.why"
loclnum="15" loccnumb="7" loccnume="10"
sum="70900cabfcc887614c28215d0ac16b18"
proved="true"
expanded="true"
expanded="false"
shape="ainfix =ainvc5.c0.2">
<proof
prover="5"
......@@ -514,5 +514,452 @@
</proof>
</goal>
</theory>
<theory
name="SquareTest"
locfile="examples/check-builtin/real/../real.why"
loclnum="19" loccnumb="7" loccnume="17"
verified="true"
expanded="false">
<goal
name="Sqrt_zero"
locfile="examples/check-builtin/real/../real.why"
loclnum="23" loccnumb="8" loccnume="17"
sum="07d931db2f76f36bb664b47c010a0842"
proved="true"
expanded="false"
shape="ainfix =asqrtc0.0c0.0">
<proof
prover="5"
timelimit="3"
obsolete="false"
archived="false">
<result status="unknown" time="0.00"/>
</proof>
<proof
prover="1"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="0"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="2"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="6"
timelimit="3"
obsolete="false"
archived="false">
<result status="unknown" time="0.00"/>
</proof>
</goal>
<goal
name="Sqrt_one"
locfile="examples/check-builtin/real/../real.why"
loclnum="24" loccnumb="8" loccnume="16"
sum="7e296fe9986bd1fdabe51ad79f9d0769"
proved="true"
expanded="false"
shape="ainfix =asqrtc1.0c1.0">
<proof
prover="5"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="1"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="0"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="2"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="6"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="Sqrt_four"
locfile="examples/check-builtin/real/../real.why"
loclnum="25" loccnumb="8" loccnume="17"
sum="d5f5001e27c8787c3384ab4f365ba3c3"
proved="true"
expanded="false"
shape="ainfix =asqrtc4.0c2.0">
<proof
prover="5"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="1"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="0"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="2"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="6"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
</theory>
<theory
name="ExpLogTest"
locfile="examples/check-builtin/real/../real.why"
loclnum="29" loccnumb="7" loccnume="17"
verified="true"
expanded="false">
<goal
name="Log_e"
locfile="examples/check-builtin/real/../real.why"
loclnum="33" loccnumb="8" loccnume="13"
sum="5d5559f827756f1d565d4171bbd37c0a"
proved="true"
expanded="false"
shape="ainfix =alogaec1.0">
<proof
prover="5"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="1"
timelimit="3"
obsolete="false"
archived="false">
<result status="highfailure" time="0.00"/>
</proof>
<proof
prover="0"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="2"
timelimit="3"
obsolete="false"
archived="false">
<result status="highfailure" time="0.00"/>
</proof>
<proof
prover="6"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
</theory>
<theory
name="PowerIntTest"
locfile="examples/check-builtin/real/../real.why"
loclnum="38" loccnumb="7" loccnume="19"
verified="true"
expanded="false">
<goal
name="Pow_2_2"
locfile="examples/check-builtin/real/../real.why"
loclnum="42" loccnumb="8" loccnume="15"
sum="445233a777aa7b9782354cc55191daf9"
proved="true"
expanded="false"
shape="ainfix =apowerc2.0c2c4.0">
<proof
prover="5"
timelimit="3"
obsolete="false"
archived="false">
<result status="timeout" time="3.02"/>