search

SymbolicPathFinder / jpf-symbc

Symbolic PathFinder
https://github.com/SymbolicPathFinder/jpf-symbc
124 stars 89 forks source link

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

Open y553546436 opened 3 years ago

y553546436 commented 3 years ago

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.