diff options
Diffstat (limited to 'src/theory/quantifiers/expr_miner.h')
-rw-r--r-- | src/theory/quantifiers/expr_miner.h | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/src/theory/quantifiers/expr_miner.h b/src/theory/quantifiers/expr_miner.h index 3933b9635..702dbf5aa 100644 --- a/src/theory/quantifiers/expr_miner.h +++ b/src/theory/quantifiers/expr_miner.h @@ -85,7 +85,12 @@ class ExprMiner : protected EnvObj * of the argument "query", which is a formula whose free variables (of * kind BOUND_VARIABLE) are a subset of d_vars. */ - void initializeChecker(std::unique_ptr<SolverEngine>& smte, Node query); + void initializeChecker(std::unique_ptr<SolverEngine>& checker, Node query); + /** Also with configurable options and logic */ + void initializeChecker(std::unique_ptr<SolverEngine>& checker, + Node query, + const Options& opts, + const LogicInfo& logicInfo); /** * Run the satisfiability check on query and return the result * (sat/unsat/unknown). |