summaryrefslogtreecommitdiff
path: root/src/theory/shared_terms_database.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/shared_terms_database.h')
-rw-r--r--src/theory/shared_terms_database.h3
1 files changed, 1 insertions, 2 deletions
diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h
index efc2b2154..655c2aa88 100644
--- a/src/theory/shared_terms_database.h
+++ b/src/theory/shared_terms_database.h
@@ -28,7 +28,7 @@
#include "theory/trust_node.h"
#include "theory/uf/equality_engine.h"
#include "theory/uf/proof_equality_engine.h"
-#include "util/statistics_registry.h"
+#include "util/statistics_stats.h"
namespace cvc5 {
@@ -163,7 +163,6 @@ class SharedTermsDatabase : public context::ContextNotifyObj {
context::Context* context,
context::UserContext* userContext,
ProofNodeManager* pnm);
- ~SharedTermsDatabase();
//-------------------------------------------- initialization
/** Called to set the equality engine. */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback