From 947f790f9f7e41b69e93a261f77fe1ad0e75c9fa Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Tue, 16 Aug 2022 21:29:29 -0400 Subject: [PATCH] debug in sat --- src/sat/solver.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/sat/solver.ml b/src/sat/solver.ml index 007b2c34..d4f23864 100644 --- a/src/sat/solver.ml +++ b/src/sat/solver.ml @@ -1240,15 +1240,15 @@ let acts_raise self (l : Lit.t list) (p : Proof_step.id) : 'a = let check_consequence_lits_false_ self l p : unit = let store = self.store in Log.debugf 50 (fun k -> - k "(@[sat.check-consequence-lits: %a@ :for %a@])" + k "(@[sat.check-consequence-lits:@ :consequence (@[%a@])@ :for %a@])" (Util.pp_list (Atom.debug store)) l (Atom.debug store) p); match List.find (fun a -> Atom.is_true store a) l with | a -> invalid_argf "slice.acts_propagate:@ Consequence should contain only false literals,@ \ - but @[%a@] is true" - (Atom.debug store) (Atom.neg a) + but @[%a@] is true@ when propagating %a" + (Atom.debug store) p (Atom.debug store) a | exception Not_found -> () let acts_propagate (self : t) f (expl : reason) =