1 files changed, 5 insertions, 1 deletions
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index 7955d59a8..32342a9ba 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -981,7 +981,7 @@ void SynthConjecture::printSynthSolution(std::ostream& out)
 
       bool is_unique_term = true;
 
-      if (status != 0 && options::sygusRewSynth())
+      if (status != 0 && (options::sygusRewSynth() || options::sygusQueryGen()))
       {
         std::map<Node, ExpressionMinerManager>::iterator its =
             d_exprm.find(prog);
@@ -993,6 +993,10 @@ void SynthConjecture::printSynthSolution(std::ostream& out)
           {
             d_exprm[prog].enableRewriteRuleSynth();
           }
+          if (options::sygusQueryGen())
+          {
+            d_exprm[prog].enableQueryGeneration(options::sygusQueryGenThresh());
+          }
           its = d_exprm.find(prog);
         }
         bool rew_print = false;