Commit 13025a8c authored by Martin Clochard's avatar Martin Clochard

double-wp example: minor session fix.

parent b9175266
...@@ -1715,8 +1715,8 @@ ...@@ -1715,8 +1715,8 @@
</goal> </goal>
</theory> </theory>
<theory name="Compile_com" sum="1e8c2b4ce7668ca36cc6cb1a420dff9b" expanded="true"> <theory name="Compile_com" sum="1e8c2b4ce7668ca36cc6cb1a420dff9b" expanded="true">
<goal name="WP_parameter compile_com" expl="VC for compile_com"> <goal name="WP_parameter compile_com" expl="VC for compile_com" expanded="true">
<transf name="split_goal_wp"> <transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter compile_com.1" expl="1. precondition"> <goal name="WP_parameter compile_com.1" expl="1. precondition">
<proof prover="4"><result status="valid" time="0.07"/></proof> <proof prover="4"><result status="valid" time="0.07"/></proof>
</goal> </goal>
...@@ -1910,7 +1910,7 @@ ...@@ -1910,7 +1910,7 @@
<proof prover="4"><result status="valid" time="0.37"/></proof> <proof prover="4"><result status="valid" time="0.37"/></proof>
</goal> </goal>
<goal name="WP_parameter compile_com.34.1.1.5" expl="5."> <goal name="WP_parameter compile_com.34.1.1.5" expl="5.">
<proof prover="4" edited="compiler-Compile_com-WP_parameter_compile_com_2.why"><result status="valid" time="0.35"/></proof> <proof prover="4"><result status="valid" time="0.22"/></proof>
</goal> </goal>
<goal name="WP_parameter compile_com.34.1.1.6" expl="6."> <goal name="WP_parameter compile_com.34.1.1.6" expl="6.">
<proof prover="4"><result status="valid" time="1.36"/></proof> <proof prover="4"><result status="valid" time="1.36"/></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