Commit af6b98c6 authored by MARCHE Claude's avatar MARCHE Claude

test counterexamples in IDE

parent 929d29c6
module TestCEX
use import int.Int
goal g: forall x "model". x=0
end
module TestCopyPaste
......@@ -40,7 +47,7 @@ module TestTaskPrinting
goal g1: averyveryveryveryveryverylongname 1 + averyveryveryveryveryverylongname 2 +
averyveryveryveryveryverylongname 3 + averyveryveryveryveryverylongname 4 >= 0
(*goal g2: let x = 1 in x + 1 >= 0*)
goal g2: let x = 1 in x + 1 >= 0
goal g3: let x = 1 in averyveryveryveryveryverylongname x + averyveryveryveryveryverylongname 1 >= 0
......
......@@ -10,6 +10,11 @@
<prover id="5" name="Eprover" version="2.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="6" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../demo-itp.mlw">
<theory name="TestCEX" sum="55ceea8b24a88c1829a53af2c814f1a6">
<goal name="g">
<proof prover="2" timelimit="5"><result status="unknown" time="0.00"/></proof>
</goal>
</theory>
<theory name="TestCopyPaste" sum="22d35cc9b3a5547f481892208f0547bc">
<goal name="g1">
<transf name="split_goal_wp" >
......@@ -49,9 +54,11 @@
<goal name="g2">
</goal>
</theory>
<theory name="TestTaskPrinting" sum="801f15aa4345fd2ac2cb9efbcefa4d4b">
<theory name="TestTaskPrinting" sum="01fbd777d08f356d2f390e335249eeb9">
<goal name="g1">
</goal>
<goal name="g2">
</goal>
<goal name="g3">
</goal>
<goal name="g4">
......@@ -64,8 +71,6 @@
</goal>
<goal name="g8">
</goal>
<goal name="g2">
</goal>
</theory>
<theory name="TestAutomaticIntro" sum="6566463f1ee0314d808add53aa21307c">
<goal name="g">
......@@ -120,9 +125,9 @@
<proof prover="2"><result status="unknown" time="1.00"/></proof>
</goal>
<goal name="power_sum.1" expl="recursive case" proved="true">
<proof prover="0" obsolete="true"><result status="valid" time="0.87" steps="15"/></proof>
<proof prover="1" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="2" obsolete="true"><result status="unknown" time="1.01"/></proof>
<proof prover="0"><result status="valid" time="0.87" steps="15"/></proof>
<proof prover="1"><result status="timeout" time="1.00"/></proof>
<proof prover="2"><result status="unknown" time="1.01"/></proof>
<transf name="case" proved="true" arg1="(n=0)">
<goal name="power_sum.1.0" expl="true case (recursive case)" proved="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
......
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