diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2012-11-29 00:59:06 +0000 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-11-29 00:59:06 +0000 |
commit | ff6ac38127fbb03e6c11a210b6b16d647b8785ea (patch) | |
tree | f656b1207ab75f0634593093ce5ed99a03f6c657 /src/smt | |
parent | 91673d6cefa63bc0f706101946e0c01fcd429071 (diff) |
Fixing function models with Boolean terms. Also, LAMBDA's should not be const.
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 28 |
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); } |