Add example where autotuner crashed when trying to activate congruenc…

…e domain when termination was enabled
goblint · Nov 23, 2023 · 9b954b5 · 9b954b5
1 parent 5be07e5
commit 9b954b5
Showing 1 changed file with 14 additions and 0 deletions.
diff --git a/tests/regression/78-termination/51-modulo.c b/tests/regression/78-termination/51-modulo.c
@@ -0,0 +1,14 @@
+// SKIP TERM PARAM: --enable ana.autotune.enabled --enable ana.sv-comp.functions --enable ana.sv-comp.enabled  --set ana.autotune.activated "['congruence']" --set ana.specification "CHECK( init(main()), LTL(F end) )"
+
+// This task previously crashed due to the autotuner
+int main() {
+	int a;
+    int odd, count = 0;
+    while(a > 1) {
+      odd = a % 2;
+      if(!odd) a = a / 2;
+      else a = a - 1;
+      count++;
+    }
+    return count;
+}