projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: f02b9bc) | patch
Fix issue related to use of Boolean term variable for set/bag choose (#8423)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 29 Mar 2022 16:46:14 +0000 (11:46 -0500)
committerGitHub <noreply@github.com>
Tue, 29 Mar 2022 16:46:14 +0000 (16:46 +0000)
commit8c92533a49b715a70d7ef187ef470901fd0c11c8
tree9986543f00f3fbeed37f169cc710c0c1da5ea433tree
parentf02b9bca33f9092c6d793e977326acc315f3b073commit | diff
Fix issue related to use of Boolean term variable for set/bag choose (#8423)

Fixes cvc5/cvc5-projects#501.

I am considering making this detail internal to SkolemManager to avoid similar issues in the future. However, there are some subtle performance implications in doing so, so this will be addressed later.
src/theory/bags/theory_bags.cpp diff | blob | history
src/theory/sets/cardinality_extension.cpp diff | blob | history
src/theory/sets/theory_sets.cpp diff | blob | history
src/theory/sets/theory_sets_private.cpp diff | blob | history
test/regress/cli/CMakeLists.txt diff | blob | history
test/regress/cli/regress0/sets/proj-issue501-choose-bool-term-var.smt2 [new file with mode: 0644] blob