From c9657cc7955cc7888f5ae42a8004ab0ff1c08f1b Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Wed, 4 Feb 2015 14:58:00 +0100 Subject: [PATCH] Small log message update --- solver/mcsolver.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/solver/mcsolver.ml b/solver/mcsolver.ml index 760e1a48..1c7e6c3a 100644 --- a/solver/mcsolver.ml +++ b/solver/mcsolver.ml @@ -253,7 +253,7 @@ module Make (L : Log_intf.S)(E : Expr_intf.S) (* cancel down to [lvl] excluded *) let cancel_until lvl = - L.debug 5 "Backtracking to decision level %d (excluded)" lvl; + L.debug 1 "Backtracking to decision level %d (excluded)" lvl; if decision_level () > lvl then begin env.qhead <- Vec.get env.trail_lim lvl; env.tatoms_qhead <- env.qhead; @@ -285,7 +285,7 @@ module Make (L : Log_intf.S)(E : Expr_intf.S) assert (Vec.size env.trail_lim = Vec.size env.tenv_queue) let report_unsat ({atoms=atoms} as confl) = - L.debug 4 "Unsat conflict : %a" St.pp_clause confl; + L.debug 5 "Unsat conflict : %a" St.pp_clause confl; env.unsat_conflict <- Some confl; env.is_unsat <- true; raise Unsat