Fixing function models with Boolean terms. Also, LAMBDA's should not be const.

1 files changed, 14 insertions, 14 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 7df98ef08..8330b2a20 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2778,21 +2778,9 @@ void SmtEngine::checkModel(bool hardFailure) {
 
       Notice() << "SmtEngine::checkModel(): adding substitution: " << func << " |-> " << val << endl;
 
-      // (1) check that the value is actually a value
-      if(!val.isConst()) {
-        Notice() << "SmtEngine::checkModel(): *** PROBLEM: MODEL VALUE NOT A CONSTANT ***" << endl;
-        stringstream ss;
-        ss << "SmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl
-           << "model value for " << func << endl
-           << "             is " << val << endl
-           << "and that is not a constant (.isConst() == false)." << endl
-           << "Run with `--check-models -v' for additional diagnostics.";
-        InternalError(ss.str());
-      }
-
-      // (2) if the value is a lambda, ensure the lambda doesn't contain the
+      // (1) if the value is a lambda, ensure the lambda doesn't contain the
       // function symbol (since then the definition is recursive)
-      if(val.getKind() == kind::LAMBDA) {
+      if (val.getKind() == kind::LAMBDA) {
         // first apply the model substitutions we have so far
         Node n = substitutions.apply(val[1]);
         // now check if n contains func by doing a substitution
@@ -2816,6 +2804,18 @@ void SmtEngine::checkModel(bool hardFailure) {
         }
       }
 
+      // (2) check that the value is actually a value
+      else if (!val.isConst()) {
+        Notice() << "SmtEngine::checkModel(): *** PROBLEM: MODEL VALUE NOT A CONSTANT ***" << endl;
+        stringstream ss;
+        ss << "SmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl
+           << "model value for " << func << endl
+           << "             is " << val << endl
+           << "and that is not a constant (.isConst() == false)." << endl
+           << "Run with `--check-models -v' for additional diagnostics.";
+        InternalError(ss.str());
+      }
+
       // (3) checks complete, add the substitution
       substitutions.addSubstitution(func, val);
     }