Fix assertion list for globally defined recursive functions (#5084)

This was uncovered by a (spurious) proof checking failure on proof-new.

diff --git a/src/smt/assertions.cpp b/src/smt/assertions.cpp
index 714622bae37e566e0e291ff3c151fd0fe3cdd430..e6a0af548beb07240afddc3dd1c7450189d2a135 100644 (file)
--- a/src/smt/assertions.cpp
+++ b/src/smt/assertions.cpp
@@ -101,12 +101,6 @@ void Assertions::initializeCheckSat(const std::vector<Node>& assumptions,
     Node n = d_absValues.substituteAbstractValues(e);
     // Ensure expr is type-checked at this point.
     ensureBoolean(n);
-
-    /* Add assumption  */
-    if (d_assertionList != nullptr)
-    {
-      d_assertionList->push_back(n);
-    }
     addFormula(n, inUnsatCore, true, true, false);
   }
   if (d_globalDefineFunRecLemmas != nullptr)
@@ -124,10 +118,6 @@ void Assertions::initializeCheckSat(const std::vector<Node>& assumptions,
 void Assertions::assertFormula(const Node& n, bool inUnsatCore)
 {
   ensureBoolean(n);
-  if (d_assertionList != nullptr)
-  {
-    d_assertionList->push_back(n);
-  }
   bool maybeHasFv = language::isInputLangSygus(options::inputLanguage());
   addFormula(n, inUnsatCore, true, false, maybeHasFv);
 }
@@ -149,6 +139,11 @@ context::CDList<Node>* Assertions::getAssertionList()
 void Assertions::addFormula(
     TNode n, bool inUnsatCore, bool inInput, bool isAssumption, bool maybeHasFv)
 {
+  // add to assertion list if it exists
+  if (d_assertionList != nullptr)
+  {
+    d_assertionList->push_back(n);
+  }
   if (n.isConst() && n.getConst<bool>())
   {
     // true, nothing to do