From dbf9609b4c6712e9130888dd65405c2b03ea6c5f Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Wed, 2 Mar 2016 18:06:14 +0000
Subject: [PATCH] added assertion

---
 src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
index 022a2273a..c260178ad 100644
--- a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
+++ b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
@@ -167,6 +167,7 @@ struct blaster_rewriter_cfg : public default_rewriter_cfg {
 
     void pop(unsigned num_scopes) {
         if (num_scopes > 0) {
+            SASSERT(num_scopes <= m_keyval_lim.size());
             unsigned new_sz = m_keyval_lim.size() - num_scopes;
             unsigned lim = m_keyval_lim[new_sz];
             for (unsigned i = m_keys.size(); i > lim; ) {