From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Fri, 1 Dec 2017 23:10:12 +0000 (-0800)
Subject: Fix reset-assertions (#1413)
X-Git-Tag: cvc5-1.0.0~5435
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3b079e452a606988d8e5c73251a74a027dc622e7;p=cvc5.git

Fix reset-assertions (#1413)

This commit fixes two issues with reset-assertions:

- pending pops were not done in SmtEngine, resulting in the following
  assertion failure:

  d_userLevels.size() == 0 && d_userContext->getLevel() == 1

- all definitions were erased on reset-assertion in an SMT2 file,
  leading to errors about undefined types
---

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 3e8d5f0bb..032fdc673 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -417,7 +417,10 @@ void Smt2::reset() {
 }
 
 void Smt2::resetAssertions() {
-  this->Parser::reset();
+  // Remove all declarations except the ones at level 0.
+  while (this->scopeLevel() > 0) {
+    this->popScope();
+  }
 }
 
 void Smt2::setLogic(std::string name) {
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index f9d3c9909..3cbb3252e 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -5621,6 +5621,7 @@ void SmtEngine::reset() throw() {
 
 void SmtEngine::resetAssertions() throw() {
   SmtScope smts(this);
+  doPendingPops();
 
   Trace("smt") << "SMT resetAssertions()" << endl;
   if(Dump.isOn("benchmark")) {
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 09d214c35..9d049e9d2 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -74,6 +74,7 @@ SMT2_TESTS = \
 	issue1063-overloading-dt-sel.smt2 \
 	issue1063-overloading-dt-fun.smt2 \
 	non-fatal-errors.smt2 \
+	reset-assertions.smt2 \
 	sqrt2-sort-inf-unk.smt2 \
 	rec-fun-const-parse-bug.smt2
 
diff --git a/test/regress/regress0/reset-assertions.smt2 b/test/regress/regress0/reset-assertions.smt2
new file mode 100644
index 000000000..3c37f2cba
--- /dev/null
+++ b/test/regress/regress0/reset-assertions.smt2
@@ -0,0 +1,17 @@
+; EXPECT: sat
+; EXPECT: sat
+(set-logic QF_ALL)
+(set-option :incremental true)
+(set-option :produce-models true)
+
+(declare-fun x () Real)
+(declare-fun y () Real)
+(assert (> x 0.0))
+(assert (> y 0.0))
+(assert (= (+ (* 2 x) y) 4))
+(check-sat)
+(reset-assertions)
+
+(declare-fun a () (Array Int Int))
+(assert (= (select a 4) 10))
+(check-sat)