summaryrefslogtreecommitdiff
path: root/src/smt/smt_engine.cpp
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@cs.nyu.edu>2014-11-07 10:15:41 -0500
committerMorgan Deters <mdeters@cs.nyu.edu>2014-11-07 10:15:41 -0500
commit3a3a57583fd8bd4af5c3b99b0047c9b20de38bb1 (patch)
tree1045a0a8fc03ca2a83d94da18c307ba3147eef4f /src/smt/smt_engine.cpp
parentb07abc9bf4dbd20eb086b584fcb140be97f69a85 (diff)
Revert "Fix missing case in model postprocessor (resolves bug #595)."
This reverts commit 61042cf551b19d06673be2b069bacc7cb1cd775a. Conflicts: test/regress/regress0/Makefile.am
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r--src/smt/smt_engine.cpp1
1 files changed, 0 insertions, 1 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 921d75315..577fa7413 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -3568,7 +3568,6 @@ Result SmtEngine::assertFormula(const Expr& ex, bool inUnsatCore) throw(TypeChec
Node SmtEngine::postprocess(TNode node, TypeNode expectedType) const {
ModelPostprocessor mpost;
NodeVisitor<ModelPostprocessor> visitor;
- Debug("boolean-terms") << "postproc: visit " << node << endl;
Node value = visitor.run(mpost, node);
Debug("boolean-terms") << "postproc: got " << value << " expect type " << expectedType << endl;
Node realValue = mpost.rewriteAs(value, expectedType);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback