From 08b4c4ea1403e82dfa56e02af218b58547727dc0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 8 Jun 2021 19:48:05 -0700 Subject: [PATCH] #5336 --- src/sat/smt/arith_solver.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) 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);