Tool ULTIMATE Automizer 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]
Date of execution 2017-12-02 01:06:24 CET 2017-12-03 03:07:09 CET 2017-12-03 03:49:57 CET 2017-12-03 03:57:59 CET 2017-12-03 04:29:07 CET 2017-12-02 23:12:02 CET 2017-12-03 03:11:19 CET
Run set uautomizer.sv-comp18.ReachSafety-Floats cpa-seq-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.ReachSafety-Floats uautomizer-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.ReachSafety-Floats cpa-witness2test-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.ReachSafety-Floats fshell-witness2test-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.ReachSafety-Floats cpa-seq-validate-correctness-witnesses-uautomizer.sv-comp18-correctness-witness.ReachSafety-Floats uautomizer-validate-correctness-witnesses-uautomizer.sv-comp18-correctness-witness.ReachSafety-Floats
Options --full-output -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/uautomizer.2017-12-02_0106.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/uautomizer.2017-12-02_0106.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/uautomizer.2017-12-02_0106.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/uautomizer.2017-12-02_0106.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/uautomizer.2017-12-02_0106.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/uautomizer.2017-12-02_0106.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 43   690 390 false(unreach-call) 1 wit inspect 81    360 false(unreach-call) 1 wit inspect 43     690   unknown 0 wit inspect 2.9  180 true -32 wit inspect .73   18    - wit inspect - wit inspect
floats-cdfpl/newton_1_5_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 120   740 1100 false(unreach-call) 1 wit inspect 64    370 timeout 0 wit inspect 97     690   unknown 0 wit inspect 3.5  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 20   680 180 false(unreach-call) 1 wit inspect 43    370 false(unreach-call) 1 wit inspect 21     670   unknown 0 wit inspect 3.9  210 true -32 wit inspect .71   18    - wit inspect - wit inspect
floats-cdfpl/newton_1_7_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 40   690 280 false(unreach-call) 1 wit inspect 28    360 false(unreach-call) 1 wit inspect 44     680   unknown 0 wit inspect 3.0  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 27   680 230 false(unreach-call) 1 wit inspect 18    360 false(unreach-call) 1 wit inspect 30     670   unknown 0 wit inspect 2.9  210 true -32 wit inspect .68   18    - wit inspect - wit inspect
floats-cdfpl/newton_2_6_false-unreach-call_true-termination.i timeout 0 wit inspect 900   1100 7200 error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .020 5.0 error (invalid witness file) 0 wit inspect .86 49 error (invalid witness file) 0 wit inspect .0016 .31 - wit inspect - wit inspect
floats-cdfpl/newton_2_7_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 130   860 1000 timeout 0 wit inspect 92    450 timeout 0 wit inspect 97     820   unknown 0 wit inspect 3.5  210 true -32 wit inspect .60   18    - wit inspect - wit inspect
floats-cdfpl/newton_2_8_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 27   840 240 false(unreach-call) 1 wit inspect 51    460 false(unreach-call) 1 wit inspect 29     820   unknown 0 wit inspect 3.4  180 true -32 wit inspect .78   18    - wit inspect - wit inspect
floats-cdfpl/newton_3_6_false-unreach-call_true-termination.i timeout 0 wit inspect 900   1000 8700 error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect 1.0  49 error (invalid witness file) 0 wit inspect .0015 .26 - wit inspect - wit inspect
floats-cdfpl/newton_3_7_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 160   920 1200 timeout 0 wit inspect 91    560 timeout 0 wit inspect 97     870   unknown 0 wit inspect 3.7  180 true -32 wit inspect .62   18    - wit inspect - wit inspect
floats-cdfpl/newton_3_8_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 260   990 1700 timeout 0 wit inspect 91    570 timeout 0 wit inspect 97     930   unknown 0 wit inspect 2.9  190 true -32 wit inspect .59   18    - wit inspect - wit inspect
floats-cdfpl/sine_1_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 19   570 170 timeout 0 wit inspect 91    360 false(unreach-call) 1 wit inspect 22     570   unknown 0 wit inspect 3.0  180 true -32 wit inspect .80   18    - wit inspect - wit inspect
floats-cdfpl/sine_2_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 23   570 240 false(unreach-call) 1 wit inspect 65    330 false(unreach-call) 1 wit inspect 28     550   unknown 0 wit inspect 3.5  180 true -32 wit inspect .63   18    - wit inspect - wit inspect
floats-cdfpl/sine_3_false-unreach-call_true-termination.i timeout 0 wit inspect 900   870 6300 error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .81 47 error (invalid witness file) 0 wit inspect .0014 .26 - wit inspect - wit inspect
floats-cdfpl/square_1_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 160   500 1300 unknown 0 wit inspect 8.5  300 timeout 0 wit inspect 97     450   unknown 0 wit inspect 3.4  180 true -32 wit inspect .80   18    - wit inspect - wit inspect
floats-cdfpl/square_2_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 81   430 620 unknown 0 wit inspect 6.3  300 timeout 0 wit inspect 97     410   unknown 0 wit inspect 2.6  180 true -32 wit inspect .77   18    - wit inspect - wit inspect
floats-cdfpl/square_3_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 820   930 5800 unknown 0 wit inspect 7.5  310 timeout 0 wit inspect 97     430   unknown 0 wit inspect 3.5  180 true -32 wit inspect .81   18    - wit inspect - wit inspect
floats-cdfpl/newton_1_1_true-unreach-call_true-termination.i timeout 0 wit inspect 900   1100 5700 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 41 error (2) 0 wit inspect .018 4.9
floats-cdfpl/newton_1_2_true-unreach-call_true-termination.i timeout 0 wit inspect 900   1000 6600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 43 error (2) 0 wit inspect .020 4.9
floats-cdfpl/newton_1_3_true-unreach-call_true-termination.i timeout 0 wit inspect 900   930 5500 - 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/newton_2_1_true-unreach-call_true-termination.i timeout 0 wit inspect 900   1000 8000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 43 error (2) 0 wit inspect .019 5.0
floats-cdfpl/newton_2_2_true-unreach-call_true-termination.i timeout 0 wit inspect 900   1000 6400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 42 error (2) 0 wit inspect .019 4.8
floats-cdfpl/newton_2_3_true-unreach-call_true-termination.i timeout 0 wit inspect 900   950 5800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .020 4.9
floats-cdfpl/newton_2_4_true-unreach-call_true-termination.i timeout 0 wit inspect 900   1000 6100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 43 error (2) 0 wit inspect .018 4.9
floats-cdfpl/newton_2_5_true-unreach-call_true-termination.i timeout 0 wit inspect 900   1000 6700 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 42 error (2) 0 wit inspect .024 4.8
floats-cdfpl/newton_3_1_true-unreach-call_true-termination.i timeout 0 wit inspect 900   1100 6000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .021 4.9
floats-cdfpl/newton_3_2_true-unreach-call_true-termination.i timeout 0 wit inspect 900   1100 7800 - 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_3_true-unreach-call_true-termination.i timeout 0 wit inspect 900   1200 6000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .024 5.0
floats-cdfpl/newton_3_4_true-unreach-call_true-termination.i timeout 0 wit inspect 900   1100 5800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .018 4.8
floats-cdfpl/newton_3_5_true-unreach-call_true-termination.i timeout 0 wit inspect 900   1100 6600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 42 error (2) 0 wit inspect .020 4.9
floats-cdfpl/sine_4_true-unreach-call_true-termination.i timeout 0 wit inspect 900   860 6700 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 44 error (2) 0 wit inspect .019 4.9
floats-cdfpl/sine_5_true-unreach-call_true-termination.i timeout 0 wit inspect 900   930 6200 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .019 4.8
floats-cdfpl/sine_6_true-unreach-call_true-termination.i timeout 0 wit inspect 900   840 6200 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .018 4.8
floats-cdfpl/sine_7_true-unreach-call_true-termination.i timeout 0 wit inspect 900   810 6700 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .020 4.9
floats-cdfpl/sine_8_true-unreach-call_true-termination.i timeout 0 wit inspect 900   860 7500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 45 error (2) 0 wit inspect .018 4.8
floats-cdfpl/square_4_true-unreach-call_true-termination.i true 2 wit inspect 610   820 5800 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 670    570 true 2 wit inspect 720     700  
floats-cdfpl/square_5_true-unreach-call_true-termination.i true 2 wit inspect 450   780 3500 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 510    510 true 2 wit inspect 470     740  
floats-cdfpl/square_6_true-unreach-call_true-termination.i true 2 wit inspect 330   840 2400 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 300    500 true 2 wit inspect 370     780  
floats-cdfpl/square_7_true-unreach-call_true-termination.i true 2 wit inspect 150   720 1300 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    480 true 2 wit inspect 190     710  
floats-cdfpl/square_8_true-unreach-call_true-termination.i true 2 wit inspect 110   630 820 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 70    360 true 2 wit inspect 120     620  
floats-cbmc-regression/float-div1_true-unreach-call.i true 2 wit inspect 31   670 310 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.9  320 true 2 wit inspect 35     600  
floats-cbmc-regression/float-flags-simp1_true-unreach-call.i true 2 wit inspect 27   700 260 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 10    800 true 2 wit inspect 35     700  
floats-cbmc-regression/float-no-simp1_true-unreach-call_true-termination.i true 2 wit inspect 8.5 280 63 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  250 true 2 wit inspect 8.9   230  
floats-cbmc-regression/float-no-simp2_true-unreach-call.i true 2 wit inspect 40   440 460 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 20    300 true 2 wit inspect 43     390  
floats-cbmc-regression/float-no-simp3_true-unreach-call_true-termination.i true 2 wit inspect 8.4 270 73 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  250 true 2 wit inspect 11     230  
floats-cbmc-regression/float-no-simp4_true-unreach-call.i true 2 wit inspect 31   550 340 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.9  270 true 2 wit inspect 39     570  
floats-cbmc-regression/float-no-simp6_true-unreach-call_true-termination.i true 2 wit inspect 9.3 300 85 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 10     290  
floats-cbmc-regression/float-no-simp7_true-unreach-call_true-termination.i true 2 wit inspect 8.5 290 68 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  250 true 2 wit inspect 9.5   250  
floats-cbmc-regression/float-no-simp8_true-unreach-call.i true 2 wit inspect 9.1 310 70 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  260 true 2 wit inspect 7.2   300  
floats-cbmc-regression/float-rounding1_true-unreach-call.i unknown 0 wit inspect 3.7 220 30 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 42 error (2) 0 wit inspect .019 4.8
floats-cbmc-regression/float-to-double1_true-unreach-call.i true 2 wit inspect 100   510 1200 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  260 true 2 wit inspect 270     540  
floats-cbmc-regression/float-to-double2_true-unreach-call_true-termination.i true 2 wit inspect 8.2 280 63 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  260 true 2 wit inspect 8.8   230  
floats-cbmc-regression/float-zero-sum1_true-unreach-call_true-termination.i true 2 wit inspect 9.8 300 76 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 7.7   290  
floats-cbmc-regression/float11_true-unreach-call_true-termination.i true 2 wit inspect 8.8 280 72 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  250 true 2 wit inspect 10     250  
floats-cbmc-regression/float12_true-unreach-call_true-termination.i true 2 wit inspect 13   310 150 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 15     260  
floats-cbmc-regression/float13_true-unreach-call_true-termination.i true 2 wit inspect 9.2 290 82 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 12     270  
floats-cbmc-regression/float14_true-unreach-call.i true 2 wit inspect 9.3 300 84 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.2  250 true 2 wit inspect 9.9   290  
floats-cbmc-regression/float18_true-unreach-call.i unknown 0 wit inspect 3.7 220 29 - 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
floats-cbmc-regression/float19_true-unreach-call.i true 2 wit inspect 10   290 97 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  260 true 2 wit inspect 10     280  
floats-cbmc-regression/float1_true-unreach-call_true-termination.i true 2 wit inspect 8.6 280 78 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  250 true 2 wit inspect 9.2   230  
floats-cbmc-regression/float20_true-unreach-call_true-termination.i true 2 wit inspect 14   390 120 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 16     400  
floats-cbmc-regression/float21_true-unreach-call.i true 2 wit inspect 68   580 740 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.0  300 true 2 wit inspect 83     620  
floats-cbmc-regression/float22_true-unreach-call_true-termination.i true 2 wit inspect 280   1100 2900 - wit inspect - wit inspect - wit inspect - wit inspect false(unreach-call) -16 wit inspect 6.4  280 true 2 wit inspect 310     1100  
floats-cbmc-regression/float2_true-unreach-call_true-termination.i true 2 wit inspect 8.8 300 67 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 10     270  
floats-cbmc-regression/float3_true-unreach-call_true-termination.i true 2 wit inspect 12   350 110 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  270 true 2 wit inspect 14     340  
floats-cbmc-regression/float4_true-unreach-call.i true 2 wit inspect 74   490 960 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 78    330 true 2 wit inspect 80     440  
floats-cbmc-regression/float5_true-unreach-call_true-termination.i true 2 wit inspect 21   320 230 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  260 true 2 wit inspect 25     270  
floats-cbmc-regression/float6_true-unreach-call_true-termination.i true 2 wit inspect 9.5 300 79 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.4  260 true 2 wit inspect 11     290  
floats-cbmc-regression/float8_true-unreach-call.i true 2 wit inspect 10   310 82 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.6  270 true 2 wit inspect 8.0   310  
floats-cbmc-regression/float_lib1_true-unreach-call.i error (7) 0 wit inspect 8.1 250 68 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 44 error (2) 0 wit inspect .021 5.0
floats-cbmc-regression/float_lib2_true-unreach-call.i true 2 wit inspect 13   490 120 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4  250 true 2 wit inspect 20     530  
float-benchs/cast_float_ptr_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 9.1 270 77 false(unreach-call) 1 wit inspect 3.3  270 false(unreach-call) 1 wit inspect 7.4   270   unknown 0 wit inspect 2.7  210 true -32 wit inspect .78   18    - wit inspect - wit inspect
float-benchs/cast_union_loose_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 9.2 280 87 false(unreach-call) 1 wit inspect 4.4  270 false(unreach-call) 1 wit inspect 11     280   unknown 0 wit inspect 3.4  210 true -32 wit inspect .79   18    - wit inspect - wit inspect
float-benchs/cast_union_tight_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 9.4 290 87 false(unreach-call) 1 wit inspect 3.2  270 false(unreach-call) 1 wit inspect 11     290   unknown 0 wit inspect 3.6  210 true -32 wit inspect .78   18    - wit inspect - wit inspect
float-benchs/float_int_inv_square_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 8.6 310 67 false(unreach-call) 1 wit inspect 3.8  270 false(unreach-call) 1 wit inspect 12     280   unknown 0 wit inspect 3.6  190 true -32 wit inspect .75   18    - wit inspect - wit inspect
float-benchs/inv_Newton_false-unreach-call.c timeout 0 wit inspect 900   1800 5800 error (invalid witness file) 0 wit inspect .50 41 error (2) 0 wit inspect .021 4.8 error (invalid witness file) 0 wit inspect .87 49 error (invalid witness file) 0 wit inspect .0018 .26 - wit inspect - wit inspect
float-benchs/inv_square_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 8.5 310 70 false(unreach-call) 1 wit inspect 3.0  270 false(unreach-call) 1 wit inspect 11     300   unknown 0 wit inspect 3.3  190 true -32 wit inspect .59   18    - wit inspect - wit inspect
float-benchs/nan_double_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 4.1 240 34 false(unreach-call) 1 wit inspect 3.8  260 false(unreach-call) 1 wit inspect 5.4   220   unknown 0 wit inspect 3.1  180 true -32 wit inspect .74   18    - wit inspect - wit inspect
float-benchs/nan_float_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 4.0 240 31 false(unreach-call) 1 wit inspect 4.2  260 false(unreach-call) 1 wit inspect 2.9   220   unknown 0 wit inspect 2.8  180 true -32 wit inspect .65   18    - wit inspect - wit inspect
float-benchs/sin_interpolated_index_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 370   2100 4100 false(unreach-call) 1 wit inspect 8.2  360 timeout 0 wit inspect 97     1100   unknown 0 wit inspect 3.0  210 true -32 wit inspect .61   18    - wit inspect - wit inspect
float-benchs/sqrt_poly2_false-unreach-call.c false(unreach-call) 1 wit inspect 15   600 120 false(unreach-call) 1 wit inspect 8.2  410 false(unreach-call) 1 wit inspect 20     600   unknown 0 wit inspect 3.2  190 true -32 wit inspect .62   19    - wit inspect - wit inspect
float-benchs/Muller_Kahan_true-unreach-call_true-termination.c timeout 0 wit inspect 900   3400 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .018 4.8
float-benchs/Rump_double_true-unreach-call_true-termination.c true 2 wit inspect 19   1000 200 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 23     990  
float-benchs/Rump_float_true-unreach-call_true-termination.c true 2 wit inspect 11   440 100 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 12     420  
float-benchs/addsub_double_exact_true-unreach-call_true-termination.c true 2 wit inspect 8.9 290 81 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 9.6   280  
float-benchs/addsub_float_exact_true-unreach-call_true-termination.c true 2 wit inspect 8.9 290 69 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 9.6   240  
float-benchs/addsub_float_inexact_true-unreach-call_true-termination.c true 2 wit inspect 8.7 290 69 - 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 140   2700 1200 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .019 4.9
float-benchs/bary_diverge_true-unreach-call_true-termination.c timeout 0 wit inspect 900   3100 9600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 41 error (2) 0 wit inspect .020 4.9
float-benchs/cast_float_union_true-unreach-call.c true 2 wit inspect 4.1 240 37 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  250 true 2 wit inspect 5.2   230  
float-benchs/cos_polynomial_true-unreach-call_true-termination.c timeout 0 wit inspect 900   2900 6600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .019 4.9
float-benchs/divmul_buf_diverge_true-unreach-call_true-termination.c timeout 0 wit inspect 900   5400 11000 - 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
float-benchs/divmul_diverge_true-unreach-call_true-termination.c timeout 0 wit inspect 900   5400 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .72 41 error (2) 0 wit inspect .019 4.8
float-benchs/drift_tenth_true-unreach-call_true-termination.c error (7) 0 wit inspect 770   850 7900 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 43 error (2) 0 wit inspect .025 5.0
float-benchs/exp_loop_true-unreach-call.c timeout 0 wit inspect 900   1300 8600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 41 error (2) 0 wit inspect .019 4.9
float-benchs/feedback_diverge_true-unreach-call_true-termination.c timeout 0 wit inspect 900   5300 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .018 4.8
float-benchs/filter1_true-unreach-call_true-termination.c error (7) 0 wit inspect 530   1400 4200 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 42 error (2) 0 wit inspect .021 4.8
float-benchs/filter2_alt_true-unreach-call.c timeout 0 wit inspect 900   1300 9600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 43 error (2) 0 wit inspect .020 4.9
float-benchs/filter2_iterated_true-unreach-call.c error (7) 0 wit inspect 35   2200 370 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .024 4.8
float-benchs/filter2_reinit_true-unreach-call_true-termination.c timeout 0 wit inspect 900   2000 7400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 46 error (2) 0 wit inspect .018 4.9
float-benchs/filter2_set_true-unreach-call_true-termination.c error (7) 0 wit inspect 400   3400 4200 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 42 error (2) 0 wit inspect .017 4.9
float-benchs/filter2_true-unreach-call_true-termination.c timeout 0 wit inspect 900   2100 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .023 5.0
float-benchs/filter_iir_true-unreach-call.c timeout 0 wit inspect 900   1500 8200 - 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/float_double_true-unreach-call_true-termination.c true 2 wit inspect 8.6 280 73 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 9.5   250  
float-benchs/image_filter_true-unreach-call.c timeout 0 wit inspect 900   6900 8400 - 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/interpolation2_true-unreach-call_true-termination.c timeout 0 wit inspect 900   760 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .022 4.8
float-benchs/interpolation_true-unreach-call_true-termination.c timeout 0 wit inspect 900   930 8500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .019 5.0
float-benchs/inv_sqrt_Quake_true-unreach-call_true-termination.c error (7) 0 wit inspect 150   2400 1400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .020 5.0
float-benchs/inv_square_int_true-unreach-call_true-termination.c true 2 wit inspect 33   390 380 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  260 true 2 wit inspect 16     310  
float-benchs/inv_square_true-unreach-call_true-termination.c true 2 wit inspect 61   400 710 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3  260 true 2 wit inspect 56     350  
float-benchs/loop_true-unreach-call.c timeout 0 wit inspect 900   1100 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .020 4.9
float-benchs/mea8000_true-unreach-call.c timeout 0 wit inspect 900   5600 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 42 error (2) 0 wit inspect .020 4.9
float-benchs/nan_double_range_true-unreach-call_true-termination.c true 2 wit inspect 8.9 290 68 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  250 true 2 wit inspect 10     250  
float-benchs/nan_float_range_true-unreach-call_true-termination.c true 2 wit inspect 10   300 91 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  250 true 2 wit inspect 11     250  
float-benchs/rlim_exit_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 .52 41 error (2) 0 wit inspect .023 4.9
float-benchs/rlim_invariant_true-unreach-call_true-termination.c error (7) 0 wit inspect 770   910 8400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .018 5.0
float-benchs/sin_interpolated_bigrange_loose_true-unreach-call_true-termination.c timeout 0 wit inspect 900   2400 5300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .41 44 error (2) 0 wit inspect .019 4.9
float-benchs/sin_interpolated_bigrange_tight_true-unreach-call_true-termination.c timeout 0 wit inspect 900   2200 6000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 45 error (2) 0 wit inspect .018 4.8
float-benchs/sin_interpolated_index_true-unreach-call_true-termination.c timeout 0 wit inspect 900   2200 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 44 error (2) 0 wit inspect .022 4.9
float-benchs/sin_interpolated_negation_true-unreach-call.c timeout 0 wit inspect 900   2600 5500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .025 4.9
float-benchs/sin_interpolated_smallrange_true-unreach-call.c timeout 0 wit inspect 900   2300 5500 - 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/sqrt_Householder_constant_true-unreach-call.c error (7) 0 wit inspect 250   3100 2100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 42 error (2) 0 wit inspect .020 4.9
float-benchs/sqrt_Householder_interval_true-unreach-call.c error (7) 0 wit inspect 150   2800 1500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .018 4.9
float-benchs/sqrt_Householder_pseudoconstant_true-unreach-call.c error (7) 0 wit inspect 90   2600 760 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 41 error (2) 0 wit inspect .019 4.9
float-benchs/sqrt_Newton_pseudoconstant_true-unreach-call.c error (7) 0 wit inspect 87   2600 910 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .018 5.0
float-benchs/sqrt_biNewton_pseudoconstant_true-unreach-call.c error (7) 0 wit inspect 84   2600 870 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 42 error (2) 0 wit inspect .019 4.8
float-benchs/sqrt_poly_true-unreach-call_true-termination.c true 2 wit inspect 240   1800 1700 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 45    500 true 2 wit inspect 140     1100  
float-benchs/water_pid_true-unreach-call_true-termination.c error (7) 0 wit inspect 160   3000 1400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .024 4.9
float-benchs/zonotope_2_true-unreach-call_true-termination.c timeout 0 wit inspect 900   2800 7700 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 43 error (2) 0 wit inspect .018 4.8
float-benchs/zonotope_3_true-unreach-call_true-termination.c timeout 0 wit inspect 900   5400 14000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 44 error (2) 0 wit inspect .020 4.9
float-benchs/zonotope_loose_true-unreach-call_true-termination.c true 2 wit inspect 190   1500 1800 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  310 true 2 wit inspect 130     930  
float-benchs/zonotope_tight_true-unreach-call_true-termination.c true 2 wit inspect 170   1300 1300 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3  310 true 2 wit inspect 130     930  
floats-esbmc-regression/Double_div_true-unreach-call.i error (7) 0 wit inspect 290   2700 2200 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .021 4.8
floats-esbmc-regression/Float_div_true-unreach-call.i error (7) 0 wit inspect 190   600 1600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .018 4.9
floats-esbmc-regression/ceil_nondet_true-unreach-call.i unknown 0 wit inspect 7.5 230 64 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .022 5.0
floats-esbmc-regression/ceil_true-unreach-call.i unknown 0 wit inspect 3.8 220 29 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .020 4.9
floats-esbmc-regression/copysign_true-unreach-call.i unknown 0 wit inspect 3.7 220 31 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 45 error (2) 0 wit inspect .018 4.8
floats-esbmc-regression/digits_for_true-unreach-call.i timeout 0 wit inspect 900   3200 7000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 41 error (2) 0 wit inspect .024 4.9
floats-esbmc-regression/digits_while_true-unreach-call.i timeout 0 wit inspect 900   3100 7000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .018 4.9
floats-esbmc-regression/fabs_true-unreach-call.i true 2 wit inspect 9.5 310 72 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.9  250 true 2 wit inspect 10     280  
floats-esbmc-regression/fdim_true-unreach-call.i unknown 0 wit inspect 3.6 220 27 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 42 error (2) 0 wit inspect .024 4.8
floats-esbmc-regression/floor_nondet_true-unreach-call.i unknown 0 wit inspect 7.5 230 63 - 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-esbmc-regression/floor_true-unreach-call.i unknown 0 wit inspect 3.7 220 32 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .019 4.9
floats-esbmc-regression/fmax_true-unreach-call.i true 2 wit inspect 8.5 290 66 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  250 true 2 wit inspect 8.9   270  
floats-esbmc-regression/fmin_true-unreach-call.i true 2 wit inspect 8.6 290 72 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  250 true 2 wit inspect 11     260  
floats-esbmc-regression/fmod2_true-unreach-call.i unknown 0 wit inspect 7.5 230 62 - wit inspect - wit inspect - wit