Z3 and floating points: check useFpForReals when translating gt and lt expressions

SymbolicPathFinder / jpf-symbc

Symbolic PathFinder

https://github.com/SymbolicPathFinder/jpf-symbc

130 stars 91 forks source link

Z3 and floating points: check useFpForReals when translating gt and lt expressions #34

Open itnef opened 5 years ago

itnef commented 5 years ago

If this isn't checked and handled, then +symbolic.dp=z3 +symbolic.fp=true fails on arithmetic comparisons with a typecast exception (java.lang.ClassCastException: com.microsoft.z3.FPExpr cannot be cast to com.microsoft.z3.ArithExpr)