Commit 30ea49f9 authored by MARCHE Claude's avatar MARCHE Claude

update some sessions in examples/logic

parent b22739b4
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../ns_clone.why" expanded="true">
<theory name="Sig" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="Struct" sum="cbf570a03a30b3c63542974d17fdfab0" expanded="true">
<goal name="Sig.AddMem" expanded="true">
<proof prover="1"><result status="valid" time="0.01" steps="7"/></proof>
</goal>
</theory>
<theory name="Shared" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="AbstractUser" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="ConcreteUser" sum="b6317bbd033d14844a7e4e39cac2f612" expanded="true">
<goal name="Sig.AddMem" expanded="true">
<proof prover="1"><result status="valid" time="0.01" steps="4"/></proof>
</goal>
</theory>
</file>
</why3session>
......@@ -3,6 +3,7 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Coq" version="8.6" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="1" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="6" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
......@@ -12,7 +13,7 @@
</theory>
<theory name="List" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
<theory name="SortedList" sum="086b3da725131c3280f67a5bf1dd5a0c" expanded="true">
<theory name="SortedList" sum="7f273ac6373797565d205e4fa9753174" expanded="true">
<goal name="sorted_inf" expanded="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
</goal>
......@@ -20,7 +21,16 @@
<proof prover="0" edited="sorted_list_SortedList_sorted_mem_1.v"><result status="valid" time="0.31"/></proof>
</goal>
</theory>
<theory name="SortedIntList" sum="b630995dca805d46336501a60025b5e3" expanded="true">
<theory name="SortedIntList" sum="ce9bd728ce43e4241b415494dcf8a403" expanded="true">
<goal name="SortedList.O.le_refl" expanded="true">
<proof prover="1"><result status="valid" time="0.00" steps="1"/></proof>
</goal>
<goal name="SortedList.O.le_asym" expanded="true">
<proof prover="1"><result status="valid" time="0.00" steps="3"/></proof>
</goal>
<goal name="SortedList.O.le_trans" expanded="true">
<proof prover="1"><result status="valid" time="0.00" steps="3"/></proof>
</goal>
<goal name="sorted123" expanded="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></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