summaryrefslogtreecommitdiff
path: root/src/theory/bv/theory_bv.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/bv/theory_bv.h')
-rw-r--r--src/theory/bv/theory_bv.h4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 27138abfc..1da15abf8 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -22,7 +22,6 @@
#include "context/cdhashset.h"
#include "context/cdlist.h"
#include "context/context.h"
-#include "smt/smt_globals.h"
#include "theory/bv/bv_subtheory.h"
#include "theory/bv/theory_bv_utils.h"
#include "theory/theory.h"
@@ -56,7 +55,8 @@ class TheoryBV : public Theory {
public:
- TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, SmtGlobals* globals);
+ TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out,
+ Valuation valuation, const LogicInfo& logicInfo);
~TheoryBV();
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback