From 9b954b5cd0b14a146267bc80c476d6a81e281643 Mon Sep 17 00:00:00 2001
From: Julian Erhard <julian.erhard@tum.de>
Date: Thu, 23 Nov 2023 15:00:25 +0100
Subject: [PATCH] Add example where autotuner crashed when trying to activate
 congruence domain when termination was enabled

---
 tests/regression/78-termination/51-modulo.c | 14 ++++++++++++++
 1 file changed, 14 insertions(+)
 create mode 100644 tests/regression/78-termination/51-modulo.c

diff --git a/tests/regression/78-termination/51-modulo.c b/tests/regression/78-termination/51-modulo.c
new file mode 100644
index 0000000000..5f5b8f1924
--- /dev/null
+++ 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;
+}