From b70f1f0319a0d7f607f3f752e21a4957ee020645 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 27 Jan 2017 09:47:18 -0800
Subject: [PATCH] fix overflow exposed in #880

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/smt_solver.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index ab6be5d91..59a5ddf8f 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -122,7 +122,8 @@ namespace smt {
                 SASSERT(n <= lvl);
                 unsigned new_lvl = lvl - n;
                 unsigned old_sz = m_scopes[new_lvl];
-                for (unsigned i = cur_sz - 1; i >= old_sz; i--) {
+                for (unsigned i = cur_sz; i > old_sz; ) {
+                    --i;
                     expr * key = m_assumptions[i].get();
                     SASSERT(m_name2assertion.contains(key));
                     expr * value = m_name2assertion.find(key);