From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Fri, 14 Mar 2014 02:27:22 +0000 (-0400)
Subject: rewriter fix, weaken an assertion
X-Git-Tag: cvc5-1.0.0~7002^2~3
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=dead33e1660596c75f2bfc5ee86ed39600a92a45;p=cvc5.git

rewriter fix, weaken an assertion
---

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index e5167dd6d..17eaf80aa 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -397,8 +397,7 @@ const Elements& getElements(TNode setterm, SettermElementsMap& settermElementsMa
         Unhandled();
       }
     } else {
-      Assert(numChildren == 0);
-      Assert(k == kind::VARIABLE);
+      Assert(k == kind::VARIABLE || k == kind::APPLY_UF);
       /* assign emptyset, which is default */
     }
 
diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp
index 87c6db8f2..109d8bb0e 100644
--- a/src/theory/sets/theory_sets_rewriter.cpp
+++ b/src/theory/sets/theory_sets_rewriter.cpp
@@ -81,7 +81,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
     // rewrite (A subset-or-equal B) as (A union B = B)
     TNode A = node[0];
     TNode B = node[1];
-    return RewriteResponse(REWRITE_AGAIN,
+    return RewriteResponse(REWRITE_AGAIN_FULL,
                            nm->mkNode(kind::EQUAL,
                                       nm->mkNode(kind::UNION, A, B),
                                       B) );