Tool CPAchecker CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741 CPA-witness2test 1.6.1-svn 26773 CProver witness2test 0.1 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon*
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB]
Date of execution 2017-12-05 07:52:24 CET 2017-12-05 13:10:09 CET 2017-12-05 13:34:02 CET 2017-12-05 13:37:41 CET 2017-12-05 13:41:35 CET 2017-12-05 12:37:13 CET 2017-12-05 13:13:01 CET
Run set interpchecker.sv-comp18.ReachSafety-Floats cpa-seq-validate-violation-witnesses-interpchecker.sv-comp18-violation-witness.ReachSafety-Floats uautomizer-validate-violation-witnesses-interpchecker.sv-comp18-violation-witness.ReachSafety-Floats cpa-witness2test-validate-violation-witnesses-interpchecker.sv-comp18-violation-witness.ReachSafety-Floats fshell-witness2test-validate-violation-witnesses-interpchecker.sv-comp18-violation-witness.ReachSafety-Floats cpa-seq-validate-correctness-witnesses-interpchecker.sv-comp18-correctness-witness.ReachSafety-Floats uautomizer-validate-correctness-witnesses-interpchecker.sv-comp18-correctness-witness.ReachSafety-Floats
Options -sv-comp18-interpcpachecker -heap 10000M -disable-java-assertions -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/interpchecker.2017-12-05_0752.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop cpa.smg.memoryAllocationFunctions=malloc,__kmalloc,kmalloc,kzalloc,kzalloc_node,ldv_zalloc,ldv_malloc -setprop cpa.smg.arrayAllocationFunctions=calloc,kmalloc_array,kcalloc -setprop cpa.smg.zeroingMemoryAllocation=calloc,kzalloc,kcalloc,kzalloc_node,ldv_zalloc -setprop cpa.smg.deallocationFunctions=free,kfree,kfree_const --full-output --validate ../../results-verified/interpchecker.2017-12-05_0752.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/interpchecker.2017-12-05_0752.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true --graphml-witness ../../results-verified/interpchecker.2017-12-05_0752.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/interpchecker.2017-12-05_0752.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/interpchecker.2017-12-05_0752.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
floats-cdfpl/newton_1_4_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 3.0 280 28 true -32 wit inspect 3.0  260 false(unreach-call) 1 wit inspect 44     670   unknown 0 wit inspect 2.7  210 true -32 wit inspect .57   18    - wit inspect - wit inspect
floats-cdfpl/newton_1_5_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 3.0 280 25 true -32 wit inspect 2.9  260 timeout 0 wit inspect 97     700   unknown 0 wit inspect 2.6  180 true -32 wit inspect .59   18    - wit inspect - wit inspect
floats-cdfpl/newton_1_6_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 3.0 270 25 true -32 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 21     680   unknown 0 wit inspect 2.7  190 true -32 wit inspect .61   18    - wit inspect - wit inspect
floats-cdfpl/newton_1_7_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 2.9 260 26 true -32 wit inspect 2.8  250 false(unreach-call) 1 wit inspect 41     670   unknown 0 wit inspect 2.8  190 true -32 wit inspect .58   18    - wit inspect - wit inspect
floats-cdfpl/newton_1_8_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 3.0 270 30 true -32 wit inspect 2.9  260 false(unreach-call) 1 wit inspect 34     670   unknown 0 wit inspect 2.7  180 true -32 wit inspect .60   18    - wit inspect - wit inspect
floats-cdfpl/newton_2_6_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 3.3 280 30 true -32 wit inspect 3.0  250 timeout 0 wit inspect 97     840   unknown 0 wit inspect 2.8  190 true -32 wit inspect .58   18    - wit inspect - wit inspect
floats-cdfpl/newton_2_7_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 3.3 270 31 true -32 wit inspect 3.0  260 timeout 0 wit inspect 97     820   unknown 0 wit inspect 2.8  210 true -32 wit inspect .58   18    - wit inspect - wit inspect
floats-cdfpl/newton_2_8_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 3.2 270 31 true -32 wit inspect 2.9  250 false(unreach-call) 1 wit inspect 29     810   unknown 0 wit inspect 2.8  210 true -32 wit inspect .58   19    - wit inspect - wit inspect
floats-cdfpl/newton_3_6_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 3.7 310 30 true -32 wit inspect 3.0  250 timeout 0 wit inspect 97     910   unknown 0 wit inspect 2.8  210 true -32 wit inspect .60   18    - wit inspect - wit inspect
floats-cdfpl/newton_3_7_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 3.6 300 29 true -32 wit inspect 3.2  260 timeout 0 wit inspect 97     880   unknown 0 wit inspect 2.8  210 true -32 wit inspect .59   18    - wit inspect - wit inspect
floats-cdfpl/newton_3_8_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 3.5 270 32 true -32 wit inspect 3.2  250 timeout 0 wit inspect 97     930   unknown 0 wit inspect 2.8  210 true -32 wit inspect .60   19    - wit inspect - wit inspect
floats-cdfpl/sine_1_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 3.1 280 28 true -32 wit inspect 3.0  250 false(unreach-call) 1 wit inspect 20     570   unknown 0 wit inspect 2.7  180 true -32 wit inspect .57   18    - wit inspect - wit inspect
floats-cdfpl/sine_2_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 2.8 280 28 true -32 wit inspect 3.0  260 false(unreach-call) 1 wit inspect 27     580   unknown 0 wit inspect 2.6  180 true -32 wit inspect .57   18    - wit inspect - wit inspect
floats-cdfpl/sine_3_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 2.8 270 25 true -32 wit inspect 2.9  260 timeout 0 wit inspect 97     630   unknown 0 wit inspect 2.7  180 true -32 wit inspect .60   18    - wit inspect - wit inspect
floats-cdfpl/square_1_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 2.9 280 28 true -32 wit inspect 2.8  250 timeout 0 wit inspect 97     470   unknown 0 wit inspect 2.7  180 true -32 wit inspect .61   18    - wit inspect - wit inspect
floats-cdfpl/square_2_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 2.9 280 25 true -32 wit inspect 2.8  260 false(unreach-call) 1 wit inspect 86     430   unknown 0 wit inspect 2.7  180 true -32 wit inspect .57   18    - wit inspect - wit inspect
floats-cdfpl/square_3_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 3.0 280 22 true -32 wit inspect 2.8  250 timeout 0 wit inspect 97     440   unknown 0 wit inspect 2.7  190 true -32 wit inspect .59   18    - wit inspect - wit inspect
floats-cdfpl/newton_1_1_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 3.0 270 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 timeout 0 wit inspect 960     1000  
floats-cdfpl/newton_1_2_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 3.1 280 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  250 timeout 0 wit inspect 960     1000  
floats-cdfpl/newton_1_3_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 3.0 270 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  260 timeout 0 wit inspect 960     950  
floats-cdfpl/newton_2_1_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 3.4 290 31 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  260 timeout 0 wit inspect 960     990  
floats-cdfpl/newton_2_2_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 3.2 280 32 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  250 timeout 0 wit inspect 960     1000  
floats-cdfpl/newton_2_3_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 3.3 290 28 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  260 timeout 0 wit inspect 960     940  
floats-cdfpl/newton_2_4_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 3.3 280 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  260 timeout 0 wit inspect 960     1000  
floats-cdfpl/newton_2_5_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 3.2 270 30 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  260 timeout 0 wit inspect 960     1000  
floats-cdfpl/newton_3_1_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 3.6 270 34 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  260 timeout 0 wit inspect 960     1100  
floats-cdfpl/newton_3_2_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 3.5 280 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  260 timeout 0 wit inspect 960     1100  
floats-cdfpl/newton_3_3_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 3.4 270 32 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 timeout 0 wit inspect 960     1200  
floats-cdfpl/newton_3_4_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 3.7 300 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  260 timeout 0 wit inspect 960     1000  
floats-cdfpl/newton_3_5_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 3.5 280 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 timeout 0 wit inspect 960     1100  
floats-cdfpl/sine_4_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 3.0 280 28 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 timeout 0 wit inspect 960     840  
floats-cdfpl/sine_5_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 2.9 270 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.8  260 timeout 0 wit inspect 960     830  
floats-cdfpl/sine_6_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 2.9 270 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 timeout 0 wit inspect 960     830  
floats-cdfpl/sine_7_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 3.0 280 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  250 timeout 0 wit inspect 960     780  
floats-cdfpl/sine_8_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 3.1 270 24 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  260 timeout 0 wit inspect 960     830  
floats-cdfpl/square_4_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 3.1 280 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  260 true 2 wit inspect 640     760  
floats-cdfpl/square_5_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 3.1 280 24 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 550     750  
floats-cdfpl/square_6_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 2.9 270 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  260 true 2 wit inspect 360     810  
floats-cdfpl/square_7_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 2.9 260 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  260 true 2 wit inspect 160     720  
floats-cdfpl/square_8_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 3.0 280 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  260 true 2 wit inspect 140     620  
floats-cbmc-regression/float-div1_true-unreach-call.i false(unreach-call) -16 wit inspect 4.0 290 35 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  250 true 2 wit inspect 34     610  
floats-cbmc-regression/float-flags-simp1_true-unreach-call.i false(unreach-call) -16 wit inspect 4.0 290 37 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.1  250 true 2 wit inspect 11     330  
floats-cbmc-regression/float-no-simp1_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 2.8 270 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.8  260 true 2 wit inspect 8.7   240  
floats-cbmc-regression/float-no-simp2_true-unreach-call.i true 2 wit inspect 3.8 280 35 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 20    300 true 2 wit inspect 42     400  
floats-cbmc-regression/float-no-simp3_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 2.7 280 24 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  260 true 2 wit inspect 9.2   230  
floats-cbmc-regression/float-no-simp4_true-unreach-call.i timeout 0 wit inspect 900   8100 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .50 41 error (2) 0 wit inspect .030 4.9
floats-cbmc-regression/float-no-simp6_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 2.7 270 22 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  260 true 2 wit inspect 10     280  
floats-cbmc-regression/float-no-simp7_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 2.8 260 23 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  260 true 2 wit inspect 9.9   250  
floats-cbmc-regression/float-no-simp8_true-unreach-call.i true 2 wit inspect 3.7 280 33 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.2  250 true 2 wit inspect 9.6   300  
floats-cbmc-regression/float-rounding1_true-unreach-call.i error 0 wit inspect 3.0 270 28 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 43 error (2) 0 wit inspect .021 4.8
floats-cbmc-regression/float-to-double1_true-unreach-call.i true 2 wit inspect 3.4 280 30 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3  260 true 2 wit inspect 240     520  
floats-cbmc-regression/float-to-double2_true-unreach-call_true-termination.i true 2 wit inspect 2.7 260 24 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 8.4   240  
floats-cbmc-regression/float-zero-sum1_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 2.8 280 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  260 true 2 wit inspect 11     280  
floats-cbmc-regression/float11_true-unreach-call_true-termination.i true 2 wit inspect 2.7 270 23 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 9.7   240  
floats-cbmc-regression/float12_true-unreach-call_true-termination.i true 2 wit inspect 2.7 270 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  250 true 2 wit inspect 14     260  
floats-cbmc-regression/float13_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 2.7 270 22 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  250 true 2 wit inspect 11     270  
floats-cbmc-regression/float14_true-unreach-call.i false(unreach-call) -16 wit inspect 4.1 290 37 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  250 true 2 wit inspect 12     300  
floats-cbmc-regression/float18_true-unreach-call.i true 2 wit inspect 7.7 460 64 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 63    660 unknown 0 wit inspect 3.7   200  
floats-cbmc-regression/float19_true-unreach-call.i false(unreach-call) -16 wit inspect 3.8 280 33 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  250 true 2 wit inspect 10     280  
floats-cbmc-regression/float1_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 2.7 260 24 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  260 true 2 wit inspect 8.4   240  
floats-cbmc-regression/float20_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 2.8 270 24 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  260 true 2 wit inspect 15     390  
floats-cbmc-regression/float21_true-unreach-call.i false(unreach-call) -16 wit inspect 3.7 280 35 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  250 true 2 wit inspect 21     440  
floats-cbmc-regression/float22_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 2.9 270 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3  260 true 2 wit inspect 67     610  
floats-cbmc-regression/float2_true-unreach-call_true-termination.i true 2 wit inspect 2.9 270 24 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 11     300  
floats-cbmc-regression/float3_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 2.9 270 24 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  260 true 2 wit inspect 13     350  
floats-cbmc-regression/float4_true-unreach-call.i true 2 wit inspect 4.0 280 33 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 59    330 true 2 wit inspect 76     440  
floats-cbmc-regression/float5_true-unreach-call_true-termination.i true 2 wit inspect 3.0 280 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  260 true 2 wit inspect 23     290  
floats-cbmc-regression/float6_true-unreach-call_true-termination.i true 2 wit inspect 3.2 260 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  260 true 2 wit inspect 11     280  
floats-cbmc-regression/float8_true-unreach-call.i true 2 wit inspect 3.7 280 32 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.4  270 true 2 wit inspect 11     290  
floats-cbmc-regression/float_lib1_true-unreach-call.i error (parsing failed) 0 wit inspect 1.7 130 15 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .019 5.0
floats-cbmc-regression/float_lib2_true-unreach-call.i false(unreach-call) -16 wit inspect 3.9 290 34 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.1  250 true 2 wit inspect 15     480  
float-benchs/cast_float_ptr_false-unreach-call_true-termination.c exception 0 wit inspect 2.4 260 21 error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .026 5.0 error (invalid witness file) 0 wit inspect .85 49 error (invalid witness file) 0 wit inspect .0041 .34 - wit inspect - wit inspect
float-benchs/cast_union_loose_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.9 260 28 true -32 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 10     280   unknown 0 wit inspect 2.7  190 true -32 wit inspect .58   18    - wit inspect - wit inspect
float-benchs/cast_union_tight_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.8 270 27 true -32 wit inspect 3.0  260 false(unreach-call) 1 wit inspect 10     270   unknown 0 wit inspect 3.0  210 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
float-benchs/float_int_inv_square_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.0 280 27 false(unreach-call) 1 wit inspect 2.9  270 false(unreach-call) 1 wit inspect 8.9   300   unknown 0 wit inspect 2.7  210 true -32 wit inspect .59   19    - wit inspect - wit inspect
float-benchs/inv_Newton_false-unreach-call.c timeout 0 wit inspect 900   4200 11000 error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .021 4.8 error (invalid witness file) 0 wit inspect .88 49 error (invalid witness file) 0 wit inspect .0039 .32 - wit inspect - wit inspect
float-benchs/inv_square_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.1 280 30 false(unreach-call) 1 wit inspect 3.1  270 false(unreach-call) 1 wit inspect 8.8   290   unknown 0 wit inspect 2.9  210 true -32 wit inspect .61   18    - wit inspect - wit inspect
float-benchs/nan_double_false-unreach-call_true-termination.c true -32 wit inspect 2.8 280 23 false(unreach-call) 1 wit inspect 3.2  260 false(unreach-call) 1 wit inspect 4.0   220   unknown 0 wit inspect .91 52 error (1) 0 wit inspect .098  9.0  - wit inspect - wit inspect
float-benchs/nan_float_false-unreach-call_true-termination.c true -32 wit inspect 2.8 260 24 false(unreach-call) 1 wit inspect 3.4  260 false(unreach-call) 1 wit inspect 4.2   220   unknown 0 wit inspect .88 51 error (1) 0 wit inspect .077  9.0  - wit inspect - wit inspect
float-benchs/sin_interpolated_index_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.1 270 29 true -32 wit inspect 3.9  260 false(unreach-call) 1 wit inspect 20     1100   unknown 0 wit inspect 3.1  210 true -32 wit inspect .60   18    - wit inspect - wit inspect
float-benchs/sqrt_poly2_false-unreach-call.c false(unreach-call) 1 wit inspect 3.1 270 27 true -32 wit inspect 3.2  260 false(unreach-call) 1 wit inspect 17     610   unknown 0 wit inspect 2.9  210 true -32 wit inspect .61   18    - wit inspect - wit inspect
float-benchs/Muller_Kahan_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 81   3700 880 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.1  270 out of memory 0 wit inspect 82     7000  
float-benchs/Rump_double_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 2.9 280 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  270 true 2 wit inspect 22     990  
float-benchs/Rump_float_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 2.9 280 24 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.8  260 true 2 wit inspect 14     420  
float-benchs/addsub_double_exact_true-unreach-call_true-termination.c true 2 wit inspect 2.9 280 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  250 true 2 wit inspect 8.9   280  
float-benchs/addsub_float_exact_true-unreach-call_true-termination.c true 2 wit inspect 2.9 280 28 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 10     250  
float-benchs/addsub_float_inexact_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 2.8 280 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 11     260  
float-benchs/arctan_Pade_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 3.2 270 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  260 true 2 wit inspect 120     2300  
float-benchs/bary_diverge_true-unreach-call_true-termination.c timeout 0 wit inspect 900   2100 14000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .025 4.9
float-benchs/cast_float_union_true-unreach-call.c true 2 wit inspect 2.6 270 22 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  270 true 2 wit inspect 4.6   230  
float-benchs/cos_polynomial_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 3.3 260 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  260 timeout 0 wit inspect 960     1200  
float-benchs/divmul_buf_diverge_true-unreach-call_true-termination.c true 2 wit inspect 6.2 370 53 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3400 timeout 0 wit inspect 960     4700  
float-benchs/divmul_diverge_true-unreach-call_true-termination.c true 2 wit inspect 5.7 310 46 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2000 timeout 0 wit inspect 960     4600  
float-benchs/drift_tenth_true-unreach-call_true-termination.c true 2 wit inspect 8.1 460 62 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 12    310 true 2 wit inspect 210     600  
float-benchs/exp_loop_true-unreach-call.c false(unreach-call) -16 wit inspect 4.5 290 40 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2300 timeout 0 wit inspect 960     1400  
float-benchs/feedback_diverge_true-unreach-call_true-termination.c timeout 0 wit inspect 910   4000 9900 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 44 error (2) 0 wit inspect .023 4.9
float-benchs/filter1_true-unreach-call_true-termination.c true 2 wit inspect 6.5 410 47 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.3  400 true 2 wit inspect 400     910  
float-benchs/filter2_alt_true-unreach-call.c timeout 0 wit inspect 900   1500 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .018 4.8
float-benchs/filter2_iterated_true-unreach-call.c timeout 0 wit inspect 900   1800 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .018 5.0
float-benchs/filter2_reinit_true-unreach-call_true-termination.c true 2 wit inspect 200   2400 2100 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1200 timeout 0 wit inspect 960     1900  
float-benchs/filter2_set_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 5.4 290 41 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3100 timeout 0 wit inspect 960     3600  
float-benchs/filter2_true-unreach-call_true-termination.c true 2 wit inspect 210   2800 2300 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1300 timeout 0 wit inspect 960     2100  
float-benchs/filter_iir_true-unreach-call.c false(unreach-call) -16 wit inspect 3.7 280 33 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  260 timeout 0 wit inspect 960     1400  
float-benchs/float_double_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 2.8 270 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  260 true 2 wit inspect 9.3   270  
float-benchs/image_filter_true-unreach-call.c timeout 0 wit inspect 910   4300 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .018 4.9
float-benchs/interpolation2_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 3.7 270 32 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4  260 timeout 0 wit inspect 960     760  
float-benchs/interpolation_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 3.8 270 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  260 timeout 0 wit inspect 960     760  
float-benchs/inv_sqrt_Quake_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 2.9 260 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  250 true 2 wit inspect 150     870  
float-benchs/inv_square_int_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 3.0 270 28 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 3.4  270 true 2 wit inspect 38     340  
float-benchs/inv_square_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 3.0 280 30 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 3.2  270 true 2 wit inspect 47     360  
float-benchs/loop_true-unreach-call.c timeout 0 wit inspect 900   5400 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .018 5.0
float-benchs/mea8000_true-unreach-call.c timeout 0 wit inspect 910   4900 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .018 4.9
float-benchs/nan_double_range_true-unreach-call_true-termination.c true 2 wit inspect 2.9 260 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  250 true 2 wit inspect 9.4   240  
float-benchs/nan_float_range_true-unreach-call_true-termination.c true 2 wit inspect 2.8 260 24 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  250 true 2 wit inspect 9.8   250  
float-benchs/rlim_exit_true-unreach-call_true-termination.c true 2 wit inspect 8.9 470 75 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1800 timeout 0 wit inspect 960     4700  
float-benchs/rlim_invariant_true-unreach-call_true-termination.c true 2 wit inspect 11   480 81 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.8  310 error (7) 0 wit inspect 760     790  
float-benchs/sin_interpolated_bigrange_loose_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 5.0 310 42 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.3  260 timeout 0 wit inspect 960     2300  
float-benchs/sin_interpolated_bigrange_tight_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 4.6 320 37 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.7  260 timeout 0 wit inspect 960     2100  
float-benchs/sin_interpolated_index_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 3.3 270 31 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  260 true 2 wit inspect 100     980  
float-benchs/sin_interpolated_negation_true-unreach-call.c exception 0 wit inspect 34   1600 280 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 42 error (2) 0 wit inspect .017 4.9
float-benchs/sin_interpolated_smallrange_true-unreach-call.c timeout 0 wit inspect 900   4600 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .022 5.0
float-benchs/sqrt_Householder_constant_true-unreach-call.c false(unreach-call) -16 wit inspect 4.9 280 42 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.7  260 error (7) 0 wit inspect 250     3000  
float-benchs/sqrt_Householder_interval_true-unreach-call.c false(unreach-call) -16 wit inspect 3.1 260 28 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2800 error (7) 0 wit inspect 170     2800  
float-benchs/sqrt_Householder_pseudoconstant_true-unreach-call.c false(unreach-call) -16 wit inspect 3.1 270 27 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2800 error (7) 0 wit inspect 88     2600  
float-benchs/sqrt_Newton_pseudoconstant_true-unreach-call.c false(unreach-call) -16 wit inspect 3.1 260 26 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2800 error (7) 0 wit inspect 89     2600  
float-benchs/sqrt_biNewton_pseudoconstant_true-unreach-call.c false(unreach-call) -16 wit inspect 3.2 270 26 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2800 error (7) 0 wit inspect 120     2700  
float-benchs/sqrt_poly_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 3.1 280 25 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1200 true 2 wit inspect 77     950  
float-benchs/water_pid_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 4.7 290 42 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.8  260 error (7) 0 wit inspect 76     1600  
float-benchs/zonotope_2_true-unreach-call_true-termination.c timeout 0 wit inspect 910   5000 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 44 error (2) 0 wit inspect .022 4.9
float-benchs/zonotope_3_true-unreach-call_true-termination.c timeout 0 wit inspect 900   4900 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 43 error (2) 0 wit inspect .018 4.9
float-benchs/zonotope_loose_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 3.1 280 29 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 3.3  300 true 2 wit inspect 66     610  
float-benchs/zonotope_tight_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 3.3 280 28 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 4.0  300 true 2 wit inspect 65     620  
floats-esbmc-regression/Double_div_true-unreach-call.i timeout 0 wit inspect 900   4000 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 43 error (2) 0 wit inspect .019 4.8
floats-esbmc-regression/Float_div_true-unreach-call.i timeout 0 wit inspect 900   4000 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 43 error (2) 0 wit inspect .017 5.0
floats-esbmc-regression/ceil_nondet_true-unreach-call.i error 0 wit inspect 3.1 280 27 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 42 error (2) 0 wit inspect .018 4.8
floats-esbmc-regression/ceil_true-unreach-call.i false(unreach-call) -16 wit inspect 4.0 280 35 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0  250 unknown 0 wit inspect 4.2   210  
floats-esbmc-regression/copysign_true-unreach-call.i false(unreach-call) -16 wit inspect 4.8 300 41 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.3  250 unknown 0 wit inspect 3.8   210  
floats-esbmc-regression/digits_for_true-unreach-call.i assertion 0 wit inspect 2.4 270 20 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .019 4.8
floats-esbmc-regression/digits_while_true-unreach-call.i assertion 0 wit inspect 2.3 270 21 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 41 error (2) 0 wit inspect .017 4.8
floats-esbmc-regression/fabs_true-unreach-call.i false(unreach-call) -16 wit inspect 3.8 280 33 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.6  260 true 2 wit inspect 12     620  
floats-esbmc-regression/fdim_true-unreach-call.i false(unreach-call) -16 wit inspect 3.8 280 36 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  250 unknown 0 wit inspect 3.6   200  
floats-esbmc-regression/floor_nondet_true-unreach-call.i error 0 wit inspect 3.1 280 27 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .023 5.0
floats-esbmc-regression/floor_true-unreach-call.i false(unreach-call) -16 wit inspect 4.1 290 35 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.7  250 unknown 0 wit inspect 4.8   210  
floats-esbmc-regression/fmax_true-unreach-call.i false(unreach-call) -16 wit inspect 3.8 280 35 - wit inspect - wit inspect - wit inspect - wit inspect