[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.

diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index e588bc1a9479438473cb9c1eea53f5bf3957499d..6f2ddbf63509a0e247bde4bfcba277f30b9d0141 100644 (file)
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -289,9 +289,13 @@ bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete)
   else if (k == kind::FLOATINGPOINT_TO_FP_REAL)
   {
     // Get the values
-    Assert(m->hasTerm(abstract));
-    Assert(m->hasTerm(concrete[0]));
-    Assert(m->hasTerm(concrete[1]));
+    Assert(m->hasTerm(abstract)) << "Term " << abstract << " not in model";
+    Assert(m->hasTerm(concrete[0]))
+        << "Term " << concrete[0] << " not in model";
+    // Note: while the value for concrete[1] that we get from the model has to
+    // be const, it is not necessarily the case that `m->hasTerm(concrete[1])`.
+    // The arithmetic solver computes values for the variables in shared terms
+    // but does not necessarily add the shared terms themselves.
 
     Node abstractValue = m->getValue(abstract);
     Node rmValue = m->getValue(concrete[0]);

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 25f61c27c8339061b14f5df3ede57daf04af5e13..f322ffafccb6e19dbb4347c90e71f1b2de454af5 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -613,6 +613,7 @@ set(regress_0_tests
   regress0/fp/issue5734.smt2
   regress0/fp/issue6164.smt2
   regress0/fp/issue7002.smt2
+  regress0/fp/issue7569.smt2
   regress0/fp/proj-issue329-prereg-context.smt2
   regress0/fp/rti_3_5_bug.smt2
   regress0/fp/simple.smt2

diff --git a/test/regress/regress0/fp/issue7569.smt2 b/test/regress/regress0/fp/issue7569.smt2
new file mode 100644 (file)
index 0000000..c4bffc3
--- /dev/null
+++ b/test/regress/regress0/fp/issue7569.smt2
@@ -0,0 +1,7 @@
+(set-logic QF_ALL)
+(declare-const X (_ FloatingPoint 8 24))
+(declare-const R Real)
+(assert (= X ((_ to_fp 8 24) RTZ (- R))))
+(assert (= X ((_ to_fp 8 24) RTZ 0)))
+(set-info :status sat)
+(check-sat)