tmp

Stevendeo · Dec 4, 2023 · 0c7aa31 · 0c7aa31
1 parent 86ef6d0
commit 0c7aa31
Show file tree

Hide file tree

Showing 4 changed files with 3 additions and 6 deletions.
diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml
@@ -36,7 +36,7 @@ module Sy = Symbols
 module O = Options
 
 let pp_debug (type a) (msg : (a, Format.formatter, unit) format) : a =
-  if true then
+  if false then
     Fmt.pf (O.Output.get_fmt_diagnostic ()) ("[Solving]" ^^ msg)
   else
     Format.ifprintf (O.Output.get_fmt_diagnostic ()) msg

diff --git a/src/lib/frontend/frontend.ml b/src/lib/frontend/frontend.ml
@@ -309,8 +309,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
     ignore loc;
     Util.loop ~f:(fun _ res () -> Stack.push res env.consistent_dep_stack)
       ~max:n ~elt:(env.res, env.expl) ~init:();
-    Steps.apply_without_step_limit (fun () -> SAT.push env.sat_env n);
-    SAT.push env.sat_env n
+    Steps.apply_without_step_limit (fun () -> SAT.push env.sat_env n)
 
   let internal_pop ?(loc = Loc.dummy) (n : int) (env : env) : unit =
     ignore loc;

diff --git a/src/lib/reasoners/fun_sat_frontend.ml b/src/lib/reasoners/fun_sat_frontend.ml
@@ -53,14 +53,12 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
      manually save and restore environments. *)
 
   let push_cdcl_tableaux t i =
-    Format.printf "PPUUSSHH@.";
     assert (i > 0);
     for _ = 1 to i do
       Stack.push t cdcl_tab_push_pop_stack
     done
 
   let pop_cdcl_tableaux _t i =
-    Format.printf "PPOOPP@.";
     assert (i > 0);
     let rec aux acc = function
       | 1 -> acc

diff --git a/tests/cram.t/prelude.ae b/tests/cram.t/prelude.ae
@@ -10,5 +10,5 @@ logic f : real -> real
 
 theory F_theory extends FPA =
   axiom f_triggers :
-    forall x : real [ int_floor(x), x in ]0., ?] ]. my_leq(f(x), x)
+    forall x: real [ int_floor(x), x in ]0., ?] ]. my_leq(f(x), x)
 end