From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 2 Dec 2020 00:00:49 +0000 (-0600)
Subject: Fix issues related to model declarations (#5560)
X-Git-Tag: cvc5-1.0.0~2531
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=798644e64f438f320577a444110744041e39d1ff;p=cvc5.git

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 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);
 
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index fb8914a36..fda5c69eb 100644
--- 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
index 000000000..56d3b2458
--- /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
index 000000000..714159c9f
--- /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)