Running example class TestZ3 only gets one "div by 0" error message

[y553546436]

When running src/examples/TestZ3.jpf, I got one error message:

java.lang.ArithmeticException: div by 0
	at TestZ3.testMod(TestZ3.java:195)
	at TestZ3.main(TestZ3.java:209)

which is because in the testMod method, the concrete value carried by the symbolic argument y is 0.