diff --git a/src/api/julia/z3jl.cpp b/src/api/julia/z3jl.cpp
index dc18e37b6..d0ad1b152 100644
--- a/src/api/julia/z3jl.cpp
+++ b/src/api/julia/z3jl.cpp
@@ -216,7 +216,7 @@ JLCXX_MODULE define_julia_module(jlcxx::Module &m)
         .MM(expr, is_string_value)
         .MM(expr, get_escaped_string)
         .MM(expr, get_string)
-        .MM(expr, fpa_rounding_mode)
+        .MM(expr, fpa_rounding_mode_sort)
         .MM(expr, decl)
         .MM(expr, num_args)
         .MM(expr, arg)
diff --git a/src/sat/smt/bv_internalize.cpp b/src/sat/smt/bv_internalize.cpp
index f06d2d0df..8e6867dc7 100644
--- a/src/sat/smt/bv_internalize.cpp
+++ b/src/sat/smt/bv_internalize.cpp
@@ -563,7 +563,6 @@ namespace bv {
         SASSERT(e->get_num_args() >= 1);
         expr_ref_vector bits(m), new_bits(m), arg_bits(m);
         
-        unsigned i = e->get_num_args() - 1;
         get_arg_bits(e, 0, bits);
         for (unsigned i = 1; i < e->get_num_args(); ++i) {
             arg_bits.reset();
diff --git a/src/sat/smt/bv_solver.cpp b/src/sat/smt/bv_solver.cpp
index 0c57508ef..2762a1244 100644
--- a/src/sat/smt/bv_solver.cpp
+++ b/src/sat/smt/bv_solver.cpp
@@ -355,8 +355,6 @@ namespace bv {
             ctx.drat_eq_def(leq, eq);
         }
 
-        static unsigned s_count = 0;
-
         sat::literal_vector lits;
         switch (c.m_kind) {
         case bv_justification::kind_t::eq2bit:
diff --git a/src/tactic/core/symmetry_reduce_tactic.cpp b/src/tactic/core/symmetry_reduce_tactic.cpp
index 9823be26d..17049e2d1 100644
--- a/src/tactic/core/symmetry_reduce_tactic.cpp
+++ b/src/tactic/core/symmetry_reduce_tactic.cpp
@@ -338,10 +338,8 @@ private:
         app_parents const& get_parents() { return m_use_funs; }
 
         void operator()(app* n) {
-            func_decl* f;
-            unsigned sz = n->get_num_args();
-            for (unsigned i = 0; i < sz; ++i) {
-                expr* e = n->get_arg(i);
+            func_decl* f = n->get_decl();
+            for (expr* e : *n) {
                 if (is_app(e)) {
                     auto& value = m_use_funs.insert_if_not_there(to_app(e), 0);
                     if (!value) value = alloc(fun_set);