diff options
| author | Morgan Deters <mdeters@gmail.com> | 2012-11-26 19:39:03 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2012-11-26 19:39:03 +0000 |
| commit | f96338937ca65d309913d90dbd3f1b8301ee92d6 (patch) | |
| tree | 92dcb1287de3925a789c3a5aa0803b8c84e4c4d1 /src | |
| parent | 78f459b303ed292a297a36cd0c435fdd025b0865 (diff) | |
rolling back r4625 for now (closes bug 464), Andy we should talk about this a bit more..
Diffstat (limited to 'src')
| -rw-r--r-- | src/smt/smt_engine.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
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()); } |