From d8e62cac94cb36d12fc4c7d1ec3d197f089f1858 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 1 Oct 2014 14:51:14 -0700 Subject: [PATCH] enable flattening even if som is set by default Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/poly_rewriter_def.h | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/ast/rewriter/poly_rewriter_def.h b/src/ast/rewriter/poly_rewriter_def.h index 036221f96..12da0069d 100644 --- a/src/ast/rewriter/poly_rewriter_def.h +++ b/src/ast/rewriter/poly_rewriter_def.h @@ -34,6 +34,8 @@ void poly_rewriter::updt_params(params_ref const & _p) { m_hoist_mul = p.hoist_mul(); m_hoist_cmul = p.hoist_cmul(); m_som_blowup = p.som_blowup(); + if (!m_flat) m_som = false; + if (m_som) m_hoist_mul = false; } template