diff options
| -rw-r--r-- | src/theory/sets/theory_sets_private.cpp | 3 | ||||
| -rw-r--r-- | src/theory/sets/theory_sets_rewriter.cpp | 2 |
2 files changed, 2 insertions, 3 deletions
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) ); |