summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/fmf/model_engine.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/fmf/model_engine.h')
-rw-r--r--src/theory/quantifiers/fmf/model_engine.h4
1 files changed, 3 insertions, 1 deletions
diff --git a/src/theory/quantifiers/fmf/model_engine.h b/src/theory/quantifiers/fmf/model_engine.h
index f818a6362..b5ab86f20 100644
--- a/src/theory/quantifiers/fmf/model_engine.h
+++ b/src/theory/quantifiers/fmf/model_engine.h
@@ -18,6 +18,7 @@
#ifndef CVC5__THEORY__QUANTIFIERS__MODEL_ENGINE_H
#define CVC5__THEORY__QUANTIFIERS__MODEL_ENGINE_H
+#include "smt/env_obj.h"
#include "theory/quantifiers/fmf/model_builder.h"
#include "theory/quantifiers/quant_module.h"
#include "theory/theory_model.h"
@@ -42,7 +43,8 @@ private:
int d_triedLemmas;
int d_totalLemmas;
public:
- ModelEngine(QuantifiersState& qs,
+ ModelEngine(Env& env,
+ QuantifiersState& qs,
QuantifiersInferenceManager& qim,
QuantifiersRegistry& qr,
TermRegistry& tr,
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback