projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 3877646) | patch
Make blockModelValues robust to non-closed enumerable types (#8055)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 2 Mar 2022 05:12:08 +0000 (23:12 -0600)
committerGitHub <noreply@github.com>
Wed, 2 Mar 2022 05:12:08 +0000 (05:12 +0000)
commita7910026d54c24c7ef1b58c0b90069142302c314
tree8ff9097a865b73eefb275677ea9d2ed15dc3d647tree
parent387764620aa438a34bd78c2f18a6095350002c18commit | diff
Make blockModelValues robust to non-closed enumerable types (#8055)

Fixes cvc5/cvc5-projects#420.

Also fixes the trivial case where there is nothing to block, in which case we should add false (via mkOr) not true.
src/smt/model_blocker.cpp diff | blob | history
test/unit/api/cpp/solver_black.cpp diff | blob | history