simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-09 20:55:39 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

fix(analyze-final): mistake in production of unsat cores

Browse source
This commit is contained in:
Simon Cruanes 2019-01-19 18:13:41 -06:00 • committed by Guillaume Bury
parent f8281bfcc2
commit 0d7ae34880
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/core/Internal.ml
View file

@ -1685,7 +1685,7 @@ module Make(Plugin : PLUGIN)
let analyze_final (self:t) (a:atom) : atom list = let analyze_final (self:t) (a:atom) : atom list =
Log.debugf 5 (fun k->k "(@[sat.analyze-final@ :lit %a@])" Atom.debug a); Log.debugf 5 (fun k->k "(@[sat.analyze-final@ :lit %a@])" Atom.debug a);
assert (Atom.is_false a); assert (Atom.is_false a);
let core = ref [a.neg] in let core = ref [a] in
let idx = ref (Vec.size self.trail - 1) in let idx = ref (Vec.size self.trail - 1) in
Var.mark a.var; Var.mark a.var;
let seen = ref [a.var] in let seen = ref [a.var] in