diff --git a/colibri2/core/interp.ml b/colibri2/core/interp.ml
index eb5db96ac1e8cff792125fe83589238151ded222..a59f0c524489547072a27c853b558989c07a2dac 100644
--- a/colibri2/core/interp.ml
+++ b/colibri2/core/interp.ml
@@ -470,15 +470,19 @@ module Fix_model = struct
                     |> (fun s -> s 0)
                     |> Sequence.to_list |> Sequence.of_list
                   in
-                  let seq =
-                    Sequence.map seq ~f:(fun v d ->
-                        Egraph.set_env d Data.env (During { r with nextnode });
-                        Debug.dprintf4 debug "FixModel by setting %a to %a"
-                          Node.pp n Value.pp v;
-                        Egraph.register d n;
-                        Egraph.set_value d n v)
-                  in
-                  seq)
+                  if Sequence.is_empty seq then
+                    (* Usually because the limit has been reached *)
+                    Egraph.contradiction d
+                  else
+                    let seq =
+                      Sequence.map seq ~f:(fun v d ->
+                          Egraph.set_env d Data.env (During { r with nextnode });
+                          Debug.dprintf4 debug "FixModel by setting %a to %a"
+                            Node.pp n Value.pp v;
+                          Egraph.register d n;
+                          Egraph.set_value d n v)
+                    in
+                    seq)
         in
         aux r.nextnode
 end
diff --git a/colibri2/tests/solve/colibri/sat/div_zero.smt2 b/colibri2/tests/solve/colibri/sat/div_zero.smt2
index 8d767d6113ec3984b5daea9c3c6af2184cc2a10b..3bd2746efdbe975c757b3f9e89b0514bb7d84a3d 100644
--- a/colibri2/tests/solve/colibri/sat/div_zero.smt2
+++ b/colibri2/tests/solve/colibri/sat/div_zero.smt2
@@ -1,7 +1,7 @@
 ;; produced by colibri.drv ;;
 (set-logic ALL)
 (set-info :smt-lib-version 2.6)
-(set-info :status-colibri2 sat)
+(set-info :status-colibri2 steplimitreached)
 (declare-sort tuple0 0)
 
 ;;  uncomment to pass the VC to cvc4 or z3
diff --git a/colibri2/tests/solve/colibri/sat/mod_repr.smt2 b/colibri2/tests/solve/colibri/sat/mod_repr.smt2
index aec432c088cca35a615e9a855f8e2e28db0c8a0a..7a7e46330ad2dd09d0d8995c260707004b314e7b 100644
--- a/colibri2/tests/solve/colibri/sat/mod_repr.smt2
+++ b/colibri2/tests/solve/colibri/sat/mod_repr.smt2
@@ -1,7 +1,7 @@
 ;; produced by colibri.drv ;;
 (set-logic ALL)
 (set-info :smt-lib-version 2.6)
-(set-info :status-colibri2 sat)
+(set-info :status-colibri2 steplimitreached)
 
 (define-fun mod1 ((x Int) (y Int)) Int (ite (< 0 y) (mod x y) (+ (mod x y) y)))