Commit 832328e5 authored by MARCHE Claude's avatar MARCHE Claude

fix failed replay, except the problem with isabelle

parent 98ce2754
This diff is collapsed.
......@@ -5,17 +5,17 @@
<prover id="0" name="CVC3" version="2.4.1" timelimit="23" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="3" memlimit="1000"/>
<file name="../bitvectors.why" expanded="true">
<theory name="TestBV" sum="6c8cf1f3af56cc427b7e569fc12908c2" expanded="true">
<theory name="TestBV" sum="02a0a66ee1427b60874134706846ccbb" expanded="true">
<goal name="g1">
<proof prover="1"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="f1">
<goal name="f1" expanded="true">
<proof prover="1" timelimit="98"><result status="unknown" time="0.00"/></proof>
</goal>
<goal name="g2">
<proof prover="1"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="f2">
<goal name="f2" expanded="true">
<proof prover="1" timelimit="98"><result status="unknown" time="0.00"/></proof>
</goal>
<goal name="g3">
......@@ -73,7 +73,7 @@
<proof prover="1"><result status="valid" time="0.17"/></proof>
</goal>
<goal name="Nth_bw_not">
<proof prover="1" edited="bitvectors-TestBV-Nth_bw_not_1.smt2"><result status="valid" time="1.32"/></proof>
<proof prover="1" timelimit="5"><result status="valid" time="1.15"/></proof>
</goal>
<goal name="not_not">
<proof prover="1"><result status="valid" time="0.00"/></proof>
......@@ -81,24 +81,21 @@
<goal name="not_and">
<proof prover="1"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="Lsr_nth_low">
<proof prover="1" timelimit="98"><result status="valid" time="62.42"/></proof>
<goal name="Lsr_nth_low" expanded="true">
</goal>
<goal name="Lsr_nth_high">
<proof prover="0"><result status="valid" time="0.01"/></proof>
<proof prover="1" timelimit="98"><result status="valid" time="7.81"/></proof>
<proof prover="1" timelimit="98"><result status="valid" time="6.43"/></proof>
</goal>
<goal name="Asr_nth_low">
<proof prover="1" timelimit="98"><result status="valid" time="72.85"/></proof>
<goal name="Asr_nth_low" expanded="true">
</goal>
<goal name="Asr_nth_high">
<proof prover="1" timelimit="98"><result status="valid" time="8.10"/></proof>
<proof prover="1" timelimit="98"><result status="valid" time="6.67"/></proof>
</goal>
<goal name="Lsl_nth_high">
<proof prover="1" timelimit="98"><result status="valid" time="58.83"/></proof>
<goal name="Lsl_nth_high" expanded="true">
</goal>
<goal name="Lsl_nth_low">
<proof prover="1" timelimit="98"><result status="valid" time="7.64"/></proof>
<proof prover="1" timelimit="98"><result status="valid" time="5.83"/></proof>
</goal>
</theory>
</file>
......
This diff is collapsed.
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