mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

#5336

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-06-08 19:48:05 -07:00
parent fb6cd8e132
commit 08b4c4ea14
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/sat/smt/arith_solver.cpp
View file

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