projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 1c74482) | patch
Do not make assumption about model for Boolean variables in FMF (#7407)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 20 Oct 2021 14:34:10 +0000 (09:34 -0500)
committerGitHub <noreply@github.com>
Wed, 20 Oct 2021 14:34:10 +0000 (14:34 +0000)
commit3e9e1c54ef54627e4f38094910effb32f6ad7cd2
tree5084b97b59e90dc3abdfa844907084ca25b6b311tree
parent1c744822538cff4e598b411514c4580848f1517bcommit | diff
Do not make assumption about model for Boolean variables in FMF (#7407)

Fixes cases where models can be wrong for FMF with Boolean variables in the bodies of quantified formulas.

Fixes #6744, all benchmarks on that issue are fixed. This PR adds 2 of the regressions from that issue.
src/theory/quantifiers/fmf/full_model_check.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/fmf/issue6744-2-unc-bool-var.smt2 [new file with mode: 0644] blob
test/regress/regress1/fmf/issue6744-3-unc-bool-var.smt2 [new file with mode: 0644] blob