simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2026-01-29 12:54:50 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

Remove some excessive debug messages

Browse source
This commit is contained in:
Guillaume Bury 2015-03-19 12:47:36 +01:00
parent 8ee66bf88f
commit 198890b68c
1 changed files with 0 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
solver/mcsolver.ml
View file

@ -290,7 +290,6 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
raise Unsat raise Unsat
let enqueue_bool a lvl reason = let enqueue_bool a lvl reason =
L.debug 99 "Entering enqueue_bool";
assert (not a.neg.is_true); assert (not a.neg.is_true);
if a.is_true then if a.is_true then
L.debug 10 "Litteral %a already in queue" pp_atom a L.debug 10 "Litteral %a already in queue" pp_atom a
@ -304,7 +303,6 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
end end
let enqueue_assign v value lvl = let enqueue_assign v value lvl =
L.debug 99 "Entering enqueue_assign";
v.tag.assigned <- Some value; v.tag.assigned <- Some value;
v.level <- lvl; v.level <- lvl;
Vec.push env.trail (Either.mk_left v); Vec.push env.trail (Either.mk_left v);