From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 3 Nov 2021 10:27:20 +0000 (-0500)
Subject: Fix preregistration for floating point theory (#7558)
X-Git-Tag: cvc5-1.0.0~903
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=324434a74b35d0e58bdb551c9155e9fb32844d07;p=cvc5.git

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 8364aa81b..e588bc1a9 100644
--- 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 ffc92c20e..7839dc7f2 100644
--- 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
index 000000000..f32a4ed33
--- /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)))