From: Morgan Deters <mdeters@gmail.com>
Date: Mon, 26 Nov 2012 19:39:03 +0000 (+0000)
Subject: rolling back r4625 for now (closes bug 464), Andy we should talk about this a bit... 
X-Git-Tag: cvc5-1.0.0~7556
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f96338937ca65d309913d90dbd3f1b8301ee92d6;p=cvc5.git

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

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());
   }