From f1f6ec366974cd979164c255cb7ad84232144013 Mon Sep 17 00:00:00 2001
From: Claude Marche <Claude.Marche@inria.fr>
Date: Wed, 9 May 2012 14:43:40 +0200
Subject: [PATCH] CVC# bug is NOT fixed

---
 .gitignore                                  |   2 +
 ROADMAP                                     |   2 +
 examples/tests-provers/cvc3.why             |  13 ++
 examples/tests-provers/cvc3/why3session.xml | 184 ++++++++++++++++++++
 4 files changed, 201 insertions(+)
 create mode 100644 examples/tests-provers/cvc3.why
 create mode 100644 examples/tests-provers/cvc3/why3session.xml

diff --git a/.gitignore b/.gitignore
index c707a4b16..ff79429d4 100644
--- a/.gitignore
+++ b/.gitignore
@@ -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
diff --git a/ROADMAP b/ROADMAP
index 000091c4a..c4b33cc6c 100644
--- a/ROADMAP
+++ b/ROADMAP
@@ -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"
diff --git a/examples/tests-provers/cvc3.why b/examples/tests-provers/cvc3.why
new file mode 100644
index 000000000..77a9ce514
--- /dev/null
+++ b/examples/tests-provers/cvc3.why
@@ -0,0 +1,13 @@
+
+
+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
diff --git a/examples/tests-provers/cvc3/why3session.xml b/examples/tests-provers/cvc3/why3session.xml
new file mode 100644
index 000000000..28d7c06a4
--- /dev/null
+++ b/examples/tests-provers/cvc3/why3session.xml
@@ -0,0 +1,184 @@
+<?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>
-- 
GitLab