[FP] Do not assert that model has shared term (#7585)
authorAndres Noetzli <andres.noetzli@gmail.com>
Fri, 5 Nov 2021 19:18:02 +0000 (12:18 -0700)
committerGitHub <noreply@github.com>
Fri, 5 Nov 2021 19:18:02 +0000 (19:18 +0000)
commite187b4c5709fc7b15e3d4c0e751224824208d28b
tree0ec51d926687736c338f73da8e8ca6d910776df9
parent51c3b3d6bb992550476220dd44a57a3e7987dce0
[FP] Do not assert that model has shared term (#7585)

Fixes #7569. Currently, the FP solver asserts that
m->hasTerm(sharedTerm) is always true for the real term in the
conversion from real to floating-point value. This is not necessarily
the case because the arithmetic solver computes values for the variables
in the shared terms but not necessarily for the terms themselves. This
commit removes the assertion and instead relies on the fact that a later
assertion checks that m->getValue(sharedTerm).isConst(), which is the
property that we are actually interested in.
src/theory/fp/theory_fp.cpp
test/regress/CMakeLists.txt
test/regress/regress0/fp/issue7569.smt2 [new file with mode: 0644]