Print always smtlib comments in the models

OCamlPro · Sep 15, 2023 · 3254796 · 3254796
1 parent 61b7d1a
commit 3254796
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 9 deletions.
diff --git a/src/lib/frontend/models.ml b/src/lib/frontend/models.ml
@@ -449,20 +449,20 @@ module SmtlibCounterExample = struct
     if not (Options.get_objectives_in_interpretation()) &&
        not (Util.MI.is_empty objectives)
     then begin
-      Format.fprintf fmt "@[<v 3>(objectives";
+      Format.fprintf fmt "@[<v 3>; (objectives";
       Util.MI.iter
         (fun _i (e, x) ->
-           Format.fprintf fmt "@ (%a %a)"
+           Format.fprintf fmt "@ ; (%a %a)"
              E.print e
              (fun fmt () ->
                 match x with
                 | Obj_pinfty -> Format.fprintf fmt "+oo"
                 | Obj_minfty -> Format.fprintf fmt "-oo"
                 | Obj_val s -> Format.fprintf fmt "%s" s
-                | Obj_unk -> Format.fprintf fmt "(interval -oo +oo)"
+                | Obj_unk -> Format.fprintf fmt "; (interval -oo +oo)"
              ) ()
         )objectives;
-      Printer.print_fmt fmt "@]@ )"
+      Printer.print_fmt fmt "@]@ ; )"
     end
 
 end
@@ -471,9 +471,11 @@ end
 module Why3CounterExample = struct
 
   let output_constraints fmt prop_model =
-    let assertions = SE.fold (fun e acc ->
-        (dprintf "%t(assert %a)@ " acc SmtlibCounterExample.pp_term e)
-      ) prop_model (dprintf "") in
+    let assertions =
+      SE.fold (fun e acc ->
+          (dprintf "%t;(assert %a)@ " acc SmtlibCounterExample.pp_term e)
+        ) prop_model (dprintf "")
+    in
     Format.fprintf fmt "@ ; constraints@ ";
     MS.iter (fun _ (name,ty,args_ty) ->
         match args_ty with

diff --git a/src/lib/reasoners/intervalCalculus.ml b/src/lib/reasoners/intervalCalculus.ml
@@ -2129,7 +2129,7 @@ let optimizing_split env uf opt =
     | Sim.Core.Sat _   -> assert false (* because we maximized *)
     | Sim.Core.Unsat _ -> assert false (* we know sim is SAT *)
     | Sim.Core.Unbounded _ ->
-      Format.eprintf
+      Printer.print_dbg
         "%a is unbounded. Let other methods assign a value for it@."
         E.print e;
       let value = if to_max then Th_util.Pinfinity else Th_util.Minfinity in
@@ -2139,7 +2139,7 @@ let optimizing_split env uf opt =
       let {Sim.Core.max_v; _} = Lazy.force mx in
       let max_p = Q.add max_v.bvalue.v c in
       let optim = if to_max then max_p else Q.mult Q.m_one max_p in
-      Format.eprintf
+      Printer.print_dbg
         "%a has a %s: %a@."
         E.print e
         (if to_max then "maximum" else "minimum")