From 96da64b450fc6dd6f5cf701587db38adbe8ba177 Mon Sep 17 00:00:00 2001
From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Thu, 24 Sep 2020 15:47:41 -0700
Subject: SyGuS: Add default grammar for FP. (#5133)

---
 src/theory/theory_model_builder.cpp | 2 --
 1 file changed, 2 deletions(-)

(limited to 'src/theory/theory_model_builder.cpp')

diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp
index dfdea59d6..0f69566d6 100644
--- a/src/theory/theory_model_builder.cpp
+++ b/src/theory/theory_model_builder.cpp
@@ -1208,8 +1208,6 @@ Node TheoryEngineModelBuilder::normalize(TheoryModel* m, TNode r, bool evalOnly)
     if (childrenConst)
     {
       retNode = Rewriter::rewrite(retNode);
-      Assert(retNode.getKind() == kind::APPLY_UF
-             || !retNode.getType().isFirstClass() || retNode.isConst());
     }
   }
   d_normalizedCache[r] = retNode;
-- 
cgit v1.2.3