rolling back r4625 for now (closes bug 464), Andy we should talk about this a bit...

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 03834825de9406e29c300e227f25039c53a60421..5ea16f20f22089a18843049295ecdc3ca783384c 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2641,7 +2641,7 @@ void SmtEngine::addToModelCommandAndDump(const Command& c, bool userVisible, con
   // 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(userVisible && (!d_fullyInited || options::produceModels())) {
+  if(/* userVisible && */ (!d_fullyInited || options::produceModels())) {
     doPendingPops();
     d_modelCommands->push_back(c.clone());
   }