mixed constraint

[dah-fari7009]

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]

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]

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

[dah-fari7009]

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