projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ba3a69d) | patch
Fix issue with multiple infinities in CEGQI for LIRA (#4114)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 19 Mar 2020 01:13:27 +0000 (20:13 -0500)
committerGitHub <noreply@github.com>
Thu, 19 Mar 2020 01:13:27 +0000 (20:13 -0500)
commitf1b58cf3d090d252e9349d491c4b43c46bf52b0e
treeab6758fa11cfa56e80646582277229ed610c22c3tree
parentba3a69d7915292ddb649bdb8b4830623b337818ccommit | diff
Fix issue with multiple infinities in CEGQI for LIRA (#4114)

Fixes #4086.

Quantifier instantiation involves two symbolic representations of infinities for real and int and was not handled correctly previously.
src/theory/quantifiers/cegqi/vts_term_cache.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/quantifiers/issue4086-infs.smt2 [new file with mode: 0644] blob