aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-05-20 01:28:33 -0400
committerGravatar Jason Gross <jasongross9@gmail.com>2017-05-20 10:58:45 -0400
commitbdf568b0ef007f0ea814e3ed7844c07c2831f900 (patch)
tree27d18a9ddb17a742be2ef5d1624bf5a9560a8084 /src
parent792dba0826c865dcc8e8de9e3765c5f4160d925c (diff)
Fix extra opp in freeze
No idea why it's valid both ways, but apparently it is.
Diffstat (limited to 'src')
-rw-r--r--src/Compilers/Z/Bounds/Pipeline/Definition.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/Compilers/Z/Bounds/Pipeline/Definition.v b/src/Compilers/Z/Bounds/Pipeline/Definition.v
index 5aadc8dfd..5408c944c 100644
--- a/src/Compilers/Z/Bounds/Pipeline/Definition.v
+++ b/src/Compilers/Z/Bounds/Pipeline/Definition.v
@@ -95,6 +95,7 @@ Definition PostWfPipeline
let e := if opts.(anf) then InlineConst (ANormal e) else e in
let e := RewriteAdc e in
let e := InlineConstAndOpp (Linearize (SimplifyArith true e)) in
+ let e := if opts.(anf) then InlineConstAndOpp (ANormal e) else e in
let e := InlineConstAndOpp (Linearize (SimplifyArith true e)) in
(*let e := CSE false e in*)
let e := MapCast _ e input_bounds in