diff options
| author | Tim King <taking@cs.nyu.edu> | 2017-10-17 13:17:20 -0700 |
|---|---|---|
| committer | Mathias Preiner <mathias.preiner@gmail.com> | 2017-10-17 13:17:20 -0700 |
| commit | 27dac5e91eee563d62795e43d5e7ac5f6c878730 (patch) | |
| tree | 267f842042ee02af6a32dad20e99615abb1e0a4d /src/theory/sets | |
| parent | 0958ceced1107fe4be1c9f585bf5fad8fa73a7a7 (diff) | |
Fixing 2 instances of an unused variable. (#1253)
Diffstat (limited to 'src/theory/sets')
| -rw-r--r-- | src/theory/sets/theory_sets_rewriter.cpp | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp index 8c3fe67d3..084ca6c96 100644 --- a/src/theory/sets/theory_sets_rewriter.cpp +++ b/src/theory/sets/theory_sets_rewriter.cpp @@ -15,10 +15,11 @@ **/ #include "theory/sets/theory_sets_rewriter.h" -#include "theory/sets/normal_form.h" -#include "theory/sets/rels_utils.h" + #include "expr/attribute.h" #include "options/sets_options.h" +#include "theory/sets/normal_form.h" +#include "theory/sets/rels_utils.h" namespace CVC4 { namespace theory { @@ -92,7 +93,7 @@ RewriteResponse flattenNode(TNode n, TNode trivialNode, TNode skipNode) static const unsigned MAX_CHILDREN = (1u << __CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN ) - 1; AlwaysAssert(childList.size() < MAX_CHILDREN, "do not support formulas this big"); - ChildList::iterator cur = childList.begin(), next, en = childList.end(); + ChildList::iterator cur = childList.begin(), en = childList.end(); Node ret = (*cur); ++cur; while( cur != en ) { |