diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index 5b0df8147..c69534b08 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -78,7 +78,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg { void updt_local_params(params_ref const & _p) { rewriter_params p(_p); - m_flat = p.flat(); + m_flat = true; m_max_memory = megabytes_to_bytes(p.max_memory()); m_max_steps = p.max_steps(); m_pull_cheap_ite = p.pull_cheap_ite(); diff --git a/src/params/rewriter_params.pyg b/src/params/rewriter_params.pyg index 18bb29e56..290f7b1da 100644 --- a/src/params/rewriter_params.pyg +++ b/src/params/rewriter_params.pyg @@ -3,7 +3,6 @@ def_module_params('rewriter', export=True, params=(max_memory_param(), max_steps_param(), - ("flat", BOOL, True, "create nary applications for and,or,+,*,bvadd,bvmul,bvand,bvor,bvxor"), ("push_ite_arith", BOOL, False, "push if-then-else over arithmetic terms."), ("push_ite_bv", BOOL, False, "push if-then-else over bit-vector terms."), ("pull_cheap_ite", BOOL, False, "pull if-then-else terms when cheap."),