Ensure that Xliteral.print_view is only used in boxes

OCamlPro · Feb 25, 2025 · 7efe4e2 · 7efe4e2
1 parent b9832c2
commit 7efe4e2
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 18 deletions.
diff --git a/src/lib/reasoners/ccx.ml b/src/lib/reasoners/ccx.ml
@@ -188,17 +188,12 @@ module Main : S = struct
             Expr.print t (pp_list_no_space print) ctx
 
     let rel_add_cst t ctx =
-      if ctx != [] then
-        let c = ref 0 in
-        let print fmt (a, _ex) =
-          incr c;
-          Format.fprintf fmt " %d) %a@ " !c (A.print_view X.print) a
-        in
-        if Options.get_debug_cc () then
-          print_dbg
-            ~module_name:"Ccx" ~function_name:"rel_add_cst"
-            "constraints of Rel.add(%a)@ %a"
-            Expr.print t (pp_list_no_space print) ctx
+      if not (Compat.List.is_empty ctx) then
+        Log.debug
+          (fun k -> k "constraints of Rel.add(%a):@ %a"
+              E.print t
+              Fmt.(braces @@ list ~sep:comma
+                   @@ pair (A.print_view X.print) nop) ctx)
 
     let add_to_use t =
       if Options.get_debug_cc () then

diff --git a/src/lib/reasoners/theory.ml b/src/lib/reasoners/theory.ml
@@ -632,13 +632,11 @@ module Main_Default : S = struct
     | Pinfinity | Minfinity | Limit _ | Value _ ->
       let (lview, is_cs, _) = opt_split.case_split in
       assert is_cs;
-
-      if Options.get_debug_optimize () then
-        Printer.print_dbg "Objective for %a is %a [split: %a]"
-          Objective.Function.pp obj
-          Objective.Value.pp opt_split.value
-          Shostak.L.print (Shostak.L.make lview);
-
+      Logs.debug ~src:Options.Sources.optimize
+        (fun k -> k "Objective for %a is %a [split: %a]"
+            Objective.Function.pp obj
+            Objective.Value.pp opt_split.value
+            Shostak.L.print (Shostak.L.make lview));
       add_objective
         obj opt_split.value
         (Shostak.(Literal.make @@ LSem (L.make lview)))