summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/term_registry.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/term_registry.cpp')
-rw-r--r--src/theory/quantifiers/term_registry.cpp6
1 files changed, 4 insertions, 2 deletions
diff --git a/src/theory/quantifiers/term_registry.cpp b/src/theory/quantifiers/term_registry.cpp
index 324217798..36dc8865c 100644
--- a/src/theory/quantifiers/term_registry.cpp
+++ b/src/theory/quantifiers/term_registry.cpp
@@ -29,7 +29,9 @@ namespace cvc5 {
namespace theory {
namespace quantifiers {
-TermRegistry::TermRegistry(QuantifiersState& qs, QuantifiersRegistry& qr)
+TermRegistry::TermRegistry(Env& env,
+ QuantifiersState& qs,
+ QuantifiersRegistry& qr)
: d_presolve(qs.getUserContext(), true),
d_presolveCache(qs.getUserContext()),
d_termEnum(new TermEnumeration),
@@ -42,7 +44,7 @@ TermRegistry::TermRegistry(QuantifiersState& qs, QuantifiersRegistry& qr)
if (options::sygus() || options::sygusInst())
{
// must be constructed here since it is required for datatypes finistInit
- d_sygusTdb.reset(new TermDbSygus(qs));
+ d_sygusTdb.reset(new TermDbSygus(env, qs));
}
Trace("quant-engine-debug") << "Initialize quantifiers engine." << std::endl;
Trace("quant-engine-debug")
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback