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

1 files changed, 4 insertions, 1 deletions

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) {