1 files changed, 4 insertions, 0 deletions
diff --git a/src/smt_util/command.cpp b/src/smt_util/command.cpp
index 8cc8a421c..83298836f 100644
--- a/src/smt_util/command.cpp
+++ b/src/smt_util/command.cpp
@@ -1110,6 +1110,7 @@ GetProofCommand::GetProofCommand() throw() {
 
 void GetProofCommand::invoke(SmtEngine* smtEngine) throw() {
   try {
+    d_smtEngine = smtEngine;
     d_result = smtEngine->getProof();
     d_commandStatus = CommandSuccess::instance();
   } catch(UnsafeInterruptException& e) {
@@ -1127,6 +1128,7 @@ void GetProofCommand::printResult(std::ostream& out, uint32_t verbosity) const t
   if(! ok()) {
     this->Command::printResult(out, verbosity);
   } else {
+    smt::SmtScope scope(d_smtEngine);
     d_result->toStream(out);
   }
 }
@@ -1134,12 +1136,14 @@ void GetProofCommand::printResult(std::ostream& out, uint32_t verbosity) const t
 Command* GetProofCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
   GetProofCommand* c = new GetProofCommand();
   c->d_result = d_result;
+  c->d_smtEngine = d_smtEngine;
   return c;
 }
 
 Command* GetProofCommand::clone() const {
   GetProofCommand* c = new GetProofCommand();
   c->d_result = d_result;
+  c->d_smtEngine = d_smtEngine;
   return c;
 }