Review changes

OCamlPro · Nov 14, 2023 · aeb6f24 · aeb6f24
1 parent 29c3841
commit aeb6f24
Showing 1 changed file with 11 additions and 7 deletions.
diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml
@@ -155,16 +155,15 @@ let main () =
   in
 
   let print_model ppf (Model ((module SAT), env)) =
-    let ur = SAT.get_unknown_reason env in
-    Printer.print_fmt (Options.Output.get_fmt_diagnostic ())
-      "@[<v 0>; Returned unknown reason = %a@]"
-      Sat_solver_sig.pp_unknown_reason_opt ur;
     match SAT.get_model env with
     | None ->
+      let ur = SAT.get_unknown_reason env in
       Printer.print_fmt (Options.Output.get_fmt_diagnostic ())
         "@[<v 0>It seems that no model has been computed so \
          far. You may need to change your model generation strategy \
-         or to increase your timeouts."
+         or to increase your timeouts. \
+         Returned unknown reason = %a@]"
+        Sat_solver_sig.pp_unknown_reason_opt ur;
 
     | Some (lazy model) ->
       Models.output_concrete_model ppf model
@@ -205,8 +204,13 @@ let main () =
       | `Sat partial_model | `Unknown partial_model ->
         begin
           let mdl = Model ((module SAT), partial_model) in
-          if Options.(get_interpretation () && get_dump_models ()) then
-            print_model (Options.Output.get_fmt_models ()) mdl;
+          if Options.(get_interpretation () && get_dump_models ()) then begin
+            let ur = SAT.get_unknown_reason partial_model in
+            Printer.print_fmt (Options.Output.get_fmt_diagnostic ())
+              "@[<v 0>Returned unknown reason = %a@]"
+              Sat_solver_sig.pp_unknown_reason_opt ur;
+            print_model (Options.Output.get_fmt_models ()) mdl
+          end;
           Some mdl
         end
       | `Unsat -> None