From 31f5fdd1aef89fcba8ad90c831abd67731059719 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Mon, 16 Mar 2015 13:27:51 +0100 Subject: [PATCH] Debugging... --- solver/mcsolver.ml | 9 +++++---- solver/mcsolver_types.ml | 4 ++-- 2 files changed, 7 insertions(+), 6 deletions(-) diff --git a/solver/mcsolver.ml b/solver/mcsolver.ml index f9ab63ba..6d0d51ae 100644 --- a/solver/mcsolver.ml +++ b/solver/mcsolver.ml @@ -612,10 +612,11 @@ module Make (L : Log_intf.S)(E : Expr_intf.S) (* Propagation (boolean and theory) *) let new_atom f = - let a = add_atom f in - L.debug 10 "New atom : %a" St.pp_atom a; - ignore (th_eval a); - a + L.debug 100 "New_atom"; + let a = add_atom f in + L.debug 10 "New atom : %a" St.pp_atom a; + ignore (th_eval a); + a let slice_get i = Either.destruct (Vec.get env.trail i) (function {level; tag={term; assigned = Some v}} -> Th.Assign (term, v), level | _ -> assert false) diff --git a/solver/mcsolver_types.ml b/solver/mcsolver_types.ml index 87071248..d5d1942a 100644 --- a/solver/mcsolver_types.ml +++ b/solver/mcsolver_types.ml @@ -172,9 +172,9 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)(Th : Plugin_intf.S with let add_term t = make_semantic_var t let add_atom lit = - Log.debug 100 "entering add_atom"; + L.debug 100 "entering add_atom"; let var, negated = make_boolean_var lit in - Log.debug 100 "found atom"; + L.debug 100 "found atom"; if negated then var.tag.na else var.tag.pa let make_clause name ali sz_ali is_learnt premise =