From 1aeea763ff4371ad0025df36fbf6881505a240a0 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Wed, 2 Mar 2016 18:39:28 +0000
Subject: [PATCH] Assertion fix in inc_sat_solver

---
 src/sat/sat_solver/inc_sat_solver.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index 3d1950179..1c156d83e 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -187,7 +187,7 @@ public:
         }
         m_bb_rewriter.pop(n);
         m_map.pop(n);
-        SASSERT(n >= m_num_scopes);
+        SASSERT(n <= m_num_scopes);
         m_solver.user_pop(n);
         m_num_scopes -= n;
         while (n > 0) {