1 files changed, 182 insertions, 0 deletions
diff --git a/Test/optimization/Optimization0.bpl.expect b/Test/optimization/Optimization0.bpl.expect
new file mode 100644
index 00000000..d2f9b606
--- /dev/null
+++ b/Test/optimization/Optimization0.bpl.expect
@@ -0,0 +1,182 @@
+*** MODEL
+%lbl%@280 -> false
+%lbl%+260 -> true
+%lbl%+39 -> true
+x@0 -> 43
+ControlFlow -> {
+  0 0 -> 260
+  0 260 -> 39
+  0 39 -> (- 280)
+  else -> 260
+}
+tickleBool -> {
+  true -> true
+  false -> true
+  else -> true
+}
+may_fail -> {
+  43 -> false
+  else -> false
+}
+*** END_MODEL
+Optimization0.bpl(13,5): Error BP5001: This assertion might not hold.
+Execution trace:
+    Optimization0.bpl(10,5): anon0
+*** MODEL
+%lbl%@328 -> false
+%lbl%+306 -> true
+%lbl%+66 -> true
+%lbl%+68 -> true
+x@0@@0 -> 24
+ControlFlow -> {
+  0 0 -> 306
+  0 306 -> 66
+  0 68 -> (- 328)
+  0 66 -> 68
+  else -> 306
+}
+tickleBool -> {
+  true -> true
+  false -> true
+  else -> true
+}
+may_fail -> {
+  24 -> false
+  else -> false
+}
+*** END_MODEL
+Optimization0.bpl(25,5): Error BP5001: This assertion might not hold.
+Execution trace:
+    Optimization0.bpl(20,7): anon0
+    Optimization0.bpl(21,5): anon3_Else
+    Optimization0.bpl(24,5): anon2
+*** MODEL
+%lbl%@360 -> false
+%lbl%+342 -> true
+%lbl%+95 -> true
+%lbl%+99 -> true
+x@0@@1 -> 10
+ControlFlow -> {
+  0 0 -> 342
+  0 342 -> 95
+  0 95 -> 99
+  0 99 -> (- 360)
+  else -> 342
+}
+tickleBool -> {
+  true -> true
+  false -> true
+  else -> true
+}
+*** END_MODEL
+Optimization0.bpl(37,5): Error BP5001: This assertion might not hold.
+Execution trace:
+    Optimization0.bpl(32,7): anon0
+    Optimization0.bpl(33,5): anon3_LoopHead
+    Optimization0.bpl(33,5): anon3_LoopDone
+*** MODEL
+%lbl%@393 -> false
+%lbl%+122 -> true
+%lbl%+382 -> true
+x@0@@2 -> 41
+ControlFlow -> {
+  0 0 -> 382
+  0 382 -> 122
+  0 122 -> (- 393)
+  else -> 382
+}
+tickleBool -> {
+  true -> true
+  false -> true
+  else -> true
+}
+may_fail -> {
+  41 -> false
+  else -> false
+}
+*** END_MODEL
+Optimization0.bpl(47,5): Error BP5001: This assertion might not hold.
+Execution trace:
+    Optimization0.bpl(44,5): anon0
+*** MODEL
+%lbl%@421 -> false
+%lbl%+147 -> true
+%lbl%+151 -> true
+%lbl%+399 -> true
+x@0@@3 -> 42
+ControlFlow -> {
+  0 0 -> 399
+  0 399 -> 147
+  0 147 -> 151
+  0 151 -> (- 421)
+  else -> 399
+}
+tickleBool -> {
+  true -> true
+  false -> true
+  else -> true
+}
+may_fail -> {
+  42 -> false
+  else -> false
+}
+*** END_MODEL
+Optimization0.bpl(59,5): Error BP5001: This assertion might not hold.
+Execution trace:
+    Optimization0.bpl(54,7): anon0
+    Optimization0.bpl(56,11): anon3_Then
+    Optimization0.bpl(58,5): anon2
+*** MODEL
+%lbl%@453 -> false
+%lbl%+178 -> true
+%lbl%+182 -> true
+%lbl%+435 -> true
+x@0@@4 -> 1
+ControlFlow -> {
+  0 0 -> 435
+  0 435 -> 178
+  0 178 -> 182
+  0 182 -> (- 453)
+  else -> 435
+}
+tickleBool -> {
+  true -> true
+  false -> true
+  else -> true
+}
+*** END_MODEL
+Optimization0.bpl(71,5): Error BP5001: This assertion might not hold.
+Execution trace:
+    Optimization0.bpl(66,7): anon0
+    Optimization0.bpl(67,5): anon3_LoopHead
+    Optimization0.bpl(67,5): anon3_LoopDone
+*** MODEL
+%lbl%@497 -> false
+%lbl%+209 -> true
+%lbl%+213 -> true
+%lbl%+475 -> true
+x@0@@5 -> 2
+ControlFlow -> {
+  0 0 -> 475
+  0 475 -> 209
+  0 209 -> 213
+  0 213 -> (- 497)
+  else -> 475
+}
+tickleBool -> {
+  true -> true
+  false -> true
+  else -> true
+}
+may_fail -> {
+  2 -> false
+  else -> false
+}
+*** END_MODEL
+Optimization0.bpl(83,5): Error BP5001: This assertion might not hold.
+Execution trace:
+    Optimization0.bpl(78,7): anon0
+    Optimization0.bpl(80,11): anon3_Then
+    Optimization0.bpl(82,5): anon2
+
+Boogie program verifier finished with 0 verified, 7 errors