Fixed but with getAssertions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 1a9887e93d53f08f99dc4f9a28c4f16a4c67bb51..6511f689ae2bdeffda67bbbeee716c464aeb1b3f 100644 (file)
--- 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();
   }