From 6455de9dd32b0bb75e86383cda0d8f172cb6ef7d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 21 Mar 2024 09:39:13 -0700 Subject: [PATCH] fix #7179 Ensure that flat associative rewriting is disabled if rewriter.flat is set to false. --- src/ast/rewriter/th_rewriter.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index ee8b79be5..844c51940 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -17,6 +17,7 @@ Notes: --*/ #include "params/rewriter_params.hpp" +#include "params/poly_rewriter_params.hpp" #include "ast/rewriter/th_rewriter.h" #include "ast/rewriter/bool_rewriter.h" #include "ast/rewriter/arith_rewriter.h" @@ -83,7 +84,8 @@ struct th_rewriter_cfg : public default_rewriter_cfg { void updt_local_params(params_ref const & _p) { rewriter_params p(_p); - m_flat = true; + poly_rewriter_params pp(_p); + m_flat = pp.flat(); m_max_memory = megabytes_to_bytes(p.max_memory()); m_max_steps = p.max_steps(); m_pull_cheap_ite = p.pull_cheap_ite();