From 89081ba6a8a62a117cbfef99aa7c8e4bf0bf1b39 Mon Sep 17 00:00:00 2001
From: Clark Barrett <barrett@cs.nyu.edu>
Date: Tue, 13 Nov 2012 02:47:09 +0000
Subject: [PATCH] Relaxing too-strict assertion

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

diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index 6363cfb27..7853c2d17 100644
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -516,7 +516,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
           if (assignable) {
             if ((assignOne || !evaluable) && fullModel) {
               assignOne = false;
-              Assert(!t.isBoolean());
+              Assert(!t.isBoolean() || (*i2).getKind() == kind::APPLY_UF);
               Node n;
               if (t.getCardinality().isInfinite()) {
                 n = typeConstSet.nextTypeEnum(t, true);
-- 
2.30.2