diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp
index d36d7b96b..0925daf32 100644
--- a/src/nlsat/nlsat_solver.cpp
+++ b/src/nlsat/nlsat_solver.cpp
@@ -1546,9 +1546,8 @@ namespace nlsat {
             lbool r = l_undef;
             while (true) {
                 r = search();
-                if (r != l_true) break;     
-                vector<rational> lows;
-                vector<var>      vars;
+                if (r != l_true) break; 
+                vector<std::pair<var, rational>> bounds;                
 
                 for (var x = 0; x < num_vars(); x++) {
                     if (m_is_int[x] && m_assignment.is_assigned(x) && !m_am.is_int(m_assignment.value(x))) {
@@ -1556,24 +1555,24 @@ namespace nlsat {
                         v = m_assignment.value(x);
                         rational lo;
                         m_am.int_lt(v, vlo);
-                        if (!m_am.is_int(vlo)) continue;
+                        if (!m_am.is_int(vlo)) 
+                            continue;
                         m_am.to_rational(vlo, lo);
                         // derive tight bounds.
                         while (true) {
                             lo++;
                             if (!m_am.gt(v, lo.to_mpq())) { lo--; break; }
                         }
-                        lows.push_back(lo);
-                        vars.push_back(x);
+                        bounds.push_back(std::make_pair(x, lo));
                     }
                 }
-                if (lows.empty()) break;
+                if (bounds.empty()) break;
 
                 init_search();                
-                for (unsigned i = 0; i < lows.size(); ++i) {
-                    rational lo = lows[i];
-                    rational hi = lo + rational::one();
-                    var x = vars[i];
+                for (auto const& b : bounds) {
+                    var x = b.first;
+                    rational lo = b.second;
+                    rational hi = lo + 1; // rational::one();
                     bool is_even = false;                        
                     polynomial_ref p(m_pm);
                     rational one(1);
diff --git a/src/shell/dimacs_frontend.cpp b/src/shell/dimacs_frontend.cpp
index 9b0a235c6..25e8aa0bc 100644
--- a/src/shell/dimacs_frontend.cpp
+++ b/src/shell/dimacs_frontend.cpp
@@ -225,6 +225,7 @@ unsigned read_dimacs(char const * file_name) {
     params_ref p = gparams::get_module("sat");
     params_ref par = gparams::get_module("parallel");
     p.set_bool("produce_models", true);
+    p.set_bool("cardinality.solver", false);
     sat_params sp(p);
     reslimit limit;
     sat::solver solver(p, limit);
@@ -248,7 +249,7 @@ unsigned read_dimacs(char const * file_name) {
     params_ref p2;
     p2.copy(p);
     p2.set_sym("drat.file", symbol::null);
-    
+
     sat::solver solver2(p2, limit);
     if (p.get_bool("dimacs.core", false)) {
         g_solver = &solver2;        
diff --git a/src/smt/diff_logic.h b/src/smt/diff_logic.h
index 167e1f2a9..fe788a454 100644
--- a/src/smt/diff_logic.h
+++ b/src/smt/diff_logic.h
@@ -511,6 +511,7 @@ public:
     // Return false if the resultant graph has a negative cycle. The negative
     // cycle can be extracted using traverse_neg_cycle.
     // The method assumes the graph is feasible before the invocation.
+
     bool enable_edge(edge_id id) {
         edge& e = m_edges[id];
         SASSERT(is_feasible_dbg());