Fix --tear-down-incrementalfixTearDownIncremental

3 files changed, 33 insertions, 7 deletions

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 668fc9382..b6cc2ad17 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -4735,7 +4735,21 @@ std::ostream& operator<<(std::ostream& out, const Statistics& stats)
 
 Solver::Solver(Options* opts)
 {
-  d_nodeMgr.reset(new NodeManager());
+  init(opts, std::move(std::make_unique<NodeManager>()));
+}
+
+Solver::~Solver() {}
+
+/* Helpers and private functions                                              */
+/* -------------------------------------------------------------------------- */
+
+Solver::Solver(Options* opts, std::unique_ptr<NodeManager> nm)
+{
+  init(opts, std::move(nm));
+}
+
+void Solver::init(Options* opts, std::unique_ptr<NodeManager> nm) {
+  d_nodeMgr.swap(nm);
   d_originalOptions.reset(new Options());
   if (opts != nullptr)
   {
@@ -4747,11 +4761,6 @@ Solver::Solver(Options* opts)
   resetStatistics();
 }
 
-Solver::~Solver() {}
-
-/* Helpers and private functions                                              */
-/* -------------------------------------------------------------------------- */
-
 NodeManager* Solver::getNodeManager(void) const { return d_nodeMgr.get(); }
 
 void Solver::increment_term_stats(Kind kind) const
@@ -7187,6 +7196,17 @@ void Solver::push(uint32_t nscopes) const
   CVC5_API_TRY_CATCH_END;
 }
 
+void Solver::reset(Options* opts)
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  //////// all checks before this line
+  std::unique_ptr<NodeManager> nm(std::move(d_nodeMgr));
+  this->~Solver();
+  new (this) Solver(opts, std::move(nm));
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+
 void Solver::resetAssertions(void) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index a1421cf12..1a2899a56 100644
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -3931,6 +3931,8 @@ class CVC5_EXPORT Solver
    */
   void push(uint32_t nscopes = 1) const;
 
+  void reset(Options* opts);
+
   /**
    * Remove all assertions.
    * SMT-LIB:
@@ -4134,6 +4136,10 @@ class CVC5_EXPORT Solver
   Statistics getStatistics() const;
 
  private:
+  Solver(Options* opts, std::unique_ptr<NodeManager> nm);
+
+  void init(Options* opts, std::unique_ptr<NodeManager> nm);
+
   /** @return the node manager of this solver */
   NodeManager* getNodeManager(void) const;
   /** Reset the API statistics */
diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index 6bdc1abc9..1cbde6226 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -118,7 +118,7 @@ void CommandExecutor::reset()
    * NodeManager copies the options into a new options object before SmtEngine
    * configures additional options based on the given CL options.
    * We can thus safely reuse CommandExecutor::d_options here. */
-  d_solver.reset(new api::Solver(&d_options));
+  d_solver->reset(&d_options);
 }
 
 bool CommandExecutor::doCommandSingleton(Command* cmd)