Commit 0799cf0d authored by MARCHE Claude's avatar MARCHE Claude
Browse files

update obsolete sessions

parent e3a14168
......@@ -7,7 +7,7 @@
<prover id="2" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="3" name="Z3" version="4.3.2" timelimit="5" memlimit="1000"/>
<file name="../bitvector_examples.mlw" expanded="true">
<theory name="Test_proofinuse" sum="ee2b0706c948b7fbb0dceccdae7fcbb8">
<theory name="Test_proofinuse" sum="c5dfeca877f9a6895578ed88973f9ccd">
<goal name="WP_parameter shift_is_div" expl="VC for shift_is_div">
<transf name="split_goal_wp">
<goal name="WP_parameter shift_is_div.1" expl="1. assertion">
......@@ -19,7 +19,7 @@
<proof prover="1"><result status="valid" time="0.18"/></proof>
</goal>
<goal name="WP_parameter shift_is_div.3" expl="3. assertion">
<proof prover="1"><result status="valid" time="1.39"/></proof>
<proof prover="1"><result status="valid" time="0.83"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
......@@ -37,11 +37,11 @@
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="ttt">
<proof prover="0"><result status="valid" time="0.71" steps="655"/></proof>
<proof prover="0"><result status="valid" time="0.71" steps="706"/></proof>
<proof prover="2"><result status="valid" time="0.08"/></proof>
</goal>
</theory>
<theory name="Hackers_delight" sum="f6b9335c83a49e64cc1c287e49abcc67">
<theory name="Hackers_delight" sum="ef26a3ba915efe6965c76dd6bae0f770">
<goal name="DM1">
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
......@@ -104,7 +104,7 @@
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
</theory>
<theory name="Hackers_delight_mod" sum="358ae27e3c7dd0ffc3bad38307e7ee71">
<theory name="Hackers_delight_mod" sum="f06501bd9462dbd6d4d261fa5161c4c6">
<goal name="WP_parameter dm1" expl="VC for dm1">
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
......@@ -161,7 +161,7 @@
<proof prover="2"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="WP_parameter bp1&apos;" expl="VC for bp1&apos;">
<proof prover="0"><result status="valid" time="0.05" steps="109"/></proof>
<proof prover="0"><result status="valid" time="0.05" steps="110"/></proof>
<proof prover="1"><result status="valid" time="0.35"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
......@@ -173,67 +173,67 @@
<proof prover="2"><result status="valid" time="0.07"/></proof>
</goal>
</theory>
<theory name="Test_imperial_violet" sum="9d49ecf681253b01c1150fab4a271ed5">
<theory name="Test_imperial_violet" sum="27ff634810d82c784940f7a0737fca5d">
<goal name="bv32_bounds_bv">
<proof prover="0"><result status="valid" time="0.13" steps="141"/></proof>
<proof prover="0"><result status="valid" time="0.13" steps="144"/></proof>
<proof prover="1"><result status="valid" time="0.25"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="to_int_ule">
<proof prover="0"><result status="valid" time="0.04" steps="70"/></proof>
<proof prover="0"><result status="valid" time="0.04" steps="71"/></proof>
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="to_int_ult">
<proof prover="0"><result status="valid" time="0.04" steps="70"/></proof>
<proof prover="0"><result status="valid" time="0.04" steps="71"/></proof>
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="bv32_bounds_0">
<proof prover="0"><result status="valid" time="0.04" steps="71"/></proof>
<proof prover="0"><result status="valid" time="0.04" steps="72"/></proof>
<proof prover="1"><result status="valid" time="0.13"/></proof>
</goal>
<goal name="bv32_bounds">
<proof prover="0"><result status="valid" time="0.03" steps="73"/></proof>
<proof prover="0"><result status="valid" time="0.03" steps="74"/></proof>
<proof prover="1"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="WP_parameter add" expl="VC for add">
<proof prover="1"><result status="valid" time="3.15"/></proof>
<proof prover="1"><result status="valid" time="0.82"/></proof>
</goal>
</theory>
<theory name="Test_from_bitvector_example" sum="2ebd89b51a2ede04c66611b03895c2c2" expanded="true">
<theory name="Test_from_bitvector_example" sum="56c18dd003e28012f65d635db1cd8cc9" expanded="true">
<goal name="Test1">
<proof prover="0"><result status="valid" time="0.14" steps="93"/></proof>
<proof prover="0"><result status="valid" time="0.14" steps="96"/></proof>
<proof prover="1"><result status="valid" time="0.22"/></proof>
<proof prover="2"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="Test2">
<proof prover="0"><result status="valid" time="0.04" steps="131"/></proof>
<proof prover="0"><result status="valid" time="0.04" steps="134"/></proof>
<proof prover="1"><result status="valid" time="0.42"/></proof>
<proof prover="2"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="Test3">
<proof prover="0"><result status="valid" time="0.06" steps="83"/></proof>
<proof prover="0"><result status="valid" time="0.06" steps="85"/></proof>
<proof prover="1"><result status="valid" time="0.19"/></proof>
<proof prover="2"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="Test4">
<proof prover="0"><result status="valid" time="0.04" steps="131"/></proof>
<proof prover="0"><result status="valid" time="0.04" steps="133"/></proof>
<proof prover="1"><result status="valid" time="0.41"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="Test5">
<proof prover="0"><result status="valid" time="0.06" steps="89"/></proof>
<proof prover="0"><result status="valid" time="0.06" steps="92"/></proof>
<proof prover="1"><result status="valid" time="0.24"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="Test6">
<proof prover="0"><result status="valid" time="0.06" steps="127"/></proof>
<proof prover="1"><result status="valid" time="0.58"/></proof>
<proof prover="0"><result status="valid" time="0.06" steps="129"/></proof>
<proof prover="1"><result status="valid" time="0.33"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
......@@ -248,172 +248,172 @@
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter lsr29" expl="VC for lsr29" expanded="true">
<proof prover="1"><result status="valid" time="0.74"/></proof>
<proof prover="1"><result status="valid" time="0.40"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter lsr28" expl="VC for lsr28">
<proof prover="0"><result status="valid" time="0.24" steps="196"/></proof>
<proof prover="1"><result status="valid" time="0.76"/></proof>
<proof prover="0"><result status="valid" time="0.24" steps="197"/></proof>
<proof prover="1"><result status="valid" time="0.40"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter lsr27" expl="VC for lsr27">
<proof prover="0"><result status="valid" time="0.18" steps="196"/></proof>
<proof prover="1"><result status="valid" time="0.88"/></proof>
<proof prover="0"><result status="valid" time="0.18" steps="197"/></proof>
<proof prover="1"><result status="valid" time="0.44"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter lsr26" expl="VC for lsr26">
<proof prover="0"><result status="valid" time="0.16" steps="196"/></proof>
<proof prover="1"><result status="valid" time="0.71"/></proof>
<proof prover="0"><result status="valid" time="0.16" steps="197"/></proof>
<proof prover="1"><result status="valid" time="0.44"/></proof>
<proof prover="2"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter lsr20" expl="VC for lsr20">
<proof prover="0"><result status="valid" time="0.24" steps="196"/></proof>
<proof prover="1"><result status="valid" time="0.72"/></proof>
<proof prover="0"><result status="valid" time="0.24" steps="197"/></proof>
<proof prover="1"><result status="valid" time="0.44"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter lsr13" expl="VC for lsr13">
<proof prover="0"><result status="valid" time="0.24" steps="196"/></proof>
<proof prover="1"><result status="valid" time="0.72"/></proof>
<proof prover="0"><result status="valid" time="0.24" steps="197"/></proof>
<proof prover="1"><result status="valid" time="0.44"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter lsr8" expl="VC for lsr8">
<proof prover="0"><result status="valid" time="0.25" steps="196"/></proof>
<proof prover="1"><result status="valid" time="0.72"/></proof>
<proof prover="0"><result status="valid" time="0.25" steps="197"/></proof>
<proof prover="1"><result status="valid" time="0.44"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="to_int_0x00000001">
<proof prover="0"><result status="valid" time="0.20" steps="227"/></proof>
<proof prover="0"><result status="valid" time="0.20" steps="229"/></proof>
<proof prover="1"><result status="valid" time="0.20"/></proof>
<proof prover="2"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="to_int_0x00000003">
<proof prover="0"><result status="valid" time="0.14" steps="196"/></proof>
<proof prover="0"><result status="valid" time="0.14" steps="197"/></proof>
<proof prover="1"><result status="valid" time="0.54"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="to_int_0x00000007" expanded="true">
<proof prover="1"><result status="valid" time="0.74"/></proof>
<proof prover="1"><result status="valid" time="0.39"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="to_int_0x0000000F">
<proof prover="0"><result status="valid" time="0.14" steps="196"/></proof>
<proof prover="1"><result status="valid" time="0.75"/></proof>
<proof prover="0"><result status="valid" time="0.14" steps="197"/></proof>
<proof prover="1"><result status="valid" time="0.40"/></proof>
<proof prover="2"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="to_int_0x0000001F">
<proof prover="0"><result status="valid" time="0.20" steps="196"/></proof>
<proof prover="1"><result status="valid" time="0.71"/></proof>
<proof prover="0"><result status="valid" time="0.20" steps="197"/></proof>
<proof prover="1"><result status="valid" time="0.44"/></proof>
<proof prover="2"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="to_int_0x0000003F">
<proof prover="0"><result status="valid" time="0.14" steps="196"/></proof>
<proof prover="1"><result status="valid" time="0.71"/></proof>
<proof prover="0"><result status="valid" time="0.14" steps="197"/></proof>
<proof prover="1"><result status="valid" time="0.44"/></proof>
<proof prover="2"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="to_int_0x0000007F">
<proof prover="0"><result status="valid" time="0.21" steps="196"/></proof>
<proof prover="1"><result status="valid" time="0.73"/></proof>
<proof prover="0"><result status="valid" time="0.21" steps="197"/></proof>
<proof prover="1"><result status="valid" time="0.44"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="to_int_0x000000FF" expanded="true">
<proof prover="1"><result status="valid" time="0.73"/></proof>
<proof prover="1"><result status="valid" time="0.44"/></proof>
<proof prover="2"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="to_int_0x000001FF">
<proof prover="0"><result status="valid" time="0.14" steps="196"/></proof>
<proof prover="1"><result status="valid" time="0.73"/></proof>
<proof prover="0"><result status="valid" time="0.14" steps="197"/></proof>
<proof prover="1"><result status="valid" time="0.44"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="to_int_0x000003FF">
<proof prover="0"><result status="valid" time="0.14" steps="196"/></proof>
<proof prover="1"><result status="valid" time="0.73"/></proof>
<proof prover="0"><result status="valid" time="0.14" steps="197"/></proof>
<proof prover="1"><result status="valid" time="0.44"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="to_int_0x000007FF">
<proof prover="0"><result status="valid" time="0.14" steps="196"/></proof>
<proof prover="1"><result status="valid" time="0.74"/></proof>
<proof prover="0"><result status="valid" time="0.14" steps="197"/></proof>
<proof prover="1"><result status="valid" time="0.44"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="to_int_0x00000FFF">
<proof prover="0"><result status="valid" time="0.24" steps="196"/></proof>
<proof prover="1"><result status="valid" time="0.72"/></proof>
<proof prover="0"><result status="valid" time="0.24" steps="197"/></proof>
<proof prover="1"><result status="valid" time="0.44"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="to_int_0x00001FFF">
<proof prover="0"><result status="valid" time="0.14" steps="196"/></proof>
<proof prover="1"><result status="valid" time="0.71"/></proof>
<proof prover="0"><result status="valid" time="0.14" steps="197"/></proof>
<proof prover="1"><result status="valid" time="0.44"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="to_int_0x00003FFF">
<proof prover="0"><result status="valid" time="0.21" steps="196"/></proof>
<proof prover="1"><result status="valid" time="0.73"/></proof>
<proof prover="0"><result status="valid" time="0.21" steps="197"/></proof>
<proof prover="1"><result status="valid" time="0.44"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="to_int_0x00007FFF">
<proof prover="0"><result status="valid" time="0.18" steps="196"/></proof>
<proof prover="1"><result status="valid" time="0.72"/></proof>
<proof prover="0"><result status="valid" time="0.18" steps="197"/></proof>
<proof prover="1"><result status="valid" time="0.44"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="to_int_0x0000FFFF">
<proof prover="0"><result status="valid" time="0.19" steps="196"/></proof>
<proof prover="1"><result status="valid" time="0.72"/></proof>
<proof prover="0"><result status="valid" time="0.19" steps="197"/></proof>
<proof prover="1"><result status="valid" time="0.44"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="to_int_0x0001FFFF">
<proof prover="0"><result status="valid" time="0.14" steps="196"/></proof>
<proof prover="1"><result status="valid" time="0.72"/></proof>
<proof prover="0"><result status="valid" time="0.14" steps="197"/></proof>
<proof prover="1"><result status="valid" time="0.44"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="to_int_0x0003FFFF">
<proof prover="0"><result status="valid" time="0.13" steps="196"/></proof>
<proof prover="1"><result status="valid" time="0.73"/></proof>
<proof prover="0"><result status="valid" time="0.13" steps="197"/></proof>
<proof prover="1"><result status="valid" time="0.44"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="to_int_0x0007FFFF">
<proof prover="0"><result status="valid" time="0.18" steps="196"/></proof>
<proof prover="1"><result status="valid" time="0.72"/></proof>
<proof prover="0"><result status="valid" time="0.18" steps="197"/></proof>
<proof prover="1"><result status="valid" time="0.44"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="to_int_0x000FFFFF">
<proof prover="0"><result status="valid" time="0.14" steps="196"/></proof>
<proof prover="1"><result status="valid" time="0.73"/></proof>
<proof prover="0"><result status="valid" time="0.14" steps="197"/></proof>
<proof prover="1"><result status="valid" time="0.44"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="to_int_0x00FFFFFF">
<proof prover="0"><result status="valid" time="0.14" steps="196"/></proof>
<proof prover="1"><result status="valid" time="0.72"/></proof>
<proof prover="0"><result status="valid" time="0.14" steps="197"/></proof>
<proof prover="1"><result status="valid" time="0.44"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="to_int_0xFFFFFFFF">
<proof prover="0"><result status="valid" time="0.04" steps="74"/></proof>
<proof prover="0"><result status="valid" time="0.04" steps="75"/></proof>
<proof prover="1"><result status="valid" time="0.16"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
......
......@@ -6,7 +6,7 @@
<prover id="1" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="2" name="Z3" version="4.3.2" timelimit="5" memlimit="1000"/>
<file name="../hackers-delight.mlw" expanded="true">
<theory name="Hackers_delight" sum="f68afbb08101be54ae51e015e4048def" expanded="true">
<theory name="Hackers_delight" sum="f0a189c908de4dca4a7d7f3ad4145727" expanded="true">
<goal name="countZero" expanded="true">
<proof prover="1"><result status="valid" time="0.05"/></proof>
<proof prover="2"><result status="valid" time="0.09"/></proof>
......@@ -33,7 +33,7 @@
<proof prover="1"><result status="valid" time="1.41"/></proof>
</goal>
<goal name="iso" expanded="true">
<proof prover="1"><result status="valid" time="0.40"/></proof>
<proof prover="1"><result status="valid" time="0.25"/></proof>
</goal>
<goal name="grayIsGray" expanded="true">
<proof prover="1"><result status="valid" time="0.05"/></proof>
......@@ -92,7 +92,7 @@
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="Ae" expanded="true">
<proof prover="0"><result status="valid" time="0.05" steps="72"/></proof>
<proof prover="0"><result status="valid" time="0.05" steps="73"/></proof>
<proof prover="1"><result status="valid" time="0.04"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
</goal>
......@@ -118,7 +118,7 @@
<proof prover="1"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="Au" expanded="true">
<proof prover="1"><result status="valid" time="0.13"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="Av" expanded="true">
<proof prover="1"><result status="valid" time="0.12"/></proof>
......
......@@ -7,7 +7,7 @@
<prover id="2" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="3" name="Z3" version="4.3.2" timelimit="5" memlimit="1000"/>
<file name="../bitvectors.why" expanded="true">
<theory name="TestBV" sum="362573c1d9c043dd414d1edaaa78f89f" expanded="true">
<theory name="TestBV" sum="c1af0d73b67219351e5904090236ec3e" expanded="true">
<goal name="g1" expanded="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
......@@ -62,12 +62,12 @@
<proof prover="1"><result status="timeout" time="4.97"/></proof>
</goal>
<goal name="g4a" expanded="true">
<proof prover="0"><result status="valid" time="0.28" steps="158"/></proof>
<proof prover="0"><result status="valid" time="0.28" steps="163"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="g4b" expanded="true">
<proof prover="0"><result status="valid" time="0.19" steps="159"/></proof>
<proof prover="0"><result status="valid" time="0.19" steps="164"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
......@@ -96,12 +96,12 @@
<proof prover="1"><result status="timeout" time="4.99"/></proof>
</goal>
<goal name="g6a" expanded="true">
<proof prover="0"><result status="valid" time="0.03" steps="74"/></proof>
<proof prover="0"><result status="valid" time="0.03" steps="75"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="g6b" expanded="true">
<proof prover="0"><result status="valid" time="0.02" steps="74"/></proof>
<proof prover="0"><result status="valid" time="0.02" steps="75"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
......@@ -136,7 +136,7 @@
<proof prover="3"><result status="timeout" time="4.99"/></proof>
</goal>
<goal name="gtt" expanded="true">
<proof prover="0"><result status="valid" time="0.13" steps="122"/></proof>
<proof prover="0"><result status="valid" time="0.13" steps="124"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
......
......@@ -1030,24 +1030,24 @@
</transf>
</goal>
</theory>
<theory name="Bits" sum="87ba23b038d8da5026df22be3839311c" expanded="true">
<theory name="Bits" sum="26f530a3770b8f7025b1561338100703" expanded="true">
<goal name="WP_parameter zero" expl="VC for zero" expanded="true">
<proof prover="11"><result status="valid" time="0.03" steps="80"/></proof>
</goal>
<goal name="WP_parameter remove_singleton" expl="VC for remove_singleton" expanded="true">
<proof prover="11"><result status="valid" time="0.80" steps="578"/></proof>
<proof prover="11"><result status="valid" time="0.80" steps="538"/></proof>
</goal>
<goal name="WP_parameter add_singleton" expl="VC for add_singleton" expanded="true">
<proof prover="2"><result status="valid" time="1.30"/></proof>
</goal>
<goal name="WP_parameter mul2" expl="VC for mul2" expanded="true">
<proof prover="11"><result status="valid" time="0.27" steps="218"/></proof>
<proof prover="11"><result status="valid" time="0.27" steps="226"/></proof>
</goal>
<goal name="WP_parameter div2" expl="VC for div2" expanded="true">
<proof prover="11"><result status="valid" time="0.18" steps="109"/></proof>
<proof prover="11"><result status="valid" time="0.18" steps="118"/></proof>
</goal>
<goal name="WP_parameter diff" expl="VC for diff" expanded="true">
<proof prover="11"><result status="valid" time="0.27" steps="228"/></proof>
<proof prover="11"><result status="valid" time="0.27" steps="211"/></proof>
</goal>
<goal name="WP_parameter rightmost_bit_trick" expl="VC for rightmost_bit_trick" expanded="true">
<proof prover="2" timelimit="20"><result status="timeout" time="19.98"/></proof>
......@@ -1055,7 +1055,7 @@
<proof prover="11"><result status="timeout" time="4.98"/></proof>
</goal>
<goal name="WP_parameter below" expl="VC for below" expanded="true">
<proof prover="11"><result status="valid" time="0.18" steps="118"/></proof>
<proof prover="11"><result status="valid" time="0.18" steps="119"/></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