Extract the exit formula from Power.

simplify/simplify.ml

@@ -268,7 +268,7 @@ let simplify_power loops (f_body, f_exit, l, it) =
   | (FConst c1, FConst c2) when (not (is_symb it)) ->
      let it = int_of_symb it in
      FConst (Abstract_wcet.pow loops c1 c2 l it)
-  | _,_ -> FPower (f_body, f_exit, l, it)
+  | _,_ -> FPlus [f_exit; FPower (f_body, bot_f, l, it)]
 
 let rec simplify_product loops (k,f) =
   if k = 0 then

simplify/test/power.expect

 (l:1;{16,13}) loops: endl
 (l:1;{16,9}) loops: endl
-((l:1;{5,3,2}), (l:1;{4,1}), l:2)^p:1 loops: endl
-2.(((l:1;{5,3,2}), (l:1;{4,1}), l:2)^p:1) loops: endl
+((l:1;{4,1}) + ((l:1;{5,3,2}), (__top;{,0}), l:2)^p:1) loops: endl
+((l:1;{8,2}) + 2.(((l:1;{5,3,2}), (__top;{,0}), l:2)^p:1)) loops: endl