Tool 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:29:20 CET 2017-12-01 08:07:14 CET 2017-12-01 08:15:38 CET 2017-12-01 08:19:10 CET 2017-12-01 04:11:27 CET 2017-12-01 07:35:08 CET
Run set cpa-seq.sv-comp18.ReachSafety-Floats cpa-seq-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.ReachSafety-Floats uautomizer-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.ReachSafety-Floats cpa-witness2test-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.ReachSafety-Floats fshell-witness2test-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.ReachSafety-Floats cpa-seq-validate-correctness-witnesses-cpa-seq.sv-comp18-correctness-witness.ReachSafety-Floats uautomizer-validate-correctness-witnesses-cpa-seq.sv-comp18-correctness-witness.ReachSafety-Floats
Options -svcomp18 -heap 10000M -benchmark -timelimit 900s -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-seq.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/cpa-seq.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-seq.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/cpa-seq.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-seq.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/cpa-seq.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 51   350 370 false(unreach-call) 1 wit inspect 56    360 false(unreach-call) 1 wit inspect 49     680   unknown 0 wit inspect 2.8  210 true -32 wit inspect .58   18    - wit inspect - wit inspect
floats-cdfpl/newton_1_5_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 21   350 160 false(unreach-call) 1 wit inspect 22    360 timeout 0 wit inspect 97     690   unknown 0 wit inspect 3.5  180 true -32 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 18   360 130 false(unreach-call) 1 wit inspect 19    360 false(unreach-call) 1 wit inspect 24     670   unknown 0 wit inspect 2.7  210 true -32 wit inspect .58   18    - wit inspect - wit inspect
floats-cdfpl/newton_1_7_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 48   360 340 false(unreach-call) 1 wit inspect 48    360 false(unreach-call) 1 wit inspect 47     680   unknown 0 wit inspect 2.8  210 true -32 wit inspect .58   18    - wit inspect - wit inspect
floats-cdfpl/newton_1_8_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 11   350 83 false(unreach-call) 1 wit inspect 14    370 false(unreach-call) 1 wit inspect 34     670   unknown 0 wit inspect 2.6  180 true -32 wit inspect .58   18    - wit inspect - wit inspect
floats-cdfpl/newton_2_6_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 14   450 120 false(unreach-call) 1 wit inspect 15    460 timeout 0 wit inspect 97     810   unknown 0 wit inspect 2.8  210 true -32 wit inspect .72   18    - wit inspect - wit inspect
floats-cdfpl/newton_2_7_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 70   460 470 false(unreach-call) 1 wit inspect 70    470 timeout 0 wit inspect 97     830   unknown 0 wit inspect 2.7  180 true -32 wit inspect .68   18    - wit inspect - wit inspect
floats-cdfpl/newton_2_8_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 15   450 120 false(unreach-call) 1 wit inspect 16    460 false(unreach-call) 1 wit inspect 28     810   unknown 0 wit inspect 2.7  190 true -32 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 630   1100 4700 false(unreach-call) 1 wit inspect 8.6  560 timeout 0 wit inspect 97     910   unknown 0 wit inspect 3.9  210 false(unreach-call) 1 wit inspect .58   19    - wit inspect - wit inspect
floats-cdfpl/newton_3_7_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 340   570 2400 false(unreach-call) 1 wit inspect 7.8  560 timeout 0 wit inspect 97     880   unknown 0 wit inspect 3.0  210 false(unreach-call) 1 wit inspect .70   18    - wit inspect - wit inspect
floats-cdfpl/newton_3_8_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 17   560 140 false(unreach-call) 1 wit inspect 20    560 timeout 0 wit inspect 97     930   unknown 0 wit inspect 2.8  190 true -32 wit inspect .74   18    - wit inspect - wit inspect
floats-cdfpl/sine_1_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 7.4 300 61 false(unreach-call) 1 wit inspect 8.8  310 false(unreach-call) 1 wit inspect 22     570   unknown 0 wit inspect 2.6  210 true -32 wit inspect .59   18    - wit inspect - wit inspect
floats-cdfpl/sine_2_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 37   330 320 false(unreach-call) 1 wit inspect 43    330 false(unreach-call) 1 wit inspect 28     550   unknown 0 wit inspect 3.2  180 true -32 wit inspect .61   18    - wit inspect - wit inspect
floats-cdfpl/sine_3_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 6.0 300 48 false(unreach-call) 1 wit inspect 6.8  310 timeout 0 wit inspect 97     610   unknown 0 wit inspect 2.7  180 true -32 wit inspect .58   18    - wit inspect - wit inspect
floats-cdfpl/square_1_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 44   360 390 false(unreach-call) 1 wit inspect 3.5  300 timeout 0 wit inspect 97     450   unknown 0 wit inspect 2.7  190 false(unreach-call) 1 wit inspect .67   18    - wit inspect - wit inspect
floats-cdfpl/square_2_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 210   510 1600 false(unreach-call) 1 wit inspect 3.7  320 timeout 0 wit inspect 97     420   unknown 0 wit inspect 2.7  190 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
floats-cdfpl/square_3_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 90   390 710 false(unreach-call) 1 wit inspect 3.8  320 timeout 0 wit inspect 97     450   unknown 0 wit inspect 3.5  210 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
floats-cdfpl/newton_1_1_true-unreach-call_true-termination.i timeout 0 wit inspect 900   720 6000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .024 4.9
floats-cdfpl/newton_1_2_true-unreach-call_true-termination.i timeout 0 wit inspect 900   810 7500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 45 error (2) 0 wit inspect .024 5.0
floats-cdfpl/newton_1_3_true-unreach-call_true-termination.i timeout 0 wit inspect 900   620 6400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .020 4.9
floats-cdfpl/newton_2_1_true-unreach-call_true-termination.i timeout 0 wit inspect 900   550 6200 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 41 error (2) 0 wit inspect .019 4.8
floats-cdfpl/newton_2_2_true-unreach-call_true-termination.i timeout 0 wit inspect 900   1000 6200 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 42 error (2) 0 wit inspect .020 4.9
floats-cdfpl/newton_2_3_true-unreach-call_true-termination.i timeout 0 wit inspect 900   560 5700 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 41 error (2) 0 wit inspect .019 5.0
floats-cdfpl/newton_2_4_true-unreach-call_true-termination.i timeout 0 wit inspect 900   650 6700 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 45 error (2) 0 wit inspect .019 4.9
floats-cdfpl/newton_2_5_true-unreach-call_true-termination.i timeout 0 wit inspect 900   640 6900 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 44 error (2) 0 wit inspect .024 5.0
floats-cdfpl/newton_3_1_true-unreach-call_true-termination.i timeout 0 wit inspect 900   910 7700 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .023 4.8
floats-cdfpl/newton_3_2_true-unreach-call_true-termination.i timeout 0 wit inspect 900   670 5700 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .021 4.9
floats-cdfpl/newton_3_3_true-unreach-call_true-termination.i timeout 0 wit inspect 900   790 6300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 43 error (2) 0 wit inspect .022 4.9
floats-cdfpl/newton_3_4_true-unreach-call_true-termination.i timeout 0 wit inspect 900   810 6100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .019 4.9
floats-cdfpl/newton_3_5_true-unreach-call_true-termination.i timeout 0 wit inspect 900   700 6500 - 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
floats-cdfpl/sine_4_true-unreach-call_true-termination.i timeout 0 wit inspect 900   660 7500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .020 4.9
floats-cdfpl/sine_5_true-unreach-call_true-termination.i timeout 0 wit inspect 900   750 9200 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .019 4.9
floats-cdfpl/sine_6_true-unreach-call_true-termination.i timeout 0 wit inspect 900   900 7100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 43 error (2) 0 wit inspect .018 4.8
floats-cdfpl/sine_7_true-unreach-call_true-termination.i timeout (true) 0 wit inspect 900   820 7200 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 640    590 timeout 0 wit inspect 960     780  
floats-cdfpl/sine_8_true-unreach-call_true-termination.i true 2 wit inspect 780   690 6800 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 560    540 timeout 0 wit inspect 960     830  
floats-cdfpl/square_4_true-unreach-call_true-termination.i true 2 wit inspect 700   710 5300 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 610    570 true 2 wit inspect 730     850  
floats-cdfpl/square_5_true-unreach-call_true-termination.i true 2 wit inspect 620   610 5100 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 470    500 true 2 wit inspect 530     710  
floats-cdfpl/square_6_true-unreach-call_true-termination.i true 2 wit inspect 440   610 3400 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 240    500 true 2 wit inspect 410     770  
floats-cdfpl/square_7_true-unreach-call_true-termination.i timeout 0 wit inspect 900   610 6000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .019 4.8
floats-cdfpl/square_8_true-unreach-call_true-termination.i true 2 wit inspect 280   500 2800 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 59    360 true 2 wit inspect 120     630  
floats-cbmc-regression/float-div1_true-unreach-call.i true 2 wit inspect 10   550 86 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.3  320 true 2 wit inspect 35     610  
floats-cbmc-regression/float-flags-simp1_true-unreach-call.i true 2 wit inspect 7.4 410 58 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 12    790 true 2 wit inspect 34     710  
floats-cbmc-regression/float-no-simp1_true-unreach-call_true-termination.i true 2 wit inspect 2.6 270 22 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 9.4   240  
floats-cbmc-regression/float-no-simp2_true-unreach-call.i true 2 wit inspect 11   310 140 - 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 2.6 270 23 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  250 true 2 wit inspect 9.1   230  
floats-cbmc-regression/float-no-simp4_true-unreach-call.i true 2 wit inspect 5.0 300 42 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.5  260 true 2 wit inspect 45     580  
floats-cbmc-regression/float-no-simp6_true-unreach-call_true-termination.i true 2 wit inspect 2.4 240 19 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 10     290  
floats-cbmc-regression/float-no-simp7_true-unreach-call_true-termination.i true 2 wit inspect 2.3 250 20 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  250 true 2 wit inspect 12     250  
floats-cbmc-regression/float-no-simp8_true-unreach-call.i true 2 wit inspect 2.9 260 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.5  260 true 2 wit inspect 10     300  
floats-cbmc-regression/float-rounding1_true-unreach-call.i unknown 0 wit inspect 6.3 440 57 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 43 error (2) 0 wit inspect .019 4.9
floats-cbmc-regression/float-to-double1_true-unreach-call.i true 2 wit inspect 4.9 300 40 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.6  270 true 2 wit inspect 120     440  
floats-cbmc-regression/float-to-double2_true-unreach-call_true-termination.i true 2 wit inspect 2.3 230 21 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 9.5   240  
floats-cbmc-regression/float-zero-sum1_true-unreach-call_true-termination.i true 2 wit inspect 2.5 250 24 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  250 true 2 wit inspect 12     290  
floats-cbmc-regression/float11_true-unreach-call_true-termination.i true 2 wit inspect 2.3 250 19 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  250 true 2 wit inspect 10     240  
floats-cbmc-regression/float12_true-unreach-call_true-termination.i true 2 wit inspect 2.9 270 28 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 15     260  
floats-cbmc-regression/float13_true-unreach-call_true-termination.i true 2 wit inspect 2.4 250 23 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 10     250  
floats-cbmc-regression/float14_true-unreach-call.i true 2 wit inspect 3.1 260 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  260 true 2 wit inspect 12     290  
floats-cbmc-regression/float18_true-unreach-call.i true 2 wit inspect 3.0 250 28 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 22    410 unknown 0 wit inspect 3.9   200  
floats-cbmc-regression/float19_true-unreach-call.i true 2 wit inspect 4.6 300 43 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.2  280 true 2 wit inspect 13     270  
floats-cbmc-regression/float1_true-unreach-call_true-termination.i true 2 wit inspect 2.5 260 19 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 9.0   240  
floats-cbmc-regression/float20_true-unreach-call_true-termination.i true 2 wit inspect 2.4 250 24 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 16     390  
floats-cbmc-regression/float21_true-unreach-call.i true 2 wit inspect 5.1 300 49 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.1  300 true 2 wit inspect 79     590  
floats-cbmc-regression/float22_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 4.7 300 39 - wit inspect - wit inspect - wit inspect - wit inspect false(unreach-call) -16 wit inspect 5.3  270 true 2 wit inspect 98     670  
floats-cbmc-regression/float2_true-unreach-call_true-termination.i true 2 wit inspect 2.3 250 23 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 10     270  
floats-cbmc-regression/float3_true-unreach-call_true-termination.i true 2 wit inspect 2.3 240 21 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  270 true 2 wit inspect 15     330  
floats-cbmc-regression/float4_true-unreach-call.i true 2 wit inspect 27   330 340 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 84    330 true 2 wit inspect 82     430  
floats-cbmc-regression/float5_true-unreach-call_true-termination.i true 2 wit inspect 2.4 260 20 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  260 true 2 wit inspect 30     270  
floats-cbmc-regression/float6_true-unreach-call_true-termination.i true 2 wit inspect 2.5 250 22 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  260 true 2 wit inspect 12     290  
floats-cbmc-regression/float8_true-unreach-call.i true 2 wit inspect 14   300 150 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.5  270 true 2 wit inspect 13     290  
floats-cbmc-regression/float_lib1_true-unreach-call.i error (parsing failed) 0 wit inspect 1.7 130 16 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .50 43 error (2) 0 wit inspect .020 4.9
floats-cbmc-regression/float_lib2_true-unreach-call.i true 2 wit inspect 2.9 250 24 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.5  250 true 2 wit inspect 17     520  
float-benchs/cast_float_ptr_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.8 260 26 false(unreach-call) 1 wit inspect 3.2  270 false(unreach-call) 1 wit inspect 14     270   unknown 0 wit inspect 3.2  180 true -32 wit inspect .60   18    - wit inspect - wit inspect
float-benchs/cast_union_loose_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.4 270 30 false(unreach-call) 1 wit inspect 3.4  270 true -32 wit inspect 4.7   230   unknown 0 wit inspect 2.9  180 true -32 wit inspect .58   18    - wit inspect - wit inspect
float-benchs/cast_union_tight_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.1 280 29 false(unreach-call) 1 wit inspect 3.2  270 true -32 wit inspect 5.8   230   unknown 0 wit inspect 2.7  210 true -32 wit inspect .58   19    - wit inspect - wit inspect
float-benchs/float_int_inv_square_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.6 260 25 false(unreach-call) 1 wit inspect 3.2  270 false(unreach-call) 1 wit inspect 9.7   290   unknown 0 wit inspect 3.2  190 true -32 wit inspect .59   18    - wit inspect - wit inspect
float-benchs/inv_Newton_false-unreach-call.c false(unreach-call) 1 wit inspect 3.8 350 38 false(unreach-call) 1 wit inspect 4.7  340 error (7) 0 wit inspect 19     500   unknown 0 wit inspect 3.0  210 true -32 wit inspect .60   19    - wit inspect - wit inspect
float-benchs/inv_square_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.6 260 23 false(unreach-call) 1 wit inspect 3.3  270 false(unreach-call) 1 wit inspect 10     280   unknown 0 wit inspect 3.0  210 true -32 wit inspect .58   18    - wit inspect - wit inspect
float-benchs/nan_double_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.5 250 20 false(unreach-call) 1 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 4.6   220   unknown 0 wit inspect 2.8  210 true -32 wit inspect .71   18    - wit inspect - wit inspect
float-benchs/nan_float_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.6 250 22 false(unreach-call) 1 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 4.4   220   unknown 0 wit inspect 1.9  180 true -32 wit inspect .58   18    - wit inspect - wit inspect
float-benchs/sin_interpolated_index_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 7.4 380 76 false(unreach-call) 1 wit inspect 4.8  320 false(unreach-call) 1 wit inspect 30     1300   unknown 0 wit inspect 3.1  210 false(unreach-call) 1 wit inspect .61   19    - wit inspect - wit inspect
float-benchs/sqrt_poly2_false-unreach-call.c false(unreach-call) 1 wit inspect 5.4 390 55 false(unreach-call) 1 wit inspect 6.3  390 true -32 wit inspect 4.8   230   unknown 0 wit inspect 3.2  210 true -32 wit inspect .75   19    - wit inspect - wit inspect
float-benchs/Muller_Kahan_true-unreach-call_true-termination.c true 2 wit inspect 3.3 260 31 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1800 timeout 0 wit inspect 960     4400  
float-benchs/Rump_double_true-unreach-call_true-termination.c true 2 wit inspect 2.3 250 18 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 27     990  
float-benchs/Rump_float_true-unreach-call_true-termination.c true 2 wit inspect 2.4 250 21 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 15     420  
float-benchs/addsub_double_exact_true-unreach-call_true-termination.c true 2 wit inspect 2.4 250 18 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 9.6   270  
float-benchs/addsub_float_exact_true-unreach-call_true-termination.c true 2 wit inspect 2.3 240 21 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 10     250  
float-benchs/addsub_float_inexact_true-unreach-call_true-termination.c true 2 wit inspect 2.4 240 20 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  250 true 2 wit inspect 10     250  
float-benchs/arctan_Pade_true-unreach-call_true-termination.c true 2 wit inspect 87   560 810 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 31    500 error (7) 0 wit inspect 150     2700  
float-benchs/bary_diverge_true-unreach-call_true-termination.c timeout 0 wit inspect 900   4700 9200 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .020 4.8
float-benchs/cast_float_union_true-unreach-call.c true 2 wit inspect 2.4 250 24 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  250 true 2 wit inspect 5.0   240  
float-benchs/cos_polynomial_true-unreach-call_true-termination.c timeout 0 wit inspect 900   1600 5900 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .020 4.9
float-benchs/divmul_buf_diverge_true-unreach-call_true-termination.c timeout 0 wit inspect 900   2800 8400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .39 45 error (2) 0 wit inspect .019 4.9
float-benchs/divmul_diverge_true-unreach-call_true-termination.c timeout 0 wit inspect 900   2700 9200 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .020 4.9
float-benchs/drift_tenth_true-unreach-call_true-termination.c true 2 wit inspect 2.4 250 21 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 16    380 true 2 wit inspect 230     670  
float-benchs/exp_loop_true-unreach-call.c true 2 wit inspect 790   8500 8000 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 650    7000 timeout 0 wit inspect 960     1800  
float-benchs/feedback_diverge_true-unreach-call_true-termination.c timeout 0 wit inspect 900   1900 8800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 43 error (2) 0 wit inspect .019 4.8
float-benchs/filter1_true-unreach-call_true-termination.c true 2 wit inspect 18   790 130 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 13    430 false(unreach-call) -16 wit inspect 420     820  
float-benchs/filter2_alt_true-unreach-call.c timeout 0 wit inspect 900   1200 7000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .020 4.8
float-benchs/filter2_iterated_true-unreach-call.c timeout 0 wit inspect 900   2400 8200 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 41 error (2) 0 wit inspect .019 5.0
float-benchs/filter2_reinit_true-unreach-call_true-termination.c timeout 0 wit inspect 900   3000 8100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .020 5.0
float-benchs/filter2_set_true-unreach-call_true-termination.c timeout 0 wit inspect 910   3800 8300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .020 5.0
float-benchs/filter2_true-unreach-call_true-termination.c timeout 0 wit inspect 900   3900 9700 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .020 4.9
float-benchs/filter_iir_true-unreach-call.c true 2 wit inspect 2.7 260 23 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2700 timeout 0 wit inspect 960     1400  
float-benchs/float_double_true-unreach-call_true-termination.c true 2 wit inspect 2.3 240 21 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  250 true 2 wit inspect 10     250  
float-benchs/image_filter_true-unreach-call.c out of memory 0 wit inspect 690   15000 7800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 44 error (2) 0 wit inspect .024 4.9
float-benchs/interpolation2_true-unreach-call_true-termination.c timeout 0 wit inspect 900   660 9800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .026 4.8
float-benchs/interpolation_true-unreach-call_true-termination.c true 2 wit inspect 11   410 140 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 21    370 timeout 0 wit inspect 960     870  
float-benchs/inv_sqrt_Quake_true-unreach-call_true-termination.c true 2 wit inspect 5.5 300 64 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.5  290 true 2 wit inspect 140     830  
float-benchs/inv_square_int_true-unreach-call_true-termination.c true 2 wit inspect 3.3 280 32 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  260 true 2 wit inspect 70     350  
float-benchs/inv_square_true-unreach-call_true-termination.c true 2 wit inspect 3.4 280 34 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  260 true 2 wit inspect 60     360  
float-benchs/loop_true-unreach-call.c timeout 0 wit inspect 900   3500 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .025 4.9
float-benchs/mea8000_true-unreach-call.c timeout 0 wit inspect 900   4900 9800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .80 43 error (2) 0 wit inspect .019 5.0
float-benchs/nan_double_range_true-unreach-call_true-termination.c true 2 wit inspect 3.0 270 24 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 9.5   240  
float-benchs/nan_float_range_true-unreach-call_true-termination.c true 2 wit inspect 3.0 270 28 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 12     250  
float-benchs/rlim_exit_true-unreach-call_true-termination.c timeout 0 wit inspect 900   3000 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .019 4.9
float-benchs/rlim_invariant_true-unreach-call_true-termination.c true 2 wit inspect 8.8 500 70 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.8  320 error (7) 0 wit inspect 740     810  
float-benchs/sin_interpolated_bigrange_loose_true-unreach-call_true-termination.c timeout 0 wit inspect 900   1200 8500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .022 4.8
float-benchs/sin_interpolated_bigrange_tight_true-unreach-call_true-termination.c timeout 0 wit inspect 900   1400 8300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 41 error (2) 0 wit inspect .021 4.8
float-benchs/sin_interpolated_index_true-unreach-call_true-termination.c timeout 0 wit inspect 900   720 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .023 4.9
float-benchs/sin_interpolated_negation_true-unreach-call.c timeout 0 wit inspect 900   2700 7200 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 44 error (2) 0 wit inspect .020 4.8
float-benchs/sin_interpolated_smallrange_true-unreach-call.c timeout 0 wit inspect 900   4000 9000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 41 error (2) 0 wit inspect .023 4.8
float-benchs/sqrt_Householder_constant_true-unreach-call.c true 2 wit inspect 3.9 260 29 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1600 false(unreach-call) -16 wit inspect 31     1100  
float-benchs/sqrt_Householder_interval_true-unreach-call.c timeout 0 wit inspect 900   1300 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .019 4.9
float-benchs/sqrt_Householder_pseudoconstant_true-unreach-call.c timeout 0 wit inspect 900   2600 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 41 error (2) 0 wit inspect .020 5.0
float-benchs/sqrt_Newton_pseudoconstant_true-unreach-call.c timeout 0 wit inspect 900   1800 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .021 5.0
float-benchs/sqrt_biNewton_pseudoconstant_true-unreach-call.c timeout 0 wit inspect 900   1900 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .021 4.9
float-benchs/sqrt_poly_true-unreach-call_true-termination.c true 2 wit inspect 45   510 440 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 40    490 true 2 wit inspect 140     1000  
float-benchs/water_pid_true-unreach-call_true-termination.c true 2 wit inspect 4.4 270 35 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1600 error (7) 0 wit inspect 190     2900  
float-benchs/zonotope_2_true-unreach-call_true-termination.c timeout 0 wit inspect 900   2300 6900 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .019 4.9
float-benchs/zonotope_3_true-unreach-call_true-termination.c true 2 wit inspect 160   2300 1900 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.7  390 false(unreach-call) -16 wit inspect 25     400  
float-benchs/zonotope_loose_true-unreach-call_true-termination.c true 2 wit inspect 5.4 330 54 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8  310 true 2 wit inspect 120     910  
float-benchs/zonotope_tight_true-unreach-call_true-termination.c true 2 wit inspect 5.5 330 63 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.9  310 true 2 wit inspect 120     960  
floats-esbmc-regression/Double_div_true-unreach-call.i true 2 wit inspect 5.8 460 43 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 19    580 timeout 0 wit inspect 960     1800  
floats-esbmc-regression/Float_div_true-unreach-call.i true 2 wit inspect 3.4 260 28 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8  320 timeout 0 wit inspect 960     1200  
floats-esbmc-regression/ceil_nondet_true-unreach-call.i unknown 0 wit inspect 5.9 410 47 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 44 error (2) 0 wit inspect .017 4.9
floats-esbmc-regression/ceil_true-unreach-call.i true 2 wit inspect 3.1 250 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.7  260 unknown 0 wit inspect 3.7   200  
floats-esbmc-regression/copysign_true-unreach-call.i true 2 wit inspect 3.0 250 28 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.6  260 unknown 0 wit inspect 3.9   200  
floats-esbmc-regression/digits_for_true-unreach-call.i assertion 0 wit inspect 1.9 180 17 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 42 error (2) 0 wit inspect .019 4.9
floats-esbmc-regression/digits_while_true-unreach-call.i assertion 0 wit inspect 1.9 180 18 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .020 4.9
floats-esbmc-regression/fabs_true-unreach-call.i true 2 wit inspect 4.8 290 40 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  250 true 2 wit inspect 10     280  
floats-esbmc-regression/fdim_true-unreach-call.i true 2 wit inspect 3.0 250 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.6  260 unknown 0 wit inspect 4.0   200  
floats-esbmc-regression/floor_nondet_true-unreach-call.i unknown 0 wit inspect 5.8 420 52 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 43 error (2) 0 wit inspect .020 4.9
floats-esbmc-regression/floor_true-unreach-call.i true 2 wit inspect 3.1 250 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  260 unknown 0 wit inspect 4.1   200  
floats-esbmc-regression/fmax_true-unreach-call.i true 2 wit inspect 3.1 260 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4  250 true 2 wit inspect 9.8   290  
floats-esbmc-regression/fmin_true-unreach-call.i true 2 wit inspect 2.9 250 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4  250 true 2 wit inspect 9.4   270  
floats-esbmc-regression/fmod2_true-unreach-call.i true 2 wit inspect 11   500 120 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.7  470 unknown 0 wit inspect 7.3   200  
floats-esbmc-regression/fmod3_true-unreach-call.i true 2 wit inspect 11   500 110 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.3  470 unknown 0 wit inspect 7.6   200  
floats-esbmc-regression/fmod_true-unreach-call.i true 2 wit inspect 2.9 250 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0  250 unknown 0 wit inspect 3.9   210  
floats-esbmc-regression/isgreater_true-unreach-call.i true 2 wit inspect 3.2 250 28 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  260 true 2 wit inspect 9.1   270  
floats-esbmc-regression/isgreaterequal_true-unreach-call.i true 2 wit inspect 2.9 250 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  260 true 2 wit inspect 11     260  
floats-esbmc-regression/isless_true-unreach-call.i true 2 wit inspect 3.0 260 23 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  250 true 2 wit inspect 9.3   260  
floats-esbmc-regression/islessequal_true-unreach-call.i true 2 wit inspect 3.0 260 28 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  250 true 2 wit inspect 9.2   260  
floats-esbmc-regression/islessgreater_true-unreach-call.i true 2 wit inspect 2.9 250 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  250 true 2 wit inspect 8.6   270  
floats-esbmc-regression/isunordered_true-unreach-call.i true 2 wit inspect 3.1 260 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  260 true 2 wit inspect 11     260  
floats-esbmc-regression/lrint_true-unreach-call.i unknown 0 wit inspect 6.3 440 46 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .46 43 error (2) 0 wit inspect .018 4.9
floats-esbmc-regression/modf_true-unreach-call.i true 2 wit inspect 2.9 250 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8  250 unknown 0 wit inspect 3.7   200  
floats-esbmc-regression/nan_true-unreach-call.i true 2 wit inspect 3.0 250 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8  260 true 2 wit inspect 11     280  
floats-esbmc-regression/nearbyint2_true-unreach-call.i unknown 0 wit inspect 6.8 440 57 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .019 4.9
floats-esbmc-regression/nearbyint_true-unreach-call.i unknown 0 wit inspect 8.6 460 68 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .020 4.9
floats-esbmc-regression/remainder_true-unreach-call.i true 2 wit inspect 3.0 260 23 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.4  260 unknown 0 wit inspect 4.6   200  
floats-esbmc-regression/rint2_true-unreach-call.i unknown 0 wit inspect 6.9 440 59 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 42 error (2) 0 wit inspect .019 4.9
floats-esbmc-regression/rint_true-unreach-call.i unknown 0 wit inspect 7.6 440 63 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .018 5.0
floats-esbmc-regression/round_nondet_true-unreach-call.i unknown 0 wit inspect 6.7 430 56 - 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
floats-esbmc-regression/round_true-unreach-call.i true 2 wit inspect 3.1 260 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3  260 unknown 0 wit inspect 4.2   200  
floats-esbmc-regression/rounding_functions_true-unreach-call.i true 2 wit inspect 3.3 260 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.5  260 unknown 0 wit inspect 3.9   210  
floats-esbmc-regression/trunc_nondet_2_true-unreach-call.i true 2 wit inspect 10   310 110 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.8  270 unknown 0 wit inspect 8.1   210  
floats-esbmc-regression/trunc_nondet_true-unreach-call.i unknown 0 wit inspect 6.0 400 44 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .019 4.9
floats-esbmc-regression/trunc_true-unreach-call.i true 2 wit inspect 2.9 260 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  250 unknown 0 wit inspect 4.4   200  
floats-esbmc-regression/Double_div_bad_false-unreach-call.i false(unreach-call) 1 wit inspect 88   2000 1100 false(unreach-call) 1 wit inspect 26    960 timeout 0 wit inspect 97     6100   unknown 0 wit inspect 20    680 false(unreach-call) 1 wit inspect 2.1    62    - wit inspect - wit inspect
floats-esbmc-regression/Float_div_bad_false-unreach-call.i false(unreach-call) 1 wit inspect 10   460 80 false(unreach-call) 1 wit inspect 8.5  290 timeout 0 wit inspect 96     4000   unknown 0 wit inspect 6.2  290 false(unreach-call) 1 wit inspect .78   25    - wit inspect - wit inspect
floats-esbmc-regression/digits_bad_for_false-unreach-call.i assertion 0 wit inspect 1.9 210 16 error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .88 49 error (invalid witness file) 0 wit inspect .0013 .30 - wit inspect - wit inspect
floats-esbmc-regression/digits_bad_while_false-unreach-call.i assertion 0 wit inspect 1.8 180 18 error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .83 47 error (invalid witness file) 0 wit inspect .0016 .26 - 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 181 45000   140000 400000 31 29 440 11000 31 -83 1500 26000 31 0 110 6400 31 -664 20   580 141 144 7400   42000 141 68 13000 49000
    correct results 113 197 6000   50000 51000 29 29 440 11000 13 13 310 7200 0 8 8 6.7 200 80 160 3100   25000 58 116 3700 24000
        correct true 84 168 4200   37000 38000 0 0 0 0 80 160 3100   25000 58 116 3700 24000
        correct false 29 29 1800   13000 14000 29 29 440 11000 13 13 310 7200 0 8 8 6.7 200 0 0
    incorrect results 1 -16 4.7 300 39 0 3 -96 15 680 0 21 -672 13   390 1 -16 5.3 270 3 -48 480 2300
        incorrect true 0 0 3 -96 15 680 0 21 -672 13   390 0 0
        incorrect false 1 -16 4.7 300 39 0 0 0 0 1 -16 5.3 270 3 -48 480 2300
score (172 tasks, max score: 313) 181 29 -83 0 -664 144 68
Run set cpa-seq.sv-comp18.ReachSafety-Floats cpa-seq-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.ReachSafety-Floats uautomizer-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.ReachSafety-Floats cpa-witness2test-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.ReachSafety-Floats fshell-witness2test-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.ReachSafety-Floats cpa-seq-validate-correctness-witnesses-cpa-seq.sv-comp18-correctness-witness.ReachSafety-Floats uautomizer-validate-correctness-witnesses-cpa-seq.sv-comp18-correctness-witness.ReachSafety-Floats