From: Clark Barrett <barrett@cs.nyu.edu>
Date: Tue, 1 Sep 2015 20:07:05 +0000 (-0700)
Subject: Fixed but with getAssertions
X-Git-Tag: cvc5-1.0.0~6252^2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6f9186c6eac5ce04c6ff3318e807909031528f59;p=cvc5.git

Fixed but with getAssertions
---

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 1a9887e93..6511f689a 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -4401,6 +4401,7 @@ void SmtEngine::printSynthSolution( std::ostream& out ) {
 vector<Expr> SmtEngine::getAssertions() throw(ModalException) {
   SmtScope smts(this);
   finalOptionsAreSet();
+  doPendingPops();
   if(Dump.isOn("benchmark")) {
     Dump("benchmark") << GetAssertionsCommand();
   }