Fix issue 719

src/bin/common/solving_loop.ml

@@ -81,7 +81,7 @@ let main () =
           Options.Time.set_timeout (Options.get_timelimit ());
         end;
       SAT.reset_refs ();
-      let partial_model, _, _ =
+      let partial_model, consistent, _ =
         List.fold_left
           (FE.process_decl FE.print_status used_context consistent_dep_stack)
           (SAT.empty (), true, Explanation.empty) cnf
@@ -93,7 +93,12 @@ let main () =
           (Steps.get_steps ())
           (Signals_profiling.get_timers ())
           (Options.Output.get_fmt_err ());
-      Some partial_model
+      (* If the status of the SAT environment is inconsistent,
+         we have to drop the partial model in order to prevent
+         printing wrong model. *)
+      if consistent then
+        Some partial_model
+      else None
     with Util.Timeout ->
       if not (Options.get_timelimit_per_goal()) then exit 142;
       None

tests/models/issues/719.models.expected

@@ -0,0 +1,3 @@
+
+unsat
+(error "No model produced.")

tests/models/issues/719.models.smt2

@@ -0,0 +1,18 @@
+(set-logic ALL)
+(set-option :produce-models true)
+(declare-const a (Array Int Int))
+(declare-const s Int)
+(assert (and (<= 0 s) (<= s 10)))
+(assert (forall ((k Int)) (=> (and (<= 0 k) (< k s)) (<= (select a k) (select a s)))))
+(assert (forall ((k Int)) (=> (and (< s k) (<= k 10)) (<= (select a s) (select a k)))))
+(assert (
+  forall ((p Int) (q Int))
+    (=> (and (<= 0 p) (< p q) (<= q (- s 1))) (<= (select a p) (select a q)))))
+(assert (
+  forall ((p Int) (q Int))
+    (=> (and (<= (+ s 1) p) (< p q) (<= q 10)) (<= (select a p) (select a q)))))
+(assert (not (
+  forall ((p Int) (q Int))
+    (=> (and (<= 0 p) (< p q) (<= q 10)) (<= (select a p) (select a q))))))
+(check-sat)
+(get-model)