projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: f3a2e38) | patch
Fix spurious checks to closed proofs (#7484)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 25 Oct 2021 20:38:28 +0000 (15:38 -0500)
committerGitHub <noreply@github.com>
Mon, 25 Oct 2021 20:38:28 +0000 (20:38 +0000)
commit85f57e1b106e0c91ef73a51ff3ad5194d6634b60
treeeb65ed078673c8557d077c960cfc3c216a17dbc1tree
parentf3a2e3814d0a3f32fe1e9e24de954bc2d9ff999ecommit | diff
Fix spurious checks to closed proofs (#7484)

This leads to issues when (1) proofs are enabled, (2) unsat cores are enabled and full proofs are disabled in a subsolver.

This is the case for the abduction algorithm that uses unsat core learning, when proofs are explicitly enabled. This led to spurious assertion failures when testing proof new.
src/theory/theory_engine.cpp diff | blob | history