1 files changed, 5 insertions, 3 deletions
diff --git a/src/theory/quantifiers/sygus/enum_value_manager.cpp b/src/theory/quantifiers/sygus/enum_value_manager.cpp
index 8a2d70bfa..e7b3bbaa9 100644
--- a/src/theory/quantifiers/sygus/enum_value_manager.cpp
+++ b/src/theory/quantifiers/sygus/enum_value_manager.cpp
@@ -33,13 +33,15 @@ namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
-EnumValueManager::EnumValueManager(Node e,
+EnumValueManager::EnumValueManager(Env& env,
                                    QuantifiersState& qs,
                                    QuantifiersInferenceManager& qim,
                                    TermRegistry& tr,
                                    SygusStatistics& s,
+                                   Node e,
                                    bool hasExamples)
-    : d_enum(e),
+    : EnvObj(env),
+      d_enum(e),
       d_qstate(qs),
       d_qim(qim),
       d_treg(tr),
@@ -108,7 +110,7 @@ Node EnumValueManager::getEnumeratedValue(bool& activeIncomplete)
             d_samplerRrV->initializeSygus(
                 d_tds, e, options::sygusSamples(), false);
             // use the default output for the output of sygusRewVerify
-            out = d_qstate.options().base.out;
+            out = options().base.out;
           }
           d_secd.reset(new SygusEnumeratorCallbackDefault(
               e, &d_stats, d_eec.get(), d_samplerRrV.get(), out));