simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 03:05:31 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

Small log message update

Browse source
This commit is contained in:
Guillaume Bury 2015-02-04 14:58:00 +01:00
parent 07b49c8481
commit c9657cc795
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
solver/mcsolver.ml
View file

@ -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