diff --git a/src/math/dd/dd_bdd.cpp b/src/math/dd/dd_bdd.cpp
index ccc5b67d2..86f2b9408 100644
--- a/src/math/dd/dd_bdd.cpp
+++ b/src/math/dd/dd_bdd.cpp
@@ -318,7 +318,7 @@ namespace dd {
             goto go_down;
         }
         else {
-            while (current_cost() != best_cost) {
+            while (current_cost() > best_cost) {
                 sift_up(--lvl);
             }
             return;
@@ -339,7 +339,7 @@ namespace dd {
             goto go_up;
         }
         else {
-            while (current_cost() != best_cost) {
+            while (current_cost() > best_cost) {
                 sift_up(lvl++);
             }
             return;
diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp
index 3fc5f80e6..49a73b269 100644
--- a/src/opt/maxres.cpp
+++ b/src/opt/maxres.cpp
@@ -289,10 +289,8 @@ public:
                Give preference to cores that have large minimal values.
             */
             sort_assumptions(asms);              
-            m_last_index = std::min(m_last_index, asms.size()-1);
-            m_last_index = 0;
-            unsigned index = m_last_index>0?m_last_index-1:0;
             m_last_index = 0;
+            unsigned index = 0;
             bool first = index > 0;
             SASSERT(index < asms.size() || asms.empty());
             IF_VERBOSE(10, verbose_stream() << "start hill climb " << index << " asms: " << asms.size() << "\n";);
diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp
index f8186e446..fd961d94b 100644
--- a/src/sat/sat_config.cpp
+++ b/src/sat/sat_config.cpp
@@ -99,7 +99,7 @@ namespace sat {
         else
             m_local_search_mode = local_search_mode::wsat;
         m_local_search_dbg_flips = p.local_search_dbg_flips();
-        m_binspr            = p.binspr();
+        //m_binspr            = p.binspr();
         m_binspr            = false;     // prevent adventurous users from trying feature that isn't ready
         m_anf_simplify      = p.anf();
         m_anf_delay         = p.anf_delay();
diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp
index 097451035..ec5d953bf 100644
--- a/src/smt/theory_pb.cpp
+++ b/src/smt/theory_pb.cpp
@@ -1325,37 +1325,37 @@ namespace smt {
 
     bool theory_pb::gc() {
 
-
         unsigned z = 0, nz = 0;
         m_occs.reset();
         for (unsigned i = 0; i < m_card_trail.size(); ++i) {
             bool_var v = m_card_trail[i];
-            if (v == null_bool_var) continue;
+            if (v == null_bool_var) 
+                continue;
             card* c = m_var_infos[v].m_card;
-            if (c) {
-                c->reset_propagations();
-                literal lit = c->lit();
-                if (c->is_aux() && ctx.get_assign_level(lit) > ctx.get_search_level()) {
-                    double activity = ctx.get_activity(v);
-                    if (activity <= 0) {
-                        nz++;
-                    }
-                    else {
-                        z++;
-                        clear_watch(*c);
-                        m_var_infos[v].m_card = nullptr;
-                        dealloc(c);
-                        m_card_trail[i] = null_bool_var;
-                        ctx.remove_watch(v);
-                        // TBD: maybe v was used in a clause for propagation.
-                        m_occs.insert(v);
-                    }
+            if (!c) 
+                continue;
+            c->reset_propagations();
+            literal lit = c->lit();
+            if (c->is_aux() && ctx.get_assign_level(lit) > ctx.get_search_level()) {
+                double activity = ctx.get_activity(v);
+                if (activity <= 0) {
+                    nz++;
+                }
+                else {
+                    z++;
+                    clear_watch(*c);
+                    m_var_infos[v].m_card = nullptr;
+                    dealloc(c);
+                    m_card_trail[i] = null_bool_var;
+                    ctx.remove_watch(v);
+                    // TBD: maybe v was used in a clause for propagation.
+                    m_occs.insert(v);
                 }
             }
         }
-        clause_vector const& lemmas = ctx.get_lemmas();
-        for (unsigned i = 0; i < lemmas.size(); ++i) {
-            clause* cl = lemmas[i];
+
+#if 0        
+        for (clause* cl : ctx.get_lemmas()) {
             if (!cl->deleted()) {
                 for (literal lit : *cl) {
                     if (m_occs.contains(lit.var())) {
@@ -1365,9 +1365,6 @@ namespace smt {
             }
         }
 
-        //std::cout << "zs: " << z << " nzs: " << nz << " lemmas: " << ctx.get_lemmas().size() << " trail: " << m_card_trail.size() << "\n";
-        return z*10 >= nz;
-
         m_occs.reset();
         for (unsigned i = 0; i < lemmas.size(); ++i) {
             clause* cl = lemmas[i];
@@ -1377,6 +1374,8 @@ namespace smt {
                 m_occs.insert(idx);
             }
         }
+#endif
+        return z*10 >= nz;
     }