summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorTim King <taking@cs.nyu.edu>2017-11-15 09:40:20 -0800
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>2017-11-15 11:40:20 -0600
commiteddabf66104dcc061943655e530d8d8b8d8a7041 (patch)
treedc56df6a02767cf014690d0fecdd8eaab1ed84f9
parent35b57e733af6e1588cd3b8625db932fb1d66a9a2 (diff)
Removes an unused variable from Theory. (#1375)
-rw-r--r--src/theory/theory.h6
1 files changed, 0 insertions, 6 deletions
diff --git a/src/theory/theory.h b/src/theory/theory.h
index d9e89902c..0f820ac8e 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -229,12 +229,6 @@ private:
void printFacts(std::ostream& os) const;
void debugPrintFacts() const;
- /**
- * Whether proofs are enabled
- *
- */
- bool d_proofEnabled;
-
public:
/**
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback