Tool 2LS 0.6.0 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741 CPA-witness2test 1.6.1-svn 26773 CProver witness2test 0.1 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon*
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB]
Date of execution 2017-11-30 11:20:26 CET 2017-12-01 07:32:03 CET 2017-12-01 08:01:50 CET 2017-12-01 08:11:41 CET 2017-12-01 08:15:34 CET 2017-12-01 04:23:32 CET 2017-12-01 07:36:49 CET
Run set 2ls.sv-comp18.ReachSafety-Floats cpa-seq-validate-violation-witnesses-2ls.sv-comp18-violation-witness.ReachSafety-Floats uautomizer-validate-violation-witnesses-2ls.sv-comp18-violation-witness.ReachSafety-Floats cpa-witness2test-validate-violation-witnesses-2ls.sv-comp18-violation-witness.ReachSafety-Floats fshell-witness2test-validate-violation-witnesses-2ls.sv-comp18-violation-witness.ReachSafety-Floats cpa-seq-validate-correctness-witnesses-2ls.sv-comp18-correctness-witness.ReachSafety-Floats uautomizer-validate-correctness-witnesses-2ls.sv-comp18-correctness-witness.ReachSafety-Floats
Options --graphml-witness witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/2ls.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop cpa.smg.memoryAllocationFunctions=malloc,__kmalloc,kmalloc,kzalloc,kzalloc_node,ldv_zalloc,ldv_malloc -setprop cpa.smg.arrayAllocationFunctions=calloc,kmalloc_array,kcalloc -setprop cpa.smg.zeroingMemoryAllocation=calloc,kzalloc,kcalloc,kzalloc_node,ldv_zalloc -setprop cpa.smg.deallocationFunctions=free,kfree,kfree_const --full-output --validate ../../results-verified/2ls.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/2ls.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true --graphml-witness ../../results-verified/2ls.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/2ls.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/2ls.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
floats-cdfpl/newton_1_4_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 4.3   56 42    false(unreach-call) 1 wit inspect 4.3  350 false(unreach-call) 1 wit inspect 46     680   unknown 0 wit inspect 3.5  180 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
floats-cdfpl/newton_1_5_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 5.2   56 57    false(unreach-call) 1 wit inspect 4.4  350 timeout 0 wit inspect 97     700   unknown 0 wit inspect 3.6  210 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
floats-cdfpl/newton_1_6_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 2.8   55 29    false(unreach-call) 1 wit inspect 5.2  360 false(unreach-call) 1 wit inspect 24     680   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .78   18    - wit inspect - wit inspect
floats-cdfpl/newton_1_7_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 1.1   53 14    false(unreach-call) 1 wit inspect 4.6  360 false(unreach-call) 1 wit inspect 40     680   unknown 0 wit inspect 2.8  210 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
floats-cdfpl/newton_1_8_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 3.8   54 38    false(unreach-call) 1 wit inspect 4.6  360 false(unreach-call) 1 wit inspect 28     670   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .63   18    - wit inspect - wit inspect
floats-cdfpl/newton_2_6_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 7.6   110 84    true -32 wit inspect 3.2  260 timeout 0 wit inspect 97     810   unknown 0 wit inspect 3.6  210 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
floats-cdfpl/newton_2_7_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 4.1   92 47    true -32 wit inspect 2.3  260 timeout 0 wit inspect 97     820   unknown 0 wit inspect 3.0  180 false(unreach-call) 1 wit inspect .69   18    - wit inspect - wit inspect
floats-cdfpl/newton_2_8_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 12     100 120    true -32 wit inspect 3.2  260 false(unreach-call) 1 wit inspect 30     810   unknown 0 wit inspect 3.0  180 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
floats-cdfpl/newton_3_6_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 83     220 1100    true -32 wit inspect 3.2  260 timeout 0 wit inspect 97     900   unknown 0 wit inspect 3.7  210 false(unreach-call) 1 wit inspect .62   18    - wit inspect - wit inspect
floats-cdfpl/newton_3_7_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 50     220 440    true -32 wit inspect 3.1  260 timeout 0 wit inspect 97     870   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .74   18    - wit inspect - wit inspect
floats-cdfpl/newton_3_8_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 29     190 250    true -32 wit inspect 3.0  250 timeout 0 wit inspect 97     920   unknown 0 wit inspect 2.9  180 false(unreach-call) 1 wit inspect .67   18    - wit inspect - wit inspect
floats-cdfpl/sine_1_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .49  38 5.2  false(unreach-call) 1 wit inspect 3.8  300 false(unreach-call) 1 wit inspect 22     550   unknown 0 wit inspect 2.9  210 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
floats-cdfpl/sine_2_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .64  38 9.0  true -32 wit inspect 2.9  250 false(unreach-call) 1 wit inspect 30     570   unknown 0 wit inspect 2.9  180 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
floats-cdfpl/sine_3_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .30  38 3.0  true -32 wit inspect 2.9  250 timeout 0 wit inspect 97     620   unknown 0 wit inspect 2.8  180 false(unreach-call) 1 wit inspect .62   18    - wit inspect - wit inspect
floats-cdfpl/square_1_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 1.3   38 16    true -32 wit inspect 3.2  260 true -32 wit inspect 4.1   210   unknown 0 wit inspect 3.0  210 false(unreach-call) 1 wit inspect .80   18    - wit inspect - wit inspect
floats-cdfpl/square_2_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 1.1   37 13    true -32 wit inspect 2.9  260 true -32 wit inspect 4.5   210   unknown 0 wit inspect 3.3  210 false(unreach-call) 1 wit inspect .61   18    - wit inspect - wit inspect
floats-cdfpl/square_3_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .95  38 11    true -32 wit inspect 2.8  250 true -32 wit inspect 5.6   220   unknown 0 wit inspect 3.1  210 false(unreach-call) 1 wit inspect .73   18    - wit inspect - wit inspect
floats-cdfpl/newton_1_1_true-unreach-call_true-termination.i true 2 wit inspect 8.3   73 78    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    600 timeout 0 wit inspect 960     1000  
floats-cdfpl/newton_1_2_true-unreach-call_true-termination.i true 2 wit inspect 10     70 95    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    580 timeout 0 wit inspect 960     1000  
floats-cdfpl/newton_1_3_true-unreach-call_true-termination.i true 2 wit inspect 10     73 120    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    590 timeout 0 wit inspect 960     890  
floats-cdfpl/newton_2_1_true-unreach-call_true-termination.i true 2 wit inspect 33     150 400    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    580 timeout 0 wit inspect 960     980  
floats-cdfpl/newton_2_2_true-unreach-call_true-termination.i true 2 wit inspect 28     140 230    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    850 timeout 0 wit inspect 960     970  
floats-cdfpl/newton_2_3_true-unreach-call_true-termination.i true 2 wit inspect 23     130 170    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    530 timeout 0 wit inspect 960     940  
floats-cdfpl/newton_2_4_true-unreach-call_true-termination.i true 2 wit inspect 44     140 480    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    580 timeout 0 wit inspect 960     1000  
floats-cdfpl/newton_2_5_true-unreach-call_true-termination.i true 2 wit inspect 60     140 580    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    550 timeout 0 wit inspect 960     1000  
floats-cdfpl/newton_3_1_true-unreach-call_true-termination.i true 2 wit inspect 69     200 680    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    600 timeout 0 wit inspect 960     1100  
floats-cdfpl/newton_3_2_true-unreach-call_true-termination.i true 2 wit inspect 69     220 600    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    570 timeout 0 wit inspect 960     1000  
floats-cdfpl/newton_3_3_true-unreach-call_true-termination.i true 2 wit inspect 98     220 850    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    690 timeout 0 wit inspect 960     1100  
floats-cdfpl/newton_3_4_true-unreach-call_true-termination.i true 2 wit inspect 81     220 790    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    710 timeout 0 wit inspect 960     1000  
floats-cdfpl/newton_3_5_true-unreach-call_true-termination.i true 2 wit inspect 90     220 890    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    570 timeout 0 wit inspect 960     1100  
floats-cdfpl/sine_4_true-unreach-call_true-termination.i true 2 wit inspect 25     55 330    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    500 timeout 0 wit inspect 960     870  
floats-cdfpl/sine_5_true-unreach-call_true-termination.i true 2 wit inspect 2.0   41 24    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    510 timeout 0 wit inspect 960     910  
floats-cdfpl/sine_6_true-unreach-call_true-termination.i true 2 wit inspect 1.7   38 23    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    650 timeout 0 wit inspect 960     830  
floats-cdfpl/sine_7_true-unreach-call_true-termination.i true 2 wit inspect 1.4   40 17    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 820    590 timeout 0 wit inspect 960     770  
floats-cdfpl/sine_8_true-unreach-call_true-termination.i true 2 wit inspect 1.3   39 16    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 570    540 timeout 0 wit inspect 960     840  
floats-cdfpl/square_4_true-unreach-call_true-termination.i true 2 wit inspect 200     68 2600    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 660    570 true 2 wit inspect 780     720  
floats-cdfpl/square_5_true-unreach-call_true-termination.i true 2 wit inspect 680     170 8900    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 520    510 true 2 wit inspect 510     710  
floats-cdfpl/square_6_true-unreach-call_true-termination.i true 2 wit inspect 62     63 810    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 260    500 true 2 wit inspect 390     780  
floats-cdfpl/square_7_true-unreach-call_true-termination.i true 2 wit inspect 9.3   59 120    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    480 true 2 wit inspect 180     700  
floats-cdfpl/square_8_true-unreach-call_true-termination.i true 2 wit inspect .72  38 10    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 75    360 true 2 wit inspect 120     620  
floats-cbmc-regression/float-div1_true-unreach-call.i true 2 wit inspect .30  38 3.0  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.4  320 true 2 wit inspect 34     590  
floats-cbmc-regression/float-flags-simp1_true-unreach-call.i true 2 wit inspect .94  130 11    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 13    790 true 2 wit inspect 32     720  
floats-cbmc-regression/float-no-simp1_true-unreach-call_true-termination.i true 2 wit inspect .094 22 .85 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  260 true 2 wit inspect 8.4   240  
floats-cbmc-regression/float-no-simp2_true-unreach-call.i true 2 wit inspect .72  33 9.3  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 14    300 true 2 wit inspect 41     390  
floats-cbmc-regression/float-no-simp3_true-unreach-call_true-termination.i true 2 wit inspect .096 23 .92 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.6  250 true 2 wit inspect 8.8   230  
floats-cbmc-regression/float-no-simp4_true-unreach-call.i true 2 wit inspect .31  36 3.8  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.7  270 true 2 wit inspect 46     560  
floats-cbmc-regression/float-no-simp6_true-unreach-call_true-termination.i true 2 wit inspect .089 23 .71 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 11     300  
floats-cbmc-regression/float-no-simp7_true-unreach-call_true-termination.i true 2 wit inspect .080 22 .99 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 9.4   240  
floats-cbmc-regression/float-no-simp8_true-unreach-call.i true 2 wit inspect .19  28 1.5  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3  260 true 2 wit inspect 10     300  
floats-cbmc-regression/float-rounding1_true-unreach-call.i true 2 wit inspect .21  28 1.5  - wit inspect - wit inspect - wit inspect - wit inspect error 0 wit inspect 4.9  260 unknown 0 wit inspect 3.4   190  
floats-cbmc-regression/float-to-double1_true-unreach-call.i true 2 wit inspect .24  28 1.9  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  260 true 2 wit inspect 170     440  
floats-cbmc-regression/float-to-double2_true-unreach-call_true-termination.i true 2 wit inspect .089 22 .64 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  250 true 2 wit inspect 11     230  
floats-cbmc-regression/float-zero-sum1_true-unreach-call_true-termination.i true 2 wit inspect .11  22 .73 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  250 true 2 wit inspect 11     300  
floats-cbmc-regression/float11_true-unreach-call_true-termination.i true 2 wit inspect .11  22 .82 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  240 true 2 wit inspect 9.8   240  
floats-cbmc-regression/float12_true-unreach-call_true-termination.i true 2 wit inspect .10  22 .66 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 18     270  
floats-cbmc-regression/float13_true-unreach-call_true-termination.i true 2 wit inspect .12  24 1.0  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  250 true 2 wit inspect 7.4   250  
floats-cbmc-regression/float14_true-unreach-call.i true 2 wit inspect .17  28 1.9  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  250 true 2 wit inspect 9.5   290  
floats-cbmc-regression/float18_true-unreach-call.i timeout 0 wit inspect 900     1700 10000    - 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-cbmc-regression/float19_true-unreach-call.i true 2 wit inspect .19  28 1.4  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  260 true 2 wit inspect 11     280  
floats-cbmc-regression/float1_true-unreach-call_true-termination.i true 2 wit inspect .11  22 .52 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 9.2   240  
floats-cbmc-regression/float20_true-unreach-call_true-termination.i true 2 wit inspect .14  26 1.2  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 16     380  
floats-cbmc-regression/float21_true-unreach-call.i true 2 wit inspect .27  30 2.6  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.1  300 true 2 wit inspect 87     600  
floats-cbmc-regression/float22_true-unreach-call_true-termination.i true 2 wit inspect .11  23 .86 - wit inspect - wit inspect - wit inspect - wit inspect false(unreach-call) -16 wit inspect 5.2  280 true 2 wit inspect 320     1100  
floats-cbmc-regression/float2_true-unreach-call_true-termination.i true 2 wit inspect .095 22 .93 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  240 true 2 wit inspect 10     280  
floats-cbmc-regression/float3_true-unreach-call_true-termination.i true 2 wit inspect .11  24 1.1  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  270 true 2 wit inspect 15     330  
floats-cbmc-regression/float4_true-unreach-call.i true 2 wit inspect 11     45 130    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 100    330 true 2 wit inspect 77     430  
floats-cbmc-regression/float5_true-unreach-call_true-termination.i true 2 wit inspect .12  23 .77 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  260 true 2 wit inspect 28     280  
floats-cbmc-regression/float6_true-unreach-call_true-termination.i true 2 wit inspect .099 23 1.1  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  250 true 2 wit inspect 12     290  
floats-cbmc-regression/float8_true-unreach-call.i true 2 wit inspect .55  30 5.7  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.6  270 true 2 wit inspect 11     300  
floats-cbmc-regression/float_lib1_true-unreach-call.i true 2 wit inspect 6.6   34 72    - wit inspect - wit inspect - wit inspect - wit inspect error (parsing failed) 0 wit inspect 2.5  140 error (7) 0 wit inspect 9.3   250  
floats-cbmc-regression/float_lib2_true-unreach-call.i true 2 wit inspect .24  29 2.0  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  260 true 2 wit inspect 17     520  
float-benchs/cast_float_ptr_false-unreach-call_true-termination.c error (134) 0 wit inspect .095 22 .72 error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .90 50 error (invalid witness file) 0 wit inspect .0014 .31 - wit inspect - wit inspect
float-benchs/cast_union_loose_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .13  26 1.2  false(unreach-call) 1 wit inspect 3.6  270 false(unreach-call) 1 wit inspect 12     270   unknown 0 wit inspect 3.5  210 false(unreach-call) 1 wit inspect .76   18    - wit inspect - wit inspect
float-benchs/cast_union_tight_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .15  24 1.1  false(unreach-call) 1 wit inspect 3.5  270 false(unreach-call) 1 wit inspect 11     270   unknown 0 wit inspect 2.8  180 false(unreach-call) 1 wit inspect .63   18    - wit inspect - wit inspect
float-benchs/float_int_inv_square_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .17  27 1.2  false(unreach-call) 1 wit inspect 3.0  260 false(unreach-call) 1 wit inspect 9.1   300   unknown 0 wit inspect 3.1  180 false(unreach-call) 1 wit inspect .63   18    - wit inspect - wit inspect
float-benchs/inv_Newton_false-unreach-call.c timeout 0 wit inspect 900     820 6800    error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .96 49 error (invalid witness file) 0 wit inspect .0014 .30 - wit inspect - wit inspect
float-benchs/inv_square_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .17  27 1.1  false(unreach-call) 1 wit inspect 2.2  270 false(unreach-call) 1 wit inspect 9.2   290   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
float-benchs/nan_double_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .10  22 1.0  false(unreach-call) 1 wit inspect 3.0  260 false(unreach-call) 1 wit inspect 5.6   220   unknown 0 wit inspect 3.3  180 error (2) 0 wit inspect .58   18    - wit inspect - wit inspect
float-benchs/nan_float_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .11  22 .88 false(unreach-call) 1 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 5.6   220   unknown 0 wit inspect 3.6  180 error (2) 0 wit inspect .57   18    - wit inspect - wit inspect
float-benchs/sin_interpolated_index_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.2   260 34    true -32 wit inspect 3.4  260 false(unreach-call) 1 wit inspect 22     980   unknown 0 wit inspect 3.2  210 false(unreach-call) 1 wit inspect .65   18    - wit inspect - wit inspect
float-benchs/sqrt_poly2_false-unreach-call.c false(unreach-call) 1 wit inspect .64  46 6.6  true -32 wit inspect 3.3  260 false(unreach-call) 1 wit inspect 21     610   unknown 0 wit inspect 3.2  210 false(unreach-call) 1 wit inspect .61   18    - wit inspect - wit inspect
float-benchs/Muller_Kahan_true-unreach-call_true-termination.c timeout 0 wit inspect 900     610 6500    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .021 4.8
float-benchs/Rump_double_true-unreach-call_true-termination.c true 2 wit inspect .15  27 1.1  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  250 true 2 wit inspect 23     980  
float-benchs/Rump_float_true-unreach-call_true-termination.c true 2 wit inspect .12  24 .88 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  250 true 2 wit inspect 13     420  
float-benchs/addsub_double_exact_true-unreach-call_true-termination.c true 2 wit inspect .096 22 .82 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  260 true 2 wit inspect 10     270  
float-benchs/addsub_float_exact_true-unreach-call_true-termination.c true 2 wit inspect .11  22 .77 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 9.3   240  
float-benchs/addsub_float_inexact_true-unreach-call_true-termination.c true 2 wit inspect .10  22 .73 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  250 true 2 wit inspect 9.1   250  
float-benchs/arctan_Pade_true-unreach-call_true-termination.c true 2 wit inspect 55     260 670    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 36    500 error (7) 0 wit inspect 36     1000  
float-benchs/bary_diverge_true-unreach-call_true-termination.c timeout 0 wit inspect 900     460 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .019 4.9
float-benchs/cast_float_union_true-unreach-call.c true 2 wit inspect .13  23 .72 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 4.6   230  
float-benchs/cos_polynomial_true-unreach-call_true-termination.c true 2 wit inspect 7.0   110 60    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1400 timeout 0 wit inspect 960     2900  
float-benchs/divmul_buf_diverge_true-unreach-call_true-termination.c true 2 wit inspect .70  32 8.0  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3400 timeout 0 wit inspect 960     4600  
float-benchs/divmul_diverge_true-unreach-call_true-termination.c timeout 0 wit inspect 900     400 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 41 error (2) 0 wit inspect .051 4.9
float-benchs/drift_tenth_true-unreach-call_true-termination.c true 2 wit inspect .42  35 5.4  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 14    330 true 2 wit inspect 450     680  
float-benchs/exp_loop_true-unreach-call.c true 2 wit inspect 19     210 220    - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 720    7000 error (7) 0 wit inspect 230     640  
float-benchs/feedback_diverge_true-unreach-call_true-termination.c timeout 0 wit inspect 900     1600 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .019 4.9
float-benchs/filter1_true-unreach-call_true-termination.c timeout 0 wit inspect 900     630 8900    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .052 4.8
float-benchs/filter2_alt_true-unreach-call.c timeout 0 wit inspect 900     180 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .020 4.9
float-benchs/filter2_iterated_true-unreach-call.c timeout 0 wit inspect 900     620 8000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .018 4.8
float-benchs/filter2_reinit_true-unreach-call_true-termination.c timeout 0 wit inspect 900     530 8400    - 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/filter2_set_true-unreach-call_true-termination.c timeout 0 wit inspect 900     380 7200    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 43 error (2) 0 wit inspect .024 4.9
float-benchs/filter2_true-unreach-call_true-termination.c timeout 0 wit inspect 900     640 7600    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 41 error (2) 0 wit inspect .019 4.9
float-benchs/filter_iir_true-unreach-call.c timeout 0 wit inspect 900     310 9900    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 45 error (2) 0 wit inspect .018 4.9
float-benchs/float_double_true-unreach-call_true-termination.c true 2 wit inspect .12  22 .83 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 11     250  
float-benchs/image_filter_true-unreach-call.c timeout 0 wit inspect 900     1100 9200    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .019 4.8
float-benchs/interpolation2_true-unreach-call_true-termination.c true 2 wit inspect .42  30 4.3  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    590 timeout 0 wit inspect 960     770  
float-benchs/interpolation_true-unreach-call_true-termination.c true 2 wit inspect .28  27 2.4  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 16    390 timeout 0 wit inspect 960     830  
float-benchs/inv_sqrt_Quake_true-unreach-call_true-termination.c true 2 wit inspect .28  30 2.9  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  270 error (7) 0 wit inspect 120     810  
float-benchs/inv_square_int_true-unreach-call_true-termination.c true 2 wit inspect .13  27 1.3  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  260 true 2 wit inspect 14     310  
float-benchs/inv_square_true-unreach-call_true-termination.c true 2 wit inspect .15  26 1.0  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  260 true 2 wit inspect 58     350  
float-benchs/loop_true-unreach-call.c timeout 0 wit inspect 900     330 7400    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .037 4.8
float-benchs/mea8000_true-unreach-call.c timeout 0 wit inspect 900     2900 9700    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 44 error (2) 0 wit inspect .020 4.9
float-benchs/nan_double_range_true-unreach-call_true-termination.c true 2 wit inspect .11  22 .68 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  260 true 2 wit inspect 9.1   240  
float-benchs/nan_float_range_true-unreach-call_true-termination.c true 2 wit inspect .12  22 .81 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  250 true 2 wit inspect 11     250  
float-benchs/rlim_exit_true-unreach-call_true-termination.c timeout 0 wit inspect 900     1800 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 43 error (2) 0 wit inspect .020 4.9
float-benchs/rlim_invariant_true-unreach-call_true-termination.c timeout 0 wit inspect 900     1800 11000    - 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/sin_interpolated_bigrange_loose_true-unreach-call_true-termination.c true 2 wit inspect 820     310 8000    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    820 timeout 0 wit inspect 960     2100  
float-benchs/sin_interpolated_bigrange_tight_true-unreach-call_true-termination.c timeout 0 wit inspect 900     320 9200    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .72 41 error (2) 0 wit inspect .024 4.9
float-benchs/sin_interpolated_index_true-unreach-call_true-termination.c true 2 wit inspect 770     310 10000    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    590 timeout 0 wit inspect 960     2100  
float-benchs/sin_interpolated_negation_true-unreach-call.c timeout 0 wit inspect 900     540 7000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .019 5.0
float-benchs/sin_interpolated_smallrange_true-unreach-call.c timeout 0 wit inspect 900     360 7100    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 42 error (2) 0 wit inspect .019 5.0
float-benchs/sqrt_Householder_constant_true-unreach-call.c timeout 0 wit inspect 900     310 6800    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .020 4.8
float-benchs/sqrt_Householder_interval_true-unreach-call.c timeout 0 wit inspect 900     330 9400    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .73 45 error (2) 0 wit inspect .022 4.8
float-benchs/sqrt_Householder_pseudoconstant_true-unreach-call.c timeout 0 wit inspect 900     330 6600    - 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_Newton_pseudoconstant_true-unreach-call.c timeout 0 wit inspect 900     390 7100    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 44 error (2) 0 wit inspect .024 4.8
float-benchs/sqrt_biNewton_pseudoconstant_true-unreach-call.c timeout 0 wit inspect 900     340 5800    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 43 error (2) 0 wit inspect .020 5.0
float-benchs/sqrt_poly_true-unreach-call_true-termination.c true 2 wit inspect 1.2   58 12    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 42    490 true 2 wit inspect 150     1100  
float-benchs/water_pid_true-unreach-call_true-termination.c timeout 0 wit inspect 900     900 8400    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 43 error (2) 0 wit inspect .019 4.9
float-benchs/zonotope_2_true-unreach-call_true-termination.c timeout 0 wit inspect 900     340 8400    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 44 error (2) 0 wit inspect .029 4.8
float-benchs/zonotope_3_true-unreach-call_true-termination.c timeout 0 wit inspect 900     1700 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .020 4.9
float-benchs/zonotope_loose_true-unreach-call_true-termination.c true 2 wit inspect .20  34 2.6  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.1  320 true 2 wit inspect 110     930  
float-benchs/zonotope_tight_true-unreach-call_true-termination.c true 2 wit inspect .22  34 2.1  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.1  310 true 2 wit inspect 130     1100  
floats-esbmc-regression/Double_div_true-unreach-call.i true 2 wit inspect 1.6   49 19    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.2  320 true 2 wit inspect 360     3000  
floats-esbmc-regression/Float_div_true-unreach-call.i true 2 wit inspect .43  32 4.4  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.7  280 error (7) 0 wit inspect 130     550  
floats-esbmc-regression/ceil_nondet_true-unreach-call.i true 2 wit inspect 3.6   89 46    - wit inspect - wit inspect - wit inspect - wit inspect error 0 wit inspect 4.2  260 unknown 0 wit inspect 11     200  
floats-esbmc-regression/ceil_true-unreach-call.i true 2 wit inspect .45  32 3.9  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3  260 unknown 0 wit inspect 4.0   210  
floats-esbmc-regression/copysign_true-unreach-call.i true 2 wit inspect .36  30 2.4  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.5  250 unknown 0 wit inspect 3.9   210  
floats-esbmc-regression/digits_for_true-unreach-call.i true 2 wit inspect 620     760 7500    - wit inspect - wit inspect - wit inspect - wit inspect assertion 0 wit inspect 4.1  260 timeout 0 wit inspect 960     2900  
floats-esbmc-regression/digits_while_true-unreach-call.i true 2 wit inspect 630     770 5600    - wit inspect - wit inspect - wit inspect - wit inspect assertion 0 wit inspect 3.7  270 timeout 0 wit inspect 960     3400  
floats-esbmc-regression/fabs_true-unreach-call.i true 2 wit inspect .23  29 2.2  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  260 true 2 wit inspect 11     280  
floats-esbmc-regression/fdim_true-unreach-call.i true 2 wit inspect .21  29 2.5  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  260 unknown 0 wit inspect 4.0   210  
floats-esbmc-regression/floor_nondet_true-unreach-call.i true 2 wit inspect 3.7   90 46    - wit inspect - wit inspect - wit inspect - wit inspect error 0 wit inspect 4.5  260 unknown 0 wit inspect 7.8   210  
floats-esbmc-regression/floor_true-unreach-call.i true 2 wit inspect .45  32 4.2  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.9  260 unknown 0 wit inspect 3.9   210  
floats-esbmc-regression/fmax_true-unreach-call.i true 2 wit inspect .35  30 2.6  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.6  250 true 2 wit inspect 9.0   270  
floats-esbmc-regression/fmin_true-unreach-call.i true 2 wit inspect .37  33 2.8  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit