From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 11 Jun 2019 20:50:06 +0000 (-0500)
Subject:  Fix spurious assertion in get-value (#3052)
X-Git-Tag: cvc5-1.0.0~4119
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a8e9dd456af98c909a19da7a8458aab9fa7f2ea2;p=cvc5.git

 Fix spurious assertion in get-value (#3052)
---

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