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: proper proof for clause deduplication

Browse source
This commit is contained in:
Simon Cruanes 2018-07-10 13:54:02 -05:00
parent 74cd2009a3
commit bf0b5185bd
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/sat/Internal.ml
View file

@ -838,7 +838,7 @@ module Make (Th : Theory_intf.S) = struct
) else if !duplicates = [] then ( ) else if !duplicates = [] then (
clause clause
) else ( ) else (
Clause.make_l !res (History [clause]) Clause.make_l !res (Simplified clause)
) )
(* Sort literals for new clause, into: (* Sort literals for new clause, into:
@ -962,7 +962,7 @@ module Make (Th : Theory_intf.S) = struct
backtrack_down_to st b_lvl; backtrack_down_to st b_lvl;
); );
assert (Vec.size st.elt_levels = Vec.size st.backtrack_levels); assert (Vec.size st.elt_levels = Vec.size st.backtrack_levels);
Log.debugf 15 (fun k->k "(@[<v>sat.trail@ %a@])" (Vec.print Atom.debug) st.trail); Log.debugf 15 (fun k->k "(@[<hv>sat.trail@,%a@])" (Vec.print ~sep:" " Atom.debug) st.trail);
() ()
(* Unsatisfiability is signaled through an exception, since it can happen (* Unsatisfiability is signaled through an exception, since it can happen