From 3f02beb8203bb4bf68e39a168254fc97e8f75338 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 3 Dec 2015 10:18:40 -0800
Subject: [PATCH] reset-assertions resets everything (also declarations, and we
 take scopes) when global-declarations is false. v2.5

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/cmd_context/cmd_context.cpp | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index f863393fb..02b2b6525 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -1493,6 +1493,11 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
 }
 
 void cmd_context::reset_assertions() {
+    if (!m_global_decls) {
+        reset(false);
+        return;
+    }
+
     if (m_opt) {
         m_opt = 0;
     }