summaryrefslogtreecommitdiff
path: root/src/theory/shared_terms_database.h
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@cs.nyu.edu>2014-06-21 21:12:36 -0400
committerMorgan Deters <mdeters@cs.nyu.edu>2014-06-21 23:41:54 -0400
commitbc7b92859698a0b23aa20dc8811be8bbe84e164e (patch)
treeda4060830ba94f71683aa4f5852924097fd19b59 /src/theory/shared_terms_database.h
parent4ba5382a32cb80aacbff11178f0da7b6493c8d48 (diff)
Fix compiler warnings (mostly unused variables).
Diffstat (limited to 'src/theory/shared_terms_database.h')
-rw-r--r--src/theory/shared_terms_database.h3
1 files changed, 0 insertions, 3 deletions
diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h
index f5724f488..dba904cdf 100644
--- a/src/theory/shared_terms_database.h
+++ b/src/theory/shared_terms_database.h
@@ -39,9 +39,6 @@ public:
private:
- /** The context */
- context::Context* d_context;
-
/** Some statistics */
IntStat d_statSharedTerms;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback