From bf40bb8005a02c992775c5a775e784985ba84bb3 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 2 Mar 2016 18:27:01 +0000 Subject: [PATCH] Bugfix for 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 d06770ac0..3d1950179 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -182,7 +182,7 @@ public: m_map.push(); } virtual void pop(unsigned n) { - if (n < m_num_scopes) { // allow inc_sat_solver to + if (n > m_num_scopes) { // allow inc_sat_solver to n = m_num_scopes; // take over for another solver. } m_bb_rewriter.pop(n);