mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 21:03:39 +00:00
Code Activity

formatting updates

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-04-12 14:28:08 -07:00
parent f61168cd53
commit 444238bc53
2 changed files with 3 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/rewriter/maximize_ac_sharing.cpp
View file

@ -92,7 +92,7 @@ br_status maximize_ac_sharing::reduce_app(func_decl * f, unsigned num_args, expr
else { else {
result = m.mk_app(f, numeral, _args[0]); result = m.mk_app(f, numeral, _args[0]);
} }
TRACE("ac_sharing_detail", tout << "result: " << mk_pp(result, m) << "\n";); TRACE("ac_sharing_detail", tout << "result: " << result << "\n";);
return BR_DONE; return BR_DONE;
} }
} }

3
src/model/value_factory.h
View file

@ -194,9 +194,8 @@ public:
while (!is_new) { while (!is_new) {
result = mk_value(next, s, is_new); result = mk_value(next, s, is_new);
next++; next++;
if (has_max && next > max_size + start) { if (has_max && next > max_size + start)
return nullptr; return nullptr;
}
} }
SASSERT(result != 0); SASSERT(result != 0);
return result; return result;