From e08bb7b5acbf9871ac3da1924ca886c4bf4a7a93 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Fri, 1 Feb 2019 21:42:11 -0600 Subject: [PATCH] fix(cc): polarity error in distinct-conflict --- src/smt/Congruence_closure.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/smt/Congruence_closure.ml b/src/smt/Congruence_closure.ml index 49ea41ed..a32cb764 100644 --- a/src/smt/Congruence_closure.ml +++ b/src/smt/Congruence_closure.ml @@ -471,9 +471,9 @@ and task_distinct_ cc acts (l:node list) tag expl : unit = begin match coll with | Some ((n1,_r1),(n2,_r2)) -> (* two classes are already equal *) - Log.debugf 5 (fun k->k "(@[cc.distinct.conflict@ %a = %a@])" N.pp n1 N.pp n2); + Log.debugf 5 (fun k->k "(@[cc.distinct.conflict@ %a = %a@ :expl %a@])" N.pp n1 N.pp n2 Explanation.pp expl); let lits = explain_unfold cc expl in - acts.Msat.acts_raise_conflict (Lit.Set.to_list lits) Proof_default + raise_conflict cc acts (Lit.Set.to_list lits) | None -> (* put a tag on all equivalence classes, that will make their merge fail *) List.iter (fun (_,n) -> add_tag_n cc n tag expl) l