search

SymbolicPathFinder / jpf-symbc

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

mixed constraint #44

Open dah-fari7009 opened 4 years ago

dah-fari7009 commented 4 years ago

Hello,

Sometimes when doing operations with both integer and double, I get this exxception: java.lang.RuntimeException: ## Error Z3

    at gov.nasa.jpf.symbc.numeric.solvers.ProblemZ3.mixed(ProblemZ3.java:1062)
    at gov.nasa.jpf.symbc.numeric.PCParser.createDPMixedConstraint(PCParser.java:370)
    at gov.nasa.jpf.symbc.numeric.PCParser.addConstraint(PCParser.java:1110)

Does this mean that z3 can not handle mixing integer and real numbers ? I remember seeing in the specification that it could. Am I understanding this correctly

dah-fari7009 commented 4 years ago

I obtained this result on this line of code int signC = 0; double xC = xC0 + signC*rC* (Math.cos(psiC)-Math.cos(psiC+dpsiC));

Is it specific to nonlinear arithmetic ?

affan commented 3 years ago

Any update on this? I am facing the same issue.

dah-fari7009 commented 3 years ago

@affan, the problem seemed to be indeed with Z3 and mixed nonlinear arithmetic, so I ended up switching to a different solver (coral)