z3 floating point arithmetic support doesn't seem to work

[itnef]

The combination
+symbolic.dp=z3 (with the provided version or any other version of z3)
+symbolic.fp=true
doesn't work.

See minimal non-working example (eclipse project) under https://github.com/itnef/symbc_z3_fp_mnwe

The simple verification task fails (stack trace (1) below).

When I try and fix this error (pull request: #34), it fails for another reason - the SMT problem is set up all right, but when trying to read back the result the method ProblemZ3.getRealValue fails to parse a floating point number. I have tried to fix this too, and it works, however I am aware that my "fix" is just a workaround and the question is where the floating point "E" is lost in the first place ... : itnef/jpf-symbc@z3-fp-fix_lt_gt...itnef:z3-fp-pseudofix2

stack trace (1)

d1_2_SYMREAL > CONST_21000.0
java.lang.ClassCastException: com.microsoft.z3.FPExpr cannot be cast to com.microsoft.z3.ArithExpr
at gov.nasa.jpf.symbc.numeric.solvers.ProblemZ3.lt(ProblemZ3.java:357)
at gov.nasa.jpf.symbc.numeric.PCParser.createDPRealConstraint(PCParser.java:450)
at gov.nasa.jpf.symbc.numeric.PCParser.addConstraint(PCParser.java:1105)
at gov.nasa.jpf.symbc.numeric.PCParser.parse(PCParser.java:1091)
at gov.nasa.jpf.symbc.numeric.SymbolicConstraintsGeneral.isSatisfiable(SymbolicConstraintsGeneral.java:128)
at gov.nasa.jpf.symbc.numeric.PathCondition.simplifyOld(PathCondition.java:393)
at gov.nasa.jpf.symbc.numeric.PathCondition.simplify(PathCondition.java:340)
at gov.nasa.jpf.symbc.bytecode.optimization.util.IFInstrSymbHelper.getNextInstructionAndSetPCChoiceDouble(IFInstrSymbHelper.java:367)
at gov.nasa.jpf.symbc.bytecode.optimization.DCMPL.execute(DCMPL.java:43)
at gov.nasa.jpf.vm.ThreadInfo.executeInstruction(ThreadInfo.java:1908)
at gov.nasa.jpf.vm.ThreadInfo.executeTransition(ThreadInfo.java:1859)
at gov.nasa.jpf.vm.SystemState.executeNextTransition(SystemState.java:765)
at gov.nasa.jpf.vm.VM.forward(VM.java:1722)
[...]

stack trace (2)

java.lang.NumberFormatException: For input string: "1.000000000000000444089209850062616169452667236328125-1019"
at sun.misc.FloatingDecimal.readJavaFormatString(FloatingDecimal.java:2043)
at sun.misc.FloatingDecimal.parseDouble(FloatingDecimal.java:110)
at java.lang.Double.parseDouble(Double.java:538)
at gov.nasa.jpf.symbc.numeric.solvers.ProblemZ3.getRealValue(ProblemZ3.java:1093)
at gov.nasa.jpf.symbc.numeric.SymbolicConstraintsGeneral.solve(SymbolicConstraintsGeneral.java:235)