From 2eca6d6488d94052bc77c43a0afab582c04c2aa0 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 7 Jun 2024 15:57:58 +0300
Subject: [PATCH] Explain 82-widen/03-mihaila-widen-slide-delay

---
 tests/regression/82-widen/02-mihaila-widen-fig7-delay.c  | 5 +++++
 tests/regression/82-widen/03-mihaila-widen-slide-delay.c | 8 +++++++-
 2 files changed, 12 insertions(+), 1 deletion(-)

diff --git a/tests/regression/82-widen/02-mihaila-widen-fig7-delay.c b/tests/regression/82-widen/02-mihaila-widen-fig7-delay.c
index 4106bf985d..e0d908ff69 100644
--- a/tests/regression/82-widen/02-mihaila-widen-fig7-delay.c
+++ b/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();
 
diff --git a/tests/regression/82-widen/03-mihaila-widen-slide-delay.c b/tests/regression/82-widen/03-mihaila-widen-slide-delay.c
index 5f511e1a4c..720bcb04d0 100644
--- a/tests/regression/82-widen/03-mihaila-widen-slide-delay.c
+++ b/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() {