Tool ESBMC ESBMC version 4.6.0 64-bit x86_64 linux 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* [apollon073; apollon077; apollon078; apollon119; apollon130] apollon* [apollon077; apollon078; apollon091; apollon114] apollon*
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [4; 8], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33554 MB; 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-01 12:59:33 CET 2017-12-02 09:20:19 CET 2017-12-02 10:53:45 CET 2017-12-02 11:06:16 CET 2017-12-02 11:21:21 CET 2017-12-02 06:57:43 CET 2017-12-02 09:56:59 CET
Run set esbmc-kind.sv-comp18.ReachSafety-Floats cpa-seq-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.ReachSafety-Floats uautomizer-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.ReachSafety-Floats cpa-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.ReachSafety-Floats fshell-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.ReachSafety-Floats cpa-seq-validate-correctness-witnesses-esbmc-kind.sv-comp18-correctness-witness.ReachSafety-Floats uautomizer-validate-correctness-witnesses-esbmc-kind.sv-comp18-correctness-witness.ReachSafety-Floats
Options -s kinduction -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-kind.2017-12-01_1259.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/esbmc-kind.2017-12-01_1259.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-kind.2017-12-01_1259.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/esbmc-kind.2017-12-01_1259.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-kind.2017-12-01_1259.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/esbmc-kind.2017-12-01_1259.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 8.4   190 89    false(unreach-call) 1 wit inspect 3.5  360 false(unreach-call) 1 wit inspect 44     680   unknown 0 wit inspect 2.0  190 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
floats-cdfpl/newton_1_5_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 6.8   190 55    false(unreach-call) 1 wit inspect 4.9  360 timeout 0 wit inspect 97     680   unknown 0 wit inspect 2.1  210 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
floats-cdfpl/newton_1_6_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 2.9   180 28    false(unreach-call) 1 wit inspect 6.2  360 false(unreach-call) 1 wit inspect 18     670   unknown 0 wit inspect 2.1  210 false(unreach-call) 1 wit inspect .61   18    - wit inspect - wit inspect
floats-cdfpl/newton_1_7_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 10     190 91    false(unreach-call) 1 wit inspect 4.9  360 false(unreach-call) 1 wit inspect 40     680   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
floats-cdfpl/newton_1_8_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 7.4   190 64    false(unreach-call) 1 wit inspect 6.0  350 false(unreach-call) 1 wit inspect 30     670   unknown 0 wit inspect 2.8  210 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
floats-cdfpl/newton_2_6_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 16     340 140    false(unreach-call) 1 wit inspect 6.5  450 timeout 0 wit inspect 97     830   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
floats-cdfpl/newton_2_7_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 16     350 170    false(unreach-call) 1 wit inspect 6.5  460 timeout 0 wit inspect 97     830   unknown 0 wit inspect 2.1  210 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
floats-cdfpl/newton_2_8_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 12     350 95    false(unreach-call) 1 wit inspect 6.2  460 false(unreach-call) 1 wit inspect 31     810   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
floats-cdfpl/newton_3_6_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 18     510 180    false(unreach-call) 1 wit inspect 10    560 timeout 0 wit inspect 97     910   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
floats-cdfpl/newton_3_7_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 160     520 1200    false(unreach-call) 1 wit inspect 6.7  560 timeout 0 wit inspect 97     880   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
floats-cdfpl/newton_3_8_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 11     510 100    false(unreach-call) 1 wit inspect 8.6  560 timeout 0 wit inspect 97     920   unknown 0 wit inspect 2.9  210 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
floats-cdfpl/sine_1_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 5.7   130 48    true -32 wit inspect 3.0  260 false(unreach-call) 1 wit inspect 23     550   unknown 0 wit inspect 2.0  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 2.8   130 27    true -32 wit inspect 3.0  260 false(unreach-call) 1 wit inspect 29     550   unknown 0 wit inspect 2.0  210 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 5.9   130 58    true -32 wit inspect 3.7  260 timeout 0 wit inspect 97     600   unknown 0 wit inspect 2.7  210 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
floats-cdfpl/square_1_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 3.1   130 35    true -32 wit inspect 3.7  250 timeout 0 wit inspect 97     440   unknown 0 wit inspect 1.9  180 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
floats-cdfpl/square_2_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 2.9   130 30    false(unreach-call) 1 wit inspect 2.9  300 timeout (false(unreach-call)) 0 wit inspect 96     430   unknown 0 wit inspect 1.9  190 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
floats-cdfpl/square_3_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 3.5   130 32    true -32 wit inspect 2.1  260 timeout 0 wit inspect 97     450   unknown 0 wit inspect 1.9  180 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
floats-cdfpl/newton_1_1_true-unreach-call_true-termination.i true 2 wit inspect 23     200 190    - 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 46     210 470    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    590 timeout 0 wit inspect 960     1000  
floats-cdfpl/newton_1_3_true-unreach-call_true-termination.i true 2 wit inspect 45     210 370    - 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 75     390 610    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    550 timeout 0 wit inspect 960     980  
floats-cdfpl/newton_2_2_true-unreach-call_true-termination.i true 2 wit inspect 91     390 610    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    800 timeout 0 wit inspect 960     1000  
floats-cdfpl/newton_2_3_true-unreach-call_true-termination.i true 2 wit inspect 81     380 470    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    540 timeout 0 wit inspect 960     930  
floats-cdfpl/newton_2_4_true-unreach-call_true-termination.i true 2 wit inspect 91     380 700    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    590 timeout 0 wit inspect 960     1000  
floats-cdfpl/newton_2_5_true-unreach-call_true-termination.i true 2 wit inspect 400     430 2800    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    600 timeout 0 wit inspect 960     1000  
floats-cdfpl/newton_3_1_true-unreach-call_true-termination.i true 2 wit inspect 190     610 1500    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    590 timeout 0 wit inspect 960     1100  
floats-cdfpl/newton_3_2_true-unreach-call_true-termination.i true 2 wit inspect 670     680 4700    - 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 250     610 2200    - 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 450     670 3300    - 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 470     640 3500    - 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 130     180 1000    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    500 timeout 0 wit inspect 960     840  
floats-cdfpl/sine_5_true-unreach-call_true-termination.i true 2 wit inspect 18     140 200    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    490 timeout 0 wit inspect 960     840  
floats-cdfpl/sine_6_true-unreach-call_true-termination.i true 2 wit inspect 7.0   130 68    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    650 timeout 0 wit inspect 960     810  
floats-cdfpl/sine_7_true-unreach-call_true-termination.i true 2 wit inspect 6.7   130 90    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 620    590 timeout 0 wit inspect 960     750  
floats-cdfpl/sine_8_true-unreach-call_true-termination.i true 2 wit inspect 5.3   130 57    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 520    540 timeout 0 wit inspect 960     820  
floats-cdfpl/square_4_true-unreach-call_true-termination.i true 2 wit inspect 130     160 980    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 650    570 true 2 wit inspect 750     880  
floats-cdfpl/square_5_true-unreach-call_true-termination.i true 2 wit inspect 110     150 780    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 480    510 true 2 wit inspect 600     720  
floats-cdfpl/square_6_true-unreach-call_true-termination.i true 2 wit inspect 22     130 180    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 270    500 true 2 wit inspect 400     810  
floats-cdfpl/square_7_true-unreach-call_true-termination.i true 2 wit inspect 30     130 300    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    480 true 2 wit inspect 190     690  
floats-cdfpl/square_8_true-unreach-call_true-termination.i true 2 wit inspect 2.7   120 30    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 76    360 true 2 wit inspect 120     640  
floats-cbmc-regression/float-div1_true-unreach-call.i true 2 wit inspect 1.2   110 13    - 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 .12  29 1.3  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 11    780 true 2 wit inspect 39     710  
floats-cbmc-regression/float-no-simp1_true-unreach-call_true-termination.i true 2 wit inspect .070 26 .79 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 9.3   240  
floats-cbmc-regression/float-no-simp2_true-unreach-call.i true 2 wit inspect 2.2   71 26    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 19    300 true 2 wit inspect 42     390  
floats-cbmc-regression/float-no-simp3_true-unreach-call_true-termination.i true 2 wit inspect .093 26 .80 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.0  250 true 2 wit inspect 9.2   230  
floats-cbmc-regression/float-no-simp4_true-unreach-call.i true 2 wit inspect .18  30 2.1  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.7  270 true 2 wit inspect 41     560  
floats-cbmc-regression/float-no-simp6_true-unreach-call_true-termination.i true 2 wit inspect .11  26 .63 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 11     290  
floats-cbmc-regression/float-no-simp7_true-unreach-call_true-termination.i true 2 wit inspect .10  26 .63 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 12     240  
floats-cbmc-regression/float-no-simp8_true-unreach-call.i true 2 wit inspect .085 27 .74 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  260 true 2 wit inspect 12     300  
floats-cbmc-regression/float-rounding1_true-unreach-call.i true 2 wit inspect .20  32 2.6  - wit inspect - wit inspect - wit inspect - wit inspect error 0 wit inspect 4.5  260 unknown 0 wit inspect 4.3   200  
floats-cbmc-regression/float-to-double1_true-unreach-call.i true 2 wit inspect .24  31 2.4  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8  260 true 2 wit inspect 120     440  
floats-cbmc-regression/float-to-double2_true-unreach-call_true-termination.i true 2 wit inspect .11  26 .68 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 6.0   250  
floats-cbmc-regression/float-zero-sum1_true-unreach-call_true-termination.i true 2 wit inspect .14  28 1.5  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  250 true 2 wit inspect 14     280  
floats-cbmc-regression/float11_true-unreach-call_true-termination.i true 2 wit inspect .090 27 .94 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 9.9   240  
floats-cbmc-regression/float12_true-unreach-call_true-termination.i true 2 wit inspect .18  32 2.4  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 18     270  
floats-cbmc-regression/float13_true-unreach-call_true-termination.i true 2 wit inspect .10  26 .90 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4  240 true 2 wit inspect 13     240  
floats-cbmc-regression/float14_true-unreach-call.i true 2 wit inspect .079 27 1.0  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4  250 true 2 wit inspect 9.6   290  
floats-cbmc-regression/float18_true-unreach-call.i true 2 wit inspect .12  27 .98 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 28    410 unknown 0 wit inspect 4.0   200  
floats-cbmc-regression/float19_true-unreach-call.i true 2 wit inspect .15  28 1.9  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4  270 true 2 wit inspect 11     290  
floats-cbmc-regression/float1_true-unreach-call_true-termination.i true 2 wit inspect .099 26 .78 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  250 true 2 wit inspect 9.0   230  
floats-cbmc-regression/float20_true-unreach-call_true-termination.i true 2 wit inspect .36  52 4.4  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 19     390  
floats-cbmc-regression/float21_true-unreach-call.i true 2 wit inspect .28  35 2.9  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.4  300 true 2 wit inspect 80     600  
floats-cbmc-regression/float22_true-unreach-call_true-termination.i true 2 wit inspect .56  58 7.3  - wit inspect - wit inspect - wit inspect - wit inspect false(unreach-call) -16 wit inspect 5.3  280 true 2 wit inspect 340     1000  
floats-cbmc-regression/float2_true-unreach-call_true-termination.i true 2 wit inspect .12  26 1.3  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  250 true 2 wit inspect 9.6   280  
floats-cbmc-regression/float3_true-unreach-call_true-termination.i true 2 wit inspect .43  56 5.0  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  270 true 2 wit inspect 15     330  
floats-cbmc-regression/float4_true-unreach-call.i true 2 wit inspect 7.4   110 100    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 88    330 true 2 wit inspect 79     430  
floats-cbmc-regression/float5_true-unreach-call_true-termination.i true 2 wit inspect .22  31 2.9  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  260 true 2 wit inspect 29     270  
floats-cbmc-regression/float6_true-unreach-call_true-termination.i true 2 wit inspect .19  29 2.0  - 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 .66  38 7.6  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.9  270 true 2 wit inspect 13     290  
floats-cbmc-regression/float_lib1_true-unreach-call.i true 2 wit inspect .72  27 7.4  - wit inspect - wit inspect - wit inspect - wit inspect error (parsing failed) 0 wit inspect 2.2  140 error (7) 0 wit inspect 11     240  
floats-cbmc-regression/float_lib2_true-unreach-call.i true 2 wit inspect .095 27 .91 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0  250 true 2 wit inspect 16     510  
float-benchs/cast_float_ptr_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .61  42 5.6  true -32 wit inspect 3.0  260 false(unreach-call) 1 wit inspect 12     260   unknown 0 wit inspect 2.0  210 error (2) 0 wit inspect .55   18    - wit inspect - wit inspect
float-benchs/cast_union_loose_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 1.2   51 9.9  true -32 wit inspect 3.8  260 false(unreach-call) 1 wit inspect 13     270   unknown 0 wit inspect 2.1  180 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
float-benchs/cast_union_tight_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 1.2   51 12    true -32 wit inspect 2.1  260 false(unreach-call) 1 wit inspect 7.2   280   unknown 0 wit inspect 2.1  210 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
float-benchs/float_int_inv_square_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .33  42 3.7  false(unreach-call) 1 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 7.0   290   unknown 0 wit inspect 2.8  210 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
float-benchs/inv_Newton_false-unreach-call.c timeout 0 wit inspect 900     1100 6300    error (invalid witness file) 0 wit inspect .41 43 error (2) 0 wit inspect .020 5.0 error (invalid witness file) 0 wit inspect .67 50 error (invalid witness file) 0 wit inspect .0011 .30 - wit inspect - wit inspect
float-benchs/inv_square_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .30  39 3.0  false(unreach-call) 1 wit inspect 3.2  270 false(unreach-call) 1 wit inspect 9.9   290   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
float-benchs/nan_double_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .20  32 2.0  false(unreach-call) 1 wit inspect 2.1  260 false(unreach-call) 1 wit inspect 5.3   220   unknown 0 wit inspect 2.9  210 error (2) 0 wit inspect .55   18    - wit inspect - wit inspect
float-benchs/nan_float_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .20  31 1.8  false(unreach-call) 1 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 4.9   220   unknown 0 wit inspect 1.9  180 error (2) 0 wit inspect .55   18    - wit inspect - wit inspect
float-benchs/sin_interpolated_index_false-unreach-call_true-termination.c false(unreach-call) 0 wit inspect 5.7   320 51    assertion 0 wit inspect 1.7  170 timeout 0 wit inspect 97     1100   assertion 0 wit inspect 2.0  170 true -32 wit inspect .62   18    - wit inspect - wit inspect
float-benchs/sqrt_poly2_false-unreach-call.c false(unreach-call) 1 wit inspect 5.4   280 55    assertion 0 wit inspect 2.1  170 false(unreach-call) 1 wit inspect 17     600   assertion 0 wit inspect 1.8  170 false(unreach-call) 1 wit inspect .57   19    - wit inspect - wit inspect
float-benchs/Muller_Kahan_true-unreach-call_true-termination.c true 2 wit inspect 4.2   260 42    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1600 timeout 0 wit inspect 960     3400  
float-benchs/Rump_double_true-unreach-call_true-termination.c true 2 wit inspect .11  26 .67 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  260 true 2 wit inspect 24     1000  
float-benchs/Rump_float_true-unreach-call_true-termination.c true 2 wit inspect .11  26 .64 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  250 true 2 wit inspect 16     410  
float-benchs/addsub_double_exact_true-unreach-call_true-termination.c true 2 wit inspect .11  26 .75 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  240 true 2 wit inspect 12     270  
float-benchs/addsub_float_exact_true-unreach-call_true-termination.c true 2 wit inspect .077 26 .79 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 11     240  
float-benchs/addsub_float_inexact_true-unreach-call_true-termination.c true 2 wit inspect .078 26 .72 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  250 true 2 wit inspect 6.6   260  
float-benchs/arctan_Pade_true-unreach-call_true-termination.c true 2 wit inspect 120     1200 1000    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 34    500 error (7) 0 wit inspect 39     1100  
float-benchs/bary_diverge_true-unreach-call_true-termination.c timeout 0 wit inspect 900     1000 8500    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .019 4.9
float-benchs/cast_float_union_true-unreach-call.c true 2 wit inspect .11  26 .67 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  260 true 2 wit inspect 4.7   230  
float-benchs/cos_polynomial_true-unreach-call_true-termination.c true 2 wit inspect 17     540 180    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1300 timeout 0 wit inspect 960     2900  
float-benchs/divmul_buf_diverge_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 .54 42 error (2) 0 wit inspect .022 4.8
float-benchs/divmul_diverge_true-unreach-call_true-termination.c timeout 0 wit inspect 900     2400 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .017 4.8
float-benchs/drift_tenth_true-unreach-call_true-termination.c true 2 wit inspect .26  37 2.9  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 13    310 true 2 wit inspect 450     650  
float-benchs/exp_loop_true-unreach-call.c true 2 wit inspect 17     110 190    - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 700    7000 timeout 0 wit inspect 960     1300  
float-benchs/feedback_diverge_true-unreach-call_true-termination.c timeout 0 wit inspect 900     2600 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .018 4.8
float-benchs/filter1_true-unreach-call_true-termination.c true 2 wit inspect 3.4   140 45    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 10    400 true 2 wit inspect 470     900  
float-benchs/filter2_alt_true-unreach-call.c timeout 0 wit inspect 900     670 9000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 41 error (2) 0 wit inspect .020 4.9
float-benchs/filter2_iterated_true-unreach-call.c timeout 0 wit inspect 900     4000 7900    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .022 4.9
float-benchs/filter2_reinit_true-unreach-call_true-termination.c timeout 0 wit inspect 900     1600 6500    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .022 5.0
float-benchs/filter2_set_true-unreach-call_true-termination.c timeout 0 wit inspect 900     1200 9000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 43 error (2) 0 wit inspect .019 4.8
float-benchs/filter2_true-unreach-call_true-termination.c timeout 0 wit inspect 900     1400 6000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 41 error (2) 0 wit inspect .020 4.9
float-benchs/filter_iir_true-unreach-call.c timeout 0 wit inspect 900     1800 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 43 error (2) 0 wit inspect .024 4.8
float-benchs/float_double_true-unreach-call_true-termination.c true 2 wit inspect .098 26 .80 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  250 true 2 wit inspect 12     240  
float-benchs/image_filter_true-unreach-call.c true 2 wit inspect 750     5700 5000    - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 68    7000 timeout 0 wit inspect 960     6700  
float-benchs/interpolation2_true-unreach-call_true-termination.c true 2 wit inspect 5.5   93 65    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    590 timeout 0 wit inspect 960     740  
float-benchs/interpolation_true-unreach-call_true-termination.c true 2 wit inspect 2.3   73 34    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 18    370 timeout 0 wit inspect 960     910  
float-benchs/inv_sqrt_Quake_true-unreach-call_true-termination.c true 2 wit inspect .73  67 9.4  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  280 true 2 wit inspect 130     880  
float-benchs/inv_square_int_true-unreach-call_true-termination.c true 2 wit inspect .23  38 3.4  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  260 true 2 wit inspect 15     310  
float-benchs/inv_square_true-unreach-call_true-termination.c true 2 wit inspect .24  34 2.2  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  260 true 2 wit inspect 62     350  
float-benchs/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 44 error (2) 0 wit inspect .019 4.9
float-benchs/mea8000_true-unreach-call.c timeout 0 wit inspect 900     1700 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .025 4.8
float-benchs/nan_double_range_true-unreach-call_true-termination.c true 2 wit inspect .13  28 1.7  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 6.8   240  
float-benchs/nan_float_range_true-unreach-call_true-termination.c true 2 wit inspect .15  28 1.5  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 8.7   250  
float-benchs/rlim_exit_true-unreach-call_true-termination.c timeout 0 wit inspect 900     2300 9100    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 41 error (2) 0 wit inspect .019 4.9
float-benchs/rlim_invariant_true-unreach-call_true-termination.c true 2 wit inspect 1.2   61 16    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.8  310 timeout 0 wit inspect 960     810  
float-benchs/sin_interpolated_bigrange_loose_true-unreach-call_true-termination.c timeout 0 wit inspect 900     4200 6700    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 41 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     3400 8600    - 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/sin_interpolated_index_true-unreach-call_true-termination.c timeout 0 wit inspect 900     740 9200    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .020 5.0
float-benchs/sin_interpolated_negation_true-unreach-call.c timeout 0 wit inspect 900     3100 6200    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 43 error (2) 0 wit inspect .019 4.9
float-benchs/sin_interpolated_smallrange_true-unreach-call.c timeout 0 wit inspect 900     2700 6900    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .020 5.0
float-benchs/sqrt_Householder_constant_true-unreach-call.c true 2 wit inspect 240     1800 1900    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3500 error (7) 0 wit inspect 250     3000  
float-benchs/sqrt_Householder_interval_true-unreach-call.c timeout 0 wit inspect 900     1500 6100    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .020 4.8
float-benchs/sqrt_Householder_pseudoconstant_true-unreach-call.c timeout 0 wit inspect 900     1500 7800    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .39 43 error (2) 0 wit inspect .019 4.8
float-benchs/sqrt_Newton_pseudoconstant_true-unreach-call.c timeout 0 wit inspect 900     1200 6000    - 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/sqrt_biNewton_pseudoconstant_true-unreach-call.c timeout 0 wit inspect 900     6400 7000    - 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_poly_true-unreach-call_true-termination.c true 2 wit inspect 5.8   310 56    - 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 true 2 wit inspect 4.8   210 57    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1600 error (7) 0 wit inspect 190     2800  
float-benchs/zonotope_2_true-unreach-call_true-termination.c timeout 0 wit inspect 900     4100 9600    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 42 error (2) 0 wit inspect .024 4.9
float-benchs/zonotope_3_true-unreach-call_true-termination.c true 2 wit inspect 1.8   96 22    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.6  340 timeout 0 wit inspect 960     5100  
float-benchs/zonotope_loose_true-unreach-call_true-termination.c true 2 wit inspect 1.2   120 13    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  310 true 2 wit inspect 120     1100  
float-benchs/zonotope_tight_true-unreach-call_true-termination.c true 2 wit inspect 1.2   120 14    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  310 true 2 wit inspect 110     950  
floats-esbmc-regression/Double_div_true-unreach-call.i true 2 wit inspect 130     81 1600    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  320 true 2 wit inspect 250     2700  
floats-esbmc-regression/Float_div_true-unreach-call.i true 2 wit inspect .63  33 7.7  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  280 true 2 wit inspect 230     590  
floats-esbmc-regression/ceil_nondet_true-unreach-call.i true 2 wit inspect .29  38 3.5  - wit inspect - wit inspect - wit inspect - wit inspect error 0 wit inspect 5.2  260 unknown 0 wit inspect 7.9   210  
floats-esbmc-regression/ceil_true-unreach-call.i true 2 wit inspect .15  27 2.1  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.6  260 unknown 0 wit inspect 2.6   200  
floats-esbmc-regression/copysign_true-unreach-call.i true 2 wit inspect .12  27 .94 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.3  250 unknown 0 wit inspect 3.7   210  
floats-esbmc-regression/digits_for_true-unreach-call.i true 2 wit inspect 2.4   190 23    - wit inspect - wit inspect - wit inspect - wit inspect assertion 0 wit inspect 4.0  250 timeout 0 wit inspect 960     3200  
floats-esbmc-regression/digits_while_true-unreach-call.i true 2 wit inspect 2.3   190 24    - wit inspect - wit inspect - wit inspect - wit inspect assertion 0 wit inspect 4.0  250 timeout 0 wit inspect 960     2900  
floats-esbmc-regression/fabs_true-unreach-call.i true 2 wit inspect .085 27 1.0  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  250 true 2 wit inspect 10     280  
floats-esbmc-regression/fdim_true-unreach-call.i true 2 wit inspect .12  27 .91 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.1  250 unknown 0 wit inspect 4.6   210  
floats-esbmc-regression/floor_nondet_true-unreach-call.i true 2 wit inspect .29  38 3.3  - wit inspect - wit inspect - wit inspect - wit inspect error 0 wit inspect 3.9  260 unknown 0 wit inspect 7.3   210  
floats-esbmc-regression/floor_true-unreach-call.i true 2 wit inspect .15  27 1.7  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  260 unknown 0 wit inspect 3.9   200  
floats-esbmc-regression/fmax_true-unreach-call.i true 2 wit inspect .080 27 .90 - wit inspect - wit