Vc: no more "liberal_for"

Instead, we put a "stop_split" over the subsequent postcondition
under the (begin > end + 1) assumption. When this assumption is
unrealizable (strict for), this allows us to discharge the whole
branch as a single goal.

examples/binary_sort.mlw

@@ -40,7 +40,7 @@ module BinarySort
     ensures { permut_sub (old a) a 0 (length a) }
   =
     label Init in
-    "vc:liberal_for" for k = 1 to length a - 1 do
+    for k = 1 to length a - 1 do
       (* a[0..k-1) is sorted; insert a[k] *)
       invariant { forall i j. 0 <= i <= j < k -> a[i] <= a[j] }
       invariant { permut_sub (a at Init) a  0 (length a) }

examples/binary_sort/why3session.xml

@@ -5,9 +5,9 @@
 <prover id="0" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="1" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
 <file name="../binary_sort.mlw" expanded="true">
-<theory name="BinarySort" sum="97d31c2132b4c1f5f4b7af1c1da2d1d7" expanded="true">
+<theory name="BinarySort" sum="99a3ce8b569542e7790285a725075c3d" expanded="true">
  <goal name="VC occ_shift" expl="VC for occ_shift" expanded="true">
- <proof prover="0"><result status="valid" time="0.56"/></proof>
+ <proof prover="0"><result status="valid" time="0.89"/></proof>
  </goal>
  <goal name="VC binary_sort" expl="VC for binary_sort" expanded="true">
  <transf name="split_goal_wp" expanded="true">
@@ -86,11 +86,8 @@
   <goal name="VC binary_sort.25" expl="25. postcondition">
   <proof prover="1"><result status="valid" time="0.00" steps="4"/></proof>
   </goal>
-  <goal name="VC binary_sort.26" expl="26. postcondition">
-  <proof prover="1"><result status="valid" time="0.00" steps="5"/></proof>
-  </goal>
-  <goal name="VC binary_sort.27" expl="27. postcondition">
-  <proof prover="1"><result status="valid" time="0.00" steps="13"/></proof>
+  <goal name="VC binary_sort.26" expl="26. out of bounds">
+  <proof prover="1"><result status="valid" time="0.00" steps="18"/></proof>
   </goal>
  </transf>
  </goal>

examples/bubble_sort.mlw

@@ -14,7 +14,7 @@ module BubbleSort
   let bubble_sort (a: array int)
     ensures { permut_all (old a) a }
     ensures { sorted a }
