From 78df8252dc3ce32205c000582e34db8e03aa2076 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Wed, 5 Jan 2022 10:31:33 -0500 Subject: [PATCH] bugfix in CC explanations --- src/cc/Sidekick_cc.ml | 7 +++++-- src/sat/Solver.ml | 3 ++- 2 files changed, 7 insertions(+), 3 deletions(-) diff --git a/src/cc/Sidekick_cc.ml b/src/cc/Sidekick_cc.ml index 20635b22..8b439b50 100644 --- a/src/cc/Sidekick_cc.ml +++ b/src/cc/Sidekick_cc.ml @@ -856,9 +856,12 @@ module Make (A: CC_ARG) let e = lazy ( let lazy st = half_expl_and_pr in explain_equal_rec_ cc st u1 t1; - (* assert that [guard /\ ¬lit] is absurd, to propagate [lit] *) + (* true literals explaining why t1=t2 *) + let guard = st.lits in + (* get a proof of [guard /\ ¬lit] being absurd, to propagate [lit] *) Expl_state.add_lit st (Lit.neg lit); - lits_and_proof_of_expl cc st + let _, pr = lits_and_proof_of_expl cc st in + guard, pr ) in fun () -> Lazy.force e in diff --git a/src/sat/Solver.ml b/src/sat/Solver.ml index 8a637b88..e39438a7 100644 --- a/src/sat/Solver.ml +++ b/src/sat/Solver.ml @@ -1743,7 +1743,8 @@ module Make(Plugin : PLUGIN) match List.find (Atom.is_true store) l with | a -> invalid_argf - "slice.acts_propagate:@ Consequence should contain only true literals, but %a isn't" + "slice.acts_propagate:@ Consequence should contain only false literals,@ \ + but @[%a@] is true" (Atom.debug store) (Atom.neg a) | exception Not_found -> ()