diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-21 21:13:12 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-21 21:14:39 -0400 |
| commit | bfbe1d5c50547a6040bec1e9f07d47185838aeee (patch) | |
| tree | 869452fb6704c99a743736fac29450c4a097f645 /src/theory/bv | |
| parent | 3264f3bb76944129074c2a3204a94f0b02740e23 (diff) | |
Fix compiler warnings in BV-related code (unused vars mostly).
Diffstat (limited to 'src/theory/bv')
| -rw-r--r-- | src/theory/bv/bv_inequality_graph.h | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h index 9a898ebe6..4a6757871 100644 --- a/src/theory/bv/bv_inequality_graph.h +++ b/src/theory/bv/bv_inequality_graph.h @@ -39,9 +39,6 @@ extern const ReasonId AxiomReasonId; class InequalityGraph : public context::ContextNotifyObj{ - - context::Context* d_context; - struct InequalityEdge { TermId next; ReasonId reason; @@ -126,7 +123,6 @@ class InequalityGraph : public context::ContextNotifyObj{ context::CDO<bool> d_inConflict; std::vector<TNode> d_conflict; - bool d_signed; ModelValues d_modelValues; void initializeModelValue(TNode node); @@ -214,12 +210,10 @@ public: InequalityGraph(context::Context* c, bool s = false) : ContextNotifyObj(c), - d_context(c), d_ineqNodes(), d_ineqEdges(), d_inConflict(c, false), d_conflict(), - d_signed(s), d_modelValues(c), d_disequalities(c), d_disequalitiesAlreadySplit(), |