projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2cbeb0d) | patch
Make ProofNodeManager mkScope more robust (#8435)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 29 Mar 2022 18:17:29 +0000 (13:17 -0500)
committerGitHub <noreply@github.com>
Tue, 29 Mar 2022 18:17:29 +0000 (18:17 +0000)
commit0e7128b8effd4cc0002641ba545075a1ac346370
tree6cb75c6bc5d30e7eda31b8116752c6fe45bb40e2tree
parent2cbeb0d7b09816c2364d61616b88bdabfd90029ecommit | diff
Make ProofNodeManager mkScope more robust (#8435)

This make mkScope more robust in two ways:

- Literals rewritten to true can be justified by MACRO_SR_PRED_INTRO.
- Literals that are rewritten to other non-rewritable free assumptions can also be linked.

This is enough to ensure that current issues with (= t false) vs (not f) are fixed for Boolean arrays.
src/proof/proof_node_manager.cpp diff | blob | history
test/regress/cli/regress0/arrays/issue5925-2.smt2 diff | blob | history
test/regress/cli/regress0/arrays/issue5925.smt2 diff | blob | history