aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-05-14 18:55:40 -0400
committerGravatar Jason Gross <jgross@mit.edu>2017-05-14 18:55:40 -0400
commit40d78e4b1a017cf68812a81633151e06a7af2178 (patch)
treee6153f80d2e3f6363bbe8e80ec77b9e2b6bac6e9 /src
parentb59f62e633da3ece4bff29823b6d19e79c3e3714 (diff)
Do more arithmetic simplifying
Needed to remove some multiplication by 0
Diffstat (limited to 'src')
-rw-r--r--src/Compilers/Z/Bounds/Pipeline/Definition.v2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/Compilers/Z/Bounds/Pipeline/Definition.v b/src/Compilers/Z/Bounds/Pipeline/Definition.v
index b9258e4f9..98f00aae8 100644
--- a/src/Compilers/Z/Bounds/Pipeline/Definition.v
+++ b/src/Compilers/Z/Bounds/Pipeline/Definition.v
@@ -81,6 +81,8 @@ Definition PostWfPipeline
e input_bounds
(let e := InlineConst e in
let e := SimplifyArith e in
+ let e := InlineConst e in
+ let e := SimplifyArith e in
let e := ANormal e in
let e := InlineConst e in
(*let e := CSE false e in*)