While the preconditions state that 0 < a, b, c the stub program has an assertion checking the values 0, 0, 0. You should consider changing the precondition to 0 <= a, b, c.