diff --git a/src/sat/sat_local_search.cpp b/src/sat/sat_local_search.cpp
index 1117a9c68..0cf509693 100644
--- a/src/sat/sat_local_search.cpp
+++ b/src/sat/sat_local_search.cpp
@@ -340,7 +340,8 @@ namespace sat {
                 m_vars[flipvar].m_time_stamp = step;
                 //if (!m_limit.inc()) break;pick_flip();
             }
-            IF_VERBOSE(1, if (tries % 10 == 0) verbose_stream() << tries << ": " << timer.get_seconds() << '\n';);
+            IF_VERBOSE(1, if (tries % 10 == 0) verbose_stream() << "(sat-local :tries " << tries << " :steps " << (tries - 1) * max_steps + step 
+                                                                << " :unsat " << m_unsat_stack.size() << " :time " << timer.get_seconds() << ")\n";);
             // the following is for tesing
 
             // tell the SAT solvers about the phase of variables.
@@ -351,7 +352,6 @@ namespace sat {
         // remove unit clauses from assumptions.
         m_constraints.shrink(num_constraints);
         //print_solution();
-        IF_VERBOSE(1, verbose_stream() << timer.get_seconds() <<  " steps: " << (tries - 1) * max_steps + step << " unsat stack: " << m_unsat_stack.size() << '\n';);
         if (m_unsat_stack.empty() && ob_constraint.empty()) { // or all variables in ob_constraint are true
             verify_solution();
             extract_model();
diff --git a/src/shell/opt_frontend.cpp b/src/shell/opt_frontend.cpp
index c15680f72..9c9bc54ab 100644
--- a/src/shell/opt_frontend.cpp
+++ b/src/shell/opt_frontend.cpp
@@ -254,6 +254,11 @@ class opb {
                 in.parse_token(";");
                 break;
             }            
+            if (in.parse_token("<=")) {
+                t = arith.mk_le(t, parse_coeff());
+                in.parse_token(";");
+                break;
+            }            
             t = arith.mk_add(t, parse_term());
         }        
         opt.add_hard_constraint(t);