rewriter fix, weaken an assertion

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index e5167dd6d5126448014f8d6223304ccbe6812745..17eaf80aaa68b3f4e2cc56e06037e69350e11446 100644 (file)
--- 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 87c6db8f2463cc8f938d857359234d30d1997dd5..109d8bb0e354672bccf28aeb13e421b1e355786a 100644 (file)
--- 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) );