summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/quantifiers_statistics.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/quantifiers_statistics.h')
-rw-r--r--src/theory/quantifiers/quantifiers_statistics.h4
1 files changed, 1 insertions, 3 deletions
diff --git a/src/theory/quantifiers/quantifiers_statistics.h b/src/theory/quantifiers/quantifiers_statistics.h
index f03d27ee3..438efd30f 100644
--- a/src/theory/quantifiers/quantifiers_statistics.h
+++ b/src/theory/quantifiers/quantifiers_statistics.h
@@ -18,8 +18,7 @@
#ifndef CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_STATISTICS_H
#define CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_STATISTICS_H
-#include "util/statistics_registry.h"
-#include "util/stats_timer.h"
+#include "util/statistics_stats.h"
namespace cvc5 {
namespace theory {
@@ -33,7 +32,6 @@ class QuantifiersStatistics
{
public:
QuantifiersStatistics();
- ~QuantifiersStatistics();
TimerStat d_time;
TimerStat d_qcf_time;
TimerStat d_ematching_time;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback