Relaxing too-strict assertion

diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index 6363cfb279cb369de517c711072fc2643d4fdd5a..7853c2d176b350686f77a73d088a2f4ead19dc22 100644 (file)
--- 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);