Tool CPAchecker 1.6.1-svn 26725 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-11-30 11:20:26 CET 2017-12-01 07:36:53 CET 2017-12-01 08:24:12 CET 2017-12-01 08:27:09 CET 2017-12-01 08:31:26 CET 2017-12-01 04:24:37 CET 2017-12-01 07:42:15 CET
Run set cpa-bam-bnb.sv-comp18.ReachSafety-Floats cpa-seq-validate-violation-witnesses-cpa-bam-bnb.sv-comp18-violation-witness.ReachSafety-Floats uautomizer-validate-violation-witnesses-cpa-bam-bnb.sv-comp18-violation-witness.ReachSafety-Floats cpa-witness2test-validate-violation-witnesses-cpa-bam-bnb.sv-comp18-violation-witness.ReachSafety-Floats fshell-witness2test-validate-violation-witnesses-cpa-bam-bnb.sv-comp18-violation-witness.ReachSafety-Floats cpa-seq-validate-correctness-witnesses-cpa-bam-bnb.sv-comp18-correctness-witness.ReachSafety-Floats uautomizer-validate-correctness-witnesses-cpa-bam-bnb.sv-comp18-correctness-witness.ReachSafety-Floats
Options -svcomp18-bam-bnb -disable-java-assertions -heap 10000m -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-bam-bnb.2017-11-30_1120.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/cpa-bam-bnb.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-bam-bnb.2017-11-30_1120.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/cpa-bam-bnb.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-bam-bnb.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/cpa-bam-bnb.2017-11-30_1120.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.5 290 31 false(unreach-call) 1 wit inspect 60    360 false(unreach-call) 1 wit inspect 53     680   unknown 0 wit inspect 2.9  210 true -32 wit inspect .61   18    - wit inspect - wit inspect
floats-cdfpl/newton_1_5_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 3.8 290 36 false(unreach-call) 1 wit inspect 23    350 timeout 0 wit inspect 97     700   unknown 0 wit inspect 2.8  210 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.7 290 35 false(unreach-call) 1 wit inspect 22    360 false(unreach-call) 1 wit inspect 23     660   unknown 0 wit inspect 3.0  190 true -32 wit inspect .59   18    - wit inspect - wit inspect
floats-cdfpl/newton_1_7_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 3.7 290 33 false(unreach-call) 1 wit inspect 54    360 false(unreach-call) 1 wit inspect 41     670   unknown 0 wit inspect 2.9  190 true -32 wit inspect .62   18    - wit inspect - wit inspect
floats-cdfpl/newton_1_8_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 3.6 290 29 false(unreach-call) 1 wit inspect 12    360 false(unreach-call) 1 wit inspect 30     670   unknown 0 wit inspect 2.2  210 true -32 wit inspect .59   18    - wit inspect - wit inspect
floats-cdfpl/newton_2_6_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 4.1 310 34 false(unreach-call) 1 wit inspect 16    450 timeout 0 wit inspect 97     810   unknown 0 wit inspect 3.1  180 true -32 wit inspect .68   18    - wit inspect - wit inspect
floats-cdfpl/newton_2_7_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 3.9 310 37 false(unreach-call) 1 wit inspect 80    470 timeout 0 wit inspect 97     820   unknown 0 wit inspect 3.0  180 true -32 wit inspect .61   18    - wit inspect - wit inspect
floats-cdfpl/newton_2_8_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 3.8 290 32 false(unreach-call) 1 wit inspect 17    460 false(unreach-call) 1 wit inspect 33     810   unknown 0 wit inspect 3.3  180 true -32 wit inspect .59   18    - wit inspect - wit inspect
floats-cdfpl/newton_3_6_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 4.4 320 35 timeout 0 wit inspect 92    570 timeout 0 wit inspect 97     900   unknown 0 wit inspect 2.8  180 true -32 wit inspect .58   18    - wit inspect - wit inspect
floats-cdfpl/newton_3_7_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 4.5 320 44 timeout 0 wit inspect 91    560 timeout 0 wit inspect 97     870   unknown 0 wit inspect 3.5  180 true -32 wit inspect .58   18    - wit inspect - wit inspect
floats-cdfpl/newton_3_8_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 4.4 310 34 false(unreach-call) 1 wit inspect 18    560 timeout 0 wit inspect 97     920   unknown 0 wit inspect 3.5  180 true -32 wit inspect .60   18    - wit inspect - wit inspect
floats-cdfpl/sine_1_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 3.6 280 32 timeout 0 wit inspect 91    360 false(unreach-call) 1 wit inspect 23     560   unknown 0 wit inspect 3.0  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 3.4 280 30 false(unreach-call) 1 wit inspect 4.2  310 false(unreach-call) 1 wit inspect 36     580   unknown 0 wit inspect 3.3  190 true -32 wit inspect .57   18    - wit inspect - wit inspect
floats-cdfpl/sine_3_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 3.4 280 31 false(unreach-call) 1 wit inspect 4.9  320 timeout 0 wit inspect 97     600   unknown 0 wit inspect 2.9  210 true -32 wit inspect .61   18    - wit inspect - wit inspect
floats-cdfpl/square_1_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 3.6 290 29 false(unreach-call) 1 wit inspect 9.4  320 timeout 0 wit inspect 97     460   unknown 0 wit inspect 3.7  190 true -32 wit inspect .60   18    - wit inspect - wit inspect
floats-cdfpl/square_2_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 3.6 290 31 false(unreach-call) 1 wit inspect 56    340 timeout 0 wit inspect 97     410   unknown 0 wit inspect 3.5  180 true -32 wit inspect .57   18    - wit inspect - wit inspect
floats-cdfpl/square_3_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 3.6 290 29 false(unreach-call) 1 wit inspect 20    330 timeout 0 wit inspect 97     430   unknown 0 wit inspect 3.2  180 true -32 wit inspect .58   18    - wit inspect - wit inspect
floats-cdfpl/newton_1_1_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 3.6 290 32 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    730 timeout 0 wit inspect 960     1000  
floats-cdfpl/newton_1_2_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 3.8 290 30 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    640 timeout 0 wit inspect 960     1000  
floats-cdfpl/newton_1_3_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 3.6 290 36 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    660 timeout 0 wit inspect 960     910  
floats-cdfpl/newton_2_1_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 3.8 300 38 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    520 timeout 0 wit inspect 960     990  
floats-cdfpl/newton_2_2_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 3.9 290 32 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    540 timeout 0 wit inspect 960     970  
floats-cdfpl/newton_2_3_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 3.9 280 33 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    520 timeout 0 wit inspect 960     930  
floats-cdfpl/newton_2_4_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 4.1 310 36 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    620 timeout 0 wit inspect 960     1000  
floats-cdfpl/newton_2_5_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 3.9 290 32 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    520 timeout 0 wit inspect 960     1000  
floats-cdfpl/newton_3_1_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 4.6 330 35 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    580 timeout 0 wit inspect 960     1100  
floats-cdfpl/newton_3_2_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 4.6 330 40 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    560 timeout 0 wit inspect 960     1000  
floats-cdfpl/newton_3_3_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 4.4 330 40 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    620 timeout 0 wit inspect 960     1100  
floats-cdfpl/newton_3_4_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 4.6 320 31 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    580 timeout 0 wit inspect 960     1000  
floats-cdfpl/newton_3_5_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 4.5 320 39 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    580 timeout 0 wit inspect 960     1100  
floats-cdfpl/sine_4_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 3.5 290 34 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    470 timeout 0 wit inspect 960     840  
floats-cdfpl/sine_5_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 3.6 280 30 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 450    500 timeout 0 wit inspect 960     910  
floats-cdfpl/sine_6_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 3.5 280 29 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    440 timeout 0 wit inspect 960     820  
floats-cdfpl/sine_7_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 3.5 280 35 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 450    530 timeout 0 wit inspect 960     790  
floats-cdfpl/sine_8_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 3.6 280 33 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    630 timeout 0 wit inspect 960     830  
floats-cdfpl/square_4_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 3.5 280 31 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 830    600 true 2 wit inspect 730     830  
floats-cdfpl/square_5_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 3.6 290 30 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    530 true 2 wit inspect 440     750  
floats-cdfpl/square_6_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 3.4 280 34 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    620 true 2 wit inspect 440     800  
floats-cdfpl/square_7_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 3.7 290 28 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 720    510 true 2 wit inspect 180     720  
floats-cdfpl/square_8_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 3.5 280 28 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 180    370 true 2 wit inspect 120     630  
floats-cbmc-regression/float-div1_true-unreach-call.i false(unreach-call) -16 wit inspect 5.1 310 42 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 4.9  300 true 2 wit inspect 35     600  
floats-cbmc-regression/float-flags-simp1_true-unreach-call.i false(unreach-call) -16 wit inspect 6.3 330 51 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 4.0  270 true 2 wit inspect 15     350  
floats-cbmc-regression/float-no-simp1_true-unreach-call_true-termination.i true 2 wit inspect 2.8 270 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 8.8   230  
floats-cbmc-regression/float-no-simp2_true-unreach-call.i true 2 wit inspect 3.6 280 32 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 21    300 true 2 wit inspect 44     400  
floats-cbmc-regression/float-no-simp3_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 2.9  250 true 2 wit inspect 11     230  
floats-cbmc-regression/float-no-simp4_true-unreach-call.i false(unreach-call) -16 wit inspect 5.0 320 45 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 4.6  260 true 2 wit inspect 12     310  
floats-cbmc-regression/float-no-simp6_true-unreach-call_true-termination.i true 2 wit inspect 2.9 270 28 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 11     290  
floats-cbmc-regression/float-no-simp7_true-unreach-call_true-termination.i true 2 wit inspect 2.9 270 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 11     250  
floats-cbmc-regression/float-no-simp8_true-unreach-call.i true 2 wit inspect 3.5 280 31 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  260 true 2 wit inspect 11     290  
floats-cbmc-regression/float-rounding1_true-unreach-call.i error 0 wit inspect 3.3 280 33 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .019 5.0
floats-cbmc-regression/float-to-double1_true-unreach-call.i true 2 wit inspect 3.7 280 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  260 true 2 wit inspect 120     460  
floats-cbmc-regression/float-to-double2_true-unreach-call_true-termination.i true 2 wit inspect 2.7 270 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 11     230  
floats-cbmc-regression/float-zero-sum1_true-unreach-call_true-termination.i true 2 wit inspect 3.0 270 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 12     280  
floats-cbmc-regression/float11_true-unreach-call_true-termination.i true 2 wit inspect 2.8 270 22 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 10     250  
floats-cbmc-regression/float12_true-unreach-call_true-termination.i true 2 wit inspect 2.8 270 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 17     280  
floats-cbmc-regression/float13_true-unreach-call_true-termination.i true 2 wit inspect 2.8 270 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  250 true 2 wit inspect 12     260  
floats-cbmc-regression/float14_true-unreach-call.i true 2 wit inspect 3.7 280 36 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  250 true 2 wit inspect 10     290  
floats-cbmc-regression/float18_true-unreach-call.i true 2 wit inspect 4.1 280 33 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 23    410 unknown 0 wit inspect 4.2   210  
floats-cbmc-regression/float19_true-unreach-call.i false(unreach-call) -16 wit inspect 5.3 320 40 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 4.0  270 true 2 wit inspect 14     280  
floats-cbmc-regression/float1_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 3.1  250 true 2 wit inspect 9.8   230  
floats-cbmc-regression/float20_true-unreach-call_true-termination.i true 2 wit inspect 2.9 270 28 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  250 true 2 wit inspect 20     380  
floats-cbmc-regression/float21_true-unreach-call.i false(unreach-call) -16 wit inspect 4.9 300 39 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 3.8  260 true 2 wit inspect 28     460  
floats-cbmc-regression/float22_true-unreach-call_true-termination.i error 0 wit inspect 3.5 290 29 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .019 4.9
floats-cbmc-regression/float2_true-unreach-call_true-termination.i true 2 wit inspect 2.7 270 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 11     280  
floats-cbmc-regression/float3_true-unreach-call_true-termination.i error 0 wit inspect 3.3 280 34 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 42 error (2) 0 wit inspect .019 4.9
floats-cbmc-regression/float4_true-unreach-call.i true 2 wit inspect 3.8 270 34 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 81    330 true 2 wit inspect 77     440  
floats-cbmc-regression/float5_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 4.2  260 true 2 wit inspect 29     280  
floats-cbmc-regression/float6_true-unreach-call_true-termination.i true 2 wit inspect 3.0 280 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  250 true 2 wit inspect 12     290  
floats-cbmc-regression/float8_true-unreach-call.i true 2 wit inspect 3.9 300 37 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.1  270 true 2 wit inspect 13     290  
floats-cbmc-regression/float_lib1_true-unreach-call.i error (parsing failed) 0 wit inspect 1.7 140 15 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .75 42 error (2) 0 wit inspect .019 4.8
floats-cbmc-regression/float_lib2_true-unreach-call.i true 2 wit inspect 4.2 310 36 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  250 true 2 wit inspect 19     540  
float-benchs/cast_float_ptr_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.6 280 28 false(unreach-call) 1 wit inspect 3.3  260 false(unreach-call) 1 wit inspect 11     270   unknown 0 wit inspect 3.2  180 true -32 wit inspect .60   18    - wit inspect - wit inspect
float-benchs/cast_union_loose_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 4.0 310 33 false(unreach-call) 1 wit inspect 3.9  270 true -32 wit inspect 4.7   230   unknown 0 wit inspect 2.8  180 true -32 wit inspect .57   18    - wit inspect - wit inspect
float-benchs/cast_union_tight_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.5 290 31 false(unreach-call) 1 wit inspect 3.4  270 true -32 wit inspect 5.8   230   unknown 0 wit inspect 3.5  180 true -32 wit inspect .60   18    - wit inspect - wit inspect
float-benchs/float_int_inv_square_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.4 280 31 false(unreach-call) 1 wit inspect 3.5  270 false(unreach-call) 1 wit inspect 9.6   290   unknown 0 wit inspect 3.2  190 true -32 wit inspect .58   18    - wit inspect - wit inspect
float-benchs/inv_Newton_false-unreach-call.c false(unreach-call) 0 wit inspect 4.2 320 37 unknown 0 wit inspect 8.7  340 timeout 0 wit inspect 97     760   unknown 0 wit inspect 2.9  210 true -32 wit inspect .60   18    - wit inspect - wit inspect
float-benchs/inv_square_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.5 290 32 false(unreach-call) 1 wit inspect 3.1  270 false(unreach-call) 1 wit inspect 11     310   unknown 0 wit inspect 3.2  210 true -32 wit inspect .60   18    - wit inspect - wit inspect
float-benchs/nan_double_false-unreach-call_true-termination.c true -32 wit inspect 2.9 270 26 false(unreach-call) 1 wit inspect 3.6  260 false(unreach-call) 1 wit inspect 5.8   220   unknown 0 wit inspect .96 51 error (1) 0 wit inspect .086  8.9  - wit inspect - wit inspect
float-benchs/nan_float_false-unreach-call_true-termination.c true -32 wit inspect 2.8 270 24 false(unreach-call) 1 wit inspect 3.6  280 false(unreach-call) 1 wit inspect 4.9   210   unknown 0 wit inspect .89 53 error (1) 0 wit inspect .073  9.0  - wit inspect - wit inspect
float-benchs/sin_interpolated_index_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 4.0 300 39 unknown 0 wit inspect 3.9  320 false(unreach-call) 1 wit inspect 23     1100   unknown 0 wit inspect 3.0  210 true -32 wit inspect .64   18    - wit inspect - wit inspect
float-benchs/sqrt_poly2_false-unreach-call.c false(unreach-call) 1 wit inspect 4.0 290 34 false(unreach-call) 1 wit inspect 7.8  410 true -32 wit inspect 5.8   220   unknown 0 wit inspect 3.2  180 true -32 wit inspect .58   19    - wit inspect - wit inspect
float-benchs/Muller_Kahan_true-unreach-call_true-termination.c error 0 wit inspect 110   3700 1200 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .74 43 error (2) 0 wit inspect .021 4.8
float-benchs/Rump_double_true-unreach-call_true-termination.c true 2 wit inspect 2.7 270 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 20     1000  
float-benchs/Rump_float_true-unreach-call_true-termination.c true 2 wit inspect 2.7 270 24 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 15     420  
float-benchs/addsub_double_exact_true-unreach-call_true-termination.c true 2 wit inspect 2.7 280 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 9.5   270  
float-benchs/addsub_float_exact_true-unreach-call_true-termination.c true 2 wit inspect 2.8 270 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 10     260  
float-benchs/addsub_float_inexact_true-unreach-call_true-termination.c true 2 wit inspect 2.8 270 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 10     250  
float-benchs/arctan_Pade_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 4.1 290 35 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 9.6  420 true 2 wit inspect 120     2400  
float-benchs/bary_diverge_true-unreach-call_true-termination.c timeout 0 wit inspect 900   7500 9700 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 41 error (2) 0 wit inspect .019 4.9
float-benchs/cast_float_union_true-unreach-call.c true 2 wit inspect 3.1 300 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  250 true 2 wit inspect 6.0   230  
float-benchs/cos_polynomial_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 4.1 290 33 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    590 timeout 0 wit inspect 960     1200  
float-benchs/divmul_buf_diverge_true-unreach-call_true-termination.c timeout 0 wit inspect 900   4200 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 41 error (2) 0 wit inspect .021 4.8
float-benchs/divmul_diverge_true-unreach-call_true-termination.c timeout 0 wit inspect 900   4200 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 43 error (2) 0 wit inspect .019 4.9
float-benchs/drift_tenth_true-unreach-call_true-termination.c true 2 wit inspect 3.5 270 30 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 19    380 true 2 wit inspect 300     660  
float-benchs/exp_loop_true-unreach-call.c false(unreach-call) -16 wit inspect 4.7 300 36 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 3.4  270 timeout 0 wit inspect 960     1200  
float-benchs/feedback_diverge_true-unreach-call_true-termination.c timeout 0 wit inspect 900   7100 8600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 45 error (2) 0 wit inspect .018 4.8
float-benchs/filter1_true-unreach-call_true-termination.c true 2 wit inspect 3.5 280 32 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 10    400 true 2 wit inspect 430     850  
float-benchs/filter2_alt_true-unreach-call.c error 0 wit inspect 4.3 320 38 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .020 5.0
float-benchs/filter2_iterated_true-unreach-call.c error 0 wit inspect 4.1 300 39 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 43 error (2) 0 wit inspect .019 4.8
float-benchs/filter2_reinit_true-unreach-call_true-termination.c timeout 0 wit inspect 900   3400 14000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .021 4.9
float-benchs/filter2_set_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 5.1 310 40 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 9.1  390 error (7) 0 wit inspect 540     3200  
float-benchs/filter2_true-unreach-call_true-termination.c true 2 wit inspect 34   1400 300 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1300 timeout 0 wit inspect 960     2000  
float-benchs/filter_iir_true-unreach-call.c true 2 wit inspect 3.3 280 28 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2800 timeout 0 wit inspect 960     1400  
float-benchs/float_double_true-unreach-call_true-termination.c true 2 wit inspect 2.8 270 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  260 true 2 wit inspect 11     260  
float-benchs/image_filter_true-unreach-call.c timeout 0 wit inspect 900   4700 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 41 error (2) 0 wit inspect .020 4.9
float-benchs/interpolation2_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 4.1 310 35 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 4.0  300 timeout 0 wit inspect 960     660  
float-benchs/interpolation_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 4.2 310 33 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 4.4  290 timeout 0 wit inspect 960     830  
float-benchs/inv_sqrt_Quake_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 3.8 290 37 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 3.9  280 error (7) 0 wit inspect 45     650  
float-benchs/inv_square_int_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 3.5 290 36 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 3.8  260 true 2 wit inspect 23     350  
float-benchs/inv_square_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 3.5 280 28 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 3.9  270 true 2 wit inspect 57     320  
float-benchs/loop_true-unreach-call.c timeout 0 wit inspect 900   4400 8100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 41 error (2) 0 wit inspect .023 4.9
float-benchs/mea8000_true-unreach-call.c timeout 0 wit inspect 900   4000 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .018 4.8
float-benchs/nan_double_range_true-unreach-call_true-termination.c true 2 wit inspect 2.7 270 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.1  250 true 2 wit inspect 12     240  
float-benchs/nan_float_range_true-unreach-call_true-termination.c true 2 wit inspect 2.8 270 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 11     250  
float-benchs/rlim_exit_true-unreach-call_true-termination.c timeout 0 wit inspect 900   4300 9300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .021 4.8
float-benchs/rlim_invariant_true-unreach-call_true-termination.c true 2 wit inspect 3.7 280 33 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.9  310 error (7) 0 wit inspect 170     560  
float-benchs/sin_interpolated_bigrange_loose_true-unreach-call_true-termination.c error 0 wit inspect 3.2 290 26 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 42 error (2) 0 wit inspect .023 4.8
float-benchs/sin_interpolated_bigrange_tight_true-unreach-call_true-termination.c error 0 wit inspect 2.7 270 24 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 43 error (2) 0 wit inspect .019 4.9
float-benchs/sin_interpolated_index_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 4.2 320 40 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 3.8  320 true 2 wit inspect 50     960  
float-benchs/sin_interpolated_negation_true-unreach-call.c error 0 wit inspect 2.7 270 25 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .022 4.8
float-benchs/sin_interpolated_smallrange_true-unreach-call.c error 0 wit inspect 2.8 270 22 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 41 error (2) 0 wit inspect .023 4.9
float-benchs/sqrt_Householder_constant_true-unreach-call.c error 0 wit inspect 3.8 290 35 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .020 4.8
float-benchs/sqrt_Householder_interval_true-unreach-call.c false(unreach-call) -16 wit inspect 3.9 290 36 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 error (7) 0 wit inspect 110     1500  
float-benchs/sqrt_Householder_pseudoconstant_true-unreach-call.c false(unreach-call) -16 wit inspect 4.2 290 41 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 6.7  480 error (7) 0 wit inspect 130     2700  
float-benchs/sqrt_Newton_pseudoconstant_true-unreach-call.c false(unreach-call) -16 wit inspect 4.1 290 38 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 8.2  480 error (7) 0 wit inspect 51     1200  
float-benchs/sqrt_biNewton_pseudoconstant_true-unreach-call.c false(unreach-call) -16 wit inspect 4.2 290 35 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 6.4  490 error (7) 0 wit inspect 89     2600  
float-benchs/sqrt_poly_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 3.7 290 33 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 6.6  340 true 2 wit inspect 150     1100  
float-benchs/water_pid_true-unreach-call_true-termination.c error 0 wit inspect 9.5 490 74 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .020 4.9
float-benchs/zonotope_2_true-unreach-call_true-termination.c true 2 wit inspect 4.2 290 35 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    870 timeout 0 wit inspect 960     2400  
float-benchs/zonotope_3_true-unreach-call_true-termination.c timeout 0 wit inspect 900   4200 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .019 4.9
float-benchs/zonotope_loose_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 3.5 280 32 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 4.4  300 true 2 wit inspect 120     970  
float-benchs/zonotope_tight_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 3.6 290 36 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 4.4  300 true 2 wit inspect 120     970  
floats-esbmc-regression/Double_div_true-unreach-call.i timeout 0 wit inspect 900   4200 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 42 error (2) 0 wit inspect .024 4.9
floats-esbmc-regression/Float_div_true-unreach-call.i timeout 0 wit inspect 900   4100 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 42 error (2) 0 wit inspect .019 4.9
floats-esbmc-regression/ceil_nondet_true-unreach-call.i error 0 wit inspect 3.6 290 34 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 45 error (2) 0 wit inspect .022 4.9
floats-esbmc-regression/ceil_true-unreach-call.i true 2 wit inspect 4.1 280 40 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  260 unknown 0 wit inspect 3.9   200  
floats-esbmc-regression/copysign_true-unreach-call.i true 2 wit inspect 4.9 290 39 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.6  260 unknown 0 wit inspect 3.8   210  
floats-esbmc-regression/digits_for_true-unreach-call.i assertion 0 wit inspect 2.4 270 22 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .019 5.0
floats-esbmc-regression/digits_while_true-unreach-call.i assertion 0 wit inspect 2.5 270 23 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .019 4.9
floats-esbmc-regression/fabs_true-unreach-call.i true 2 wit inspect 4.4 310 41 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  260 true 2 wit inspect 9.5   280  
floats-esbmc-regression/fdim_true-unreach-call.i true 2 wit inspect 4.2 280 37 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8  250 unknown 0 wit inspect 4.9   200  
floats-esbmc-regression/floor_nondet_true-unreach-call.i error 0 wit inspect 3.5 300 27 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .018 4.8
floats-esbmc-regression/floor_true-unreach-call.i true 2 wit inspect 4.0 280 35 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  260 unknown 0 wit inspect 3.7   210  
floats-esbmc-regression/fmax_true-unreach-call.i true 2 wit inspect 4.1 280 37 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.6  250 true 2 wit inspect 9.2   280  
floats-esbmc-regression/fmin_true-unreach-call.i true 2 wit inspect 4.3 310