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

fix(proof): emit proper result for RUP steps

Browse source
This commit is contained in:
Simon Cruanes 2021-11-28 16:35:04 -05:00
parent 15e16a515d
commit 1bf05d51ce
No known key found for this signature in database
GPG key ID: 4AC01D0849AA62B6
1 changed files with 1 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/sat/Solver.ml
View file

@ -1028,8 +1028,7 @@ module Make(Plugin : PLUGIN)
(Atom.debug_a store) atoms);
let proof =
let lits =
Clause.atoms_a store c
|> Iter.of_array
Iter.of_array atoms
|> Iter.map (Atom.lit store)
in
Proof.emit_redundant_clause lits