don't include internal variables in model output

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index b9025a2ce003ccd968603e177c50c914b39f14c4..7c913578bd1523dcc57604bdd092d092f026b1fd 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -381,7 +381,7 @@ public:
     if(Dump.isOn("skolems") && comment != "") {
       Dump("skolems") << CommentCommand(id + " is " + comment);
     }
-    d_smt.addToModelCommandAndDump(c, "skolems");
+    d_smt.addToModelCommandAndDump(c, false, "skolems");
   }
 
   Node applySubstitutions(TNode node) const {
@@ -2629,8 +2629,8 @@ CVC4::SExpr SmtEngine::getAssignment() throw(ModalException) {
   return SExpr(sexprs);
 }
 
-void SmtEngine::addToModelCommandAndDump(const Command& c, const char* dumpTag) {
-  Trace("smt") << "SMT addToModelCommand(" << c << ")" << endl;
+void SmtEngine::addToModelCommandAndDump(const Command& c, bool userVisible, const char* dumpTag) {
+  Trace("smt") << "SMT addToModelCommandAndDump(" << c << ")" << endl;
   SmtScope smts(this);
   // If we aren't yet fully inited, the user might still turn on
   // produce-models.  So let's keep any commands around just in
@@ -2640,7 +2640,7 @@ void SmtEngine::addToModelCommandAndDump(const Command& c, const char* dumpTag)
   // decouple SmtEngine and ExprManager if the user does a few
   // ExprManager::mkSort() before SmtEngine::setOption("produce-models")
   // and expects to find their cardinalities in the model.
-  if( !d_fullyInited || options::produceModels() ) {
+  if(userVisible && (!d_fullyInited || options::produceModels())) {
     doPendingPops();
     d_modelCommands->push_back(c.clone());
   }

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 3a7fbe389d70e6b9b83dd2358154e04c08eb773d..2590bc8e23637ae7f4f6a7710f473a1095c0f5db 100644 (file)
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -304,7 +304,7 @@ class CVC4_PUBLIC SmtEngine {
    * Add to Model command.  This is used for recording a command
    * that should be reported during a get-model call.
    */
-  void addToModelCommandAndDump(const Command& c, const char* dumpTag = "declarations");
+  void addToModelCommandAndDump(const Command& c, bool userVisible = true, const char* dumpTag = "declarations");
 
   /**
    * Get the model (only if immediately preceded by a SAT