Output: [|-init+1>=0; init>=0|]