diff --git a/src/library/blast/simplifier.cpp b/src/library/blast/simplifier.cpp index 0ae138bb6..e00345a66 100644 --- a/src/library/blast/simplifier.cpp +++ b/src/library/blast/simplifier.cpp @@ -958,9 +958,14 @@ result simplifier::fuse(expr const & e) { buffer locals; variables.clear(); for (auto v_ns : variable_to_numerals) { - expr local = m_tmp_tctx->mk_tmp_local(T); - locals.push_back(local); - variables.push_back(v_ns.first); + expr local; + if (!is_one(v_ns.first)) { + local = m_tmp_tctx->mk_tmp_local(T); + locals.push_back(local); + variables.push_back(v_ns.first); + } else { + local = v_ns.first; + } expr term = zero; expr term_ls = zero; diff --git a/tests/lean/simplifier18.lean b/tests/lean/simplifier18.lean index 412d639e1..41ba4bc21 100644 --- a/tests/lean/simplifier18.lean +++ b/tests/lean/simplifier18.lean @@ -17,7 +17,11 @@ set_option simplify.fuse true #simplify eq simplifier.som 0 2 * x2 - 8 * x2 * 4 * x1 #simplify eq simplifier.som 0 x2 * x1 + 3 * x1 + (2 * x2 - 8 * x2 * 4 * x1) + x1 * x2 #simplify eq simplifier.som 0 (x1 * x3 + x1 * 2 + x2 * 3 * x3 + x1 * x2) - 2* x2 * x1 + 1 * x2 * x1 - 3 * x1 * x3 -#simplify eq simplifier.som 0 200 * x2 * 200 -#simplify eq simplifier.som 0 x1 * 200 * x2 * 200 -#simplify eq simplifier.som 0 x1 * 200 * x2 * x3 * 200 -#simplify eq simplifier.som 0 x1 * 200 * x2 * x3 * x4 * 200 +#simplify eq simplifier.som 0 2 * 2 + x1 +#simplify eq simplifier.som 0 x2 * (2 * 2) + x1 +#simplify eq simplifier.som 0 2 * 2 * x2 + x1 +#simplify eq simplifier.som 0 2 * x2 * 2 + x1 +#simplify eq simplifier.som 0 200 * x2 * 200 + x1 +#simplify eq simplifier.som 0 x1 * 200 * x2 * 200 + x1 +#simplify eq simplifier.som 0 x1 * 200 * x2 * x3 * 200 + x1 +#simplify eq simplifier.som 0 x1 * 200 * x2 * x3 * x4 * 200 + x1 diff --git a/tests/lean/simplifier18.lean.expected.out b/tests/lean/simplifier18.lean.expected.out index 11b1f3bb9..9e8c65982 100644 --- a/tests/lean/simplifier18.lean.expected.out +++ b/tests/lean/simplifier18.lean.expected.out @@ -6,3 +6,11 @@ x2 * 2 + -(x2 * x1 * 32) x2 * 2 + -(x2 * x1 * 32) x2 * 2 + (x1 * 3 + -(x2 * x1 * 30)) x1 * 2 + (-(x3 * x1 * 2) + x3 * x2 * 3) +x1 + 4 +x1 + x2 * 4 +x1 + x2 * 4 +x1 + x2 * 4 +x1 + x2 * 40000 +x1 + x2 * x1 * 40000 +x1 + x3 * (x2 * x1) * 40000 +x1 + x4 * (x3 * (x2 * x1)) * 40000