diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-03-13 22:27:22 -0400 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-03-20 17:18:58 -0400 |
commit | dead33e1660596c75f2bfc5ee86ed39600a92a45 (patch) | |
tree | 469095ad5852fc1ddcac8d82eb41200f22c9e709 /src | |
parent | b5914204bd29c3bc3480fdec234882cedaad2c2a (diff) |
rewriter fix, weaken an assertion
Diffstat (limited to 'src')
-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) ); |