diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-04-09 08:13:37 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-04-09 13:13:37 +0000 |
commit | 26fc2731dc0366a70c5145571ff4d2c460b3148f (patch) | |
tree | 0701c84a4eabf0687d22733c2cd261bf07a148c6 /src/theory/quantifiers | |
parent | de06ddbed29109ce83b6a2fc0b042fcf64fa6ad4 (diff) |
Use expr miner timeout (#6321)
We currently were ignoring the option --sygus-expr-miner-timeout=N. This corrects the issue.
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/expr_miner.cpp | 9 |
1 files changed, 8 insertions, 1 deletions
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"); |