Tool ULTIMATE Kojak 0.1.23-3204b741 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] 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-02 02:33:02 CET 2017-12-03 03:22:18 CET 2017-12-03 03:55:21 CET 2017-12-03 04:22:06 CET 2017-12-03 04:36:43 CET 2017-12-03 00:36:56 CET 2017-12-03 03:32:10 CET
Run set ukojak.sv-comp18.ReachSafety-Floats cpa-seq-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.ReachSafety-Floats uautomizer-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.ReachSafety-Floats cpa-witness2test-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.ReachSafety-Floats fshell-witness2test-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.ReachSafety-Floats cpa-seq-validate-correctness-witnesses-ukojak.sv-comp18-correctness-witness.ReachSafety-Floats uautomizer-validate-correctness-witnesses-ukojak.sv-comp18-correctness-witness.ReachSafety-Floats
Options --full-output -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/ukojak.2017-12-02_0233.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/ukojak.2017-12-02_0233.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/ukojak.2017-12-02_0233.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/ukojak.2017-12-02_0233.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/ukojak.2017-12-02_0233.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/ukojak.2017-12-02_0233.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 error (7) 0 wit inspect 100   1200 750 error (invalid witness file) 0 wit inspect .63 42 error (2) 0 wit inspect .021 4.9 error (invalid witness file) 0 wit inspect 1.1  47 error (invalid witness file) 0 wit inspect .0014 .26 - wit inspect - wit inspect
floats-cdfpl/newton_1_5_false-unreach-call_true-termination.i error (7) 0 wit inspect 94   1100 700 error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect 1.1  47 error (invalid witness file) 0 wit inspect .0017 .27 - wit inspect - wit inspect
floats-cdfpl/newton_1_6_false-unreach-call_true-termination.i error (7) 0 wit inspect 96   1100 830 error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .83 47 error (invalid witness file) 0 wit inspect .0014 .34 - wit inspect - wit inspect
floats-cdfpl/newton_1_7_false-unreach-call_true-termination.i error (7) 0 wit inspect 99   1100 780 error (invalid witness file) 0 wit inspect .40 41 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .83 49 error (invalid witness file) 0 wit inspect .0017 .28 - wit inspect - wit inspect
floats-cdfpl/newton_1_8_false-unreach-call_true-termination.i error (7) 0 wit inspect 96   1200 660 error (invalid witness file) 0 wit inspect .69 42 error (2) 0 wit inspect .025 4.9 error (invalid witness file) 0 wit inspect .70 49 error (invalid witness file) 0 wit inspect .0011 .34 - wit inspect - wit inspect
floats-cdfpl/newton_2_6_false-unreach-call_true-termination.i error (7) 0 wit inspect 55   1500 460 error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .82 47 error (invalid witness file) 0 wit inspect .0019 .26 - wit inspect - wit inspect
floats-cdfpl/newton_2_7_false-unreach-call_true-termination.i error (7) 0 wit inspect 48   1400 550 error (invalid witness file) 0 wit inspect .68 44 error (2) 0 wit inspect .021 4.9 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0015 .26 - wit inspect - wit inspect
floats-cdfpl/newton_2_8_false-unreach-call_true-termination.i error (7) 0 wit inspect 69   1600 550 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect 1.1  47 error (invalid witness file) 0 wit inspect .0016 .30 - wit inspect - wit inspect
floats-cdfpl/newton_3_6_false-unreach-call_true-termination.i error (7) 0 wit inspect 71   2000 650 error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0015 .34 - wit inspect - wit inspect
floats-cdfpl/newton_3_7_false-unreach-call_true-termination.i error (7) 0 wit inspect 58   2000 560 error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .023 4.9 error (invalid witness file) 0 wit inspect .90 49 error (invalid witness file) 0 wit inspect .0017 .27 - wit inspect - wit inspect
floats-cdfpl/newton_3_8_false-unreach-call_true-termination.i error (7) 0 wit inspect 57   2000 480 error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .024 4.8 error (invalid witness file) 0 wit inspect .82 49 error (invalid witness file) 0 wit inspect .0011 .34 - wit inspect - wit inspect
floats-cdfpl/sine_1_false-unreach-call_true-termination.i error (7) 0 wit inspect 49   660 370 error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .95 49 error (invalid witness file) 0 wit inspect .0016 .27 - wit inspect - wit inspect
floats-cdfpl/sine_2_false-unreach-call_true-termination.i error (7) 0 wit inspect 51   620 460 error (invalid witness file) 0 wit inspect .50 41 error (2) 0 wit inspect .025 4.8 error (invalid witness file) 0 wit inspect .68 49 error (invalid witness file) 0 wit inspect .0021 .28 - wit inspect - wit inspect
floats-cdfpl/sine_3_false-unreach-call_true-termination.i error (7) 0 wit inspect 51   620 430 error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .024 4.8 error (invalid witness file) 0 wit inspect 1.1  50 error (invalid witness file) 0 wit inspect .0019 .30 - wit inspect - wit inspect
floats-cdfpl/square_1_false-unreach-call_true-termination.i error (7) 0 wit inspect 32   380 250 error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .021 4.9 error (invalid witness file) 0 wit inspect 1.1  47 error (invalid witness file) 0 wit inspect .0018 .26 - wit inspect - wit inspect
floats-cdfpl/square_2_false-unreach-call_true-termination.i error (7) 0 wit inspect 28   380 210 error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect 1.0  49 error (invalid witness file) 0 wit inspect .0014 .34 - wit inspect - wit inspect
floats-cdfpl/square_3_false-unreach-call_true-termination.i error (7) 0 wit inspect 35   380 360 error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .021 4.9 error (invalid witness file) 0 wit inspect 1.0  49 error (invalid witness file) 0 wit inspect .0016 .26 - wit inspect - wit inspect
floats-cdfpl/newton_1_1_true-unreach-call_true-termination.i error (7) 0 wit inspect 110   1200 760 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 41 error (2) 0 wit inspect .017 4.9
floats-cdfpl/newton_1_2_true-unreach-call_true-termination.i error (7) 0 wit inspect 100   1100 750 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 44 error (2) 0 wit inspect .018 4.8
floats-cdfpl/newton_1_3_true-unreach-call_true-termination.i error (7) 0 wit inspect 93   1200 760 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .018 4.9
floats-cdfpl/newton_2_1_true-unreach-call_true-termination.i error (7) 0 wit inspect 66   1400 750 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .40 43 error (2) 0 wit inspect .018 5.0
floats-cdfpl/newton_2_2_true-unreach-call_true-termination.i error (7) 0 wit inspect 67   1500 560 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .75 46 error (2) 0 wit inspect .018 4.9
floats-cdfpl/newton_2_3_true-unreach-call_true-termination.i error (7) 0 wit inspect 62   1400 510 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 43 error (2) 0 wit inspect .019 4.8
floats-cdfpl/newton_2_4_true-unreach-call_true-termination.i error (7) 0 wit inspect 59   1500 560 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .018 4.9
floats-cdfpl/newton_2_5_true-unreach-call_true-termination.i error (7) 0 wit inspect 61   1500 520 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .019 4.9
floats-cdfpl/newton_3_1_true-unreach-call_true-termination.i error (7) 0 wit inspect 66   2000 520 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 44 error (2) 0 wit inspect .018 4.9
floats-cdfpl/newton_3_2_true-unreach-call_true-termination.i error (7) 0 wit inspect 70   2000 590 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .72 45 error (2) 0 wit inspect .020 4.9
floats-cdfpl/newton_3_3_true-unreach-call_true-termination.i error (7) 0 wit inspect 72   1900 790 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .41 44 error (2) 0 wit inspect .018 5.0
floats-cdfpl/newton_3_4_true-unreach-call_true-termination.i error (7) 0 wit inspect 58   2000 450 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .018 5.0
floats-cdfpl/newton_3_5_true-unreach-call_true-termination.i error (7) 0 wit inspect 60   2000 530 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 44 error (2) 0 wit inspect .020 5.0
floats-cdfpl/sine_4_true-unreach-call_true-termination.i error (7) 0 wit inspect 51   630 460 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .019 5.0
floats-cdfpl/sine_5_true-unreach-call_true-termination.i error (7) 0 wit inspect 49   650 360 - 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
floats-cdfpl/sine_6_true-unreach-call_true-termination.i error (7) 0 wit inspect 51   640 430 - 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-cdfpl/sine_7_true-unreach-call_true-termination.i error (7) 0 wit inspect 48   640 360 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 41 error (2) 0 wit inspect .018 4.8
floats-cdfpl/sine_8_true-unreach-call_true-termination.i error (7) 0 wit inspect 50   660 400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .019 5.0
floats-cdfpl/square_4_true-unreach-call_true-termination.i error (7) 0 wit inspect 39   370 300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 45 error (2) 0 wit inspect .020 4.8
floats-cdfpl/square_5_true-unreach-call_true-termination.i error (7) 0 wit inspect 31   380 270 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .019 4.8
floats-cdfpl/square_6_true-unreach-call_true-termination.i error (7) 0 wit inspect 34   380 240 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .018 4.8
floats-cdfpl/square_7_true-unreach-call_true-termination.i error (7) 0 wit inspect 32   370 250 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 41 error (2) 0 wit inspect .020 5.0
floats-cdfpl/square_8_true-unreach-call_true-termination.i error (7) 0 wit inspect 42   380 320 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 45 error (2) 0 wit inspect .020 4.8
floats-cbmc-regression/float-div1_true-unreach-call.i error (7) 0 wit inspect 110   560 1100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 41 error (2) 0 wit inspect .019 4.8
floats-cbmc-regression/float-flags-simp1_true-unreach-call.i true 2 wit inspect 17   530 150 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 13    790 true 2 wit inspect 42     700  
floats-cbmc-regression/float-no-simp1_true-unreach-call_true-termination.i true 2 wit inspect 8.7 260 76 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  240 true 2 wit inspect 8.6   230  
floats-cbmc-regression/float-no-simp2_true-unreach-call.i error (7) 0 wit inspect 31   360 420 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 44 error (2) 0 wit inspect .019 4.9
floats-cbmc-regression/float-no-simp3_true-unreach-call_true-termination.i true 2 wit inspect 8.9 260 73 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 8.8   230  
floats-cbmc-regression/float-no-simp4_true-unreach-call.i true 2 wit inspect 17   500 160 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.2  270 true 2 wit inspect 38     580  
floats-cbmc-regression/float-no-simp6_true-unreach-call_true-termination.i true 2 wit inspect 11   340 96 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 11     290  
floats-cbmc-regression/float-no-simp7_true-unreach-call_true-termination.i true 2 wit inspect 9.2 250 77 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 9.1   240  
floats-cbmc-regression/float-no-simp8_true-unreach-call.i true 2 wit inspect 9.7 290 78 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  250 true 2 wit inspect 11     300  
floats-cbmc-regression/float-rounding1_true-unreach-call.i unknown 0 wit inspect 3.7 230 27 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 41 error (2) 0 wit inspect .019 4.9
floats-cbmc-regression/float-to-double1_true-unreach-call.i true 2 wit inspect 17   280 200 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  260 true 2 wit inspect 120     440  
floats-cbmc-regression/float-to-double2_true-unreach-call_true-termination.i true 2 wit inspect 8.7 260 79 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 9.3   250  
floats-cbmc-regression/float-zero-sum1_true-unreach-call_true-termination.i true 2 wit inspect 9.1 250 69 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 10     290  
floats-cbmc-regression/float11_true-unreach-call_true-termination.i true 2 wit inspect 9.7 310 72 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  250 true 2 wit inspect 10     240  
floats-cbmc-regression/float12_true-unreach-call_true-termination.i true 2 wit inspect 14   280 140 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 14     270  
floats-cbmc-regression/float13_true-unreach-call_true-termination.i true 2 wit inspect 11   350 100 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  250 true 2 wit inspect 10     270  
floats-cbmc-regression/float14_true-unreach-call.i true 2 wit inspect 9.9 300 79 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.9  260 true 2 wit inspect 11     310  
floats-cbmc-regression/float18_true-unreach-call.i unknown 0 wit inspect 3.8 230 32 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 41 error (2) 0 wit inspect .019 4.8
floats-cbmc-regression/float19_true-unreach-call.i true 2 wit inspect 9.8 270 84 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.7  260 true 2 wit inspect 11     280  
floats-cbmc-regression/float1_true-unreach-call_true-termination.i true 2 wit inspect 8.4 260 77 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 9.2   240  
floats-cbmc-regression/float20_true-unreach-call_true-termination.i true 2 wit inspect 39   490 370 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  250 true 2 wit inspect 16     400  
floats-cbmc-regression/float21_true-unreach-call.i true 2 wit inspect 63   630 730 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.6  290 true 2 wit inspect 68     600  
floats-cbmc-regression/float22_true-unreach-call_true-termination.i timeout 0 wit inspect 900   1000 9800 - 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/float2_true-unreach-call_true-termination.i true 2 wit inspect 8.9 260 75 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.8  250 true 2 wit inspect 11     270  
floats-cbmc-regression/float3_true-unreach-call_true-termination.i true 2 wit inspect 13   300 120 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  270 true 2 wit inspect 14     330  
floats-cbmc-regression/float4_true-unreach-call.i error (7) 0 wit inspect 64   410 770 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .019 5.0
floats-cbmc-regression/float5_true-unreach-call_true-termination.i true 2 wit inspect 28   280 300 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  260 true 2 wit inspect 24     270  
floats-cbmc-regression/float6_true-unreach-call_true-termination.i true 2 wit inspect 14   470 140 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  250 true 2 wit inspect 8.1   290  
floats-cbmc-regression/float8_true-unreach-call.i true 2 wit inspect 8.4 260 72 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.9  270 true 2 wit inspect 11     290  
floats-cbmc-regression/float_lib1_true-unreach-call.i error (7) 0 wit inspect 9.1 260 70 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 41 error (2) 0 wit inspect .019 5.0
floats-cbmc-regression/float_lib2_true-unreach-call.i true 2 wit inspect 19   570 190 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.6  250 true 2 wit inspect 17     530  
float-benchs/cast_float_ptr_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 11   290 100 true -32 wit inspect 3.2  260 false(unreach-call) 1 wit inspect 13     270   unknown 0 wit inspect 3.3  180 true -32 wit inspect .61   18    - wit inspect - wit inspect
float-benchs/cast_union_loose_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 11   270 97 false(unreach-call) 1 wit inspect 4.2  280 false(unreach-call) 1 wit inspect 11     280   unknown 0 wit inspect 3.5  180 true -32 wit inspect .59   18    - wit inspect - wit inspect
float-benchs/cast_union_tight_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 15   290 140 false(unreach-call) 1 wit inspect 3.2  270 false(unreach-call) 1 wit inspect 11     270   unknown 0 wit inspect 3.5  180 true -32 wit inspect .68   18    - wit inspect - wit inspect
float-benchs/float_int_inv_square_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 11   300 110 false(unreach-call) 1 wit inspect 3.2  270 false(unreach-call) 1 wit inspect 9.8   290   unknown 0 wit inspect 3.2  180 true -32 wit inspect .77   18    - wit inspect - wit inspect
float-benchs/inv_Newton_false-unreach-call.c error (7) 0 wit inspect 64   420 580 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect 1.2  51 error (invalid witness file) 0 wit inspect .0014 .34 - wit inspect - wit inspect
float-benchs/inv_square_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 9.0 280 86 false(unreach-call) 1 wit inspect 3.2  270 false(unreach-call) 1 wit inspect 10     290   unknown 0 wit inspect 2.7  180 true -32 wit inspect .61   18    - wit inspect - wit inspect
float-benchs/nan_double_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 8.1 250 68 false(unreach-call) 1 wit inspect 3.0  260 false(unreach-call) 1 wit inspect 3.2   220   unknown 0 wit inspect 2.7  180 true -32 wit inspect .61   18    - wit inspect - wit inspect
float-benchs/nan_float_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 8.0 250 70 false(unreach-call) 1 wit inspect 3.0  260 false(unreach-call) 1 wit inspect 5.5   220   unknown 0 wit inspect 3.6  190 true -32 wit inspect .58   19    - wit inspect - wit inspect
float-benchs/sin_interpolated_index_false-unreach-call_true-termination.c error (7) 0 wit inspect 32   2500 230 error (invalid witness file) 0 wit inspect .70 41 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .92 50 error (invalid witness file) 0 wit inspect .0016 .27 - wit inspect - wit inspect
float-benchs/sqrt_poly2_false-unreach-call.c error (7) 0 wit inspect 92   700 730 error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .85 49 error (invalid witness file) 0 wit inspect .0017 .26 - wit inspect - wit inspect
float-benchs/Muller_Kahan_true-unreach-call_true-termination.c timeout 0 wit inspect 900   1900 9800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .020 4.9
float-benchs/Rump_double_true-unreach-call_true-termination.c error (7) 0 wit inspect 22   1500 220 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 43 error (2) 0 wit inspect .019 4.9
float-benchs/Rump_float_true-unreach-call_true-termination.c error (7) 0 wit inspect 21   570 130 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .019 4.8
float-benchs/addsub_double_exact_true-unreach-call_true-termination.c true 2 wit inspect 11   280 96 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 9.6   270  
float-benchs/addsub_float_exact_true-unreach-call_true-termination.c true 2 wit inspect 8.9 250 81 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  250 true 2 wit inspect 9.2   260  
float-benchs/addsub_float_inexact_true-unreach-call_true-termination.c true 2 wit inspect 8.8 260 79 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 9.7   250  
float-benchs/arctan_Pade_true-unreach-call_true-termination.c error (7) 0 wit inspect 51   840 340 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .018 4.9
float-benchs/bary_diverge_true-unreach-call_true-termination.c error (7) 0 wit inspect 15   280 140 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 41 error (2) 0 wit inspect .019 4.8
float-benchs/cast_float_union_true-unreach-call.c true 2 wit inspect 4.8 270 35 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 5.2   230  
float-benchs/cos_polynomial_true-unreach-call_true-termination.c error (7) 0 wit inspect 130   960 1000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 45 error (2) 0 wit inspect .018 4.8
float-benchs/divmul_buf_diverge_true-unreach-call_true-termination.c timeout 0 wit inspect 900   4700 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 41 error (2) 0 wit inspect .023 4.8
float-benchs/divmul_diverge_true-unreach-call_true-termination.c timeout 0 wit inspect 900   4800 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .74 46 error (2) 0 wit inspect .019 4.8
float-benchs/drift_tenth_true-unreach-call_true-termination.c timeout 0 wit inspect 900   660 9500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 41 error (2) 0 wit inspect .020 4.8
float-benchs/exp_loop_true-unreach-call.c error (7) 0 wit inspect 430   990 4400 - 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/feedback_diverge_true-unreach-call_true-termination.c timeout 0 wit inspect 900   4900 11000 - 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/filter1_true-unreach-call_true-termination.c error (7) 0 wit inspect 37   380 410 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 41 error (2) 0 wit inspect .019 4.8
float-benchs/filter2_alt_true-unreach-call.c error (7) 0 wit inspect 16   320 170 - 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
float-benchs/filter2_iterated_true-unreach-call.c error (7) 0 wit inspect 18   2200 180 - 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/filter2_reinit_true-unreach-call_true-termination.c error (7) 0 wit inspect 49   430 390 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .019 4.8
float-benchs/filter2_set_true-unreach-call_true-termination.c error (7) 0 wit inspect 30   530 250 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .018 4.9
float-benchs/filter2_true-unreach-call_true-termination.c error (7) 0 wit inspect 29   400 240 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 44 error (2) 0 wit inspect .018 4.8
float-benchs/filter_iir_true-unreach-call.c timeout 0 wit inspect 900   2000 6900 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 44 error (2) 0 wit inspect .023 4.9
float-benchs/float_double_true-unreach-call_true-termination.c true 2 wit inspect 8.6 270 71 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 9.2   240  
float-benchs/image_filter_true-unreach-call.c timeout 0 wit inspect 900   6800 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .021 4.9
float-benchs/interpolation2_true-unreach-call_true-termination.c error (7) 0 wit inspect 64   380 660 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 43 error (2) 0 wit inspect .017 4.8
float-benchs/interpolation_true-unreach-call_true-termination.c error (7) 0 wit inspect 650   760 6900 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .019 4.8
float-benchs/inv_sqrt_Quake_true-unreach-call_true-termination.c error (7) 0 wit inspect 69   340 900 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .018 4.9
float-benchs/inv_square_int_true-unreach-call_true-termination.c true 2 wit inspect 12   300 100 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  260 true 2 wit inspect 15     310  
float-benchs/inv_square_true-unreach-call_true-termination.c true 2 wit inspect 12   290 110 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  260 true 2 wit inspect 52     350  
float-benchs/loop_true-unreach-call.c error (7) 0 wit inspect 70   560 820 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .019 4.8
float-benchs/mea8000_true-unreach-call.c error (7) 0 wit inspect 780   5100 9800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .018 4.8
float-benchs/nan_double_range_true-unreach-call_true-termination.c true 2 wit inspect 8.2 250 65 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 9.3   240  
float-benchs/nan_float_range_true-unreach-call_true-termination.c true 2 wit inspect 8.7 260 80 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 11     250  
float-benchs/rlim_exit_true-unreach-call_true-termination.c timeout 0 wit inspect 900   5700 14000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 41 error (2) 0 wit inspect .018 4.9
float-benchs/rlim_invariant_true-unreach-call_true-termination.c error (7) 0 wit inspect 60   440 700 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 42 error (2) 0 wit inspect .019 4.8
float-benchs/sin_interpolated_bigrange_loose_true-unreach-call_true-termination.c error (7) 0 wit inspect 33   2500 230 - 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
float-benchs/sin_interpolated_bigrange_tight_true-unreach-call_true-termination.c error (7) 0 wit inspect 33   2500 250 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 42 error (2) 0 wit inspect .035 4.9
float-benchs/sin_interpolated_index_true-unreach-call_true-termination.c error (7) 0 wit inspect 38   2500 290 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 45 error (2) 0 wit inspect .018 4.9
float-benchs/sin_interpolated_negation_true-unreach-call.c error (7) 0 wit inspect 22   2500 170 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .019 4.8
float-benchs/sin_interpolated_smallrange_true-unreach-call.c error (7) 0 wit inspect 33   2500 230 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .020 4.8
float-benchs/sqrt_Householder_constant_true-unreach-call.c error (7) 0 wit inspect 94   1500 830 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 41 error (2) 0 wit inspect .019 4.9
float-benchs/sqrt_Householder_interval_true-unreach-call.c error (7) 0 wit inspect 78   1600 690 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .018 4.8
float-benchs/sqrt_Householder_pseudoconstant_true-unreach-call.c error (7) 0 wit inspect 78   1700 550 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 44 error (2) 0 wit inspect .019 4.8
float-benchs/sqrt_Newton_pseudoconstant_true-unreach-call.c error (7) 0 wit inspect 99   1800 1000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 44 error (2) 0 wit inspect .020 5.0
float-benchs/sqrt_biNewton_pseudoconstant_true-unreach-call.c error (7) 0 wit inspect 100   1800 1100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .019 4.8
float-benchs/sqrt_poly_true-unreach-call_true-termination.c error (7) 0 wit inspect 94   820 670 - 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/water_pid_true-unreach-call_true-termination.c error (7) 0 wit inspect 71   1500 540 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 41 error (2) 0 wit inspect .019 4.9
float-benchs/zonotope_2_true-unreach-call_true-termination.c error (7) 0 wit inspect 200   580 1900 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .41 43 error (2) 0 wit inspect .018 5.0
float-benchs/zonotope_3_true-unreach-call_true-termination.c timeout 0 wit inspect 900   5200 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .018 4.8
float-benchs/zonotope_loose_true-unreach-call_true-termination.c error (7) 0 wit inspect 74   760 760 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 43 error (2) 0 wit inspect .019 4.9
float-benchs/zonotope_tight_true-unreach-call_true-termination.c error (7) 0 wit inspect 72   740 660 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 42 error (2) 0 wit inspect .019 5.0
floats-esbmc-regression/Double_div_true-unreach-call.i error (7) 0 wit inspect 51   890 560 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 46 error (2) 0 wit inspect .019 4.9
floats-esbmc-regression/Float_div_true-unreach-call.i error (7) 0 wit inspect 84   530 800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .021 5.0
floats-esbmc-regression/ceil_nondet_true-unreach-call.i unknown 0 wit inspect 7.5 230 56 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .019 4.8
floats-esbmc-regression/ceil_true-unreach-call.i unknown 0 wit inspect 3.9 230 29 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 42 error (2) 0 wit inspect .019 4.9
floats-esbmc-regression/copysign_true-unreach-call.i unknown 0 wit inspect 3.6 230 31 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 41 error (2) 0 wit inspect .020 4.9
floats-esbmc-regression/digits_for_true-unreach-call.i error (7) 0 wit inspect 86   540 640 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 41 error (2) 0 wit inspect .019 5.0
floats-esbmc-regression/digits_while_true-unreach-call.i error (7) 0 wit inspect 89   520 930 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 46 error (2) 0 wit inspect .018 4.8
floats-esbmc-regression/fabs_true-unreach-call.i true 2 wit inspect 8.6 270 77 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  250 true 2 wit inspect 10     280  
floats-esbmc-regression/fdim_true-unreach-call.i unknown 0 wit inspect 3.7 230 29 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 43 error (2) 0 wit inspect .018 4.8
floats-esbmc-regression/floor_nondet_true-unreach-call.i unknown 0 wit inspect 7.4 230 61 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .40 43 error (2) 0 wit inspect .019 4.9
floats-esbmc-regression/floor_true-unreach-call.i unknown 0 wit inspect 3.5 220 32 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 43 error (2) 0 wit inspect .019 4.9
floats-esbmc-regression/fmax_true-unreach-call.i true 2 wit inspect 8.4 260 69 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.7  250 true 2 wit inspect 9.0   270  
floats-esbmc-regression/fmin_true-unreach-call.i true 2 wit inspect 8.4 260 69 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.7  260 true 2 wit inspect 8.9   280  
floats-esbmc-regression/fmod2_true-unreach-call.i unknown 0 wit inspect 7.2 230 59 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .020 4.9
floats-esbmc-regression/fmod3_true-unreach-call.i unknown 0 wit inspect 7.4 230 70 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .018 4.9
floats-esbmc-regression/fmod_true-unreach-call.i unknown 0 wit inspect 3.8 230 29 - wit