From f837652f6d3a64e31238443b632cc1b7b1b4c804 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Fri, 25 Jan 2013 17:06:02 -0500
Subject: [PATCH] fix --check-model --finite-model-find when used together
 (related to bug 486)

---
 src/smt/smt_engine.cpp       |  4 ++--
 src/theory/model.cpp         |  3 +++
 src/theory/theory_engine.cpp | 26 +++++++++++++-------------
 3 files changed, 18 insertions(+), 15 deletions(-)

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 77e43d518..66c7e4cbc 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2443,7 +2443,7 @@ Result SmtEngine::checkSat(const Expr& ex) throw(TypeCheckingException, ModalExc
   Trace("smt") << "SmtEngine::checkSat(" << e << ") => " << r << endl;
 
   // Check that SAT results generate a model correctly.
-  if(options::checkModels()){
+  if(options::checkModels()) {
     if(r.asSatisfiabilityResult().isSat() == Result::SAT ||
        (r.isUnknown() && r.whyUnknown() == Result::INCOMPLETE) ){
       checkModel(/* hard failure iff */ ! r.isUnknown());
@@ -2513,7 +2513,7 @@ Result SmtEngine::query(const Expr& ex) throw(TypeCheckingException, ModalExcept
   Trace("smt") << "SMT query(" << e << ") ==> " << r << endl;
 
   // Check that SAT results generate a model correctly.
-  if(options::checkModels()){
+  if(options::checkModels()) {
     if(r.asSatisfiabilityResult().isSat() == Result::SAT ||
        (r.isUnknown() && r.whyUnknown() == Result::INCOMPLETE) ){
       checkModel(/* hard failure iff */ ! r.isUnknown());
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;
     }
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 2ea0e866f..a23480eeb 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1378,19 +1378,19 @@ void TheoryEngine::handleUserAttribute(const char* attr, Theory* t) {
   d_attr_handle[ str ].push_back( t );
 }
 
-void TheoryEngine::checkTheoryAssertionsWithModel()
-{
-  for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) {
-    Theory* theory = d_theoryTable[theoryId];
-    if (theory && d_logicInfo.isTheoryEnabled(theoryId)) {
-      if (theoryId == THEORY_QUANTIFIERS || theoryId == THEORY_REWRITERULES) {
-        continue;
-      }
-      context::CDList<Assertion>::const_iterator it = theory->facts_begin(), it_end = theory->facts_end();
-      for (unsigned i = 0; it != it_end; ++ it, ++i) {
-        Node assertion = (*it).assertion;
-        Node val = getModel()->getValue(assertion);
-        Assert(val == d_true);
+void TheoryEngine::checkTheoryAssertionsWithModel() {
+  for(TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) {
+    if(theoryId != THEORY_REWRITERULES) {
+      Theory* theory = d_theoryTable[theoryId];
+      if(theory && d_logicInfo.isTheoryEnabled(theoryId)) {
+        for(context::CDList<Assertion>::const_iterator it = theory->facts_begin(),
+              it_end = theory->facts_end();
+            it != it_end;
+            ++it) {
+          Node assertion = (*it).assertion;
+          Node val = getModel()->getValue(assertion);
+          Assert(val == d_true);
+        }
       }
     }
   }
-- 
2.30.2