Additional Floating Point Support is Needed

[sohah]

Additional floating point support is needed, as evident by the programs below.

Source code of all methods can be found in here

To run use a configuration similar to the one below, assume that the program under test is located under examples/svcomp

target=svcomp.BellmanFord_FunUnsat01.Main

classpath=${jpf-symbc}/build/examples

symbolic.dp=z3bitvector
symbolic.min_int=-2147483648
symbolic.max_int=2147483647
symbolic.min_double=-10000.0
symbolic.max_double=10000.0
symbolic.bvlength=64
search.depth_limit=13
symbolic.strings=true
symbolic.string_dp=z3str3
symbolic.lazy=on
symbolic.jrarrays=true
listener = .symbc.SymbolicListener

symbolic.optimizechoices=true
symbolic.debug=true

float-nonlinear-calculation/Conflict.yml
float-nonlinear-calculation/EulerMethod.yml
float-nonlinear-calculation/MathSin.yml
float-nonlinear-calculation/Optimization2.yml
float-nonlinear-calculation/Optimization3.yml
float-nonlinear-calculation/Optimization4.yml
float-nonlinear-calculation/Optimization5.yml
float-nonlinear-calculation/Optimization6.yml
float-nonlinear-calculation/coral1.yml
float-nonlinear-calculation/coral10.yml
float-nonlinear-calculation/coral11.yml
float-nonlinear-calculation/coral12.yml
float-nonlinear-calculation/coral13.yml
float-nonlinear-calculation/coral14.yml
float-nonlinear-calculation/coral15.yml
float-nonlinear-calculation/coral16.yml
float-nonlinear-calculation/coral17.yml
float-nonlinear-calculation/coral18.yml
float-nonlinear-calculation/coral19.yml
float-nonlinear-calculation/coral2.yml
float-nonlinear-calculation/coral20.yml
float-nonlinear-calculation/coral21.yml
float-nonlinear-calculation/coral22.yml
float-nonlinear-calculation/coral23.yml
float-nonlinear-calculation/coral26.yml
float-nonlinear-calculation/coral27.yml
float-nonlinear-calculation/coral28.yml
float-nonlinear-calculation/coral29.yml
float-nonlinear-calculation/coral3.yml
float-nonlinear-calculation/coral30.yml
float-nonlinear-calculation/coral32.yml
float-nonlinear-calculation/coral33.yml
float-nonlinear-calculation/coral34.yml
float-nonlinear-calculation/coral35.yml
float-nonlinear-calculation/coral36.yml
float-nonlinear-calculation/coral38.yml
float-nonlinear-calculation/coral39.yml
float-nonlinear-calculation/coral4.yml
float-nonlinear-calculation/coral40.yml
float-nonlinear-calculation/coral41.yml
float-nonlinear-calculation/coral42.yml
float-nonlinear-calculation/coral43.yml
float-nonlinear-calculation/coral44.yml
float-nonlinear-calculation/coral45.yml
float-nonlinear-calculation/coral46.yml
float-nonlinear-calculation/coral49.yml
float-nonlinear-calculation/coral5.yml
float-nonlinear-calculation/coral50.yml
float-nonlinear-calculation/coral51.yml
float-nonlinear-calculation/coral52.yml
float-nonlinear-calculation/coral53.yml
float-nonlinear-calculation/coral54.yml
float-nonlinear-calculation/coral55.yml
float-nonlinear-calculation/coral56.yml
float-nonlinear-calculation/coral57.yml
float-nonlinear-calculation/coral58.yml
float-nonlinear-calculation/coral59.yml
float-nonlinear-calculation/coral6.yml
float-nonlinear-calculation/coral60.yml
float-nonlinear-calculation/coral61.yml
float-nonlinear-calculation/coral62.yml
float-nonlinear-calculation/coral63.yml
float-nonlinear-calculation/coral64.yml
float-nonlinear-calculation/coral65.yml
float-nonlinear-calculation/coral66.yml
float-nonlinear-calculation/coral67.yml
float-nonlinear-calculation/coral68.yml
float-nonlinear-calculation/coral69.yml
float-nonlinear-calculation/coral71.yml
float-nonlinear-calculation/coral72.yml
float-nonlinear-calculation/coral73.yml
float-nonlinear-calculation/coral74.yml
float-nonlinear-calculation/coral75.yml
float-nonlinear-calculation/coral79.yml
float-nonlinear-calculation/coral81.yml
float-nonlinear-calculation/coral84.yml
float-nonlinear-calculation/coral9.yml
float-nonlinear-calculation/coral91.yml