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).