projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ef9b1b9) | patch
Fix issues with mixed types in relevant domain (#8901)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Sat, 9 Jul 2022 03:07:27 +0000 (22:07 -0500)
committerGitHub <noreply@github.com>
Sat, 9 Jul 2022 03:07:27 +0000 (03:07 +0000)
commit5750f285aad69921acb1c68e9ab03307d4943369
tree58c0638518aeac766ffeebed9191b227d93cff4atree
parentef9b1b979528ce5ae1fb005c87a31220cef73b8fcommit | diff
Fix issues with mixed types in relevant domain (#8901)

Fixes #8881.

Indentation changed, leading to the large diff. The code change is only to ensure the type of the term to add to the relevant domain matches the type of the variable.
src/theory/quantifiers/instantiate.h diff | blob | history
src/theory/quantifiers/relevant_domain.cpp diff | blob | history
test/regress/cli/CMakeLists.txt diff | blob | history
test/regress/cli/regress1/quantifiers/issue8881-rd-types.smt2 [new file with mode: 0644] blob