build

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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)

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();

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:

src/tactic/core/symmetry_reduce_tactic.cpp

@@ -338,10 +338,8 @@ class symmetry_reduce_tactic::imp {
         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);