Commit f1f6ec36 authored by MARCHE Claude's avatar MARCHE Claude

CVC# bug is NOT fixed

parent 2d4bf231
......@@ -175,6 +175,8 @@ why3.conf
/examples/programs/binary_search_c/
/examples/programs/dijkstra/
/examples/why3bench.html
/examples/why3regtests.err
/examples/why3regtests.out
/examples/*/*.html
/examples/*/*/*.html
/examples/*/*/*/*.html
......
......@@ -164,6 +164,8 @@ See manual Section xx
== TODOs ==
* BUG CVC3 avec la division par 0, cf examples/tests-provers/cvc3.why
* DONE Document the Coq plugin and tactic
** DONE option timelimit <n>
** DONE renommer "coq-plugin" en "coq-tactic"
......
theory Test
use import real.Real
lemma test1 : forall x : real. x/ 0.0 = 0.0
lemma test2 : forall x:real. x/x=1.0
lemma test3 : false
end
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/usr/local/share/why3/why3session.dtd">
<why3session
name="cvc3/why3session.xml">
<prover
id="0"
name="Alt-Ergo"
version="0.94"/>
<prover
id="1"
name="CVC3"
version="2.2"/>
<prover
id="2"
name="CVC3"
version="2.4.1"/>
<prover
id="3"
name="Z3"
version="2.19"/>
<prover
id="4"
name="Z3"
version="3.2"/>
<file
name="../cvc3.why"
verified="true"
expanded="true">
<theory
name="Test"
locfile="cvc3/../cvc3.why"
loclnum="3" loccnumb="7" loccnume="11"
verified="true"
expanded="true">
<goal
name="test1"
locfile="cvc3/../cvc3.why"
loclnum="7" loccnumb="8" loccnume="13"
sum="dc3cb70423d6eca6adecf25c7851eb72"
proved="true"
expanded="true"
shape="ainfix =ainfix /V0c0.0c0.0F">
<proof
prover="3"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.01"/>
</proof>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.00"/>
</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.00"/>
</proof>
<proof
prover="4"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.01"/>
</proof>
</goal>
<goal
name="test2"
locfile="cvc3/../cvc3.why"
loclnum="9" loccnumb="8" loccnume="13"
sum="22bd943d68d90a9351eac18fab347e1f"
proved="true"
expanded="true"
shape="ainfix =ainfix /V0V0c1.0F">
<proof
prover="3"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.04"/>
</proof>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.00"/>
</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.00"/>
</proof>
<proof
prover="4"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.04"/>
</proof>
</goal>
<goal
name="test3"
locfile="cvc3/../cvc3.why"
loclnum="11" loccnumb="8" loccnume="13"
sum="6d1f1ea06944f8f4e597d966b6d38fb2"
proved="true"
expanded="true"
shape="f">
<proof
prover="3"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.00"/>
</proof>
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.00"/>
</proof>
<proof
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.00"/>
</proof>
<proof
prover="4"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
</theory>
</file>
</why3session>
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment