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

fix(cc): polarity error in distinct-conflict

Browse source
This commit is contained in:
Simon Cruanes 2019-02-01 21:42:11 -06:00
parent 3eabeb4e2e
commit e08bb7b5ac
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/smt/Congruence_closure.ml
View file

@ -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