diff options
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/quantifiers/expr_miner.cpp | 2 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_repair_const.cpp | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp index 6069745e0..14bc05335 100644 --- a/src/theory/quantifiers/expr_miner.cpp +++ b/src/theory/quantifiers/expr_miner.cpp @@ -76,7 +76,7 @@ void ExprMiner::initializeChecker(std::unique_ptr<SmtEngine>& checker, Node query) { Assert (!query.isNull()); - if (Options::current().quantifiers.sygusExprMinerCheckTimeout__setByUser) + if (Options::current().quantifiers.sygusExprMinerCheckTimeoutWasSetByUser) { initializeSubsolver(checker, true, options::sygusExprMinerCheckTimeout()); } diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp index d45a96d3b..0b5d06bd2 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp +++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp @@ -234,7 +234,7 @@ bool SygusRepairConst::repairSolution(Node sygusBody, std::unique_ptr<SmtEngine> repcChecker; // initialize the subsolver using the standard method initializeSubsolver(repcChecker, - Options::current().wasSetByUser(options::sygusRepairConstTimeout), + Options::current().quantifiers.sygusRepairConstTimeoutWasSetByUser, options::sygusRepairConstTimeout()); // renable options disabled by sygus repcChecker->setOption("miniscope-quant", "true"); |