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 3e8d5f0bbb9205fa906b81d33070a4804bcc6862..032fdc67360d77ab2f2aa4ae77e6a9d8960f4751 100644 (file)
--- 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 f9d3c9909c04dcabcb2eeefce5eb40e4e56ffbde..3cbb3252e10409bbf4e8acfbd531313b6c2df65c 100644 (file)
--- 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 09d214c3580a8bf741ee257f4e1a0eb150a3aa49..9d049e9d266c49fc17d1d3dbf8063dbc95a3665b 100644 (file)
--- 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 (file)
index 0000000..3c37f2c
--- /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)