i-4[0] = max(-inf, 0)
neg-i4[0] = max(-inf, 0)
neg-i1-pre = max(-inf, guard(add(min(neg-i4[0], inf), min(i-4[0], inf)), 0, neg-i4[0]), guard(add(min(neg-i2-pre, inf), min(i-2-pre, inf)), 0, neg-i2-pre))
i-1-pre = max(-inf, guard(add(min(neg-i4[0], inf), min(i-4[0], inf)), 0, i-4[0]), guard(add(min(neg-i2-pre, inf), min(i-2-pre, inf)), 0, i-2-pre))
neg-i3-pre = max(-inf, guard(add(min(neg-i1-pre, inf), min(i-1-pre, 2)), 0, neg-i1-pre))
i-3-pre = max(-inf, guard(add(min(neg-i1-pre, inf), min(i-1-pre, 2)), 0, min(2, i-1-pre)))
neg-i0-pre = max(-inf, guard(add(min(neg-i1-pre, -3), min(i-1-pre, inf)), 0, min(-3, neg-i1-pre)))
i-0-pre = max(-inf, guard(add(min(neg-i1-pre, -3), min(i-1-pre, inf)), 0, i-1-pre))
i-3[0] = max(-inf, add(0, i-3-pre))
neg-i3[0] = max(-inf, add(0, neg-i3-pre))
neg-i2-pre = max(-inf, guard(add(min(neg-i3[0], inf), min(i-3[0], inf)), 0, neg-i3[0]))
i-2-pre = max(-inf, guard(add(min(neg-i3[0], inf), min(i-3[0], inf)), 0, i-3[0]))
x = max(-inf, 0)
y = max(-inf, x, z)
z = max(-inf, y)