Add local widen/narrow example from A²I paper

Co-authored-by: Sarah Tilscher <[email protected]>
goblint · Aug 14, 2023 · b1b710e · b1b710e
1 parent 1be70e1
commit b1b710e
Showing 1 changed file with 22 additions and 0 deletions.
diff --git a/tests/regression/34-localwn_restart/06-td-a2i.c b/tests/regression/34-localwn_restart/06-td-a2i.c
@@ -0,0 +1,22 @@
+// PARAM: --enable ana.int.interval --set solver td3 --enable solvers.td3.remove-wpoint
+// Example from "The Top-Down Solver — An Exercise in A²I", Section 6.
+#include <goblint.h>
+
+int main() {
+  int i, j, x;
+  i = 0;
+  while (i < 42) {
+    j = 0;
+    while (j < 17) {
+      x = i + j;
+      j++;
+    }
+    __goblint_check(j == 17);
+    __goblint_check(i >= 0);
+    __goblint_check(i <= 41);
+    i++;
+  }
+  __goblint_check(i == 42);
+  __goblint_check(j == 17); // TODO
+  return 0;
+}