1 files changed, 8 insertions, 0 deletions
diff --git a/src/theory/quantifiers/expr_miner.h b/src/theory/quantifiers/expr_miner.h
index c09f40d0e..59d9989c5 100644
--- a/src/theory/quantifiers/expr_miner.h
+++ b/src/theory/quantifiers/expr_miner.h
@@ -92,6 +92,14 @@ class ExprMiner
                          ExprManagerMapCollection& varMap,
                          Node query,
                          bool& needExport);
+  /**
+   * Run the satisfiability check on query and return the result
+   * (sat/unsat/unknown).
+   *
+   * In contrast to the above method, this call should be used for cases where
+   * the model for the query is not important.
+   */
+  Result doCheck(Node query);
 };
 
 }  // namespace quantifiers