diff options
-rw-r--r-- | src/smt/smt_engine.cpp | 8 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 2 |
2 files changed, 5 insertions, 5 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index b9025a2ce..7c913578b 100644 --- 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 3a7fbe389..2590bc8e2 100644 --- 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 |