From a17d83eb1db114f0e03e0e50748aee505c670d89 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Tue, 10 Mar 2015 17:57:48 +0100 Subject: [PATCH] Fixed location of debug message --- solver/mcsolver.ml | 2 +- solver/solver.ml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/solver/mcsolver.ml b/solver/mcsolver.ml index 8665a773..1b6927a5 100644 --- a/solver/mcsolver.ml +++ b/solver/mcsolver.ml @@ -498,10 +498,10 @@ module Make (L : Log_intf.S)(E : Expr_intf.S) if env.is_unsat then raise Unsat; (* is it necessary ? *) let init_name = name 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 if Proof.has_been_proved init0 then raise Trivial; assert (Proof.is_proven init0); - L.debug 10 "Adding clause : %a" St.pp_clause init0; let atoms, init = partition atoms init0 in let size = List.length atoms in match atoms with diff --git a/solver/solver.ml b/solver/solver.ml index b5335407..55145cb8 100644 --- a/solver/solver.ml +++ b/solver/solver.ml @@ -425,7 +425,7 @@ module Make (L : Log_intf.S)(F : Formula_intf.S) cancel_until lvl; enqueue a lvl (Some clause) end - | [a] -> + | [a] -> cancel_until 0; a.var.vpremise <- History [init0]; enqueue a 0 (Some init0)