Tool ULTIMATE Taipan 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 17:23:13 CET 2017-12-03 07:22:17 CET 2017-12-03 07:45:29 CET 2017-12-03 07:47:53 CET 2017-12-03 07:50:34 CET 2017-12-03 06:47:45 CET 2017-12-03 07:25:40 CET
Run set utaipan.sv-comp18.ReachSafety-Floats cpa-seq-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.ReachSafety-Floats uautomizer-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.ReachSafety-Floats cpa-witness2test-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.ReachSafety-Floats fshell-witness2test-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.ReachSafety-Floats cpa-seq-validate-correctness-witnesses-utaipan.sv-comp18-correctness-witness.ReachSafety-Floats uautomizer-validate-correctness-witnesses-utaipan.sv-comp18-correctness-witness.ReachSafety-Floats
Options --full-output -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/utaipan.2017-12-02_1723.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/utaipan.2017-12-02_1723.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/utaipan.2017-12-02_1723.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/utaipan.2017-12-02_1723.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/utaipan.2017-12-02_1723.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/utaipan.2017-12-02_1723.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   700 320 false(unreach-call) 1 wit inspect 77    360 false(unreach-call) 1 wit inspect 40     680   unknown 0 wit inspect 2.8  210 true -32 wit inspect .57   18    - wit inspect - wit inspect
floats-cdfpl/newton_1_5_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 120   720 1100 false(unreach-call) 1 wit inspect 56    370 timeout 0 wit inspect 97     700   unknown 0 wit inspect 2.7  180 true -32 wit inspect .58   19    - wit inspect - wit inspect
floats-cdfpl/newton_1_6_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 20   680 170 false(unreach-call) 1 wit inspect 49    360 false(unreach-call) 1 wit inspect 20     670   unknown 0 wit inspect 2.7  180 true -32 wit inspect .57   18    - wit inspect - wit inspect
floats-cdfpl/newton_1_7_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 40   700 400 false(unreach-call) 1 wit inspect 22    360 false(unreach-call) 1 wit inspect 44     690   unknown 0 wit inspect 2.7  180 true -32 wit inspect .58   18    - wit inspect - wit inspect
floats-cdfpl/newton_1_8_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 26   690 270 false(unreach-call) 1 wit inspect 16    360 false(unreach-call) 1 wit inspect 27     670   unknown 0 wit inspect 2.7  180 true -32 wit inspect .60   18    - wit inspect - wit inspect
floats-cdfpl/newton_2_6_false-unreach-call_true-termination.i timeout 0 wit inspect 900   1100 6400 error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .040 4.9 error (invalid witness file) 0 wit inspect .83 47 error (invalid witness file) 0 wit inspect .0041 .34 - wit inspect - wit inspect
floats-cdfpl/newton_2_7_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 130   860 1000 false(unreach-call) 1 wit inspect 88    460 timeout 0 wit inspect 97     830   unknown 0 wit inspect 2.7  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 28   830 240 false(unreach-call) 1 wit inspect 43    460 false(unreach-call) 1 wit inspect 28     820   unknown 0 wit inspect 2.6  210 true -32 wit inspect .57   18    - wit inspect - wit inspect
floats-cdfpl/newton_3_6_false-unreach-call_true-termination.i timeout 0 wit inspect 900   1000 6000 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .048 4.8 error (invalid witness file) 0 wit inspect .87 50 error (invalid witness file) 0 wit inspect .0011 .32 - wit inspect - wit inspect
floats-cdfpl/newton_3_7_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 160   930 1200 timeout 0 wit inspect 91    560 timeout 0 wit inspect 97     880   unknown 0 wit inspect 2.8  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) 0 wit inspect 260   1000 1800 timeout 0 wit inspect 91    560 timeout 0 wit inspect 97     920   unknown 0 wit inspect 2.8  180 true -32 wit inspect .57   18    - wit inspect - wit inspect
floats-cdfpl/sine_1_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 19   580 170 timeout 0 wit inspect 91    380 false(unreach-call) 1 wit inspect 19     550   unknown 0 wit inspect 2.7  180 true -32 wit inspect .57   18    - wit inspect - wit inspect
floats-cdfpl/sine_2_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 23   570 230 false(unreach-call) 1 wit inspect 46    340 false(unreach-call) 1 wit inspect 24     560   unknown 0 wit inspect 2.7  180 true -32 wit inspect .60   18    - wit inspect - wit inspect
floats-cdfpl/sine_3_false-unreach-call_true-termination.i timeout 0 wit inspect 900   900 7100 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .025 4.8 error (invalid witness file) 0 wit inspect .82 50 error (invalid witness file) 0 wit inspect .0037 .35 - wit inspect - wit inspect
floats-cdfpl/square_1_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 160   500 1400 unknown 0 wit inspect 5.5  310 timeout 0 wit inspect 97     460   unknown 0 wit inspect 2.6  210 true -32 wit inspect .57   18    - wit inspect - wit inspect
floats-cdfpl/square_2_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 77   440 890 unknown 0 wit inspect 5.3  300 false(unreach-call) 1 wit inspect 89     430   unknown 0 wit inspect 2.9  180 true -32 wit inspect .61   18    - wit inspect - wit inspect
floats-cdfpl/square_3_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 830   930 6600 unknown 0 wit inspect 5.5  310 timeout 0 wit inspect 97     440   unknown 0 wit inspect 2.7  190 true -32 wit inspect .60   18    - wit inspect - wit inspect
floats-cdfpl/newton_1_1_true-unreach-call_true-termination.i timeout 0 wit inspect 900   1100 5600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .024 4.8
floats-cdfpl/newton_1_2_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 .67 42 error (2) 0 wit inspect .020 4.8
floats-cdfpl/newton_1_3_true-unreach-call_true-termination.i timeout 0 wit inspect 900   920 6000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .49 41 error (2) 0 wit inspect .024 4.9
floats-cdfpl/newton_2_1_true-unreach-call_true-termination.i timeout 0 wit inspect 900   1000 7500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .018 4.8
floats-cdfpl/newton_2_2_true-unreach-call_true-termination.i timeout 0 wit inspect 900   1000 5300 - 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_2_3_true-unreach-call_true-termination.i timeout 0 wit inspect 900   980 6100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 45 error (2) 0 wit inspect .027 4.8
floats-cdfpl/newton_2_4_true-unreach-call_true-termination.i timeout 0 wit inspect 900   1000 7000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 43 error (2) 0 wit inspect .025 4.8
floats-cdfpl/newton_2_5_true-unreach-call_true-termination.i timeout 0 wit inspect 900   1000 7900 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .048 4.9
floats-cdfpl/newton_3_1_true-unreach-call_true-termination.i timeout 0 wit inspect 900   1100 6800 - 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
floats-cdfpl/newton_3_2_true-unreach-call_true-termination.i timeout 0 wit inspect 900   1100 5600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 43 error (2) 0 wit inspect .023 5.0
floats-cdfpl/newton_3_3_true-unreach-call_true-termination.i timeout 0 wit inspect 900   1200 6800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 42 error (2) 0 wit inspect .018 4.8
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 .67 41 error (2) 0 wit inspect .020 4.8
floats-cdfpl/newton_3_5_true-unreach-call_true-termination.i timeout 0 wit inspect 900   1100 6200 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 45 error (2) 0 wit inspect .050 4.8
floats-cdfpl/sine_4_true-unreach-call_true-termination.i timeout 0 wit inspect 900   870 5600 - 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_5_true-unreach-call_true-termination.i timeout 0 wit inspect 900   980 8600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 41 error (2) 0 wit inspect .036 4.9
floats-cdfpl/sine_6_true-unreach-call_true-termination.i timeout 0 wit inspect 900   840 6100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 44 error (2) 0 wit inspect .049 5.0
floats-cdfpl/sine_7_true-unreach-call_true-termination.i timeout 0 wit inspect 900   800 7100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .050 4.9
floats-cdfpl/sine_8_true-unreach-call_true-termination.i timeout 0 wit inspect 900   890 5500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 44 error (2) 0 wit inspect .023 4.8
floats-cdfpl/square_4_true-unreach-call_true-termination.i true 2 wit inspect 620   840 4200 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 580    570 true 2 wit inspect 620     710  
floats-cdfpl/square_5_true-unreach-call_true-termination.i true 2 wit inspect 450   770 4000 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 560    510 true 2 wit inspect 490     730  
floats-cdfpl/square_6_true-unreach-call_true-termination.i true 2 wit inspect 330   830 2200 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 280    500 true 2 wit inspect 330     800  
floats-cdfpl/square_7_true-unreach-call_true-termination.i true 2 wit inspect 160   740 1200 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 850    480 true 2 wit inspect 160     730  
floats-cdfpl/square_8_true-unreach-call_true-termination.i true 2 wit inspect 110   650 830 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 68    360 true 2 wit inspect 110     620  
floats-cbmc-regression/float-div1_true-unreach-call.i true 2 wit inspect 31   680 280 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.2  320 true 2 wit inspect 33     610  
floats-cbmc-regression/float-flags-simp1_true-unreach-call.i true 2 wit inspect 28   720 240 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 12    790 true 2 wit inspect 31     700  
floats-cbmc-regression/float-no-simp1_true-unreach-call_true-termination.i true 2 wit inspect 8.7 290 77 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 8.7   240  
floats-cbmc-regression/float-no-simp2_true-unreach-call.i true 2 wit inspect 40   450 550 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 17    300 true 2 wit inspect 42     400  
floats-cbmc-regression/float-no-simp3_true-unreach-call_true-termination.i true 2 wit inspect 8.4 270 76 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  260 true 2 wit inspect 8.9   230  
floats-cbmc-regression/float-no-simp4_true-unreach-call.i true 2 wit inspect 39   560 480 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4  270 true 2 wit inspect 37     560  
floats-cbmc-regression/float-no-simp6_true-unreach-call_true-termination.i true 2 wit inspect 9.2 310 84 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 10     290  
floats-cbmc-regression/float-no-simp7_true-unreach-call_true-termination.i true 2 wit inspect 8.6 290 73 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  250 true 2 wit inspect 9.1   240  
floats-cbmc-regression/float-no-simp8_true-unreach-call.i true 2 wit inspect 9.6 320 79 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0  250 true 2 wit inspect 10     320  
floats-cbmc-regression/float-rounding1_true-unreach-call.i unknown 0 wit inspect 3.8 230 33 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 44 error (2) 0 wit inspect .019 4.8
floats-cbmc-regression/float-to-double1_true-unreach-call.i true 2 wit inspect 82   490 910 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  260 true 2 wit inspect 140     430  
floats-cbmc-regression/float-to-double2_true-unreach-call_true-termination.i true 2 wit inspect 8.5 280 69 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.1  250 true 2 wit inspect 9.5   240  
floats-cbmc-regression/float-zero-sum1_true-unreach-call_true-termination.i true 2 wit inspect 9.3 290 78 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 11     280  
floats-cbmc-regression/float11_true-unreach-call_true-termination.i true 2 wit inspect 8.8 290 81 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 10     240  
floats-cbmc-regression/float12_true-unreach-call_true-termination.i true 2 wit inspect 13   310 140 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 13     270  
floats-cbmc-regression/float13_true-unreach-call_true-termination.i true 2 wit inspect 9.3 290 74 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 10     250  
floats-cbmc-regression/float14_true-unreach-call.i true 2 wit inspect 9.1 310 83 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  260 true 2 wit inspect 9.6   290  
floats-cbmc-regression/float18_true-unreach-call.i unknown 0 wit inspect 3.8 220 31 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .72 43 error (2) 0 wit inspect .026 4.9
floats-cbmc-regression/float19_true-unreach-call.i true 2 wit inspect 10   290 96 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  260 true 2 wit inspect 10     280  
floats-cbmc-regression/float1_true-unreach-call_true-termination.i true 2 wit inspect 8.5 280 77 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 11     300  
floats-cbmc-regression/float20_true-unreach-call_true-termination.i true 2 wit inspect 13   390 140 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  250 true 2 wit inspect 15     380  
floats-cbmc-regression/float21_true-unreach-call.i true 2 wit inspect 62   600 660 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.1  290 true 2 wit inspect 70     600  
floats-cbmc-regression/float22_true-unreach-call_true-termination.i true 2 wit inspect 65   690 690 - wit inspect - wit inspect - wit inspect - wit inspect false(unreach-call) -16 wit inspect 5.6  280 true 2 wit inspect 290     1100  
floats-cbmc-regression/float2_true-unreach-call_true-termination.i true 2 wit inspect 9.1 310 74 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 10     290  
floats-cbmc-regression/float3_true-unreach-call_true-termination.i true 2 wit inspect 12   340 130 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  270 true 2 wit inspect 13     330  
floats-cbmc-regression/float4_true-unreach-call.i true 2 wit inspect 73   480 880 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 73    330 true 2 wit inspect 79     430  
floats-cbmc-regression/float5_true-unreach-call_true-termination.i true 2 wit inspect 21   320 220 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  260 true 2 wit inspect 22     270  
floats-cbmc-regression/float6_true-unreach-call_true-termination.i true 2 wit inspect 10   300 85 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  260 true 2 wit inspect 11     280  
floats-cbmc-regression/float8_true-unreach-call.i true 2 wit inspect 10   310 90 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.8  270 true 2 wit inspect 11     310  
floats-cbmc-regression/float_lib1_true-unreach-call.i error (7) 0 wit inspect 8.1 260 68 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .018 4.8
floats-cbmc-regression/float_lib2_true-unreach-call.i true 2 wit inspect 13   500 110 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  250 true 2 wit inspect 16     510  
float-benchs/cast_float_ptr_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 12   350 110 true -32 wit inspect 2.9  250 false(unreach-call) 1 wit inspect 10     270   unknown 0 wit inspect 2.8  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 9.6 290 85 true -32 wit inspect 2.9  260 false(unreach-call) 1 wit inspect 10     270   unknown 0 wit inspect 2.8  210 true -32 wit inspect .60   18    - wit inspect - wit inspect
float-benchs/cast_union_tight_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 9.7 290 79 true -32 wit inspect 2.9  250 false(unreach-call) 1 wit inspect 11     270   unknown 0 wit inspect 2.7  180 true -32 wit inspect .57   18    - wit inspect - wit inspect
float-benchs/float_int_inv_square_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 8.7 300 80 false(unreach-call) 1 wit inspect 3.1  270 false(unreach-call) 1 wit inspect 9.0   300   unknown 0 wit inspect 2.8  210 true -32 wit inspect .60   18    - wit inspect - wit inspect
float-benchs/inv_Newton_false-unreach-call.c timeout 0 wit inspect 900   1700 6300 error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .026 4.9 error (invalid witness file) 0 wit inspect .81 51 error (invalid witness file) 0 wit inspect .0041 .26 - wit inspect - wit inspect
float-benchs/inv_square_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 8.6 310 75 false(unreach-call) 1 wit inspect 3.0  270 false(unreach-call) 1 wit inspect 9.2   290   unknown 0 wit inspect 2.8  210 true -32 wit inspect .58   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 2.8  260 false(unreach-call) 1 wit inspect 4.4   220   unknown 0 wit inspect 2.6  180 true -32 wit inspect .60   18    - wit inspect - wit inspect
float-benchs/nan_float_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 4.1 240 35 false(unreach-call) 1 wit inspect 2.9  260 false(unreach-call) 1 wit inspect 4.1   220   unknown 0 wit inspect 2.6  180 true -32 wit inspect .60   18    - wit inspect - wit inspect
float-benchs/sin_interpolated_index_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 640   2500 6300 false(unreach-call) 1 wit inspect 9.6  360 timeout 0 wit inspect 97     1300   unknown 0 wit inspect 3.0  210 true -32 wit inspect .59   18    - wit inspect - wit inspect
float-benchs/sqrt_poly2_false-unreach-call.c false(unreach-call) 1 wit inspect 15   610 130 true -32 wit inspect 3.2  260 false(unreach-call) 1 wit inspect 16     590   unknown 0 wit inspect 2.7  180 true -32 wit inspect .61   18    - wit inspect - wit inspect
float-benchs/Muller_Kahan_true-unreach-call_true-termination.c timeout 0 wit inspect 900   7300 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .022 4.8
float-benchs/Rump_double_true-unreach-call_true-termination.c true 2 wit inspect 20   990 190 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 21     1000  
float-benchs/Rump_float_true-unreach-call_true-termination.c true 2 wit inspect 11   440 110 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  250 true 2 wit inspect 12     430  
float-benchs/addsub_double_exact_true-unreach-call_true-termination.c true 2 wit inspect 8.7 290 76 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  250 true 2 wit inspect 9.2   270  
float-benchs/addsub_float_exact_true-unreach-call_true-termination.c true 2 wit inspect 8.8 290 80 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 8.9   260  
float-benchs/addsub_float_inexact_true-unreach-call_true-termination.c true 2 wit inspect 8.8 290 78 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  250 true 2 wit inspect 9.0   250  
float-benchs/arctan_Pade_true-unreach-call_true-termination.c error (7) 0 wit inspect 410   2700 4500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 43 error (2) 0 wit inspect .050 4.8
float-benchs/bary_diverge_true-unreach-call_true-termination.c timeout 0 wit inspect 900   3000 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .018 5.0
float-benchs/cast_float_union_true-unreach-call.c true 2 wit inspect 4.4 260 37 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  240 true 2 wit inspect 4.6   230  
float-benchs/cos_polynomial_true-unreach-call_true-termination.c timeout 0 wit inspect 900   2900 6500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .018 4.9
float-benchs/divmul_buf_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 .56 44 error (2) 0 wit inspect .048 4.9
float-benchs/divmul_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 .55 41 error (2) 0 wit inspect .018 4.9
float-benchs/drift_tenth_true-unreach-call_true-termination.c error (7) 0 wit inspect 760   840 9000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 44 error (2) 0 wit inspect .018 5.0
float-benchs/exp_loop_true-unreach-call.c timeout 0 wit inspect 900   1400 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .018 4.8
float-benchs/feedback_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 .70 41 error (2) 0 wit inspect .047 4.8
float-benchs/filter1_true-unreach-call_true-termination.c error (7) 0 wit inspect 570   1100 5400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 43 error (2) 0 wit inspect .018 5.0
float-benchs/filter2_alt_true-unreach-call.c timeout 0 wit inspect 900   1300 7600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 42 error (2) 0 wit inspect .041 4.8
float-benchs/filter2_iterated_true-unreach-call.c error (7) 0 wit inspect 39   2200 530 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .048 4.9
float-benchs/filter2_reinit_true-unreach-call_true-termination.c timeout 0 wit inspect 900   2100 7900 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .053 4.9
float-benchs/filter2_set_true-unreach-call_true-termination.c error (7) 0 wit inspect 460   3400 4300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .018 4.8
float-benchs/filter2_true-unreach-call_true-termination.c timeout 0 wit inspect 900   2100 9100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 46 error (2) 0 wit inspect .018 4.8
float-benchs/filter_iir_true-unreach-call.c timeout 0 wit inspect 900   1800 8500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .024 4.9
float-benchs/float_double_true-unreach-call_true-termination.c true 2 wit inspect 9.3 290 73 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 9.3   240  
float-benchs/image_filter_true-unreach-call.c timeout 0 wit inspect 910   13000 3500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 43 error (2) 0 wit inspect .020 4.9
float-benchs/interpolation2_true-unreach-call_true-termination.c timeout 0 wit inspect 900   770 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 44 error (2) 0 wit inspect .018 4.9
float-benchs/interpolation_true-unreach-call_true-termination.c timeout 0 wit inspect 900   990 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 43 error (2) 0 wit inspect .017 4.9
float-benchs/inv_sqrt_Quake_true-unreach-call_true-termination.c error (7) 0 wit inspect 100   2400 880 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .018 4.9
float-benchs/inv_square_int_true-unreach-call_true-termination.c true 2 wit inspect 32   390 360 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  260 true 2 wit inspect 31     340  
float-benchs/inv_square_true-unreach-call_true-termination.c true 2 wit inspect 62   410 700 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  260 true 2 wit inspect 57     350  
float-benchs/loop_true-unreach-call.c timeout 0 wit inspect 900   1000 8900 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .041 4.9
float-benchs/mea8000_true-unreach-call.c timeout 0 wit inspect 900   5300 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .045 4.9
float-benchs/nan_double_range_true-unreach-call_true-termination.c true 2 wit inspect 8.6 290 68 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 8.8   240  
float-benchs/nan_float_range_true-unreach-call_true-termination.c true 2 wit inspect 10   300 93 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 10     250  
float-benchs/rlim_exit_true-unreach-call_true-termination.c timeout 0 wit inspect 900   3000 13000 - 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/rlim_invariant_true-unreach-call_true-termination.c timeout 0 wit inspect 900   930 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 41 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   2000 6700 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .035 4.9
float-benchs/sin_interpolated_bigrange_tight_true-unreach-call_true-termination.c timeout 0 wit inspect 900   2100 6300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 46 error (2) 0 wit inspect .018 4.9
float-benchs/sin_interpolated_index_true-unreach-call_true-termination.c timeout 0 wit inspect 900   2100 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .048 5.0
float-benchs/sin_interpolated_negation_true-unreach-call.c timeout 0 wit inspect 900   2400 5600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 41 error (2) 0 wit inspect .042 4.9
float-benchs/sin_interpolated_smallrange_true-unreach-call.c timeout 0 wit inspect 900   2700 5500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 42 error (2) 0 wit inspect .018 4.9
float-benchs/sqrt_Householder_constant_true-unreach-call.c error (7) 0 wit inspect 250   3000 2600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .046 4.9
float-benchs/sqrt_Householder_interval_true-unreach-call.c error (7) 0 wit inspect 160   2800 1300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 44 error (2) 0 wit inspect .046 4.9
float-benchs/sqrt_Householder_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 .53 44 error (2) 0 wit inspect .019 4.8
float-benchs/sqrt_Newton_pseudoconstant_true-unreach-call.c error (7) 0 wit inspect 110   2700 1000 - 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/sqrt_biNewton_pseudoconstant_true-unreach-call.c error (7) 0 wit inspect 110   2700 990 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 43 error (2) 0 wit inspect .018 4.9
float-benchs/sqrt_poly_true-unreach-call_true-termination.c true 2 wit inspect 200   1900 1300 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 39    490 true 2 wit inspect 140     1100  
float-benchs/water_pid_true-unreach-call_true-termination.c error (7) 0 wit inspect 130   3000 1200 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 43 error (2) 0 wit inspect .023 4.9
float-benchs/zonotope_2_true-unreach-call_true-termination.c timeout 0 wit inspect 900   1800 8900 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .019 4.9
float-benchs/zonotope_3_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 .61 41 error (2) 0 wit inspect .051 4.8
float-benchs/zonotope_loose_true-unreach-call_true-termination.c error (7) 0 wit inspect 150   1200 1300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .72 45 error (2) 0 wit inspect .024 5.0
float-benchs/zonotope_tight_true-unreach-call_true-termination.c true 2 wit inspect 190   1300 1600 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.4  310 true 2 wit inspect 110     960  
floats-esbmc-regression/Double_div_true-unreach-call.i error (7) 0 wit inspect 340   2800 2800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 43 error (2) 0 wit inspect .018 5.0
floats-esbmc-regression/Float_div_true-unreach-call.i error (7) 0 wit inspect 320   730 2700 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 46 error (2) 0 wit inspect .050 4.9
floats-esbmc-regression/ceil_nondet_true-unreach-call.i unknown 0 wit inspect 7.7 230 62 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 44 error (2) 0 wit inspect .026 4.8
floats-esbmc-regression/ceil_true-unreach-call.i unknown 0 wit inspect 4.0 220 31 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .023 4.8
floats-esbmc-regression/copysign_true-unreach-call.i unknown 0 wit inspect 3.7 230 31 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .018 4.9
floats-esbmc-regression/digits_for_true-unreach-call.i timeout 0 wit inspect 900   2700 7500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 45 error (2) 0 wit inspect .025 4.9
floats-esbmc-regression/digits_while_true-unreach-call.i timeout 0 wit inspect 900   2600 6800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 45 error (2) 0 wit inspect .049 5.0
floats-esbmc-regression/fabs_true-unreach-call.i true 2 wit inspect 9.6 310 72 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  260 true 2 wit inspect 9.3   270  
floats-esbmc-regression/fdim_true-unreach-call.i unknown 0 wit inspect 3.9 230 33 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .048 5.0
floats-esbmc-regression/floor_nondet_true-unreach-call.i unknown 0 wit inspect 7.2 220 62 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .019 4.8
floats-esbmc-regression/floor_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 .55 43 error (2) 0 wit inspect .019 4.8
floats-esbmc-regression/fmax_true-unreach-call.i true 2 wit inspect 8.5 290 68 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4  260 true 2 wit inspect 8.7   270  
floats-esbmc-regression/fmin_true-unreach-call.i true 2 wit inspect 8.6 290 70 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  260 true 2 wit inspect 9.0   270  
floats-esbmc-regression/fmod2_true-unreach-call.i unknown 0 wit inspect 7.3 230 61 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .046 4.8