[Interp] Fix model fixing

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

colibri2/tests/solve/colibri/sat/div_zero.smt2

 ;; 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

colibri2/tests/solve/colibri/sat/mod_repr.smt2

 ;; 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)))