summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/conjecture_generator.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/conjecture_generator.cpp')
-rw-r--r--src/theory/quantifiers/conjecture_generator.cpp10
1 files changed, 5 insertions, 5 deletions
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index 17eaad5c6..f9625d7ac 100644
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -86,15 +86,15 @@ void OpArgIndex::getGroundTerms( ConjectureGenerator * s, std::vector< TNode >&
}
}
-ConjectureGenerator::ConjectureGenerator(QuantifiersState& qs,
+ConjectureGenerator::ConjectureGenerator(Env& env,
+ QuantifiersState& qs,
QuantifiersInferenceManager& qim,
QuantifiersRegistry& qr,
TermRegistry& tr)
- : QuantifiersModule(qs, qim, qr, tr),
+ : QuantifiersModule(env, qs, qim, qr, tr),
d_notify(*this),
- d_uequalityEngine(
- d_notify, qs.getSatContext(), "ConjectureGenerator::ee", false),
- d_ee_conjectures(qs.getSatContext()),
+ d_uequalityEngine(d_notify, context(), "ConjectureGenerator::ee", false),
+ d_ee_conjectures(context()),
d_conj_count(0),
d_subs_confirmCount(0),
d_subs_unkCount(0),
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback