projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: deb7433) | patch
Fix issues with to_real around coverings solver (#8837)
authorGereon Kremer <gkremer@cs.stanford.edu>
Tue, 31 May 2022 19:28:52 +0000 (12:28 -0700)
committerGitHub <noreply@github.com>
Tue, 31 May 2022 19:28:52 +0000 (19:28 +0000)
commit00ad2144c5f8717a84b1b6765a33744116f9bc9f
tree864544f6ed8b702cb117f0179ac8f8496762b0bctree
parentdeb7433f54617f7a9ffad75a2514c7760a88b1d7commit | diff
Fix issues with to_real around coverings solver (#8837)

This PR fixes two issues with the (missing) handling of to_real.
The first is that equality substitution was not aware of to_real yet, possible introducing models for both x and (to_real x).
The second is that the conversion to libpoly polynomials would also not properly unpack to_real expressions.
Fixes #8835.
src/theory/arith/nl/coverings_solver.cpp diff | blob | history
src/theory/arith/nl/equality_substitution.cpp diff | blob | history
src/theory/arith/nl/poly_conversion.cpp diff | blob | history
src/theory/arith/nl/poly_conversion.h diff | blob | history
test/regress/cli/CMakeLists.txt diff | blob | history
test/regress/cli/regress0/nl/issue8835-int-second.smt2 [new file with mode: 0644] blob