From c7f8263c4138a572adbbdc56e8659cbb83ed75f1 Mon Sep 17 00:00:00 2001
From: Pierre Villemot <tiky.halbaroth@gmail.com>
Date: Thu, 21 Sep 2023 15:03:24 +0200
Subject: [PATCH] Fix model output

---
 src/lib/frontend/models.ml | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

diff --git a/src/lib/frontend/models.ml b/src/lib/frontend/models.ml
index 0454b12e08..cadba8bb0d 100644
--- 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;