Commit a4f7b8df authored by MARCHE Claude's avatar MARCHE Claude
Browse files

update two examples missing proof of witness

parent 9b35567d
......@@ -5,8 +5,12 @@
<prover id="0" name="CVC4" version="1.4" timelimit="5" steplimit="4000" memlimit="4000"/>
<prover id="1" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="4000" memlimit="4000"/>
<prover id="2" name="Z3" version="4.4.1" timelimit="5" steplimit="4000" memlimit="4000"/>
<prover id="3" name="Eprover" version="1.8-001" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../esterel.mlw" expanded="true">
<theory name="Esterel" sum="2dbbb586b93adcafe01fbe63884d474e" expanded="true">
<theory name="Esterel" sum="8bc1462db75de50f42f00666686ab8c5" expanded="true">
<goal name="VC s" expl="VC for s">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC union" expl="VC for union">
<proof prover="1"><result status="valid" time="0.16" steps="268"/></proof>
</goal>
......
......@@ -90,7 +90,7 @@ module BitsSpec
constant size : int = 32
type t = {
type t = private {
ghost mdl: set int;
}
invariant { forall i. mem i mdl -> 0 <= i < size }
......
......@@ -9,6 +9,7 @@
<prover id="4" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="5" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="6" name="CVC4" version="1.4" alternative="noBV" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="7" name="Eprover" version="1.8-001" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="9" name="Z3" version="4.4.1" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../queens_bv.mlw" expanded="true">
<theory name="S" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
......@@ -22,9 +23,15 @@
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
</theory>
<theory name="BitsSpec" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
<theory name="BitsSpec" sum="8fbc46ea269d029380a41104bd31dc1e" expanded="true">
<goal name="VC t" expl="VC for t" expanded="true">
<proof prover="7"><result status="valid" time="0.03"/></proof>
</goal>
</theory>
<theory name="Bits" sum="a3353d21cc9287edb8d335fc0316e0b3">
<theory name="Bits" sum="73f2409f2a8a5a242e9b1046c78475c0" expanded="true">
<goal name="VC t" expl="VC for t" expanded="true">
<proof prover="7"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC empty" expl="VC for empty">
<proof prover="0"><result status="valid" time="0.03" steps="95"/></proof>
</goal>
......
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