From 79b7d8a9e274ea7b18f09e35d7facb539ddce9cb Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 21 Feb 2024 10:00:11 -0800 Subject: [PATCH] throttle squash-store #7134 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/array_rewriter.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/ast/rewriter/array_rewriter.cpp b/src/ast/rewriter/array_rewriter.cpp index 228ba9914..bd67a940e 100644 --- a/src/ast/rewriter/array_rewriter.cpp +++ b/src/ast/rewriter/array_rewriter.cpp @@ -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) { ptr_buffer parents, sargs; 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); switch (r) { case l_undef: