1 files changed, 16 insertions, 0 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 0a4859971..b1d6df852 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2182,6 +2182,22 @@ void SmtEngine::setDefaults() {
         << endl;
     options::bvLazyRewriteExtf.set(false);
   }
+
+  if (!options::sygusExprMinerCheckUseExport())
+  {
+    if (options::sygusExprMinerCheckTimeout.wasSetByUser())
+    {
+      throw OptionException(
+          "--sygus-expr-miner-check-timeout=N requires "
+          "--sygus-expr-miner-check-use-export");
+    }
+    if (options::sygusRewSynthInput())
+    {
+      throw OptionException(
+          "--sygus-rr-synth-input requires "
+          "--sygus-expr-miner-check-use-export");
+    }
+  }
 }
 
 void SmtEngine::setProblemExtended(bool value)