From a689c66b1e4c4988eb497a5ee8ef0aefe7c7c31d Mon Sep 17 00:00:00 2001
From: Daniel Selsam <daniel.selsam@gmail.com>
Date: Mon, 16 Nov 2015 20:25:08 -0800
Subject: [PATCH] fix(library/blast/simplifier): handle scalar in fusion

---
 src/library/blast/simplifier.cpp          | 11 ++++++++---
 tests/lean/simplifier18.lean              | 12 ++++++++----
 tests/lean/simplifier18.lean.expected.out |  8 ++++++++
 3 files changed, 24 insertions(+), 7 deletions(-)

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<expr> 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