diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-06-11 15:50:06 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-06-11 15:50:06 -0500 |
| commit | a8e9dd456af98c909a19da7a8458aab9fa7f2ea2 (patch) | |
| tree | 6c5b7a94a45f3245a5b33b7731ce9222f29125f3 | |
| parent | b38fc2ed13342524cefe7480c06c9afbcc73aedd (diff) | |
Fix spurious assertion in get-value (#3052)
| -rw-r--r-- | src/smt/smt_engine.cpp | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 303295112..2b81b3835 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -4201,7 +4201,10 @@ Expr SmtEngine::getValue(const Expr& ex) const Trace("smt") << "--- model-post expected " << expectedType << endl; // type-check the result we got - Assert(resultNode.isNull() || resultNode.getType().isSubtypeOf(expectedType), + // Notice that lambdas have function type, which does not respect the subtype + // relation, so we ignore them here. + Assert(resultNode.isNull() || resultNode.getKind() == kind::LAMBDA + || resultNode.getType().isSubtypeOf(expectedType), "Run with -t smt for details."); // ensure it's a constant |