diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index e8f6ec6fa6f..52e017b6c3c 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -1492,10 +1492,8 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
     unsigned rlimit  = m_params.rlimit();
     scoped_watch sw(*this);
     lbool r;
-    bool was_opt = false;
 
     if (m_opt && !m_opt->empty()) {
-        was_opt = true;
         m_check_sat_result = get_opt();
         cancel_eh<reslimit> eh(m().limit());
         scoped_ctrl_c ctrlc(eh);
diff --git a/src/math/lp/lp_bound_propagator.h b/src/math/lp/lp_bound_propagator.h
index b3d58e5aee2..9fa8d0d623c 100644
--- a/src/math/lp/lp_bound_propagator.h
+++ b/src/math/lp/lp_bound_propagator.h
@@ -454,12 +454,12 @@ class lp_bound_propagator {
     
     void cheap_eq_table(unsigned rid) {
         TRACE("cheap_eqs", tout << "checking if row " << rid << " can propagate equality.\n";  print_row(tout, rid););
-        unsigned x, y;
+        unsigned x = 0, y = 0;
         mpq k;
         if (is_offset_row(rid, x, y, k)) {
             if (y == null_lpvar) {
                 // x is an implied fixed var at k.
-                unsigned x2;
+                unsigned x2 = null_lpvar;
                 if (lp().find_in_fixed_tables(k, is_int(x), x2) &&
                     !is_equal(x, x2)) {
                     SASSERT(is_int(x) == is_int(x2) && lp().column_is_fixed(x2) &&
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index fcc1550bbd2..e5451b6615a 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -391,21 +391,21 @@ class theory_lra::imp {
             TRACE("arith", tout << "Unhandled: " << mk_pp(n, m) << "\n";);
             m_underspecified.push_back(to_app(n));
         }
-        expr* e = nullptr;
-        if (a.is_div(n)) {                
-            e = a.mk_div0(to_app(n)->get_arg(0), to_app(n)->get_arg(1));
+        expr* e = nullptr, *x = nullptr, *y = nullptr;
+        if (a.is_div(n, x, y)) {                
+            e = a.mk_div0(x, y);
         }
-        else if (a.is_idiv(n)) {                
-            e = a.mk_idiv0(to_app(n)->get_arg(0), to_app(n)->get_arg(1));
+        else if (a.is_idiv(n, x, y)) {                
+            e = a.mk_idiv0(x, y);
         }
-        else if (a.is_rem(n)) {                
-            e = a.mk_rem0(to_app(n)->get_arg(0), to_app(n)->get_arg(1));
+        else if (a.is_rem(n, x, y)) {                
+            e = a.mk_rem0(x, y);
         }
-        else if (a.is_mod(n)) {                
-            e = a.mk_mod0(to_app(n)->get_arg(0), to_app(n)->get_arg(1));
+        else if (a.is_mod(n, x, y)) {                
+            e = a.mk_mod0(x, y);
         }
-        else if (a.is_power(n)) {                
-            e = a.mk_power0(to_app(n)->get_arg(0), to_app(n)->get_arg(1));
+        else if (a.is_power(n, x, y)) {                
+            e = a.mk_power0(x, y);
         }
         if (e) {
             literal lit = th.mk_eq(e, n, false);