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)
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: https://github.com/SymbolicPathFinder/jpf-symbc/pull/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 ... : https://github.com/itnef/jpf-symbc/compare/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)