Fix preregistration for floating point theory (#7558)

Preregistering terms must always add them to the equality engine of TheoryFp, otherwise there may be preregistered terms that do not occur in the equality engine of TheoryFp, thus leading to crashes during theory combination.

Fixes cvc5/cvc5-projects#329.

diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index 8364aa81b98f9c0451ed688115501ca21de701cc..e588bc1a9479438473cb9c1eea53f5bf3957499d 100644 (file)
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -476,20 +476,13 @@ void TheoryFp::registerTerm(TNode node)
 {
   Trace("fp-registerTerm") << "TheoryFp::registerTerm(): " << node << std::endl;
 
-  if (isRegistered(node))
-  {
-    return;
-  }
-
   Kind k = node.getKind();
   Assert(k != kind::FLOATINGPOINT_TO_FP_GENERIC && k != kind::FLOATINGPOINT_SUB
          && k != kind::FLOATINGPOINT_EQ && k != kind::FLOATINGPOINT_GEQ
          && k != kind::FLOATINGPOINT_GT);
 
-  CVC5_UNUSED bool success = d_registeredTerms.insert(node);
-  Assert(success);
-
-  // Add to the equality engine
+  // Add to the equality engine, always. This is required to ensure
+  // getEqualityStatus works as expected when theory combination is enabled.
   if (k == kind::EQUAL)
   {
     d_equalityEngine->addTriggerPredicate(node);
@@ -499,6 +492,15 @@ void TheoryFp::registerTerm(TNode node)
     d_equalityEngine->addTerm(node);
   }
 
+  // if not registered in this user context
+  if (isRegistered(node))
+  {
+    return;
+  }
+
+  CVC5_UNUSED bool success = d_registeredTerms.insert(node);
+  Assert(success);
+
   // Give the expansion of classifications in terms of equalities
   // This should make equality reasoning slightly more powerful.
   if ((k == kind::FLOATINGPOINT_ISNAN) || (k == kind::FLOATINGPOINT_ISZ)

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index ffc92c20e811c4f195d83a13d06a03e071c88b96..7839dc7f258e996e8dfcf75e1a8be48410904edc 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/proj-issue329-prereg-context.smt2
   regress0/fp/rti_3_5_bug.smt2
   regress0/fp/simple.smt2
   regress0/fp/word-blast.smt2

diff --git a/test/regress/regress0/fp/proj-issue329-prereg-context.smt2 b/test/regress/regress0/fp/proj-issue329-prereg-context.smt2
new file mode 100644 (file)
index 0000000..f32a4ed
--- /dev/null
+++ b/test/regress/regress0/fp/proj-issue329-prereg-context.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --fp-exp
+; EXPECT: sat
+(set-logic ALL)
+(declare-const x Float128)
+(declare-const _x String)
+(declare-fun x5 (Bool Float128) Bool)
+(check-sat-assuming ((x5 (exists ((x (Array String Bool))) (and (select x _x) (or (select x _x) (x5 (exists ((x Bool)) true) (_ -oo 15 113))))) x)))