From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 9 Apr 2021 13:13:37 +0000 (-0500)
Subject: Use expr miner timeout (#6321)
X-Git-Tag: cvc5-1.0.0~1936
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=26fc2731dc0366a70c5145571ff4d2c460b3148f;p=cvc5.git

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 801bde022..77573e7e3 100644
--- 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");