From 9f7dc493a95d7273109a3dfb4c7148c8723c03b9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Tue, 20 Nov 2012 23:14:02 +0000
Subject: [PATCH] spot a bug in simplifyArithmetic, add a test
---
src/main/scala/leon/purescala/TreeOps.scala | 1 -
src/test/scala/leon/test/purescala/TreeOpsTests.scala | 3 +++
2 files changed, 3 insertions(+), 1 deletion(-)
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index 08f4c0f06..f2158675f 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -1393,7 +1393,6 @@ object TreeOps {
case Times(IntLiteral(i), UMinus(e)) => Times(IntLiteral(-i), e)
case Times(UMinus(e), IntLiteral(i)) => Times(e, IntLiteral(-i))
case Times(IntLiteral(i1), Division(e, IntLiteral(i2))) if i2 != 0 && i1 % i2 == 0 => Times(IntLiteral(i1/i2), e)
- case Times(IntLiteral(i1), Plus(Division(e1, IntLiteral(i2)), e2)) if i2 != 0 && i1 % i2 == 0 => Times(IntLiteral(i1/i2), Plus(e1, e2))
case Division(IntLiteral(i1), IntLiteral(i2)) if i2 != 0 => IntLiteral(i1 / i2)
case Division(e, IntLiteral(1)) => e
diff --git a/src/test/scala/leon/test/purescala/TreeOpsTests.scala b/src/test/scala/leon/test/purescala/TreeOpsTests.scala
index 87ae844ec..763550e44 100644
--- a/src/test/scala/leon/test/purescala/TreeOpsTests.scala
+++ b/src/test/scala/leon/test/purescala/TreeOpsTests.scala
@@ -61,6 +61,9 @@ class TreeOpsTests extends FunSuite {
checkSameExpr(e4, simplify(e4), Set(xId))
val e5 = Plus(x, Minus(x, IntLiteral(2)))
checkSameExpr(e5, simplify(e5), Set(xId))
+
+ val e6 = Times(IntLiteral(9), Plus(Division(x, IntLiteral(3)), Division(x, IntLiteral(6))))
+ checkSameExpr(e6, simplify(e6), Set(xId))
}
--
GitLab