projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 8d63f44) | patch
Fix CEGQI for datatypes with Boolean subfields (#6630)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 27 May 2021 21:18:28 +0000 (16:18 -0500)
committerGitHub <noreply@github.com>
Thu, 27 May 2021 21:18:28 +0000 (16:18 -0500)
commitb9062490a7590708bcf158d4670a23d859fe3355
tree9bb487795a7753de1c631494012133508ecc374etree
parent8d63f44d93ae91c5b89a9cf866ba33c954465398commit | diff
Fix CEGQI for datatypes with Boolean subfields (#6630)

Fixes a solution soundness issue caused by allowing ineligible terms of kind BOOLEAN_TERM_VARIABLE to appear in instantiations.

This also corrects the expected solution on a benchmark that had an incorrect status.

Fixes #6603.
src/theory/quantifiers/cegqi/ceg_instantiator.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/quantifiers/issue5645-dt-cm-spurious.smt2 diff | blob | history
test/regress/regress0/quantifiers/issue6603-dt-bool-cegqi.smt2 [new file with mode: 0644] blob