From f96338937ca65d309913d90dbd3f1b8301ee92d6 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Mon, 26 Nov 2012 19:39:03 +0000
Subject: [PATCH] rolling back r4625 for now (closes bug 464), Andy we should
 talk about this a bit more..

---
 src/smt/smt_engine.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 03834825d..5ea16f20f 100644
--- 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());
   }
-- 
2.30.2