From e40b31aa45ca9e34b92875a8a1079ae953922956 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Sat, 9 Oct 2010 06:13:17 +0000
Subject: bug fixes to model gen

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

(limited to 'src/smt')

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 3a4fd90e9..5de1cd0b1 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -410,7 +410,7 @@ Expr SmtEngine::getValue(Expr e)
   Node resultNode = d_theoryEngine->getValue(n);
 
   // type-check the result we got
-  Assert(resultNode.getType(true) == eNode.getType());
+  Assert(resultNode.isNull() || resultNode.getType(true) == eNode.getType());
   return Expr(d_exprManager, new Node(resultNode));
 }
 
-- 
cgit v1.2.3