*** 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