Commit 0a4926e8 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Update sessions.

parent f76cc1cb
...@@ -10,7 +10,7 @@ ...@@ -10,7 +10,7 @@
<prover id="6" name="Z3" version="4.3.2" timelimit="5" steplimit="1" memlimit="1000"/> <prover id="6" name="Z3" version="4.3.2" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="7" name="Coq" version="8.4pl6" timelimit="5" steplimit="1" memlimit="1000"/> <prover id="7" name="Coq" version="8.4pl6" timelimit="5" steplimit="1" memlimit="1000"/>
<file name="../compiler.mlw" expanded="true"> <file name="../compiler.mlw" expanded="true">
<theory name="Compile_aexpr" sum="f149c7930975bd42aaeb1fca31573102" expanded="true"> <theory name="Compile_aexpr" sum="189f7fd596ec28a9b61e10970bfbea46" expanded="true">
<goal name="WP_parameter compile_aexpr" expl="VC for compile_aexpr"> <goal name="WP_parameter compile_aexpr" expl="VC for compile_aexpr">
<transf name="split_goal_wp"> <transf name="split_goal_wp">
<goal name="WP_parameter compile_aexpr.1" expl="1. precondition"> <goal name="WP_parameter compile_aexpr.1" expl="1. precondition">
...@@ -248,7 +248,7 @@ ...@@ -248,7 +248,7 @@
</transf> </transf>
</goal> </goal>
</theory> </theory>
<theory name="Compile_bexpr" sum="384513fa31fd946a4ad2aea39767d030" expanded="true"> <theory name="Compile_bexpr" sum="66e522e58f74b29ffdd570e923b8f305" expanded="true">
<goal name="WP_parameter compile_bexpr" expl="VC for compile_bexpr"> <goal name="WP_parameter compile_bexpr" expl="VC for compile_bexpr">
<transf name="split_goal_wp"> <transf name="split_goal_wp">
<goal name="WP_parameter compile_bexpr.1" expl="1. precondition"> <goal name="WP_parameter compile_bexpr.1" expl="1. precondition">
...@@ -1742,7 +1742,7 @@ ...@@ -1742,7 +1742,7 @@
</transf> </transf>
</goal> </goal>
</theory> </theory>
<theory name="Compile_com" sum="85bdd7a6f37746b44787b4d7142cdecf" expanded="true"> <theory name="Compile_com" sum="a4328280d68846b06645ac35357cff91" expanded="true">
<goal name="WP_parameter compile_com" expl="VC for compile_com"> <goal name="WP_parameter compile_com" expl="VC for compile_com">
<transf name="split_goal_wp"> <transf name="split_goal_wp">
<goal name="WP_parameter compile_com.1" expl="1. precondition"> <goal name="WP_parameter compile_com.1" expl="1. precondition">
......
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