aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
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