Commit 26b1e6de authored by Claude Marche's avatar Claude Marche

Warning on formulas of form "exists x, P -> Q". One such a bug found in stdlib !

parent 60ab9af2
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/home/cmarche/recherche/why3/share/why3session.dtd">
<why3session
name="bts/fsetint/why3session.xml" shape_version="2">
<prover
......@@ -40,36 +40,36 @@
name="l_false"
locfile="bts/fsetint/../fsetint.why"
loclnum="5" loccnumb="9" loccnume="16"
sum="e5228e61b1bf3ae1b0b7f5c3c5fc4a87"
sum="d7f2aebfd2edd578b1a93cf604aec178"
proved="false"
expanded="true"
shape="f">
<proof
prover="4"
prover="1"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="3.01"/>
<result status="unknown" time="0.01"/>
</proof>
<proof
prover="2"
prover="0"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="3.01"/>
<result status="unknown" time="0.02"/>
</proof>
<proof
prover="0"
prover="3"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.00"/>
<result status="timeout" time="3.01"/>
</proof>
<proof
prover="3"
prover="4"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -77,7 +77,7 @@
<result status="timeout" time="3.01"/>
</proof>
<proof
prover="5"
prover="2"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -85,12 +85,12 @@
<result status="timeout" time="3.01"/>
</proof>
<proof
prover="1"
prover="5"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.00"/>
<result status="timeout" time="3.01"/>
</proof>
</goal>
</theory>
......@@ -104,36 +104,36 @@
name="mem_integer"
locfile="bts/fsetint/../fsetint.why"
loclnum="13" loccnumb="8" loccnume="19"
sum="ad9722cec30603b93adbe5ee3c3947d6"
sum="242bf143cc8b33512505c233039239e5"
proved="false"
expanded="true"
shape="amemV0aintegerF">
<proof
prover="4"
prover="1"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="3.01"/>
<result status="unknown" time="0.00"/>
</proof>
<proof
prover="2"
prover="0"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="3.01"/>
<result status="unknown" time="0.00"/>
</proof>
<proof
prover="0"
prover="3"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.00"/>
<result status="timeout" time="3.11"/>
</proof>
<proof
prover="3"
prover="4"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -141,77 +141,77 @@
<result status="timeout" time="3.01"/>
</proof>
<proof
prover="5"
prover="2"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="3.01"/>
<result status="timeout" time="3.02"/>
</proof>
<proof
prover="1"
prover="5"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.00"/>
<result status="timeout" time="3.02"/>
</proof>
</goal>
<goal
name="foo"
locfile="bts/fsetint/../fsetint.why"
loclnum="15" loccnumb="7" loccnume="10"
sum="7c99b63c028149b0160d1fc1b66ea6ba"
sum="80ba20b39cf0e3e682e5c0d84d596f36"
proved="false"
expanded="true"
shape="f">
<proof
prover="4"
prover="1"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="3.01"/>
<result status="unknown" time="0.00"/>
</proof>
<proof
prover="2"
prover="0"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="3.11"/>
<result status="unknown" time="0.00"/>
</proof>
<proof
prover="0"
prover="3"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.00"/>
<result status="timeout" time="3.11"/>
</proof>
<proof
prover="3"
prover="4"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="3.11"/>
<result status="timeout" time="3.01"/>
</proof>
<proof
prover="5"
prover="2"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="3.01"/>
<result status="timeout" time="3.11"/>
</proof>
<proof
prover="1"
prover="5"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.00"/>
<result status="timeout" time="3.01"/>
</proof>
</goal>
</theory>
......@@ -230,15 +230,15 @@
expanded="true"
shape="f">
<proof
prover="4"
prover="1"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.01"/>
<result status="unknown" time="0.00"/>
</proof>
<proof
prover="2"
prover="0"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -246,36 +246,36 @@
<result status="unknown" time="0.00"/>
</proof>
<proof
prover="0"
prover="3"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.01"/>
<result status="unknown" time="0.00"/>
</proof>
<proof
prover="3"
prover="4"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.00"/>
<result status="unknown" time="0.01"/>
</proof>
<proof
prover="5"
prover="2"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.02"/>
<result status="unknown" time="0.00"/>
</proof>
<proof
prover="1"
prover="5"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.00"/>
<result status="unknown" time="0.01"/>
</proof>
</goal>
</theory>
......
......@@ -206,6 +206,12 @@ let check_used_var vars v =
let check_used_vars vars =
List.iter (check_used_var vars)
let check_exists_implies q f =
match q,f.t_node with
| Texists, Tbinop(Timplies, _,_) ->
Warning.emit ?loc:f.t_loc "form \"exists, P -> Q\" is likely an error (use \"not P \\/ Q\" if not)"
| _ -> ()
let rec term env t = match t.dt_node with
| Tvar x ->
assert (Mstr.mem x env);
......@@ -267,6 +273,7 @@ and fmla env = function
let trl = List.map (List.map trigger) trl in
let f = fmla env f1 in
check_used_vars f.Term.t_vars vl;
check_exists_implies q f;
t_quant_close q vl trl f
| Fapp (s, tl) ->
ps_app s (List.map (term env) tl)
......
......@@ -161,7 +161,7 @@ theory Fset
axiom nth_surjective:
forall s: set 'a, x: 'a. mem x s ->
exists i: int. 0 <= i < cardinal s -> x = nth i s
exists i: int. 0 <= i < cardinal s /\ x = nth i s
end
......
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