diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-04 18:10:08 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-04 18:34:41 -0400 |
commit | d1d052cf549f574aad25f42e66051170e43ac3a7 (patch) | |
tree | 16f5a945858639061877ce018bbe113c04e095aa /src | |
parent | dbaaf5c2e82eab1922438bd2e358c9299fdd0bf2 (diff) |
SmtEngine::checkModel() now checks that model values are of the correct type (related to bug #569).
Diffstat (limited to 'src')
-rw-r--r-- | src/smt/smt_engine.cpp | 17 |
1 files changed, 16 insertions, 1 deletions
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); } |