diff --git a/scripts/mk_project.py b/scripts/mk_project.py
index b947885ba69..8b2d467f95c 100644
--- a/scripts/mk_project.py
+++ b/scripts/mk_project.py
@@ -84,7 +84,7 @@ def init_project_def():
     API_files = ['z3_api.h', 'z3_ast_containers.h', 'z3_algebraic.h', 'z3_polynomial.h', 'z3_rcf.h', 'z3_fixedpoint.h', 'z3_optimization.h', 'z3_fpa.h', 'z3_spacer.h']
     add_lib('api', ['portfolio',  'realclosure', 'opt'],
             includes2install=['z3.h', 'z3_v1.h', 'z3_macros.h'] + API_files)
-    add_lib('extra_cmds', ['cmd_context', 'subpaving_tactic', 'qe', 'arith_tactics'], 'cmd_context/extra_cmds')
+    add_lib('extra_cmds', ['cmd_context', 'subpaving_tactic', 'qe', 'euf', 'arith_tactics'], 'cmd_context/extra_cmds')
     add_exe('shell', ['api', 'sat', 'extra_cmds', 'opt'], exe_name='z3')
     add_exe('test', ['api', 'fuzzing', 'simplex', 'sat_smt'], exe_name='test-z3', install=False)
     _libz3Component = add_dll('api_dll', ['api', 'sat', 'extra_cmds'], 'api/dll',
diff --git a/src/ast/ast_pp_util.h b/src/ast/ast_pp_util.h
index 16387004f48..9cec622679c 100644
--- a/src/ast/ast_pp_util.h
+++ b/src/ast/ast_pp_util.h
@@ -38,7 +38,7 @@ class ast_pp_util {
 
     decl_collector      coll;
     
-    ast_pp_util(ast_manager& m): m(m), m_env(m), m_rec_decls(0), m_decls(0), m_sorts(0), coll(m), m_defined(m) {}
+    ast_pp_util(ast_manager& m): m(m), m_env(m), m_rec_decls(0), m_decls(0), m_sorts(0), m_defined(m), coll(m) {}
 
     void reset() { coll.reset(); m_removed.reset(); m_sorts.clear(0u); m_decls.clear(0u); m_rec_decls.clear(0u); 
         m_is_defined.reset(); m_defined.reset(); m_defined_lim.reset(); }
diff --git a/src/sat/smt/arith_diagnostics.cpp b/src/sat/smt/arith_diagnostics.cpp
index bfeeaff4da0..d702806d0bf 100644
--- a/src/sat/smt/arith_diagnostics.cpp
+++ b/src/sat/smt/arith_diagnostics.cpp
@@ -162,14 +162,14 @@ namespace arith {
             args.push_back(s.literal2expr(lit));
         }
         for (unsigned i = m_eq_head; i < m_eq_tail; ++i) {
-            auto const& [a, b, is_eq] = a.m_arith_hint.eq(i);            
-            expr_ref eq(m.mk_eq(a->get_expr(), b->get_expr()), m);
+            auto const& [x, y, is_eq] = a.m_arith_hint.eq(i);            
+            expr_ref eq(m.mk_eq(x->get_expr(), y->get_expr()), m);
             if (!is_eq) eq = m.mk_not(eq);
             args.push_back(arith.mk_int(lc));
             args.push_back(eq);
         }
-        for (expr* a : args)
-            sorts.push_back(a->get_sort());
+        for (expr* arg : args)
+            sorts.push_back(arg->get_sort());
         sort* range = m.mk_proof_sort();
         func_decl* d = m.mk_func_decl(symbol(name), args.size(), sorts.data(), range);
         expr* r = m.mk_app(d, args);