From dead33e1660596c75f2bfc5ee86ed39600a92a45 Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Thu, 13 Mar 2014 22:27:22 -0400 Subject: [PATCH] rewriter fix, weaken an assertion --- src/theory/sets/theory_sets_private.cpp | 3 +-- 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) ); -- 2.30.2