Minor refactoring of subsolver initialization (#4731)

This decouples asserting a formula with initialization (previously it was a complex process to assert a formula due to having to clone/export to a new ExprManager). Now it is trivial.

This commit fixes an unintended consequence of the previous complications. Previously, SmtEngine::setOption would be set after asserting formulas to an SmtEngine subsolver, which is technically incorrect, as options should be finalized before the first assert.

This is required for further cleaning up of options listeners.

1 files changed, 0 insertions, 2 deletions

diff --git a/src/theory/smt_engine_subsolver.h b/src/theory/smt_engine_subsolver.h
index 64646ac05..cbc871cce 100644
--- a/src/theory/smt_engine_subsolver.h
+++ b/src/theory/smt_engine_subsolver.h
@@ -35,12 +35,10 @@ namespace theory {
  * of the argument "query".
  *
  * @param smte The smt engine pointer to initialize
- * @param query The query to check (if provided)
  * @param needsTimeout Whether we would like to set a timeout
  * @param timeout The timeout (in milliseconds)
  */
 void initializeSubsolver(std::unique_ptr<SmtEngine>& smte,
-                         Node query = Node::null(),
                          bool needsTimeout = false,
                          unsigned long timeout = 0);