From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 18 Sep 2020 20:49:40 +0000 (-0500)
Subject: Fix assertion list for globally defined recursive functions (#5084)
X-Git-Tag: cvc5-1.0.0~2833
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0bf5519f5f455fe779ccfbaa8ed2dfc9e98f4747;p=cvc5.git

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 714622bae..e6a0af548 100644
--- 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