From 2eff007e694baec68204021164238dcc274e695c Mon Sep 17 00:00:00 2001
From: Clark Barrett <barrett@cs.nyu.edu>
Date: Fri, 30 Nov 2012 22:44:26 +0000
Subject: Fix assertion in smt_engine's getValue Minor changes to RELASE-NOTES

---
 src/smt/smt_engine.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src')

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 25a066e4a..b5ed59912 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2622,7 +2622,7 @@ Expr SmtEngine::getValue(const Expr& ex) throw(ModalException, LogicException) {
   Assert(resultNode.isNull() || resultNode.getType().isSubtypeOf(n.getType()));
 
   // ensure it's a constant
-  Assert(resultNode.isConst());
+  Assert(resultNode.getKind() == kind::LAMBDA || resultNode.isConst());
 
   if(options::abstractValues() && resultNode.getType().isArray()) {
     resultNode = d_private->mkAbstractValue(resultNode);
-- 
cgit v1.2.3