diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-12-13 20:17:50 -0600 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-12-14 02:17:50 +0000 |
| commit | 075e3d97974c89dcbd4cf6c7a1c3b37cbb27403d (patch) | |
| tree | cb1466de550072e4a11d0a67816e6e23ef5770cb /src/theory/sets | |
| parent | 000feaeb02292d7a2873198664022801b12e5151 (diff) | |
Fix extended rewriter for binary associative operators. (#2751)
This was causing assertion failures when using Sets + Sygus.
Diffstat (limited to 'src/theory/sets')
| -rw-r--r-- | src/theory/sets/theory_sets_rewriter.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp index a3f1f9893..2a2015319 100644 --- a/src/theory/sets/theory_sets_rewriter.cpp +++ b/src/theory/sets/theory_sets_rewriter.cpp @@ -47,7 +47,7 @@ bool checkConstantMembership(TNode elementTerm, TNode setTerm) RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { NodeManager* nm = NodeManager::currentNM(); Kind kind = node.getKind(); - + Trace("sets-postrewrite") << "Process: " << node << std::endl; if(node.isConst()) { // Dare you touch the const and mangle it to something else. @@ -204,6 +204,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { if( rew!=node ){ Trace("sets-rewrite") << "Sets::rewrite " << node << " -> " << rew << std::endl; } + Trace("sets-rewrite") << "...no rewrite." << std::endl; return RewriteResponse(REWRITE_DONE, rew); } break; |