diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-11-07 09:24:15 -0500 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-11-07 09:24:15 -0500 |
| commit | 7b8902ff8775e5955472725042109896fbf67824 (patch) | |
| tree | 884425919a23724b8d54ca9eebb027c6df01a455 /src/smt/smt_engine.cpp | |
| parent | 56a523d9c4dd04cedbd812570cd80e3bc94cce4c (diff) | |
| parent | 61042cf551b19d06673be2b069bacc7cb1cd775a (diff) | |
Merge branch '1.4.x'
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, 1 insertions, 0 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 577fa7413..921d75315 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3568,6 +3568,7 @@ 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); |