projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: bcbf146) | patch
Fix handling of negation of Boolean bound variables in FMF (#6066)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 8 Mar 2021 20:11:24 +0000 (14:11 -0600)
committerGitHub <noreply@github.com>
Mon, 8 Mar 2021 20:11:24 +0000 (14:11 -0600)
commit4e2afa2282965f3f54033d43cd990cc0b0a8b200
tree6fc4b0f3f345b519dcfb1bcc5b1b37edeb1b3b93tree
parentbcbf146f0786035b0228eb4bcd13eb2bc6ca5f9bcommit | diff
Fix handling of negation of Boolean bound variables in FMF (#6066)

Fixes #5922. We were not correctly handling when a Boolean bound variable was negated.
src/theory/quantifiers/fmf/full_model_check.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/fmf/issue5922-fmf-not-x.smt2 [new file with mode: 0644] blob