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

Fixed location of debug message

Browse source
This commit is contained in:
Guillaume Bury 2015-03-10 17:57:48 +01:00
parent 1b5038e620
commit a17d83eb1d
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
solver/mcsolver.ml
View file

@ -498,10 +498,10 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
if env.is_unsat then raise Unsat; (* is it necessary ? *) if env.is_unsat then raise Unsat; (* is it necessary ? *)
let init_name = name in let init_name = name in
let init0 = make_clause init_name atoms (List.length atoms) (history <> History []) history in let init0 = make_clause init_name atoms (List.length atoms) (history <> History []) history in
L.debug 10 "Adding clause : %a" St.pp_clause init0;
try try
if Proof.has_been_proved init0 then raise Trivial; if Proof.has_been_proved init0 then raise Trivial;
assert (Proof.is_proven init0); assert (Proof.is_proven init0);
L.debug 10 "Adding clause : %a" St.pp_clause init0;
let atoms, init = partition atoms init0 in let atoms, init = partition atoms init0 in
let size = List.length atoms in let size = List.length atoms in
match atoms with match atoms with

2
solver/solver.ml
View file

@ -425,7 +425,7 @@ module Make (L : Log_intf.S)(F : Formula_intf.S)
cancel_until lvl; cancel_until lvl;
enqueue a lvl (Some clause) enqueue a lvl (Some clause)
end end
| [a] -> | [a] ->
cancel_until 0; cancel_until 0;
a.var.vpremise <- History [init0]; a.var.vpremise <- History [init0];
enqueue a 0 (Some init0) enqueue a 0 (Some init0)