diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 5f5b03e09..1d49c4386 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1569,7 +1569,6 @@ public:
             VERIFY(a.is_idiv(n, p, q));
             theory_var v  = mk_var(n);
             theory_var v1 = mk_var(p);
-            theory_var v2 = mk_var(q);
             rational r1 = get_value(v1);
             rational r2;
 
diff --git a/src/smt/watch_list.cpp b/src/smt/watch_list.cpp
index 9835142f6..778e93021 100644
--- a/src/smt/watch_list.cpp
+++ b/src/smt/watch_list.cpp
@@ -36,10 +36,10 @@ namespace smt {
     
     void watch_list::expand() {
         if (m_data == nullptr) {
-        unsigned size       = DEFAULT_WATCH_LIST_SIZE + HEADER_SIZE;
+            unsigned size       = DEFAULT_WATCH_LIST_SIZE + HEADER_SIZE;
             unsigned * mem      = reinterpret_cast<unsigned*>(alloc_svect(char, size));
 #ifdef _AMD64_
-        ++mem;  // make sure data is aligned in 64 bit machines
+            ++mem;  // make sure data is aligned in 64 bit machines
 #endif
             *mem                = 0;
             ++mem;
@@ -62,9 +62,9 @@ namespace smt {
             unsigned * mem          = reinterpret_cast<unsigned*>(alloc_svect(char, new_capacity + HEADER_SIZE));
             unsigned curr_end_cls   = end_cls_core();
 #ifdef _AMD64_
-        ++mem;  // make sure data is aligned in 64 bit machines
+            ++mem;  // make sure data is aligned in 64 bit machines
 #endif
-        *mem                    = curr_end_cls;
+            *mem                    = curr_end_cls;
             ++mem;
             SASSERT(bin_bytes <= new_capacity);
             unsigned new_begin_bin  = new_capacity - bin_bytes;