From 0bf5519f5f455fe779ccfbaa8ed2dfc9e98f4747 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 18 Sep 2020 15:49:40 -0500 Subject: [PATCH] Fix assertion list for globally defined recursive functions (#5084) This was uncovered by a (spurious) proof checking failure on proof-new. --- src/smt/assertions.cpp | 15 +++++---------- 1 file changed, 5 insertions(+), 10 deletions(-) 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& 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& 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* 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()) { // true, nothing to do -- 2.30.2