summaryrefslogtreecommitdiff
path: root/src/theory/arrays
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arrays')
-rw-r--r--src/theory/arrays/theory_arrays.cpp4
-rw-r--r--src/theory/arrays/theory_arrays.h2
2 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 3aee02316..b82216378 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -49,8 +49,8 @@ const bool d_solveWrite2 = false;
//bool d_lazyRIntro1 = true;
//bool d_eagerIndexSplitting = false;
-TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) :
- Theory(THEORY_ARRAY, c, u, out, valuation, logicInfo, qe),
+TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
+ Theory(THEORY_ARRAY, c, u, out, valuation, logicInfo),
d_numRow("theory::arrays::number of Row lemmas", 0),
d_numExt("theory::arrays::number of Ext lemmas", 0),
d_numProp("theory::arrays::number of propagations", 0),
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index e0191ccc9..a4029dc2e 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -128,7 +128,7 @@ class TheoryArrays : public Theory {
public:
- TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe);
+ TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
~TheoryArrays();
void setMasterEqualityEngine(eq::EqualityEngine* eq);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback