Explain 82-widen/03-mihaila-widen-slide-delay

tests/regression/82-widen/02-mihaila-widen-fig7-delay.c

@@ -1,5 +1,10 @@
 // PARAM: --disable ana.int.def_exc --enable ana.int.interval --enable ana.sv-comp.functions --set ana.widen.delay.local 1
 // From "Widening as Abstract Domain", Fig. 7: https://doi.org/10.1007/978-3-642-38088-4_12
+// Delay 1:
+// 0. {x -> [0,0], y -> [0,0]}
+// 1. {x -> [0,4], y -> [0,1]} (delay 0 would widen already here)
+// 2. {x -> [0,+inf], y -> [0,1]}
+// narrow: {x -> [0,103], y -> [0,1]}
 #include <goblint.h>
 extern _Bool __VERIFIER_nondet_bool();
 

tests/regression/82-widen/03-mihaila-widen-slide-delay.c

@@ -1,6 +1,12 @@
 // PARAM: --disable ana.int.def_exc --enable ana.int.interval --set ana.widen.delay.local 3
 // From "Widening as Abstract Domain" slides: https://bytebucket.org/mihaila/bindead/wiki/resources/widening-talk.pdf
-// They claim delay 2, we need 3 for some reason. Why?
+// They claim delay 2, we need 3:
+// 0. {x -> [0,0], y -> [0,0]}
+// 1. {x -> [0,4], y -> [0,0]}
+// 2. {x -> [0,8], y -> [0,0]}
+// 3. {x -> [0,12], y -> [0,1]} (delay 2 would widen already here)
+// 4. {x -> [0,+inf], y -> [0,1]}
+// narrow: {x -> [0,103], y -> [0,1]}
 #include <goblint.h>
 
 int main() {