diff options
| author | lianah <lianahady@gmail.com> | 2014-06-22 01:34:26 -0400 |
|---|---|---|
| committer | lianah <lianahady@gmail.com> | 2014-06-22 01:34:26 -0400 |
| commit | cca7d0264c74b88be9c987d3c39e16095a628395 (patch) | |
| tree | ad42c05034c7a1222daf879eac1c22d6bdf708bb /src/theory | |
| parent | c20a457581860125930b8e52fa8244302aea8e87 (diff) | |
| parent | bfbe1d5c50547a6040bec1e9f07d47185838aeee (diff) | |
Merge pull request #39 from mdeters/bv-warnings
Fix compiler warnings in BV-related code (unused vars mostly).
Diffstat (limited to 'src/theory')
| -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(), |