Commit 45b47429 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

Fixed bug 13002

parent 18b6c0cb
......@@ -73,6 +73,14 @@ theory int.Int
end
theory real.Real
remove prop ZeroLessOne
remove prop NonTrivialRing
end
(*
Local Variables:
mode: why
......
theory T
use real.Real
goal toto: true
end
module M
use import module ref.Ref
val x : ref int
let f () : int =
{ }
!x
{ result = !x }
end
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/usr/local/share/why3/why3session.dtd">
<why3session
name="./check-builtin/array/why3session.xml">
name="examples/check-builtin/array/why3session.xml">
<prover
id="0"
name="Alt-Ergo"
......@@ -12,39 +12,51 @@
version="2.2"/>
<prover
id="2"
name="CVC3"
version="2.4.1"/>
<prover
id="3"
name="Simplify"
version="1.5.4"/>
<prover
id="4"
name="Spass"
version="3.7"/>
<prover
id="3"
id="5"
name="Z3"
version="2.19"/>
<prover
id="6"
name="Z3"
version="3.2"/>
<file
name="../array.why"
verified="true"
expanded="false">
expanded="true">
<theory
name="Test_simplify_array"
locfile="./check-builtin/array/../array.why"
locfile="examples/check-builtin/array/../array.why"
loclnum="1" loccnumb="7" loccnume="26"
verified="true"
expanded="true">
<goal
name="G1"
locfile="./check-builtin/array/../array.why"
locfile="examples/check-builtin/array/../array.why"
loclnum="4" loccnumb="7" loccnume="9"
sum="4b45d6270f4a53daefb6fce54b8ebff7"
proved="true"
expanded="true"
shape="ainfix =agetasetV2V1V0V1V0FF">
<proof
prover="3"
prover="5"
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="2"
prover="4"
timelimit="10"
obsolete="false"
archived="false">
......@@ -64,24 +76,45 @@
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>
<proof
prover="3"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="G2"
locfile="./check-builtin/array/../array.why"
locfile="examples/check-builtin/array/../array.why"
loclnum="6" loccnumb="7" loccnume="9"
sum="6ccca0aeacb41ec5118c79435eb055a1"
proved="true"
expanded="true"
shape="ainfix =agetasetV5V0V4V3V1Iainfix =agetV5V3V1Iainfix =V3V0NFF">
<proof
prover="3"
prover="5"
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="2"
prover="4"
timelimit="10"
obsolete="false"
archived="false">
......@@ -101,24 +134,45 @@
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="2"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="6"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="3"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="G3"
locfile="./check-builtin/array/../array.why"
locfile="examples/check-builtin/array/../array.why"
loclnum="10" loccnumb="7" loccnume="9"
sum="6108a9e01a2539ed185406b5ade7ca86"
proved="true"
expanded="true"
shape="ainfix =agetasetV2c1V1c0V0Iainfix =agetV2c0V0FF">
<proof
prover="3"
prover="5"
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="2"
prover="4"
timelimit="10"
obsolete="false"
archived="false">
......@@ -138,24 +192,45 @@
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="2"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="6"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="3"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="G4"
locfile="./check-builtin/array/../array.why"
locfile="examples/check-builtin/array/../array.why"
loclnum="13" loccnumb="7" loccnume="9"
sum="34fa3208c06f03a03e0897d791b6fa13"
proved="true"
expanded="true"
shape="ainfix =agetasetasetV2c1V1c0V0c1V1FF">
<proof
prover="3"
prover="5"
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="2"
prover="4"
timelimit="10"
obsolete="false"
archived="false">
......@@ -175,6 +250,27 @@
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="2"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="6"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="3"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
</theory>
</file>
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/usr/local/share/why3/why3session.dtd">
<why3session
name="./check-builtin/int/why3session.xml">
name="examples/check-builtin/int/why3session.xml">
<prover
id="0"
name="Alt-Ergo"
......@@ -12,39 +12,47 @@
version="2.2"/>
<prover
id="2"
name="Simplify"
version="1.5.4"/>
<prover
id="3"
name="Spass"
version="3.7"/>
<prover
id="3"
id="4"
name="Z3"
version="2.19"/>
<prover
id="5"
name="Z3"
version="3.2"/>
<file
name="../int.why"
verified="true"
expanded="false">
expanded="true">
<theory
name="Test"
locfile="./check-builtin/int/../int.why"
locfile="examples/check-builtin/int/../int.why"
loclnum="1" loccnumb="7" loccnume="11"
verified="true"
expanded="true">
<goal
name="G1"
locfile="./check-builtin/int/../int.why"
locfile="examples/check-builtin/int/../int.why"
loclnum="3" loccnumb="7" loccnume="9"
sum="899a24cba5a3807f5638a16c2915002b"
proved="true"
expanded="true"
shape="ainfix =ainfix *c5c10c50">
<proof
prover="3"
prover="4"
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="2"
prover="3"
timelimit="10"
obsolete="false"
archived="false">
......@@ -52,7 +60,7 @@
</proof>
<proof
prover="1"
timelimit="10"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
......@@ -64,24 +72,38 @@
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="5"
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>
</goal>
<goal
name="G2"
locfile="./check-builtin/int/../int.why"
locfile="examples/check-builtin/int/../int.why"
loclnum="4" loccnumb="7" loccnume="9"
sum="15fea215e0e38f93607b4c66cdf45712"
proved="true"
expanded="true"
shape="ainfix =ainfix +ainfix -ainfix +V0V0V0V0ainfix *c2V0F">
<proof
prover="3"
prover="4"
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="2"
prover="3"
timelimit="10"
obsolete="false"
archived="false">
......@@ -89,7 +111,7 @@
</proof>
<proof
prover="1"
timelimit="10"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
......@@ -101,24 +123,38 @@
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="5"
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>
</goal>
<goal
name="CompatOrderAdd"
locfile="./check-builtin/int/../int.why"
locfile="examples/check-builtin/int/../int.why"
loclnum="6" loccnumb="7" loccnume="21"
sum="1b02d100b4d433ff30662e69e3b9a17b"
proved="true"
expanded="true"
shape="ainfix <=ainfix +V0V2ainfix +V1V2Iainfix <=V0V1F">
shape="ainfix &lt;=ainfix +V0V2ainfix +V1V2Iainfix &lt;=V0V1F">
<proof
prover="3"
prover="4"
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="2"
prover="3"
timelimit="10"
obsolete="false"
archived="false">
......@@ -126,7 +162,7 @@
</proof>
<proof
prover="1"
timelimit="10"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
......@@ -138,24 +174,38 @@
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="5"
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>
</goal>
<goal
name="CompatOrderMult"
locfile="./check-builtin/int/../int.why"
locfile="examples/check-builtin/int/../int.why"
loclnum="7" loccnumb="7" loccnume="22"
sum="7a34aecb05d3edc2b9ec4c9d5d672ce1"
proved="true"
expanded="true"
shape="ainfix <=ainfix *V0V2ainfix *V1V2Iainfix <=c0V2Iainfix <=V0V1F">
shape="ainfix &lt;=ainfix *V0V2ainfix *V1V2Iainfix &lt;=c0V2Iainfix &lt;=V0V1F">
<proof
prover="3"
prover="4"
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="2"
prover="3"
timelimit="10"
obsolete="false"
archived="false">
......@@ -163,7 +213,7 @@
</proof>
<proof
prover="1"
timelimit="10"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
......@@ -175,24 +225,38 @@
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="5"
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>
</goal>
<goal
name="InvMult"
locfile="./check-builtin/int/../int.why"
locfile="examples/check-builtin/int/../int.why"
loclnum="9" loccnumb="7" loccnume="14"
sum="2c3e1f709768ff692a56f392c66c8d6b"
proved="true"
expanded="true"
shape="ainfix =aprefix -ainfix *V0V1ainfix *V0aprefix -V1Aainfix =ainfix *aprefix -V0V1aprefix -ainfix *V0V1F">
<proof
prover="3"
prover="4"
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="2"
prover="3"
timelimit="10"
obsolete="false"
archived="false">
......@@ -200,7 +264,7 @@
</proof>
<proof
prover="1"
timelimit="10"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
......@@ -212,24 +276,38 @@
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="5"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="2"
timelimit="3"
obsolete="false"
archived="false">
<result status="unknown" time="0.00"/>
</proof>
</goal>
<goal
name="InvSquare"
locfile="./check-builtin/int/../int.why"
locfile="examples/check-builtin/int/../int.why"
loclnum="10" loccnumb="7" loccnume="16"
sum="65639547594360d52d18d4f1f673482a"
proved="true"
expanded="true"
shape="ainfix =ainfix *V0V0ainfix *aprefix -V0aprefix -V0F">
<proof
prover="3"
prover="4"
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="2"
prover="3"
timelimit="10"
obsolete="false"
archived="false">
......@@ -237,7 +315,7 @@
</proof>
<proof
prover="1"
timelimit="10"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
......@@ -249,24 +327,38 @@
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="5"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="2"
timelimit="3"
obsolete="false"
archived="false">
<result status="unknown" time="0.00"/>
</proof>
</goal>
<goal
name="ZeroMult"
locfile="./check-builtin/int/../int.why"
locfile="examples/check-builtin/int/../int.why"
loclnum="11" loccnumb="7" loccnume="15"
sum="3ad2b227ce15783b5d94003f4f806a91"
proved="true"
expanded="true"
shape="ainfix =c0ainfix *c0V0Aainfix =ainfix *V0c0c0F">
<proof
prover="3"