From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Wed, 4 Jun 2014 22:10:08 +0000 (-0400)
Subject: SmtEngine::checkModel() now checks that model values are of the correct type (related... 
X-Git-Tag: cvc5-1.0.0~6859
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d1d052cf549f574aad25f42e66051170e43ac3a7;p=cvc5.git

SmtEngine::checkModel() now checks that model values are of the correct type (related to bug #569).
---

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 8ef1d1543..f9ac1e9db 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -3697,7 +3697,22 @@ void SmtEngine::checkModel(bool hardFailure) {
         InternalError(ss.str());
       }
 
-      // (3) checks complete, add the substitution
+      // (3) check that it's the correct (sub)type
+      // This was intended to be a more general check, but for now we can't do that because
+      // e.g. "1" is an INT, which isn't a subrange type [1..10] (etc.).
+      else if(func.getType().isInteger() && !val.getType().isInteger()) {
+        Notice() << "SmtEngine::checkModel(): *** PROBLEM: MODEL VALUE NOT CORRECT TYPE ***" << endl;
+        stringstream ss;
+        ss << "SmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl
+           << "model value for " << func << endl
+           << "             is " << val << endl
+           << "value type is     " << val.getType() << endl
+           << "should be of type " << func.getType() << endl
+           << "Run with `--check-models -v' for additional diagnostics.";
+        InternalError(ss.str());
+      }
+
+      // (4) checks complete, add the substitution
       Debug("boolean-terms") << "cm: adding subs " << func << " :=> " << val << endl;
       substitutions.addSubstitution(func, val);
     }