-  = "vc:liberal_for" for i = length a - 1 downto 1 do
+  = for i = length a - 1 downto 1 do
       invariant { permut_all (old a) a }
       invariant { sorted_sub a i (length a) }
       invariant { forall k1 k2: int.

examples/bubble_sort/why3session.xml

@@ -4,7 +4,7 @@
 <why3session shape_version="4">
 <prover id="0" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
 <file name="../bubble_sort.mlw" expanded="true">
-<theory name="BubbleSort" sum="60fd49da6e09e444a960070c1adbab57" expanded="true">
+<theory name="BubbleSort" sum="37c384c8c40a0170c1bc001472c4710d" expanded="true">
  <goal name="VC bubble_sort" expl="VC for bubble_sort" expanded="true">
  <transf name="split_goal_wp" expanded="true">
   <goal name="VC bubble_sort.1" expl="1. loop invariant init">
@@ -16,62 +16,62 @@
   <goal name="VC bubble_sort.3" expl="3. loop invariant init">
   <proof prover="0"><result status="valid" time="0.01" steps="2"/></proof>
   </goal>
-  <goal name="VC bubble_sort.4" expl="4. loop bounds">
-  <proof prover="0"><result status="valid" time="0.00" steps="7"/></proof>
+  <goal name="VC bubble_sort.4" expl="4. loop invariant init">
+  <proof prover="0"><result status="valid" time="0.00" steps="8"/></proof>
   </goal>
   <goal name="VC bubble_sort.5" expl="5. loop invariant init">
-  <proof prover="0"><result status="valid" time="0.00" steps="7"/></proof>
+  <proof prover="0"><result status="valid" time="0.00" steps="8"/></proof>
   </goal>
   <goal name="VC bubble_sort.6" expl="6. loop invariant init">
-  <proof prover="0"><result status="valid" time="0.00" steps="7"/></proof>
+  <proof prover="0"><result status="valid" time="0.00" steps="17"/></proof>
   </goal>
   <goal name="VC bubble_sort.7" expl="7. loop invariant init">
-  <proof prover="0"><result status="valid" time="0.00" steps="16"/></proof>
+  <proof prover="0"><result status="valid" time="0.01" steps="10"/></proof>
   </goal>
-  <goal name="VC bubble_sort.8" expl="8. loop invariant init">
-  <proof prover="0"><result status="valid" time="0.01" steps="9"/></proof>
+  <goal name="VC bubble_sort.8" expl="8. index in array bounds">
+  <proof prover="0"><result status="valid" time="0.00" steps="13"/></proof>
   </goal>
   <goal name="VC bubble_sort.9" expl="9. index in array bounds">
-  <proof prover="0"><result status="valid" time="0.00" steps="12"/></proof>
+  <proof prover="0"><result status="valid" time="0.01" steps="13"/></proof>
   </goal>
-  <goal name="VC bubble_sort.10" expl="10. index in array bounds">
-  <proof prover="0"><result status="valid" time="0.01" steps="12"/></proof>
+  <goal name="VC bubble_sort.10" expl="10. precondition">
+  <proof prover="0"><result status="valid" time="0.01" steps="19"/></proof>
   </goal>
-  <goal name="VC bubble_sort.11" expl="11. precondition">
-  <proof prover="0"><result status="valid" time="0.01" steps="18"/></proof>
+  <goal name="VC bubble_sort.11" expl="11. loop invariant preservation">
+  <proof prover="0"><result status="valid" time="0.06" steps="151"/></proof>
   </goal>
   <goal name="VC bubble_sort.12" expl="12. loop invariant preservation">
-  <proof prover="0"><result status="valid" time="0.06" steps="150"/></proof>
+  <proof prover="0"><result status="valid" time="0.04" steps="121"/></proof>
   </goal>
   <goal name="VC bubble_sort.13" expl="13. loop invariant preservation">
-  <proof prover="0"><result status="valid" time="0.04" steps="120"/></proof>
+  <proof prover="0"><result status="valid" time="0.07" steps="186"/></proof>
   </goal>
   <goal name="VC bubble_sort.14" expl="14. loop invariant preservation">
-  <proof prover="0"><result status="valid" time="0.07" steps="185"/></proof>
+  <proof prover="0"><result status="valid" time="0.02" steps="75"/></proof>
   </goal>
   <goal name="VC bubble_sort.15" expl="15. loop invariant preservation">
-  <proof prover="0"><result status="valid" time="0.02" steps="74"/></proof>
+  <proof prover="0"><result status="valid" time="0.00" steps="14"/></proof>
   </goal>
   <goal name="VC bubble_sort.16" expl="16. loop invariant preservation">
-  <proof prover="0"><result status="valid" time="0.00" steps="13"/></proof>
+  <proof prover="0"><result status="valid" time="0.00" steps="14"/></proof>
   </goal>
   <goal name="VC bubble_sort.17" expl="17. loop invariant preservation">
-  <proof prover="0"><result status="valid" time="0.00" steps="13"/></proof>
+  <proof prover="0"><result status="valid" time="0.01" steps="26"/></proof>
   </goal>
   <goal name="VC bubble_sort.18" expl="18. loop invariant preservation">
-  <proof prover="0"><result status="valid" time="0.01" steps="25"/></proof>
+  <proof prover="0"><result status="valid" time="0.01" steps="24"/></proof>
   </goal>
   <goal name="VC bubble_sort.19" expl="19. loop invariant preservation">
-  <proof prover="0"><result status="valid" time="0.01" steps="23"/></proof>
+  <proof prover="0"><result status="valid" time="0.01" steps="11"/></proof>
   </goal>
   <goal name="VC bubble_sort.20" expl="20. loop invariant preservation">
-  <proof prover="0"><result status="valid" time="0.01" steps="10"/></proof>
+  <proof prover="0"><result status="valid" time="0.01" steps="42"/></proof>
   </goal>
   <goal name="VC bubble_sort.21" expl="21. loop invariant preservation">
-  <proof prover="0"><result status="valid" time="0.01" steps="41"/></proof>
+  <proof prover="0"><result status="valid" time="0.01" steps="24"/></proof>
   </goal>
-  <goal name="VC bubble_sort.22" expl="22. loop invariant preservation">
-  <proof prover="0"><result status="valid" time="0.01" steps="23"/></proof>
+  <goal name="VC bubble_sort.22" expl="22. out of bounds">
+  <proof prover="0"><result status="valid" time="0.00" steps="7"/></proof>
   </goal>
   <goal name="VC bubble_sort.23" expl="23. postcondition">
   <proof prover="0"><result status="valid" time="0.00" steps="5"/></proof>
@@ -79,11 +79,8 @@
   <goal name="VC bubble_sort.24" expl="24. postcondition">
   <proof prover="0"><result status="valid" time="0.00" steps="6"/></proof>
   </goal>
-  <goal name="VC bubble_sort.25" expl="25. postcondition">
-  <proof prover="0"><result status="valid" time="0.00" steps="4"/></proof>
-  </goal>
-  <goal name="VC bubble_sort.26" expl="26. postcondition">
-  <proof prover="0"><result status="valid" time="0.00" steps="4"/></proof>
+  <goal name="VC bubble_sort.25" expl="25. out of bounds">
+  <proof prover="0"><result status="valid" time="0.00" steps="12"/></proof>
   </goal>
  </transf>
  </goal>

examples/insertion_sort.mlw

@@ -12,7 +12,7 @@ module InsertionSort
 
   let insertion_sort (a: array int)
     ensures { sorted a /\ permut_all (old a) a }
-  = "vc:liberal_for" for i = 1 to length a - 1 do
+  = for i = 1 to length a - 1 do
       (* a[0..i[ is sorted; now insert a[i] *)
       invariant { sorted_sub a 0 i /\ permut_all (old a) a }
       let v = a[i] in
@@ -90,7 +90,7 @@ module InsertionSortGen
 
   let insertion_sort (a: array elt)
     ensures { sorted a /\ permut_all (old a) a }
-  = "vc:liberal_for" for i = 1 to length a - 1 do
+  = for i = 1 to length a - 1 do
       (* a[0..i[ is sorted; now insert a[i] *)
       invariant { sorted_sub a 0 i /\ permut_all (old a) a }
       let v = a[i] in

examples/insertion_sort/why3session.xml

@@ -4,7 +4,7 @@
 <why3session shape_version="4">
 <prover id="3" name="Alt-Ergo" version="1.30" timelimit="36" steplimit="0" memlimit="1000"/>
 <file name="../insertion_sort.mlw" expanded="true">
-<theory name="InsertionSort" sum="768e96847d501577e3bcd5acc10642b7" expanded="true">
+<theory name="InsertionSort" sum="0ff7000b58975d960a0cfedb21e74cdc" expanded="true">
  <goal name="VC insertion_sort" expl="VC for insertion_sort" expanded="true">
  <transf name="split_goal_wp" expanded="true">
   <goal name="VC insertion_sort.1" expl="1. loop invariant init">
@@ -79,9 +79,9 @@
  <proof prover="3"><result status="valid" time="0.01" steps="28"/></proof>
  </goal>
 </theory>
-<theory name="InsertionSortGen" sum="e5ec9b0f6ffd9cabbe60ac1a6d538886" expanded="true">
+<theory name="InsertionSortGen" sum="50a9cb1ad6d5481b25700b8f407f3dc5" expanded="true">
  <goal name="VC insertion_sort" expl="VC for insertion_sort" expanded="true">
- <proof prover="3"><result status="valid" time="2.08" steps="3069"/></proof>
+ <proof prover="3"><result status="valid" time="2.54" steps="3264"/></proof>
  </goal>
 </theory>
 </file>

examples/quicksort.mlw

@@ -79,7 +79,7 @@ module Shuffle "Knuth shuffle"
   let shuffle (a: array int) : unit
     writes  { a, Random.s }
     ensures { permut_all (old a) a }
-  = "vc:liberal_for" for i = 1 to length a - 1 do
+  = for i = 1 to length a - 1 do
       invariant { permut_all (old a) a }
       swap a i (Random.random_int (i+1))
     done

examples/quicksort/why3session.xml

@@ -4,92 +4,92 @@
 <why3session shape_version="4">
 <prover id="1" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
 <file name="../quicksort.mlw" expanded="true">
-<theory name="Quicksort" sum="63fb5fb89790878f75f7a14acacbb39a">
- <goal name="VC quick_rec" expl="VC for quick_rec">
- <transf name="split_goal_wp">
+<theory name="Quicksort" sum="eeb4a76bba86f77e3c7dbc040fdc69d2" expanded="true">
+ <goal name="VC quick_rec" expl="VC for quick_rec" expanded="true">
+ <transf name="split_goal_wp" expanded="true">
   <goal name="VC quick_rec.1" expl="1. index in array bounds">
   <proof prover="1"><result status="valid" time="0.01" steps="5"/></proof>
   </goal>
-  <goal name="VC quick_rec.2" expl="2. loop bounds">
-  <proof prover="1"><result status="valid" time="0.00" steps="5"/></proof>
+  <goal name="VC quick_rec.2" expl="2. loop invariant init">
+  <proof prover="1"><result status="valid" time="0.01" steps="6"/></proof>
   </goal>
   <goal name="VC quick_rec.3" expl="3. loop invariant init">
-  <proof prover="1"><result status="valid" time="0.01" steps="5"/></proof>
+  <proof prover="1"><result status="valid" time="0.00" steps="6"/></proof>
   </goal>
   <goal name="VC quick_rec.4" expl="4. loop invariant init">
-  <proof prover="1"><result status="valid" time="0.00" steps="5"/></proof>
+  <proof prover="1"><result status="valid" time="0.00" steps="6"/></proof>
   </goal>
   <goal name="VC quick_rec.5" expl="5. loop invariant init">
-  <proof prover="1"><result status="valid" time="0.00" steps="5"/></proof>
+  <proof prover="1"><result status="valid" time="0.01" steps="17"/></proof>
   </goal>
-  <goal name="VC quick_rec.6" expl="6. loop invariant init">
-  <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
+  <goal name="VC quick_rec.6" expl="6. index in array bounds">
+  <proof prover="1"><result status="valid" time="0.01" steps="13"/></proof>
   </goal>
-  <goal name="VC quick_rec.7" expl="7. index in array bounds">
-  <proof prover="1"><result status="valid" time="0.01" steps="12"/></proof>
+  <goal name="VC quick_rec.7" expl="7. precondition">
+  <proof prover="1"><result status="valid" time="0.01" steps="18"/></proof>
   </goal>
-  <goal name="VC quick_rec.8" expl="8. precondition">
-  <proof prover="1"><result status="valid" time="0.01" steps="17"/></proof>
+  <goal name="VC quick_rec.8" expl="8. assertion">
+  <proof prover="1"><result status="valid" time="0.01" steps="24"/></proof>
   </goal>
-  <goal name="VC quick_rec.9" expl="9. assertion">
-  <proof prover="1"><result status="valid" time="0.01" steps="23"/></proof>
+  <goal name="VC quick_rec.9" expl="9. loop invariant preservation">
+  <proof prover="1"><result status="valid" time="0.01" steps="50"/></proof>
   </goal>
   <goal name="VC quick_rec.10" expl="10. loop invariant preservation">
-  <proof prover="1"><result status="valid" time="0.01" steps="49"/></proof>
+  <proof prover="1"><result status="valid" time="0.06" steps="143"/></proof>
   </goal>
   <goal name="VC quick_rec.11" expl="11. loop invariant preservation">
-  <proof prover="1"><result status="valid" time="0.06" steps="142"/></proof>
+  <proof prover="1"><result status="valid" time="0.08" steps="177"/></proof>
   </goal>
   <goal name="VC quick_rec.12" expl="12. loop invariant preservation">
-  <proof prover="1"><result status="valid" time="0.08" steps="176"/></proof>
+  <proof prover="1"><result status="valid" time="0.02" steps="133"/></proof>
   </goal>
   <goal name="VC quick_rec.13" expl="13. loop invariant preservation">
-  <proof prover="1"><result status="valid" time="0.02" steps="132"/></proof>
+  <proof prover="1"><result status="valid" time="0.01" steps="14"/></proof>
   </goal>
   <goal name="VC quick_rec.14" expl="14. loop invariant preservation">
-  <proof prover="1"><result status="valid" time="0.01" steps="13"/></proof>
+  <proof prover="1"><result status="valid" time="0.01" steps="21"/></proof>
   </goal>
   <goal name="VC quick_rec.15" expl="15. loop invariant preservation">
-  <proof prover="1"><result status="valid" time="0.01" steps="20"/></proof>
+  <proof prover="1"><result status="valid" time="0.01" steps="21"/></proof>
   </goal>
   <goal name="VC quick_rec.16" expl="16. loop invariant preservation">
-  <proof prover="1"><result status="valid" time="0.01" steps="20"/></proof>
+  <proof prover="1"><result status="valid" time="0.00" steps="14"/></proof>
   </goal>
-  <goal name="VC quick_rec.17" expl="17. loop invariant preservation">
-  <proof prover="1"><result status="valid" time="0.00" steps="13"/></proof>
+  <goal name="VC quick_rec.17" expl="17. precondition">
+  <proof prover="1"><result status="valid" time="0.01" steps="14"/></proof>
   </goal>
-  <goal name="VC quick_rec.18" expl="18. precondition">
-  <proof prover="1"><result status="valid" time="0.01" steps="13"/></proof>
+  <goal name="VC quick_rec.18" expl="18. assertion">
+  <proof prover="1"><result status="valid" time="0.21" steps="412"/></proof>
   </goal>
-  <goal name="VC quick_rec.19" expl="19. assertion">
-  <proof prover="1"><result status="valid" time="0.21" steps="411"/></proof>
+  <goal name="VC quick_rec.19" expl="19. variant decrease">
+  <proof prover="1"><result status="valid" time="0.01" steps="14"/></proof>
   </goal>
-  <goal name="VC quick_rec.20" expl="20. variant decrease">
-  <proof prover="1"><result status="valid" time="0.01" steps="13"/></proof>
+  <goal name="VC quick_rec.20" expl="20. precondition">
+  <proof prover="1"><result status="valid" time="0.01" steps="14"/></proof>
   </goal>
-  <goal name="VC quick_rec.21" expl="21. precondition">
-  <proof prover="1"><result status="valid" time="0.01" steps="13"/></proof>
+  <goal name="VC quick_rec.21" expl="21. assertion">
+  <proof prover="1"><result status="valid" time="0.37" steps="445"/></proof>
   </goal>
-  <goal name="VC quick_rec.22" expl="22. assertion">
-  <proof prover="1"><result status="valid" time="0.23" steps="444"/></proof>
+  <goal name="VC quick_rec.22" expl="22. variant decrease">
+  <proof prover="1"><result status="valid" time="0.01" steps="18"/></proof>
   </goal>
-  <goal name="VC quick_rec.23" expl="23. variant decrease">
-  <proof prover="1"><result status="valid" time="0.01" steps="17"/></proof>
+  <goal name="VC quick_rec.23" expl="23. precondition">
+  <proof prover="1"><result status="valid" time="0.01" steps="18"/></proof>
   </goal>
-  <goal name="VC quick_rec.24" expl="24. precondition">
-  <proof prover="1"><result status="valid" time="0.01" steps="17"/></proof>
+  <goal name="VC quick_rec.24" expl="24. assertion">
+  <proof prover="1"><result status="valid" time="0.43" steps="500"/></proof>
   </goal>
   <goal name="VC quick_rec.25" expl="25. assertion">
-  <proof prover="1"><result status="valid" time="0.28" steps="499"/></proof>
+  <proof prover="1"><result status="valid" time="0.04" steps="188"/></proof>
   </goal>
-  <goal name="VC quick_rec.26" expl="26. assertion">
-  <proof prover="1"><result status="valid" time="0.04" steps="187"/></proof>
+  <goal name="VC quick_rec.26" expl="26. postcondition">
+  <proof prover="1"><result status="valid" time="0.11" steps="232"/></proof>
   </goal>
   <goal name="VC quick_rec.27" expl="27. postcondition">
-  <proof prover="1"><result status="valid" time="0.11" steps="231"/></proof>
+  <proof prover="1"><result status="valid" time="0.17" steps="440"/></proof>
   </goal>
-  <goal name="VC quick_rec.28" expl="28. postcondition">
-  <proof prover="1"><result status="valid" time="0.17" steps="439"/></proof>
+  <goal name="VC quick_rec.28" expl="28. out of bounds">
+  <proof prover="1"><result status="valid" time="0.00" steps="5"/></proof>
   </goal>
   <goal name="VC quick_rec.29" expl="29. postcondition">
   <proof prover="1"><result status="valid" time="0.00" steps="7"/></proof>
@@ -103,17 +103,17 @@
  <proof prover="1"><result status="valid" time="0.01" steps="22"/></proof>
  </goal>
 </theory>
-<theory name="Shuffle" sum="4f4860e2acd354b6d74bd600170dabe3" expanded="true">
+<theory name="Shuffle" sum="e6f2f5a70b1d5d1cc17268a13712044f" expanded="true">
  <goal name="VC shuffle" expl="VC for shuffle" expanded="true">
- <proof prover="1"><result status="valid" time="0.01" steps="57"/></proof>
+ <proof prover="1"><result status="valid" time="0.01" steps="55"/></proof>
  </goal>
 </theory>
-<theory name="QuicksortWithShuffle" sum="dc5640e3f07dca7f1e8514f0d9ce5d99">
+<theory name="QuicksortWithShuffle" sum="61b97c1776588ab1380c18fde1791ff5">
  <goal name="VC qs" expl="VC for qs">
- <proof prover="1"><result status="valid" time="0.01" steps="13"/></proof>
+ <proof prover="1"><result status="valid" time="0.01" steps="11"/></proof>
  </goal>
 </theory>
-<theory name="Quicksort3way" sum="f57c407e929f5dfb68ad22319edd4be8">
+<theory name="Quicksort3way" sum="4cc656ddd5c92b511ca8e1b98def01f6">
  <goal name="VC quick_rec" expl="VC for quick_rec">
  <proof prover="1"><result status="valid" time="3.61" steps="6499"/></proof>
  <transf name="split_goal_wp">
@@ -249,7 +249,7 @@
  <proof prover="1"><result status="valid" time="0.01" steps="22"/></proof>
  </goal>
  <goal name="VC qs" expl="VC for qs">
- <proof prover="1"><result status="valid" time="0.00" steps="13"/></proof>
+ <proof prover="1"><result status="valid" time="0.00" steps="11"/></proof>
  </goal>
 </theory>
 <theory name="Test" sum="ccc3b6dd7c4ce24c07eda4da0dce770f">

src/mlw/vc.ml

@@ -52,10 +52,8 @@ let proxy_of_expr =
 
 let sp_label = Ident.create_label "vc:sp"
 let wp_label = Ident.create_label "vc:wp"
-let lf_label = Ident.create_label "vc:liberal_for"
 
-let vc_labels = Slab.add lf_label
-  (Slab.add sp_label (Slab.add wp_label Slab.empty))
+let vc_labels = Slab.add sp_label (Slab.add wp_label Slab.empty)
 
 (* VCgen environment *)
 
@@ -102,6 +100,7 @@ let expl_check     = Ident.create_label "expl:check"
 let expl_lemma     = Ident.create_label "expl:lemma"
 let expl_absurd    = Ident.create_label "expl:unreachable point"
 let expl_for_bound = Ident.create_label "expl:loop bounds"
+let expl_off_bound = Ident.create_label "expl:out of loop bounds"
 let expl_loop_init = Ident.create_label "expl:loop invariant init"
 let expl_loop_keep = Ident.create_label "expl:loop invariant preservation"
 let expl_loop_vari = Ident.create_label "expl:loop variant decrease"
@@ -315,7 +314,7 @@ let cty_enrich_post c = match c with
 
 (* k-expressions: simplified code *)
 
-type ktag = WP | SP | Out of bool Mint.t | Push of bool
+type ktag = WP | SP | Out of bool Mint.t | Push of bool | Off of label
 
 type kode =
   | Kseq   of kode * int * kode           (* 0: sequence, N: try-with *)
@@ -378,6 +377,8 @@ let rec k_print fmt k = match k with
       (Pp.print_list Pp.space Pp.int) (Mint.keys out) k_print k
   | Ktag (Push cl, k) -> Format.fprintf fmt "@[<hov 4>PUSH %s %a@]"
       (if cl then "CLOSED" else "OPEN") k_print k
+  | Ktag (Off lab, k) -> Format.fprintf fmt "@[<hov 4>OFF %s %a@]"
+      lab.lab_string k_print k
 
 (* check if a pure k-expression can be converted to a term.
    We need this for simple conjuctions, disjuctions, and
@@ -436,6 +437,11 @@ let complete_xpost cty {eff_raises = xss} skip =
   Mxs.set_union (Mxs.set_inter cty.cty_xpost xss)
     (Mxs.map (fun () -> []) (Mxs.set_diff xss skip))
 
+let wp_solder expl wp =
+  if can_simp wp then wp else
+  let wp = t_label_add stop_split wp in
+  if lab_has_expl wp.t_label then wp else t_label_add expl wp
+
 let rec explain_inv loc f = match f.t_node with
   | Tapp _ -> vc_expl loc Slab.empty expl_type_inv f
   | _ -> t_map (explain_inv loc) (t_label ?loc Slab.empty f)
@@ -452,7 +458,6 @@ let inv_of_pvs, inv_of_loop =
     let fl = List.fold_left add_varl fl varl in
     List.map (explain_inv loc) (Typeinv.inspect kn fl))
 
-
 let assume_inv inv k = Kseq (Kval ([], inv), 0, k)
 let assert_inv inv k = Kpar (Kstop inv, assume_inv inv k)
 
@@ -748,20 +753,14 @@ let rec k_expr env lps ({e_loc = loc} as e) res xmap =
         let k = Kpar (k, Kval ([res], last)) in
         let k = List.fold_right assume_inv iinv k in
         let k = Kpar (j, k_havoc e.e_effect k) in
-        if Slab.mem lf_label e.e_label then (* "liberal for"
-          [ ASSUME a <= b ;
-            [ STOP inv[a]
-            | HAVOC ; [ ASSUME a <= v <= b /\ inv[v] ; e1 ; STOP inv[v+1]
-                      | ASSUME inv[b+1] ] ]
-          | ASSUME a > b ] *)
-          Kpar (Kseq (Kval ([], expl_bounds (ps_app le [a; b])), 0, k),
-                   Kval ([res], expl_bounds (ps_app gt [a; b])))
-        else (* "strict for"
-          [ STOP a <= b+1
-          | STOP inv[a]
-          | HAVOC ; [ ASSUME a <= v <= b /\ inv[v] ; e1 ; STOP inv[v+1]
-                    | ASSUME inv[b+1] ] ] *)
-          Kpar (Kstop (expl_bounds (ps_app le [a; b_pl_1])), k)
+        (* [ ASSUME a <= b+1 ;
+             [ STOP inv[a]
+             | HAVOC ; [ ASSUME a <= v <= b /\ inv[v] ; e1 ; STOP inv[v+1]
+                       | ASSUME inv[b+1] ] ]
+           | ASSUME a > b+1 ] *)
+        Kpar (Kseq (Kval ([], expl_bounds (ps_app le [a; b_pl_1])), 0, k),
+           Kseq (Kval ([res], expl_bounds (ps_app gt [a; b_pl_1])), 0,
+                 Ktag (Off expl_off_bound, Kcont 0)))
   in
   if Slab.mem sp_label e.e_label then Ktag (SP, k) else
   if Slab.mem wp_label e.e_label then Ktag (WP, k) else k
@@ -860,8 +859,11 @@ let reflow vc_wp k =
     | Kcont i ->
         k, Mint.singleton i true
     | Kaxiom k ->
-        let k, _ = mark vc_tag k in
+        let k, _ = mark WP k in
         Kaxiom k, Mint.singleton 0 true
+    | Ktag ((Off _) as tag, k) ->
+        let k, out = mark tag k in
+        Ktag (tag, k), out
     | Ktag ((WP|SP) as tag, k) when tag <> vc_tag ->
         let k, out = mark tag k in
         (* A switch from SP to WP is only sound when the kode
@@ -915,6 +917,8 @@ let reflow vc_wp k =
         begin match Mint.find_opt 0 q with
         | Some (q, _) -> Kseq (Kaxiom k, 0, q)
         | None -> Kaxiom k end
+    | Ktag ((Off _) as tag, k) ->
+        Ktag (tag, push k q)
     | Ktag ((WP|SP|Out _) as tag, k) ->
         Ktag (tag, push k Mint.empty)
     | Ktag (Push _, _) ->
@@ -1271,6 +1275,9 @@ let rec sp_expr kn k rdm dst = match k with
       let f = vc_expl None Slab.empty expl_lemma f in
       let rd = t_freepvs (Mint.find 0 rdm) f in
       t_true, Mint.singleton 0 (f, Mpv.empty), rd
+  | Ktag (Off expl, k) ->
+      let wp, sp, rd = sp_expr kn k rdm dst in
+      wp_solder expl wp, sp, rd
   | Ktag (Out out, k) ->
       sp_expr kn k (Mint.set_inter rdm out) dst
   | Ktag (WP, k) ->
@@ -1321,6 +1328,8 @@ and wp_expr kn k q = match k with
       let f = wp_expr kn k Mint.empty in
       let f = vc_expl None Slab.empty expl_lemma f in
       sp_implies f (Mint.find 0 q)
+  | Ktag (Off expl, k) ->
+      wp_solder expl (wp_expr kn k q)
   | Ktag (Out out, k) ->
       wp_expr kn k (Mint.set_inter q out)
   | Ktag (SP, k) ->