Skip to content

GitLab

Commit e4d6cdcb authored by MARCHE Claude's avatar MARCHE Claude
Browse files

binary search: updated session

parent 212a4d3b
Hide whitespace changes
Inline Side-by-side
examples/binary_search/why3session.xml
View file @ e4d6cdcb
......@@ -24,8 +24,8 @@
</goal>
</theory>
<theory name="BinarySearchInt32" sum="0bac534b34ae6ec72cbe896cc4f66587" expanded="true">
<goal name="WP_parameter binary_search" expl="VC for binary_search" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter binary_search" expl="VC for binary_search">
<transf name="split_goal_wp">
<goal name="WP_parameter binary_search.1" expl="1. integer overflow">
<proof prover="3"><result status="valid" time="0.02" steps="71"/></proof>
</goal>
......@@ -94,7 +94,7 @@
<goal name="WP_parameter binary_search.22" expl="22. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.04"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3" timelimit="60"><undone/></proof>
<proof prover="5"><result status="valid" time="1.27" steps="181"/></proof>
</goal>
<goal name="WP_parameter binary_search.23" expl="23. loop variant decrease">
<proof prover="3"><result status="valid" time="0.02" steps="101"/></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