diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-09-04 17:53:30 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-09-04 17:53:38 +0200 |
| commit | d3c365a60c88e33a7d73f81484db2cff5ef69bbb (patch) | |
| tree | 0b2779b9a69b6f855a01a4f22e3082e2f5faabd8 /src/theory/theory_model.cpp | |
| parent | 711815d937db09aeb7e8fa568718768113ef7176 (diff) | |
Fix bugs 605 and 667.
Diffstat (limited to 'src/theory/theory_model.cpp')
| -rw-r--r-- | src/theory/theory_model.cpp | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 05d0c896a..cf0fbcbfe 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -185,7 +185,10 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const Debug("model-getvalue-debug") << " " << n << "[" << i << "] is " << ret << std::endl; children.push_back(ret); } - ret = Rewriter::rewrite(NodeManager::currentNM()->mkNode(n.getKind(), children)); + ret = NodeManager::currentNM()->mkNode(n.getKind(), children); + Debug("model-getvalue-debug") << "ret (pre-rewrite): " << ret << std::endl; + ret = Rewriter::rewrite(ret); + Debug("model-getvalue-debug") << "ret (post-rewrite): " << ret << std::endl; if(ret.getKind() == kind::CARDINALITY_CONSTRAINT) { ret = NodeManager::currentNM()->mkConst(getCardinality(ret[0].getType().toType()).getFiniteCardinality() <= ret[1].getConst<Rational>().getNumerator()); } |