Use expr miner timeout (#6321)

We currently were ignoring the option --sygus-expr-miner-timeout=N. This corrects the issue.

diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp
index 801bde022df3b60b01decc81459a65be262c8103..77573e7e3e622e070740b90b36fbf7a88f36b8b5 100644 (file)
--- a/src/theory/quantifiers/expr_miner.cpp
+++ b/src/theory/quantifiers/expr_miner.cpp
@@ -75,7 +75,14 @@ void ExprMiner::initializeChecker(std::unique_ptr<SmtEngine>& checker,
                                   Node query)
 {
   Assert (!query.isNull());
-  initializeSubsolver(checker);
+  if (options::sygusExprMinerCheckTimeout.wasSetByUser())
+  {
+    initializeSubsolver(checker, true, options::sygusExprMinerCheckTimeout());
+  }
+  else
+  {
+    initializeSubsolver(checker);
+  }
   // also set the options
   checker->setOption("sygus-rr-synth-input", "false");
   checker->setOption("input-language", "smt2");