From a8e9dd456af98c909a19da7a8458aab9fa7f2ea2 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 11 Jun 2019 15:50:06 -0500 Subject: [PATCH] Fix spurious assertion in get-value (#3052) --- src/smt/smt_engine.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) 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 -- 2.30.2