diff --git a/src/autoTune.ml b/src/autoTune.ml
index fefdeb32fd..79f5f51a77 100644
--- a/src/autoTune.ml
+++ b/src/autoTune.ml
@@ -99,7 +99,9 @@ let rec setCongruenceRecursive fd depth neigbourFunction =
     FunctionSet.iter
       (fun vinfo ->
          print_endline ("    " ^ vinfo.vname);
-         setCongruenceRecursive (Cilfacade.find_varinfo_fundec vinfo) (depth -1) neigbourFunction
+         match Cilfacade.find_varinfo_fundec vinfo with
+         | fd -> setCongruenceRecursive fd (depth -1) neigbourFunction
+         | exception Not_found -> () (* Happens for __goblint_bounded *)
       )
       (FunctionSet.filter (*for extern and builtin functions there is no function definition in CIL*)
          (fun x -> not (isExtern x.vstorage || BatString.starts_with x.vname "__builtin"))
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;
+}