From 26fc2731dc0366a70c5145571ff4d2c460b3148f Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 9 Apr 2021 08:13:37 -0500 Subject: [PATCH] Use expr miner timeout (#6321) We currently were ignoring the option --sygus-expr-miner-timeout=N. This corrects the issue. --- src/theory/quantifiers/expr_miner.cpp | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) 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& 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"); -- 2.30.2