diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp
index 308691c6e..b33e12038 100644
--- a/src/sat/smt/arith_solver.cpp
+++ b/src/sat/smt/arith_solver.cpp
@@ -619,11 +619,11 @@ namespace arith {
         }
         else if (a.is_arith_expr(o)) {
             expr_ref_vector args(m);
-            for (auto* arg : euf::enode_args(n)) {
-                if (m.is_value(arg->get_expr()))
-                    args.push_back(arg->get_expr());
+            for (auto* arg : *to_app(o)) {
+                if (m.is_value(arg))
+                    args.push_back(arg);
                 else 
-                    args.push_back(values.get(arg->get_root_id()));
+                    args.push_back(values.get(ctx.get_enode(arg)->get_root_id()));
             }
             value = m.mk_app(to_app(o)->get_decl(), args.size(), args.data());
             ctx.get_rewriter()(value);