From: Clark Barrett <barrett@cs.nyu.edu>
Date: Tue, 13 Nov 2012 02:47:09 +0000 (+0000)
Subject: Relaxing too-strict assertion
X-Git-Tag: cvc5-1.0.0~7609
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=89081ba6a8a62a117cbfef99aa7c8e4bf0bf1b39;p=cvc5.git

Relaxing too-strict assertion
---

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);