mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 09:34:08 +00:00
Code Activity

throttle squash-store #7134

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-02-21 10:00:11 -08:00
parent a3d00ce356
commit 79b7d8a9e2
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/ast/rewriter/array_rewriter.cpp
View file

@ -206,7 +206,9 @@ br_status array_rewriter::mk_store_core(unsigned num_args, expr * const * args,
bool array_rewriter::squash_store(unsigned n, expr* const* args, expr_ref& result) { bool array_rewriter::squash_store(unsigned n, expr* const* args, expr_ref& result) {
ptr_buffer<expr> parents, sargs; ptr_buffer<expr> parents, sargs;
expr* a = args[0]; expr* a = args[0];
while (m_util.is_store(a)) { unsigned rounds = 0;
while (m_util.is_store(a) && rounds < 10) {
++rounds;
lbool r = compare_args(n - 2, args + 1, to_app(a)->get_args() + 1); lbool r = compare_args(n - 2, args + 1, to_app(a)->get_args() + 1);
switch (r) { switch (r) {
case l_undef: case l_undef: