diff options
Diffstat (limited to 'src/theory/theory_model.cpp')
-rw-r--r-- | src/theory/theory_model.cpp | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 92f834bff..cde3aef1c 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -119,11 +119,12 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const // no good. Instead, return the quantifier itself. If we're in // checkModel(), and the quantifier actually matters, we'll get an // assert-fail since the quantifier isn't a constant. - if(!d_equalityEngine->hasTerm(Rewriter::rewrite(n))) { + Node nr = Rewriter::rewrite(n); + if(!d_equalityEngine->hasTerm(nr)) { d_modelCache[n] = ret; return ret; } else { - ret = Rewriter::rewrite(n); + ret = nr; } } else { if(n.getKind() == kind::LAMBDA) { @@ -193,8 +194,7 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const ret = NodeManager::currentNM()->mkConst(getCardinality(ret[0].getType().toType()).getFiniteCardinality() <= ret[1].getConst<Rational>().getNumerator()); } if(ret.getKind() == kind::COMBINED_CARDINALITY_CONSTRAINT ){ - //FIXME - ret = NodeManager::currentNM()->mkConst(false); + //do nothing } d_modelCache[n] = ret; return ret; |