projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 3076c4e) | patch
Fix subtype issue in cegqi arithmetic (#8440)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 30 Mar 2022 18:06:34 +0000 (13:06 -0500)
committerGitHub <noreply@github.com>
Wed, 30 Mar 2022 18:06:34 +0000 (18:06 +0000)
commitcd396280ff2b1a81c7c812c0b08893e72fba8b1e
treebec0d4d3dd930a9dda5891ebfb244c684dfbb69ctree
parent3076c4e70ded49d4b54585738d2dfc1d4aed1b9ccommit | diff
Fix subtype issue in cegqi arithmetic (#8440)

Fixes #8410.

Was not properly checking for cases where an Integer variable had a Real term as its solution.
src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp diff | blob | history
src/theory/quantifiers/cegqi/ceg_arith_instantiator.h diff | blob | history
src/theory/quantifiers/cegqi/ceg_instantiator.cpp diff | blob | history
test/regress/cli/CMakeLists.txt diff | blob | history
test/regress/cli/regress1/quantifiers/issue8410-vts-subtypes.smt2 [new file with mode: 0644] blob