Fix issues related to model declarations (#5560)

This corrects two issues related to model declarations:
(1) model declaration terms were mistaken not cleared,
(2) the model needs to be explicitly destructed before the node manager because it contains references to Node.

Fixes #5540

2 files changed, 6 insertions, 1 deletions

diff --git a/src/smt/model.cpp b/src/smt/model.cpp
index 8a9f944d2..ccf73dda0 100644
--- a/src/smt/model.cpp
+++ b/src/smt/model.cpp
@@ -49,7 +49,11 @@ Node Model::getValue(TNode n) const { return d_tmodel->getValue(n); }
 
 bool Model::hasApproximations() const { return d_tmodel->hasApproximations(); }
 
-void Model::clearModelDeclarations() { d_declareSorts.clear(); }
+void Model::clearModelDeclarations()
+{
+  d_declareTerms.clear();
+  d_declareSorts.clear();
+}
 
 void Model::addDeclarationSort(TypeNode tn) { d_declareSorts.push_back(tn); }
 
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index d3ba676fc..2faad7961 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -332,6 +332,7 @@ SmtEngine::~SmtEngine()
     d_absValues.reset(nullptr);
     d_asserts.reset(nullptr);
     d_dumpm.reset(nullptr);
+    d_model.reset(nullptr);
 
     d_sygusSolver.reset(nullptr);