diff options
Diffstat (limited to 'src/Compilers/Z/Bounds/Pipeline/Definition.v')
| -rw-r--r-- | src/Compilers/Z/Bounds/Pipeline/Definition.v | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/Compilers/Z/Bounds/Pipeline/Definition.v b/src/Compilers/Z/Bounds/Pipeline/Definition.v index 8a43a0ec7..b0ec96dbb 100644 --- a/src/Compilers/Z/Bounds/Pipeline/Definition.v +++ b/src/Compilers/Z/Bounds/Pipeline/Definition.v @@ -89,12 +89,13 @@ Definition PostWfPipeline := Build_ProcessedReflectivePackage_from_option_sigma 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 := InlineConst (SimplifyArith e) in + let e := InlineConst (SimplifyArith e) in + let e := InlineConst (SimplifyArith e) in let e := if opts.(anf) then ANormal e else e in let e := InlineConst e in let e := RewriteAdc e in + let e := InlineConst (SimplifyArith e) in (*let e := CSE false e in*) let e := MapCast _ e input_bounds in option_map |