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* [apollon010; apollon035; apollon045; apollon077; apollon078; apollon138] [apollon007; apollon077; apollon078; apollon143] 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-01 08:49:27 CET 2017-12-01 22:53:44 CET 2017-12-01 23:38:04 CET 2017-12-01 23:47:42 CET 2017-12-01 23:55:24 CET 2017-12-01 22:20:30 CET 2017-12-01 23:01:53 CET
Run set esbmc-incr.sv-comp18.ReachSafety-Floats cpa-seq-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.ReachSafety-Floats uautomizer-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.ReachSafety-Floats cpa-witness2test-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.ReachSafety-Floats fshell-witness2test-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.ReachSafety-Floats cpa-seq-validate-correctness-witnesses-esbmc-incr.sv-comp18-correctness-witness.ReachSafety-Floats uautomizer-validate-correctness-witnesses-esbmc-incr.sv-comp18-correctness-witness.ReachSafety-Floats
Options -s incr -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-incr.2017-12-01_0849.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-incr.2017-12-01_0849.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-incr.2017-12-01_0849.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-incr.2017-12-01_0849.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-incr.2017-12-01_0849.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/esbmc-incr.2017-12-01_0849.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.6   190 74    false(unreach-call) 1 wit inspect 5.2  360 false(unreach-call) 1 wit inspect 41     680   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 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 6.8   190 81    false(unreach-call) 1 wit inspect 5.8  360 timeout 0 wit inspect 97     690   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .57   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 29    false(unreach-call) 1 wit inspect 5.8  350 false(unreach-call) 1 wit inspect 18     670   unknown 0 wit inspect 2.9  210 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
floats-cdfpl/newton_1_7_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 10     190 100    false(unreach-call) 1 wit inspect 4.7  360 false(unreach-call) 1 wit inspect 43     670   unknown 0 wit inspect 2.8  180 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.5   190 66    false(unreach-call) 1 wit inspect 4.9  360 false(unreach-call) 1 wit inspect 24     670   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .61   18    - wit inspect - wit inspect
floats-cdfpl/newton_2_6_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 16     340 130    false(unreach-call) 1 wit inspect 6.6  460 timeout 0 wit inspect 97     820   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .68   18    - wit inspect - wit inspect
floats-cdfpl/newton_2_7_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 16     350 130    false(unreach-call) 1 wit inspect 8.0  450 timeout 0 wit inspect 97     820   unknown 0 wit inspect 2.8  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 110    false(unreach-call) 1 wit inspect 7.2  460 false(unreach-call) 1 wit inspect 28     820   unknown 0 wit inspect 2.9  210 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
floats-cdfpl/newton_3_6_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 18     510 150    false(unreach-call) 1 wit inspect 10    560 timeout 0 wit inspect 97     900   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
floats-cdfpl/newton_3_7_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 170     520 1200    false(unreach-call) 1 wit inspect 7.5  560 timeout 0 wit inspect 97     870   unknown 0 wit inspect 3.0  210 false(unreach-call) 1 wit inspect .57   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 9.5  560 timeout 0 wit inspect 97     940   unknown 0 wit inspect 2.8  190 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.2   130 67    true -32 wit inspect 3.4  250 false(unreach-call) 1 wit inspect 17     560   unknown 0 wit inspect 2.7  180 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.9   130 27    true -32 wit inspect 3.1  250 false(unreach-call) 1 wit inspect 29     560   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
floats-cdfpl/sine_3_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 5.6   130 57    true -32 wit inspect 3.7  260 timeout 0 wit inspect 97     630   unknown 0 wit inspect 2.0  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 31    true -32 wit inspect 4.1  280 timeout 0 wit inspect 97     450   unknown 0 wit inspect 2.7  190 false(unreach-call) 1 wit inspect .61   18    - wit inspect - wit inspect
floats-cdfpl/square_2_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 2.9   130 40    false(unreach-call) 1 wit inspect 4.0  290 timeout 0 wit inspect 97     430   unknown 0 wit inspect 2.8  210 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.3   130 37    true -32 wit inspect 3.8  260 timeout 0 wit inspect 97     430   unknown 0 wit inspect 2.0  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 180    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    590 timeout 0 wit inspect 960     990  
floats-cdfpl/newton_1_2_true-unreach-call_true-termination.i true 2 wit inspect 48     210 420    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    600 timeout 0 wit inspect 960     1000  
floats-cdfpl/newton_1_3_true-unreach-call_true-termination.i true 2 wit inspect 46     210 380    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    590 timeout 0 wit inspect 960     880  
floats-cdfpl/newton_2_1_true-unreach-call_true-termination.i true 2 wit inspect 74     380 610    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    560 timeout 0 wit inspect 960     980  
floats-cdfpl/newton_2_2_true-unreach-call_true-termination.i true 2 wit inspect 90     390 1000    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    840 timeout 0 wit inspect 960     960  
floats-cdfpl/newton_2_3_true-unreach-call_true-termination.i true 2 wit inspect 79     390 580    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    550 timeout 0 wit inspect 960     940  
floats-cdfpl/newton_2_4_true-unreach-call_true-termination.i true 2 wit inspect 88     380 840    - 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 410     430 3200    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    540 timeout 0 wit inspect 960     1000  
floats-cdfpl/newton_3_1_true-unreach-call_true-termination.i true 2 wit inspect 190     610 2000    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    620 timeout 0 wit inspect 960     1100  
floats-cdfpl/newton_3_2_true-unreach-call_true-termination.i true 2 wit inspect 650     680 4400    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    560 timeout 0 wit inspect 960     1100  
floats-cdfpl/newton_3_3_true-unreach-call_true-termination.i true 2 wit inspect 240     620 1600    - 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 470     680 4700    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    700 timeout 0 wit inspect 960     1100  
floats-cdfpl/newton_3_5_true-unreach-call_true-termination.i true 2 wit inspect 500     640 3300    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    590 timeout 0 wit inspect 960     1100  
floats-cdfpl/sine_4_true-unreach-call_true-termination.i true 2 wit inspect 130     180 970    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    500 timeout 0 wit inspect 960     850  
floats-cdfpl/sine_5_true-unreach-call_true-termination.i true 2 wit inspect 19     140 170    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    510 timeout 0 wit inspect 960     880  
floats-cdfpl/sine_6_true-unreach-call_true-termination.i true 2 wit inspect 6.7   130 85    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    650 timeout 0 wit inspect 960     820  
floats-cdfpl/sine_7_true-unreach-call_true-termination.i true 2 wit inspect 6.7   130 76    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 830    590 timeout 0 wit inspect 960     760  
floats-cdfpl/sine_8_true-unreach-call_true-termination.i true 2 wit inspect 5.4   130 57    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 550    540 timeout 0 wit inspect 960     830  
floats-cdfpl/square_4_true-unreach-call_true-termination.i true 2 wit inspect 120     160 1100    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 730    570 true 2 wit inspect 770     720  
floats-cdfpl/square_5_true-unreach-call_true-termination.i true 2 wit inspect 110     150 870    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 430    510 true 2 wit inspect 560     730  
floats-cdfpl/square_6_true-unreach-call_true-termination.i true 2 wit inspect 21     130 240    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 290    500 true 2 wit inspect 420     790  
floats-cdfpl/square_7_true-unreach-call_true-termination.i true 2 wit inspect 27     130 320    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    480 true 2 wit inspect 190     730  
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 71    360 true 2 wit inspect 120     600  
floats-cbmc-regression/float-div1_true-unreach-call.i true 2 wit inspect 1.2   110 12    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.7  320 true 2 wit inspect 34     600  
floats-cbmc-regression/float-flags-simp1_true-unreach-call.i true 2 wit inspect .13  29 1.4  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 12    790 true 2 wit inspect 33     700  
floats-cbmc-regression/float-no-simp1_true-unreach-call_true-termination.i true 2 wit inspect .10  26 .69 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  250 true 2 wit inspect 8.7   240  
floats-cbmc-regression/float-no-simp2_true-unreach-call.i true 2 wit inspect 2.2   71 27    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 19    300 true 2 wit inspect 42     400  
floats-cbmc-regression/float-no-simp3_true-unreach-call_true-termination.i true 2 wit inspect .087 26 .80 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  270 true 2 wit inspect 10     230  
floats-cbmc-regression/float-no-simp4_true-unreach-call.i true 2 wit inspect .21  30 2.1  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.5  270 true 2 wit inspect 43     580  
floats-cbmc-regression/float-no-simp6_true-unreach-call_true-termination.i true 2 wit inspect .10  26 .83 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  250 true 2 wit inspect 13     290  
floats-cbmc-regression/float-no-simp7_true-unreach-call_true-termination.i true 2 wit inspect .095 26 .84 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 9.3   240  
floats-cbmc-regression/float-no-simp8_true-unreach-call.i true 2 wit inspect .12  27 .69 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.1  250 true 2 wit inspect 11     300  
floats-cbmc-regression/float-rounding1_true-unreach-call.i true 2 wit inspect .21  32 2.3  - wit inspect - wit inspect - wit inspect - wit inspect error 0 wit inspect 4.8  260 unknown 0 wit inspect 3.7   200  
floats-cbmc-regression/float-to-double1_true-unreach-call.i true 2 wit inspect .22  31 2.6  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  260 true 2 wit inspect 95     420  
floats-cbmc-regression/float-to-double2_true-unreach-call_true-termination.i true 2 wit inspect .079 26 .67 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 11     230  
floats-cbmc-regression/float-zero-sum1_true-unreach-call_true-termination.i true 2 wit inspect .13  28 1.6  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  250 true 2 wit inspect 11     290  
floats-cbmc-regression/float11_true-unreach-call_true-termination.i true 2 wit inspect .12  27 1.0  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.8  250 true 2 wit inspect 12     240  
floats-cbmc-regression/float12_true-unreach-call_true-termination.i true 2 wit inspect .21  31 2.4  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.3  250 true 2 wit inspect 19     260  
floats-cbmc-regression/float13_true-unreach-call_true-termination.i true 2 wit inspect .077 26 .74 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  250 true 2 wit inspect 14     240  
floats-cbmc-regression/float14_true-unreach-call.i true 2 wit inspect .12  27 .88 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.7  250 true 2 wit inspect 11     300  
floats-cbmc-regression/float18_true-unreach-call.i true 2 wit inspect .23  27 2.1  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 33    410 unknown 0 wit inspect 3.8   200  
floats-cbmc-regression/float19_true-unreach-call.i true 2 wit inspect .15  29 2.3  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8  260 true 2 wit inspect 7.7   280  
floats-cbmc-regression/float1_true-unreach-call_true-termination.i true 2 wit inspect .10  26 .75 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  250 true 2 wit inspect 9.8   240  
floats-cbmc-regression/float20_true-unreach-call_true-termination.i true 2 wit inspect .36  52 4.7  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 19     410  
floats-cbmc-regression/float21_true-unreach-call.i true 2 wit inspect .29  35 3.5  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.5  290 true 2 wit inspect 90     600  
floats-cbmc-regression/float22_true-unreach-call_true-termination.i true 2 wit inspect .60  58 7.2  - wit inspect - wit inspect - wit inspect - wit inspect false(unreach-call) -16 wit inspect 5.1  280 true 2 wit inspect 270     1100  
floats-cbmc-regression/float2_true-unreach-call_true-termination.i true 2 wit inspect .16  26 1.3  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 13     280  
floats-cbmc-regression/float3_true-unreach-call_true-termination.i true 2 wit inspect .39  56 4.7  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  270 true 2 wit inspect 16     320  
floats-cbmc-regression/float4_true-unreach-call.i true 2 wit inspect 7.4   110 87    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 83    330 true 2 wit inspect 78     430  
floats-cbmc-regression/float5_true-unreach-call_true-termination.i true 2 wit inspect .24  31 2.2  - 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 .16  29 2.1  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 12     280  
floats-cbmc-regression/float8_true-unreach-call.i true 2 wit inspect .64  38 7.9  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.4  270 true 2 wit inspect 15     290  
floats-cbmc-regression/float_lib1_true-unreach-call.i true 2 wit inspect .70  27 6.6  - wit inspect - wit inspect - wit inspect - wit inspect error (parsing failed) 0 wit inspect 2.8  140 error (7) 0 wit inspect 9.8   250  
floats-cbmc-regression/float_lib2_true-unreach-call.i true 2 wit inspect .11  27 .99 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.5  260 true 2 wit inspect 17     510  
float-benchs/cast_float_ptr_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .66  42 5.6  true -32 wit inspect 3.9  260 false(unreach-call) 1 wit inspect 7.7   270   unknown 0 wit inspect 2.0  210 error (2) 0 wit inspect .57   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 8.5  true -32 wit inspect 4.2  260 false(unreach-call) 1 wit inspect 7.2   280   unknown 0 wit inspect 2.9  210 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
float-benchs/cast_union_tight_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 1.2   51 12    true -32 wit inspect 3.4  260 false(unreach-call) 1 wit inspect 7.7   280   unknown 0 wit inspect 2.0  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 .35  42 3.9  false(unreach-call) 1 wit inspect 3.8  260 false(unreach-call) 1 wit inspect 10     300   unknown 0 wit inspect 3.0  210 false(unreach-call) 1 wit inspect .61   18    - wit inspect - wit inspect
float-benchs/inv_Newton_false-unreach-call.c timeout 0 wit inspect 900     1300 6000    error (invalid witness file) 0 wit inspect .56 45 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .86 49 error (invalid witness file) 0 wit inspect .0012 .29 - wit inspect - wit inspect
float-benchs/inv_square_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .32  38 3.3  false(unreach-call) 1 wit inspect 3.2  260 false(unreach-call) 1 wit inspect 9.5   290   unknown 0 wit inspect 2.7  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  31 2.4  false(unreach-call) 1 wit inspect 3.2  260 false(unreach-call) 1 wit inspect 4.9   220   unknown 0 wit inspect 2.9  190 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 .21  31 1.9  false(unreach-call) 1 wit inspect 3.2  260 false(unreach-call) 1 wit inspect 4.5   220   unknown 0 wit inspect 2.7  180 error (2) 0 wit inspect .56   18    - wit inspect - wit inspect
float-benchs/sin_interpolated_index_false-unreach-call_true-termination.c false(unreach-call) 0 wit inspect 5.5   320 63    assertion 0 wit inspect 2.5  170 timeout 0 wit inspect 97     1200   assertion 0 wit inspect 2.7  180 true -32 wit inspect .60   18    - wit inspect - wit inspect
float-benchs/sqrt_poly2_false-unreach-call.c false(unreach-call) 1 wit inspect 5.4   280 46    assertion 0 wit inspect 2.5  160 false(unreach-call) 1 wit inspect 16     600   assertion 0 wit inspect 2.6  170 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
float-benchs/Muller_Kahan_true-unreach-call_true-termination.c true 2 wit inspect .66  26 7.3  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1500 timeout 0 wit inspect 960     3400  
float-benchs/Rump_double_true-unreach-call_true-termination.c true 2 wit inspect .077 26 .84 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  250 true 2 wit inspect 29     990  
float-benchs/Rump_float_true-unreach-call_true-termination.c true 2 wit inspect .085 26 .78 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  250 true 2 wit inspect 13     420  
float-benchs/addsub_double_exact_true-unreach-call_true-termination.c true 2 wit inspect .073 26 .98 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  250 true 2 wit inspect 9.6   270  
float-benchs/addsub_float_exact_true-unreach-call_true-termination.c true 2 wit inspect .070 26 .72 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  250 true 2 wit inspect 9.4   250  
float-benchs/addsub_float_inexact_true-unreach-call_true-termination.c true 2 wit inspect .074 26 .75 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 9.6   250  
float-benchs/arctan_Pade_true-unreach-call_true-termination.c true 2 wit inspect 130     1200 910    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 26    500 error (7) 0 wit inspect 36     1000  
float-benchs/bary_diverge_true-unreach-call_true-termination.c timeout 0 wit inspect 900     1000 7800    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .79 45 error (2) 0 wit inspect .028 4.8
float-benchs/cast_float_union_true-unreach-call.c true 2 wit inspect .075 26 1.0  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 5.0   220  
float-benchs/cos_polynomial_true-unreach-call_true-termination.c true 2 wit inspect 17     540 170    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1300 timeout 0 wit inspect 960     2800  
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 .56 43 error (2) 0 wit inspect .019 4.9
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 .65 43 error (2) 0 wit inspect .022 5.0
float-benchs/drift_tenth_true-unreach-call_true-termination.c true 2 wit inspect .10  26 .93 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 13    310 true 2 wit inspect 480     630  
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 780    7000 timeout 0 wit inspect 960     1100  
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 .62 44 error (2) 0 wit inspect .020 4.8
float-benchs/filter1_true-unreach-call_true-termination.c timeout 0 wit inspect 900     1400 7800    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 42 error (2) 0 wit inspect .019 5.0
float-benchs/filter2_alt_true-unreach-call.c timeout 0 wit inspect 900     560 6800    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .74 43 error (2) 0 wit inspect .019 4.9
float-benchs/filter2_iterated_true-unreach-call.c timeout 0 wit inspect 900     3400 7200    - 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/filter2_reinit_true-unreach-call_true-termination.c timeout 0 wit inspect 900     1400 6300    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .74 43 error (2) 0 wit inspect .019 4.9
float-benchs/filter2_set_true-unreach-call_true-termination.c timeout 0 wit inspect 900     1900 7300    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 45 error (2) 0 wit inspect .019 4.8
float-benchs/filter2_true-unreach-call_true-termination.c timeout 0 wit inspect 900     1700 9000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 44 error (2) 0 wit inspect .024 4.8
float-benchs/filter_iir_true-unreach-call.c timeout 0 wit inspect 900     2300 7500    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 41 error (2) 0 wit inspect .021 4.9
float-benchs/float_double_true-unreach-call_true-termination.c true 2 wit inspect .10  26 .62 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  250 true 2 wit inspect 9.7   240  
float-benchs/image_filter_true-unreach-call.c true 2 wit inspect 660     3000 4200    - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 58    7000 timeout 0 wit inspect 960     6900  
float-benchs/interpolation2_true-unreach-call_true-termination.c true 2 wit inspect 3.1   92 45    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    580 timeout 0 wit inspect 960     680  
float-benchs/interpolation_true-unreach-call_true-termination.c true 2 wit inspect 1.3   71 16    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 17    370 timeout 0 wit inspect 960     900  
float-benchs/inv_sqrt_Quake_true-unreach-call_true-termination.c true 2 wit inspect .75  67 8.6  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  280 true 2 wit inspect 140     850  
float-benchs/inv_square_int_true-unreach-call_true-termination.c true 2 wit inspect .26  38 3.0  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  260 true 2 wit inspect 25     330  
float-benchs/inv_square_true-unreach-call_true-termination.c true 2 wit inspect .23  34 2.6  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  260 true 2 wit inspect 61     360  
float-benchs/loop_true-unreach-call.c timeout 0 wit inspect 900     1300 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 43 error (2) 0 wit inspect .024 4.8
float-benchs/mea8000_true-unreach-call.c timeout 0 wit inspect 900     1400 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 43 error (2) 0 wit inspect .022 4.9
float-benchs/nan_double_range_true-unreach-call_true-termination.c true 2 wit inspect .17  28 1.4  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  250 true 2 wit inspect 12     240  
float-benchs/nan_float_range_true-unreach-call_true-termination.c true 2 wit inspect .16  28 1.7  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4  260 true 2 wit inspect 10     250  
float-benchs/rlim_exit_true-unreach-call_true-termination.c timeout 0 wit inspect 900     2300 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .019 4.9
float-benchs/rlim_invariant_true-unreach-call_true-termination.c timeout 0 wit inspect 900     870 7800    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .021 4.8
float-benchs/sin_interpolated_bigrange_loose_true-unreach-call_true-termination.c timeout 0 wit inspect 900     4200 6400    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .72 42 error (2) 0 wit inspect .022 4.9
float-benchs/sin_interpolated_bigrange_tight_true-unreach-call_true-termination.c timeout 0 wit inspect 900     3400 6400    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 43 error (2) 0 wit inspect .018 4.8
float-benchs/sin_interpolated_index_true-unreach-call_true-termination.c timeout 0 wit inspect 900     740 8700    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .90 43 error (2) 0 wit inspect .019 4.9
float-benchs/sin_interpolated_negation_true-unreach-call.c timeout 0 wit inspect 900     13000 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 44 error (2) 0 wit inspect .024 4.8
float-benchs/sin_interpolated_smallrange_true-unreach-call.c timeout 0 wit inspect 900     13000 8300    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .72 44 error (2) 0 wit inspect .024 4.8
float-benchs/sqrt_Householder_constant_true-unreach-call.c true 2 wit inspect .49  27 5.5  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3100 error (7) 0 wit inspect 270     3000  
float-benchs/sqrt_Householder_interval_true-unreach-call.c timeout 0 wit inspect 900     1900 6500    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .74 44 error (2) 0 wit inspect .019 4.8
float-benchs/sqrt_Householder_pseudoconstant_true-unreach-call.c timeout 0 wit inspect 900     3100 7900    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .019 4.8
float-benchs/sqrt_Newton_pseudoconstant_true-unreach-call.c timeout 0 wit inspect 900     2500 9100    - 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
float-benchs/sqrt_biNewton_pseudoconstant_true-unreach-call.c timeout 0 wit inspect 900     3600 8300    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .021 4.8
float-benchs/sqrt_poly_true-unreach-call_true-termination.c true 2 wit inspect 5.9   310 61    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 50    490 true 2 wit inspect 140     1100  
float-benchs/water_pid_true-unreach-call_true-termination.c true 2 wit inspect 2.6   27 32    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1600 error (7) 0 wit inspect 210     2800  
float-benchs/zonotope_2_true-unreach-call_true-termination.c timeout 0 wit inspect 900     4000 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 41 error (2) 0 wit inspect .022 5.0
float-benchs/zonotope_3_true-unreach-call_true-termination.c timeout 0 wit inspect 900     2700 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 43 error (2) 0 wit inspect .018 4.9
float-benchs/zonotope_loose_true-unreach-call_true-termination.c true 2 wit inspect 1.2   120 12    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  310 true 2 wit inspect 120     930  
float-benchs/zonotope_tight_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.7  310 true 2 wit inspect 110     960  
floats-esbmc-regression/Double_div_true-unreach-call.i true 2 wit inspect 130     100 1600    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.7  310 true 2 wit inspect 250     2700  
floats-esbmc-regression/Float_div_true-unreach-call.i true 2 wit inspect .47  26 6.1  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.9  280 true 2 wit inspect 170     560  
floats-esbmc-regression/ceil_nondet_true-unreach-call.i true 2 wit inspect .32  38 3.9  - wit inspect - wit inspect - wit inspect - wit inspect error 0 wit inspect 5.0  260 unknown 0 wit inspect 7.3   200  
floats-esbmc-regression/ceil_true-unreach-call.i true 2 wit inspect .15  27 1.8  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0  260 unknown 0 wit inspect 4.0   200  
floats-esbmc-regression/copysign_true-unreach-call.i true 2 wit inspect .088 27 .98 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.5  260 unknown 0 wit inspect 3.9   210  
floats-esbmc-regression/digits_for_true-unreach-call.i true 2 wit inspect .37  26 4.0  - wit inspect - wit inspect - wit inspect - wit inspect assertion 0 wit inspect 3.9  260 timeout 0 wit inspect 960     3100  
floats-esbmc-regression/digits_while_true-unreach-call.i true 2 wit inspect .37  26 3.9  - wit inspect - wit inspect - wit inspect - wit inspect assertion 0 wit inspect 3.7  260 timeout 0 wit inspect 960     2900  
floats-esbmc-regression/fabs_true-unreach-call.i true 2 wit inspect .083 27 .87 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.3  250 true 2 wit inspect 11     290  
floats-esbmc-regression/fdim_true-unreach-call.i true 2 wit inspect .12  27 .82 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.7  260 unknown 0 wit inspect 3.8   210  
floats-esbmc-regression/floor_nondet_true-unreach-call.i true 2 wit inspect .32  38 4.0  - wit inspect - wit inspect - wit inspect - wit inspect error 0 wit inspect 2.7  260 unknown 0 wit inspect 8.1   200  
floats-esbmc-regression/floor_true-unreach-call.i true 2 wit inspect .19  27 1.9  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8  250 unknown 0 wit inspect 3.9   210  
floats-esbmc-regression/fmax_true-unreach-call.i true 2 wit inspect .079 27 .87 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.5  260 true 2 wit inspect 9.3   280  
floats-esbmc-regression/fmin_true-unreach-call.i true 2 wit inspect .080 27 1.1  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.1  260 true 2 wit inspect 9.2   270  
floats-esbmc-regression/fmod2_true-unreach-call.i true 2 wit inspect .18  29 1.7  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.9  470 unknown 0 wit inspect 7.7   210  
floats-esbmc-regression/fmod3_true-unreach-call.i true 2 wit inspect .16  29 1.7  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.7  470 unknown 0 wit inspect 7.7   210  
floats-esbmc-regression/fmod_true-unreach-call.i true 2 wit inspect .088 27 .92 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.3  260 unknown 0 wit inspect 4.2   200  
floats-esbmc-regression/isgreater_true-unreach-call.i true 2 wit inspect .10  27 .86 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  250 true 2 wit inspect 9.8   280  
floats-esbmc-regression/isgreaterequal_true-unreach-call.i true 2 wit inspect .080 27 .88 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8  260 true 2 wit inspect 9.1   270  
floats-esbmc-regression/isless_true-unreach-call.i true 2 wit inspect .091 27 1.1  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.6  260 true 2 wit inspect 11     270  
floats-esbmc-regression/islessequal_true-unreach-call.i true 2 wit inspect .082 27 .94 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8  260 true 2 wit inspect 11     270  
floats-esbmc-regression/islessgreater_true-unreach-call.i true 2 wit inspect .11  27 .87 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  260 true 2 wit inspect 9.2   260  
floats-esbmc-regression/isunordered_true-unreach-call.i true 2 wit inspect .079 27 1.0  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.1  260 true 2 wit inspect 6.3   280  
floats-esbmc-regression/lrint_true-unreach-call.i true 2 wit inspect .18  27 2.0  - wit inspect - wit inspect - wit inspect - wit inspect error 0 wit inspect 4.7  250 unknown 0 wit inspect 4.5   200  
floats-esbmc-regression/modf_true-unreach-call.i true 2 wit inspect .16  27 1.7  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.9  250 unknown 0 wit inspect 4.3   210  
floats-esbmc-regression/nan_true-unreach-call.i true 2 wit inspect .11  27 .69 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.7  260 true 2 wit inspect 13     290  
floats-esbmc-regression/nearbyint2_true-unreach-call.i true 2 wit inspect .21  27 1.8  - wit inspect - wit inspect - wit inspect - wit inspect error 0 wit inspect 3.8  250 unknown 0 wit inspect 4.0   210  
floats-esbmc-regression/nearbyint_true-unreach-call.i true 2 wit inspect .19  27 2.3  - wit inspect - wit inspect - wit inspect - wit inspect error 0 wit inspect 6.2  260 unknown 0 wit inspect 5.0   200  
floats-esbmc-regression/remainder_true-unreach-call.i true 2 wit inspect .21  27 1.9  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.2  260 unknown 0 wit inspect 4.0   210  
floats-esbmc-regression/rint2_true-unreach-call.i true 2 wit inspect .18  28 2.1  - wit inspect - wit inspect - wit inspect - wit inspect error 0 wit inspect 5.5  260 unknown 0 wit inspect 4.0   210  
floats-esbmc-regression/rint_true-unreach-call.i true 2 wit inspect .18  28 2.0  - wit inspect - wit inspect - wit inspect - wit inspect error 0 wit inspect 5.7  270 unknown 0 wit inspect 3.8   200  
floats-esbmc-regression/round_nondet_true-unreach-call.i true 2 wit inspect .72  81 8.1  - wit inspect - wit inspect - wit inspect - wit inspect error 0 wit inspect 5.4  260 unknown 0 wit inspect 8.2   210  
floats-esbmc-regression/round_true-unreach-call.i true 2 wit inspect .21  27 2.5  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.2  250 unknown 0 wit inspect 2.8   210  
floats-esbmc-regression/rounding_functions_true-unreach-call.i true 2 wit inspect .27  28 2.6  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.3  260 unknown 0 wit inspect 4.1   210  
floats-esbmc-regression/trunc_nondet_2_true-unreach-call.i true 2 wit inspect 1.2   44 18    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.2  270 unknown 0 wit inspect 8.2   210  
floats-esbmc-regression/trunc_nondet_true-unreach-call.i true 2 wit inspect .31  38 3.9  - wit inspect - wit inspect - wit inspect - wit inspect error 0 wit inspect 5.2  250 unknown 0 wit inspect 5.7   210  
floats-esbmc-regression/trunc_true-unreach-call.i true 2 wit inspect .16  27 1.6  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3  270 unknown 0 wit inspect 4.9   210  
floats-esbmc-regression/Double_div_bad_false-unreach-call.i false(unreach-call) 1 wit inspect 480     250 5900    false(unreach-call) 1 wit inspect 13    430 true -32 wit inspect 31     670   unknown 0 wit inspect 2.7  210 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
floats-esbmc-regression/Float_div_bad_false-unreach-call.i false(unreach-call) 1 wit inspect 1.4   30 16    false(unreach-call) 1 wit inspect 6.0  270 true -32 wit inspect 20     370   unknown 0 wit inspect 2.8  180 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
floats-esbmc-regression/digits_bad_for_false-unreach-call.i false(unreach-call) 0 wit inspect .34  28 3.9  assertion 0 wit inspect 3.0  260 true -32 wit inspect 22     460   unknown 0 wit inspect 2.6  180 true -32 wit inspect .56   18    - wit inspect - wit inspect
floats-esbmc-regression/digits_bad_while_false-unreach-call.i false(unreach-call) 0 wit inspect .35  28 4.2  assertion 0 wit inspect 2.9  250 true -32 wit inspect 40     640   unknown 0 wit inspect 2.7  210 true -32 wit inspect .60   18    - wit inspect - wit inspect
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
total 172 257 29000   100000 280000 31 -238 150 9800 31 -113 1400 17000 31 0 77 6000 31 -72 18   550 141 138 24000   60000 141 122 30000 80000
    correct results 142 257 5100   21000 43000 18 18 110 6900 15 15 270 7100 0 24 24 14   440 77 154 3400   23000 61 122 4700 28000
        correct true 115 230 4300   16000 35000 0 0 0 0 77 154 3400   23000 61 122 4700 28000
        correct false 27 27 790   5200 8400 18 18 110 6900 15 15 270 7100 0 24 24 14   440 0 0
    correct-unconfimed results 3 0 6.2 370 71 0 0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0 0
        correct-unconfirmed false 3 0 6.2 370 71 0 0 0 0 0 0
    incorrect results 0 8 -256 30 2100 4 -128 110 2100 0 3 -96 1.8 55 1 -16 5.1 280 0
        incorrect true 0 8 -256 30 2100 4 -128 110 2100 0 3 -96 1.8 55 0 0
        incorrect false 0 0 0 0 0 1 -16 5.1 280 0
score (172 tasks, max score: 313) 257 -238 -113 0 -72 138 122
Run set esbmc-incr.sv-comp18.ReachSafety-Floats cpa-seq-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.ReachSafety-Floats uautomizer-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.ReachSafety-Floats cpa-witness2test-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.ReachSafety-Floats fshell-witness2test-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.ReachSafety-Floats cpa-seq-validate-correctness-witnesses-esbmc-incr.sv-comp18-correctness-witness.ReachSafety-Floats uautomizer-validate-correctness-witnesses-esbmc-incr.sv-comp18-correctness-witness.ReachSafety-Floats