Merged bit-vector and uf proof branch.

2 files changed, 5 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;
 }
 
diff --git a/src/smt_util/command.h b/src/smt_util/command.h
index d8f9789f5..248e69b0e 100644
--- a/src/smt_util/command.h
+++ b/src/smt_util/command.h
@@ -584,6 +584,7 @@ public:
 class CVC4_PUBLIC GetProofCommand : public Command {
 protected:
   Proof* d_result;
+  SmtEngine* d_smtEngine;
 public:
   GetProofCommand() throw();
   ~GetProofCommand() throw() {}