From 798644e64f438f320577a444110744041e39d1ff Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 1 Dec 2020 18:00:49 -0600 Subject: 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 --- src/smt/model.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'src/smt/model.cpp') 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); } -- cgit v1.2.3