From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Fri, 10 May 2013 21:08:23 +0000 (-0400)
Subject: disable Logic-checking with finite model finding for now, since FMF uses Rationals... 
X-Git-Tag: cvc5-1.0.0~7287^2~33^2~29
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=10bc76f38b5fa7d213f698fa7b8de14d20e40c07;p=cvc5.git

disable Logic-checking with finite model finding for now, since FMF uses Rationals, making the check think arithmetic should be enabled (but it's not)
---

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 5ee8e5fda..ee37f331e 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -192,18 +192,23 @@ void TheoryEngine::preRegister(TNode preprocessed) {
       // Remove the top theory, if any more that means multiple theories were involved
       bool multipleTheories = Theory::setRemove(Theory::theoryOf(preprocessed), theories);
       TheoryId i;
-      while((i = Theory::setPop(theories)) != THEORY_LAST) {
-        if(!d_logicInfo.isTheoryEnabled(i)) {
-          LogicInfo newLogicInfo = d_logicInfo.getUnlockedCopy();
-          newLogicInfo.enableTheory(i);
-          newLogicInfo.lock();
-          stringstream ss;
-          ss << "The logic was specified as " << d_logicInfo.getLogicString()
-             << ", which doesn't include " << i
-             << ", but found a term in that theory." << endl
-             << "You might want to extend your logic to " << newLogicInfo
-             << endl;
-          throw LogicException(ss.str());
+      // These checks don't work with finite model finding, because it
+      // uses Rational constants to represent cardinality constraints,
+      // even though arithmetic isn't actually involved.
+      if(!options::finiteModelFind()) {
+        while((i = Theory::setPop(theories)) != THEORY_LAST) {
+          if(!d_logicInfo.isTheoryEnabled(i)) {
+            LogicInfo newLogicInfo = d_logicInfo.getUnlockedCopy();
+            newLogicInfo.enableTheory(i);
+            newLogicInfo.lock();
+            stringstream ss;
+            ss << "The logic was specified as " << d_logicInfo.getLogicString()
+               << ", which doesn't include " << i
+               << ", but found a term in that theory." << endl
+               << "You might want to extend your logic to "
+               << newLogicInfo.getLogicString() << endl;
+            throw LogicException(ss.str());
+          }
         }
       }
       if (multipleTheories) {