3 files changed, 15 insertions, 6 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 6058c66d7..e4d21c72e 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -566,6 +566,15 @@ void SmtEngine::finishInit() {
     d_assertionList = new(true) AssertionList(d_userContext);
   }
 
+  // dump out a set-logic command
+  if(Dump.isOn("benchmark")) {
+    // Dump("benchmark") << SetBenchmarkLogicCommand(logic.getLogicString());
+    LogicInfo everything;
+    everything.lock();
+    Dump("benchmark") << CommentCommand("CVC4 always dumps the most general, \"all-supported\" logic (above), as some internals might require the use of a logic more general than the input.")
+                      << SetBenchmarkLogicCommand(everything.getLogicString());
+  }
+
   // dump out any pending declaration commands
   for(unsigned i = 0; i < d_dumpCommands.size(); ++i) {
     Dump("declarations") << *d_dumpCommands[i];
@@ -697,10 +706,6 @@ SmtEngine::~SmtEngine() throw() {
 void SmtEngine::setLogic(const LogicInfo& logic) throw(ModalException) {
   SmtScope smts(this);
 
-  if(Dump.isOn("benchmark")) {
-    Dump("benchmark") << SetBenchmarkLogicCommand(logic.getLogicString());
-  }
-
   d_logic = logic;
   setLogicInternal();
 }
@@ -3016,7 +3021,7 @@ SExpr SmtEngine::getStatistic(std::string name) const throw() {
   return d_statisticsRegistry->getStatistic(name);
 }
 
-void SmtEngine::setUserAttribute(std::string& attr, Expr expr) {
+void SmtEngine::setUserAttribute(const std::string& attr, Expr expr) {
   SmtScope smts(this);
   d_theoryEngine->setUserAttribute(attr, expr.getNode());
 }
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index b2ac0b886..3a7fbe389 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -19,6 +19,7 @@
 #ifndef __CVC4__SMT_ENGINE_H
 #define __CVC4__SMT_ENGINE_H
 
+#include <string>
 #include <vector>
 
 #include "context/cdlist_forward.h"
@@ -586,7 +587,7 @@ public:
    * This function is called when an attribute is set by a user.
    * In SMT-LIBv2 this is done via the syntax (! expr :attr)
    */
-  void setUserAttribute( std::string& attr, Expr expr );
+  void setUserAttribute(const std::string& attr, Expr expr);
 
 };/* class SmtEngine */
 
diff --git a/src/smt/smt_engine.i b/src/smt/smt_engine.i
index 64a4f93e2..7fdb59467 100644
--- a/src/smt/smt_engine.i
+++ b/src/smt/smt_engine.i
@@ -2,4 +2,7 @@
 #include "smt/smt_engine.h"
 %}
 
+%ignore CVC4::SmtEngine::getProof;
+%ignore CVC4::stats::getStatisticsRegistry(SmtEngine*);
+
 %include "smt/smt_engine.h"