Fix model output

OCamlPro · Sep 21, 2023 · c7f8263 · c7f8263
1 parent 2619445
commit c7f8263
Showing 1 changed file with 1 addition and 5 deletions.
diff --git a/src/lib/frontend/models.ml b/src/lib/frontend/models.ml
@@ -493,11 +493,7 @@ let output_concrete_model fmt m =
           for which model generation is known to be incomplete. @.";
 
     Format.fprintf fmt "@[<v 2>(";
-    Why3CounterExample.output_constraints fmt m.propositional;
-
-    Printer.print_fmt ~flushed:false fmt "@[<v 0>unknown@ ";
-    Printer.print_fmt ~flushed:false fmt "@[<v 2>(model@,";
-    if Options.get_output_format () == Why3 then begin
+    if Options.get_model_type_constraints () then begin
       Why3CounterExample.output_constraints fmt m.propositional
     end;