From: Tim King <taking@cs.nyu.edu>
Date: Tue, 17 Oct 2017 20:17:20 +0000 (-0700)
Subject: Fixing 2 instances of an unused variable. (#1253)
X-Git-Tag: cvc5-1.0.0~5552
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=27dac5e91eee563d62795e43d5e7ac5f6c878730;p=cvc5.git

Fixing 2 instances of an unused variable. (#1253)
---

diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index c543c16e2..5d48c1ce2 100644
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -65,11 +65,17 @@ void SygusSplitNew::getSygusSplits( Node n, const Datatype& dt, std::vector< Nod
   splits.insert( splits.end(), d_splits[n].begin(), d_splits[n].end() );
 }
 
-
-SygusSymBreakNew::SygusSymBreakNew( TheoryDatatypes * td, quantifiers::TermDbSygus * tds, context::Context* c ) : 
-d_td( td ), d_tds( tds ), d_context( c ), 
-d_testers( c ), d_is_const( c ), d_testers_exp( c ), d_active_terms( c ), d_currTermSize( c ) {
-  d_zero = NodeManager::currentNM()->mkConst( Rational(0) );
+SygusSymBreakNew::SygusSymBreakNew(TheoryDatatypes* td,
+                                   quantifiers::TermDbSygus* tds,
+                                   context::Context* c)
+    : d_td(td),
+      d_tds(tds),
+      d_testers(c),
+      d_is_const(c),
+      d_testers_exp(c),
+      d_active_terms(c),
+      d_currTermSize(c) {
+  d_zero = NodeManager::currentNM()->mkConst(Rational(0));
 }
 
 SygusSymBreakNew::~SygusSymBreakNew() {
diff --git a/src/theory/datatypes/datatypes_sygus.h b/src/theory/datatypes/datatypes_sygus.h
index 3e37fe728..bb83b4850 100644
--- a/src/theory/datatypes/datatypes_sygus.h
+++ b/src/theory/datatypes/datatypes_sygus.h
@@ -56,7 +56,6 @@ class SygusSymBreakNew
 private:
   TheoryDatatypes * d_td;
   quantifiers::TermDbSygus * d_tds;
-  context::Context* d_context;
   typedef context::CDHashMap< Node, int, NodeHashFunction > IntMap;
   typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap;
   typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
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 ) {