Commit 6d71591f authored by MARCHE Claude's avatar MARCHE Claude
Browse files

BEWARE: several drivers for int.EuclideanDivision are buggy

this includes Alt-Ergo both 0.94 and 0.95, and CVC4
parent 6585b235
theory EuclideanDivTest
use import int.Int
use import int.EuclideanDivision
goal ok1 : div (-1) (-2) = -1
goal ok2 : mod (-1) (-2) = 1
goal smoke1 : div (-1) (-2) = 0
goal smoke2 : mod (-1) (-2) = -1
end
theory ComputerDivTest
use import int.Int
use import int.ComputerDivision
goal ok1 : div (-1) (-2) = 0
goal ok2 : mod (-1) (-2) = -1
goal smoke1 : div (-1) (-2) = -1
goal smoke2 : mod (-1) (-2) = 1
end
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="2">
<prover
id="0"
name="Alt-Ergo"
version="0.93.1"/>
<prover
id="1"
name="Alt-Ergo"
version="0.94"/>
<prover
id="2"
name="Alt-Ergo"
version="0.95"/>
<prover
id="3"
name="CVC3"
version="2.2"/>
<prover
id="4"
name="CVC3"
version="2.4.1"/>
<prover
id="5"
name="CVC4"
version="1.0"/>
<prover
id="6"
name="Z3"
version="2.19"/>
<prover
id="7"
name="Z3"
version="3.2"/>
<prover
id="8"
name="Z3"
version="4.2"/>
<file
name="../div.why"
verified="false"
expanded="true">
<theory
name="EuclideanDivTest"
locfile="../div.why"
loclnum="2" loccnumb="7" loccnume="23"
verified="true"
expanded="true">
<goal
name="ok1"
locfile="../div.why"
loclnum="7" loccnumb="7" loccnume="10"
sum="bd1d5464857216da4e12f229f8c16af3"
proved="true"
expanded="true"
shape="ainfix =adivaprefix -c1aprefix -c2aprefix -c1">
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.11"/>
</proof>
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="3"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.05"/>
</proof>
<proof
prover="4"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.06"/>
</proof>
<proof
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.00"/>
</proof>
<proof
prover="6"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.09"/>
</proof>
<proof
prover="7"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.08"/>
</proof>
<proof
prover="8"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.13"/>
</proof>
</goal>
<goal
name="ok2"
locfile="../div.why"
loclnum="8" loccnumb="7" loccnume="10"
sum="9e8488ed0545855ca9592335972be12a"
proved="true"
expanded="true"
shape="ainfix =amodaprefix -c1aprefix -c2c1">
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="3"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="4"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.01"/>
</proof>
<proof
prover="6"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="7"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="8"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="smoke1"
locfile="../div.why"
loclnum="9" loccnumb="7" loccnume="13"
sum="221247d874c6afe4157d51833127b93a"
proved="true"
expanded="true"
shape="ainfix =adivaprefix -c1aprefix -c2c0">
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.06"/>
</proof>
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="3"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.07"/>
</proof>
<proof
prover="4"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.06"/>
</proof>
<proof
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="6"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.09"/>
</proof>
<proof
prover="7"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.08"/>
</proof>
<proof
prover="8"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.13"/>
</proof>
</goal>
<goal
name="smoke2"
locfile="../div.why"
loclnum="10" loccnumb="7" loccnume="13"
sum="b1ddfe4fa8fb15054feea09334b93e53"
proved="true"
expanded="true"
shape="ainfix =amodaprefix -c1aprefix -c2aprefix -c1">
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.14"/>
</proof>
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="3"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.08"/>
</proof>
<proof
prover="4"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.07"/>
</proof>
<proof
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="6"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.09"/>
</proof>
<proof
prover="7"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.18"/>
</proof>
<proof
prover="8"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.13"/>
</proof>
</goal>
</theory>
<theory
name="ComputerDivTest"
locfile="../div.why"
loclnum="14" loccnumb="7" loccnume="22"
verified="false"
expanded="true">
<goal
name="ok1"
locfile="../div.why"
loclnum="19" loccnumb="7" loccnume="10"
sum="a049c67265c44edafdd75a0224f9a5af"
proved="true"
expanded="true"
shape="ainfix =adivaprefix -c1aprefix -c2c0">
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="3"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="4"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="6"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="7"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="8"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal
name="ok2"
locfile="../div.why"
loclnum="20" loccnumb="7" loccnume="10"
sum="1d9061981705a2ad6ecfb97316a16e07"
proved="true"
expanded="true"
shape="ainfix =amodaprefix -c1aprefix -c2aprefix -c1">
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.08"/>
</proof>
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
</proof>
<proof
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="3"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="4"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="6"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="7"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="8"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="smoke1"
locfile="../div.why"
loclnum="21" loccnumb="7" loccnume="13"
sum="2eff424bf53bf22ef609bdbba225c8a6"
proved="false"
expanded="true"
shape="ainfix =adivaprefix -c1aprefix -c2aprefix -c1">
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.03"/>
</proof>
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.02"/>
</proof>
<proof
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.02"/>
</proof>
<proof
prover="3"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.21"/>
</proof>
<proof
prover="4"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.16"/>
</proof>
<proof
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.02"/>
</proof>
<proof
prover="6"
timelimit="5"
memlimit="1000"
obsolete="false"