diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-01-25 17:06:02 -0500 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-01-25 17:39:21 -0500 |
| commit | 6d71aac1070aa7b1a8575722f4022a04b57d5763 (patch) | |
| tree | e51de5c69f3837946b5fad3e8cb9b21ac81d3683 /src/theory/model.cpp | |
| parent | 195dffbb7468e814d3dc3226666688869c13ba3d (diff) | |
fix --check-model --finite-model-find when used together (related to bug 486)
Diffstat (limited to 'src/theory/model.cpp')
| -rw-r--r-- | src/theory/model.cpp | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/theory/model.cpp b/src/theory/model.cpp index 2333a4394..713587be2 100644 --- a/src/theory/model.cpp +++ b/src/theory/model.cpp @@ -131,6 +131,9 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const children.push_back(val); } Node val = Rewriter::rewrite(NodeManager::currentNM()->mkNode(n.getKind(), children)); + if(val.getKind() == kind::CARDINALITY_CONSTRAINT) { + val = NodeManager::currentNM()->mkConst(getCardinality(val[0].getType().toType()).getFiniteCardinality() <= val[1].getConst<Rational>().getNumerator()); + } Assert(hasBoundVars || val.isConst()); return val; } |