aboutsummaryrefslogtreecommitdiff
path: root/src/Compilers/Z
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-06-17 19:36:49 -0400
committerGravatar Jason Gross <jgross@mit.edu>2017-06-17 19:36:49 -0400
commit6f18428f5336666761bc47af35c49930a22176e8 (patch)
treef989a2dbbe5d75a676b00e42978f994ef5c6832d /src/Compilers/Z
parenta6f5c03599500cca1b977fc51afffb28ef73395c (diff)
Add more simplification to pipeline
This seemes to be making it slower though....
Diffstat (limited to 'src/Compilers/Z')
-rw-r--r--src/Compilers/Z/Bounds/Pipeline/Definition.v3
1 files changed, 3 insertions, 0 deletions
diff --git a/src/Compilers/Z/Bounds/Pipeline/Definition.v b/src/Compilers/Z/Bounds/Pipeline/Definition.v
index 5a2982a57..fc31d959d 100644
--- a/src/Compilers/Z/Bounds/Pipeline/Definition.v
+++ b/src/Compilers/Z/Bounds/Pipeline/Definition.v
@@ -116,6 +116,9 @@ Definition PostWfBoundsPipeline
=> let e' := InlineConst e' in
let e' := InlineConst (Linearize (SimplifyArith false e')) in
let e' := InlineConst (Linearize (SimplifyArith false e')) in
+ let e' := InlineConst (Linearize (SimplifyArith false e')) in
+ let e' := InlineConst (Linearize (SimplifyArith false e')) in
+ let e' := InlineConst (Linearize (SimplifyArith false e')) in
let e' := if opts.(anf) then InlineConst (ANormal e') else e' in
let e' := ExprEta e' in
e'))