projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e5c444d) | patch
Fix models involving cardinality of sets of finite type (#8206)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 2 Mar 2022 22:36:05 +0000 (16:36 -0600)
committerGitHub <noreply@github.com>
Wed, 2 Mar 2022 22:36:05 +0000 (22:36 +0000)
commitc1569c97f1d2a08c528ebddb86454bfa6ea58611
treee6f97316fa1808acd469af1493779f1bed83c6f1tree
parente5c444d39c034972bce2f11c8c1c73bccd32b2bfcommit | diff
Fix models involving cardinality of sets of finite type (#8206)

Was caused by a flag not being reset, thus making it so that subsequent models did not use exclusion sets.

Fixes #5402. (Fixes the last benchmark on that issue, the first two are fixed by #8201).
src/theory/sets/cardinality_extension.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/sets/issue5402-2-card-finite.smt2 [new file with mode: 0644] blob