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

[bugfix] Allow late mcsat conflicts (wrt assigns)

Browse source
This commit is contained in:
Guillaume Bury 2017-04-07 15:13:27 +02:00
parent 5725cf5173
commit 7e95911dd8
1 changed files with 5 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/core/internal.ml
View file

@ -657,9 +657,11 @@ module Make
(* look for the next node to expand *) (* look for the next node to expand *)
while while
let q = get_atom !tr_ind in match Vec.get env.elt_queue !tr_ind with
(not (q.var.seen = Both)) || | Atom q ->
(q.var.v_level < conflict_level) (not (q.var.seen = Both)) ||
(q.var.v_level < conflict_level)
| Lit _ -> true
do do
decr tr_ind; decr tr_ind;
done; done;