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

diff --git a/src/smt/model.cpp b/src/smt/model.cpp
index 8a9f944d2337e405958dc08c47bf8670d85f40ea..ccf73dda05bbdfc401c5fc7ac1baba3d56f1e230 100644 (file)
--- 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 d3ba676fc8340c07f2fecad9f8bd81dd47c76153..2faad79610a2c75a145970b0c6ca2e7121c193aa 100644 (file)
--- 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);
 

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index fb8914a36927b7a284b9ed6c1346fd3ef824ded4..fda5c69eb9d3ad0d5734e99f02dbf4e79f399ad4 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -588,6 +588,8 @@ set(regress_0_tests
   regress0/issue5099-model-1.smt2
   regress0/issue5099-model-2.smt2
   regress0/issue5144-resetAssertions.smt2
+  regress0/issue5540-2-dump-model.smt2
+  regress0/issue5540-model-decls.smt2
   regress0/ite.cvc
   regress0/ite2.smt2
   regress0/ite3.smt2

diff --git a/test/regress/regress0/issue5540-2-dump-model.smt2 b/test/regress/regress0/issue5540-2-dump-model.smt2
new file mode 100644 (file)
index 0000000..56d3b24
--- /dev/null
+++ b/test/regress/regress0/issue5540-2-dump-model.smt2
@@ -0,0 +1,9 @@
+; SCRUBBER: sed -e 's/Bool.*$/Bool/'
+; COMMAND-LINE: --dump-models
+; EXPECT: sat
+; EXPECT: (
+; EXPECT: (define-fun v16 () Bool
+; EXPECT: )
+(set-logic UFLIA)
+(declare-fun v16 () Bool)
+(check-sat)

diff --git a/test/regress/regress0/issue5540-model-decls.smt2 b/test/regress/regress0/issue5540-model-decls.smt2
new file mode 100644 (file)
index 0000000..714159c
--- /dev/null
+++ b/test/regress/regress0/issue5540-model-decls.smt2
@@ -0,0 +1,19 @@
+; SCRUBBER: sed -e 's/Bool.*$/Bool/'
+; COMMAND-LINE: --dump-models -i
+; EXPECT:sat
+; EXPECT: (
+; EXPECT: (define-fun a () Bool
+; EXPECT: )
+; EXPECT: sat
+; EXPECT: (
+; EXPECT: (define-fun a () Bool
+; EXPECT: )
+; EXPECT: sat
+; EXPECT: (
+; EXPECT: (define-fun a () Bool
+; EXPECT: )
+(set-logic ALL)
+(declare-fun a () Bool)
+(check-sat)
+(check-sat)
+(check-sat)