projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2732194) | patch
Fix type issues with relevant domain computation (#5788)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 20 Jan 2021 21:56:26 +0000 (15:56 -0600)
committerGitHub <noreply@github.com>
Wed, 20 Jan 2021 21:56:26 +0000 (15:56 -0600)
commitaf7107611a37d45d495d0d40c50b67c08fc7de9c
tree81873b37a540158ae07476d4cee0b729d12cb6b1tree
parent273219488df1068a1abd444fc677bee57748bc32commit | diff
Fix type issues with relevant domain computation (#5788)

This fixes 2 issues with relevant domain type computation, the first involving arithmetic INST_CONSTANT that do not belong to the current quantified formula being solved for in a monomial sum, the second involving parametric datatype selectors.

Fixes #5635. Both benchmarks on that issue are unsolved (one timeout, one unknown) but throw no assertion failure.
src/theory/quantifiers/inst_strategy_enumerative.cpp diff | blob | history
src/theory/quantifiers/relevant_domain.cpp diff | blob | history
src/theory/quantifiers/term_database.cpp diff | blob | history