diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-11-07 10:15:41 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-11-07 10:15:41 -0500 |
commit | 3a3a57583fd8bd4af5c3b99b0047c9b20de38bb1 (patch) | |
tree | 1045a0a8fc03ca2a83d94da18c307ba3147eef4f /src/smt/smt_engine.cpp | |
parent | b07abc9bf4dbd20eb086b584fcb140be97f69a85 (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.cpp | 1 |
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); |