distance -> optimal_replay

parent 481ac0c5
......@@ -19,7 +19,7 @@
is the path of length d[i] from 0 to i.
*)
module Distance
module OptimalReplay
use import int.Int
use import ref.Refint
......
......@@ -18,18 +18,18 @@
name="Z3"
version="3.2"/>
<file
name="../distance.mlw"
name="../optimal_replay.mlw"
verified="true"
expanded="true">
<theory
name="Distance"
locfile="../distance.mlw"
name="OptimalReplay"
locfile="../optimal_replay.mlw"
loclnum="22" loccnumb="7" loccnume="15"
verified="true"
expanded="true">
<goal
name="WP_parameter distance"
locfile="../distance.mlw"
locfile="../optimal_replay.mlw"
loclnum="46" loccnumb="6" loccnume="14"
expl="VC for distance"
sum="d9af2d7fe72bb92ac6a4a806e8215a83"
......@@ -44,7 +44,7 @@
expanded="true">
<goal
name="WP_parameter distance.1"
locfile="../distance.mlw"
locfile="../optimal_replay.mlw"
loclnum="46" loccnumb="6" loccnume="14"
expl="1. precondition"
sum="3a77962b4adb652af702f3f92b09e45b"
......@@ -64,7 +64,7 @@
</goal>
<goal
name="WP_parameter distance.2"
locfile="../distance.mlw"
locfile="../optimal_replay.mlw"
loclnum="46" loccnumb="6" loccnume="14"
expl="2. precondition"
sum="5195efaf23d414fbc2dae89ebf716edb"
......@@ -84,7 +84,7 @@
</goal>
<goal
name="WP_parameter distance.3"
locfile="../distance.mlw"
locfile="../optimal_replay.mlw"
loclnum="46" loccnumb="6" loccnume="14"
expl="3. precondition"
sum="ae02cb184e744a79d1edde8a6c9f0c76"
......@@ -104,7 +104,7 @@
</goal>
<goal
name="WP_parameter distance.4"
locfile="../distance.mlw"
locfile="../optimal_replay.mlw"
loclnum="46" loccnumb="6" loccnume="14"
expl="4. assertion"
sum="93b18e434719cbcf73cbc61a7c0bb7c6"
......@@ -124,7 +124,7 @@
</goal>
<goal
name="WP_parameter distance.5"
locfile="../distance.mlw"
locfile="../optimal_replay.mlw"
loclnum="46" loccnumb="6" loccnume="14"
expl="5. assertion"
sum="f3af76e74fa4c3a7eee460f76f0328ef"
......@@ -144,7 +144,7 @@
</goal>
<goal
name="WP_parameter distance.6"
locfile="../distance.mlw"
locfile="../optimal_replay.mlw"
loclnum="46" loccnumb="6" loccnume="14"
expl="6. loop invariant init"
sum="49d554ed3eb0050c00118df249ba6f59"
......@@ -164,7 +164,7 @@
</goal>
<goal
name="WP_parameter distance.7"
locfile="../distance.mlw"
locfile="../optimal_replay.mlw"
loclnum="46" loccnumb="6" loccnume="14"
expl="7. loop invariant init"
sum="b5a4ea550591b6353618b6b09be5e832"
......@@ -184,7 +184,7 @@
</goal>
<goal
name="WP_parameter distance.8"
locfile="../distance.mlw"
locfile="../optimal_replay.mlw"
loclnum="46" loccnumb="6" loccnume="14"
expl="8. loop invariant init"
sum="4a7cbf790a159ccb384d119f10b15a95"
......@@ -204,7 +204,7 @@
</goal>
<goal
name="WP_parameter distance.9"
locfile="../distance.mlw"
locfile="../optimal_replay.mlw"
loclnum="46" loccnumb="6" loccnume="14"
expl="9. loop invariant init"
sum="06b718e6d1a6f9bceb0e899ecba53ff1"
......@@ -224,7 +224,7 @@
</goal>
<goal
name="WP_parameter distance.10"
locfile="../distance.mlw"
locfile="../optimal_replay.mlw"
loclnum="46" loccnumb="6" loccnume="14"
expl="10. loop invariant init"
sum="04cc8120b98f92363dd46d490b3de52c"
......@@ -244,7 +244,7 @@
</goal>
<goal
name="WP_parameter distance.11"
locfile="../distance.mlw"
locfile="../optimal_replay.mlw"
loclnum="46" loccnumb="6" loccnume="14"
expl="11. precondition"
sum="215f7d7eed009eb92079da157fc5a193"
......@@ -264,7 +264,7 @@
</goal>
<goal
name="WP_parameter distance.12"
locfile="../distance.mlw"
locfile="../optimal_replay.mlw"
loclnum="46" loccnumb="6" loccnume="14"
expl="12. precondition"
sum="836b5525a1728755c883a61886f1efc8"
......@@ -284,7 +284,7 @@
</goal>
<goal
name="WP_parameter distance.13"
locfile="../distance.mlw"
locfile="../optimal_replay.mlw"
loclnum="46" loccnumb="6" loccnume="14"
expl="13. loop invariant preservation"
sum="ed6d84f9ee27e0a3b13f0f285379a4a2"
......@@ -312,7 +312,7 @@
</goal>
<goal
name="WP_parameter distance.14"
locfile="../distance.mlw"
locfile="../optimal_replay.mlw"
loclnum="46" loccnumb="6" loccnume="14"
expl="14. loop invariant preservation"
sum="c67689261f759e8089a92d4d09f299e7"
......@@ -340,7 +340,7 @@
</goal>
<goal
name="WP_parameter distance.15"
locfile="../distance.mlw"
locfile="../optimal_replay.mlw"
loclnum="46" loccnumb="6" loccnume="14"
expl="15. loop variant decrease"
sum="14383267b47316f9592f41b7be57e7f9"
......@@ -360,7 +360,7 @@
</goal>
<goal
name="WP_parameter distance.16"
locfile="../distance.mlw"
locfile="../optimal_replay.mlw"
loclnum="46" loccnumb="6" loccnume="14"
expl="16. precondition"
sum="c7c71b3ac0f905e7fd5ac688b17addfa"
......@@ -380,7 +380,7 @@
</goal>
<goal
name="WP_parameter distance.17"
locfile="../distance.mlw"
locfile="../optimal_replay.mlw"
loclnum="46" loccnumb="6" loccnume="14"
expl="17. precondition"
sum="750b27c8a5814fa0ff732638ea09ae7c"
......@@ -400,7 +400,7 @@
</goal>
<goal
name="WP_parameter distance.18"
locfile="../distance.mlw"
locfile="../optimal_replay.mlw"
loclnum="46" loccnumb="6" loccnume="14"
expl="18. precondition"
sum="755d6c9a5de2ef7067d1ad23ac3c6a6d"
......@@ -420,7 +420,7 @@
</goal>
<goal
name="WP_parameter distance.19"
locfile="../distance.mlw"
locfile="../optimal_replay.mlw"
loclnum="46" loccnumb="6" loccnume="14"
expl="19. loop invariant preservation"
sum="cff059f9b49dd04225b07a3d643b7c57"
......@@ -440,7 +440,7 @@
</goal>
<goal
name="WP_parameter distance.20"
locfile="../distance.mlw"
locfile="../optimal_replay.mlw"
loclnum="46" loccnumb="6" loccnume="14"
expl="20. loop invariant preservation"
sum="ff9ea4f0480847b891fd4c3f7fd40f4d"
......@@ -468,7 +468,7 @@
</goal>
<goal
name="WP_parameter distance.21"
locfile="../distance.mlw"
locfile="../optimal_replay.mlw"
loclnum="46" loccnumb="6" loccnume="14"
expl="21. loop invariant preservation"
sum="6aab714cddb46283d7611b33220a3258"
......@@ -496,7 +496,7 @@
</goal>
<goal
name="WP_parameter distance.22"
locfile="../distance.mlw"
locfile="../optimal_replay.mlw"
loclnum="46" loccnumb="6" loccnume="14"
expl="22. assertion"
sum="16f6537c10807e1368122976f96f7d9b"
......@@ -516,7 +516,7 @@
</goal>
<goal
name="WP_parameter distance.23"
locfile="../distance.mlw"
locfile="../optimal_replay.mlw"
loclnum="46" loccnumb="6" loccnume="14"
expl="23. assertion"
sum="7a49172381c019e5e4b3eb2790d3c950"
......@@ -531,7 +531,7 @@
expanded="true">
<goal
name="WP_parameter distance.23.1"
locfile="../distance.mlw"
locfile="../optimal_replay.mlw"
loclnum="46" loccnumb="6" loccnume="14"
expl="1. assertion"
sum="006cfd120b685c641dba86eefc76dc64"
......@@ -546,7 +546,7 @@
expanded="true">
<goal
name="WP_parameter distance.23.1.1"
locfile="../distance.mlw"
locfile="../optimal_replay.mlw"
loclnum="46" loccnumb="6" loccnume="14"
expl="1. assertion"
sum="c6b0f33dce7d6a0ebe404b4f56f597c8"
......@@ -566,7 +566,7 @@
</goal>
<goal
name="WP_parameter distance.23.1.2"
locfile="../distance.mlw"
locfile="../optimal_replay.mlw"
loclnum="46" loccnumb="6" loccnume="14"
expl="2. assertion"
sum="69694d863ee2eb3b6f238cb3bca7c53e"
......
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