mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 19:52:29 +00:00
Code Activity

fix #7179

Browse source 
Ensure that flat associative rewriting is disabled if rewriter.flat is set to false.
This commit is contained in:
Nikolaj Bjorner 2024-03-21 09:39:13 -07:00
parent 530c6fc625
commit 6455de9dd3
1 changed files with 3 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

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