Tool skink 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* [apollon077; apollon078; apollon155] [apollon030; apollon077; apollon078] [apollon077; apollon078] 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] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 4, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33554 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 22:03:39 CET 2017-12-02 00:36:21 CET 2017-12-02 01:00:42 CET 2017-12-02 01:03:22 CET 2017-12-02 01:04:20 CET 2017-12-02 00:04:19 CET 2017-12-02 00:40:05 CET
Run set skink.sv-comp18.ReachSafety-Floats cpa-seq-validate-violation-witnesses-skink.sv-comp18-violation-witness.ReachSafety-Floats uautomizer-validate-violation-witnesses-skink.sv-comp18-violation-witness.ReachSafety-Floats cpa-witness2test-validate-violation-witnesses-skink.sv-comp18-violation-witness.ReachSafety-Floats fshell-witness2test-validate-violation-witnesses-skink.sv-comp18-violation-witness.ReachSafety-Floats cpa-seq-validate-correctness-witnesses-skink.sv-comp18-correctness-witness.ReachSafety-Floats uautomizer-validate-correctness-witnesses-skink.sv-comp18-correctness-witness.ReachSafety-Floats
Options -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/skink.2017-12-01_2203.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/skink.2017-12-01_2203.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/skink.2017-12-01_2203.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/skink.2017-12-01_2203.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/skink.2017-12-01_2203.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/skink.2017-12-01_2203.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 7.4 350 71 false(unreach-call) 1 wit inspect 86    360 true -32 wit inspect 3.3   240   unknown 0 wit inspect 1.9  190 true -32 wit inspect .57   18    - wit inspect - wit inspect
floats-cdfpl/newton_1_5_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 7.1 360 62 false(unreach-call) 1 wit inspect 64    370 true -32 wit inspect 3.0   220   unknown 0 wit inspect 1.9  180 true -32 wit inspect .61   18    - wit inspect - wit inspect
floats-cdfpl/newton_1_6_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 7.1 340 73 false(unreach-call) 1 wit inspect 52    360 true -32 wit inspect 4.7   230   unknown 0 wit inspect 2.0  190 true -32 wit inspect .59   18    - wit inspect - wit inspect
floats-cdfpl/newton_1_7_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 10   350 97 false(unreach-call) 1 wit inspect 26    360 true -32 wit inspect 4.5   220   unknown 0 wit inspect 2.0  190 true -32 wit inspect .62   18    - wit inspect - wit inspect
floats-cdfpl/newton_1_8_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 6.8 360 59 false(unreach-call) 1 wit inspect 17    360 true -32 wit inspect 2.9   230   unknown 0 wit inspect 2.0  180 true -32 wit inspect .59   18    - wit inspect - wit inspect
floats-cdfpl/newton_2_6_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 15   350 170 timeout 0 wit inspect 91    460 true -32 wit inspect 3.0   230   unknown 0 wit inspect 1.9  180 true -32 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 13   370 120 false(unreach-call) 1 wit inspect 83    460 true -32 wit inspect 4.2   230   unknown 0 wit inspect 2.0  180 true -32 wit inspect .61   18    - wit inspect - wit inspect
floats-cdfpl/newton_2_8_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 12   340 140 false(unreach-call) 1 wit inspect 47    460 true -32 wit inspect 3.1   220   unknown 0 wit inspect 2.0  180 true -32 wit inspect .57   18    - wit inspect - wit inspect
floats-cdfpl/newton_3_6_false-unreach-call_true-termination.i unknown 0 wit inspect 18   360 190 error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .023 4.9 error (invalid witness file) 0 wit inspect .64 49 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
floats-cdfpl/newton_3_7_false-unreach-call_true-termination.i unknown 0 wit inspect 18   370 200 error (invalid witness file) 0 wit inspect .61 42 error (2) 0 wit inspect .023 5.0 error (invalid witness file) 0 wit inspect .65 49 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
floats-cdfpl/newton_3_8_false-unreach-call_true-termination.i unknown 0 wit inspect 17   370 190 error (invalid witness file) 0 wit inspect .60 43 error (2) 0 wit inspect .023 4.9 error (invalid witness file) 0 wit inspect .91 47 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
floats-cdfpl/sine_1_false-unreach-call_true-termination.i unknown 0 wit inspect 5.7 330 52 error (invalid witness file) 0 wit inspect .65 41 error (2) 0 wit inspect .042 4.9 error (invalid witness file) 0 wit inspect .83 47 error (invalid witness file) 0 wit inspect .0034 .28 - wit inspect - wit inspect
floats-cdfpl/sine_2_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 7.2 340 71 false(unreach-call) 1 wit inspect 55    350 false(unreach-call) 1 wit inspect 25     570   unknown 0 wit inspect 1.9  180 true -32 wit inspect .61   18    - wit inspect - wit inspect
floats-cdfpl/sine_3_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 7.0 360 61 timeout 0 wit inspect 91    390 timeout 0 wit inspect 97     610   unknown 0 wit inspect 2.0  190 true -32 wit inspect .57   18    - wit inspect - wit inspect
floats-cdfpl/square_1_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 6.3 400 53 false(unreach-call) 1 wit inspect 23    340 timeout 0 wit inspect 97     460   unknown 0 wit inspect 1.9  180 true -32 wit inspect .58   18    - wit inspect - wit inspect
floats-cdfpl/square_2_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 6.4 400 64 timeout 0 wit inspect 91    390 false(unreach-call) 1 wit inspect 89     410   unknown 0 wit inspect 2.8  190 true -32 wit inspect .57   18    - wit inspect - wit inspect
floats-cdfpl/square_3_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 5.6 310 51 false(unreach-call) 1 wit inspect 76    350 timeout 0 wit inspect 97     440   unknown 0 wit inspect 1.9  180 true -32 wit inspect .57   18    - wit inspect - wit inspect
floats-cdfpl/newton_1_1_true-unreach-call_true-termination.i true 2 wit inspect 7.9 350 77 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    540 timeout 0 wit inspect 960     1000  
floats-cdfpl/newton_1_2_true-unreach-call_true-termination.i true 2 wit inspect 7.6 330 67 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    570 timeout 0 wit inspect 960     1000  
floats-cdfpl/newton_1_3_true-unreach-call_true-termination.i true 2 wit inspect 8.3 360 78 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    570 timeout 0 wit inspect 960     900  
floats-cdfpl/newton_2_1_true-unreach-call_true-termination.i true 2 wit inspect 21   350 230 - 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 20   380 200 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    830 timeout 0 wit inspect 960     960  
floats-cdfpl/newton_2_3_true-unreach-call_true-termination.i true 2 wit inspect 15   350 170 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    580 timeout 0 wit inspect 960     940  
floats-cdfpl/newton_2_4_true-unreach-call_true-termination.i unknown 0 wit inspect 18   400 180 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .019 4.8
floats-cdfpl/newton_2_5_true-unreach-call_true-termination.i unknown 0 wit inspect 18   400 220 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .022 4.8
floats-cdfpl/newton_3_1_true-unreach-call_true-termination.i unknown 0 wit inspect 23   370 280 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .047 4.8
floats-cdfpl/newton_3_2_true-unreach-call_true-termination.i unknown 0 wit inspect 19   380 190 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .42 44 error (2) 0 wit inspect .019 4.9
floats-cdfpl/newton_3_3_true-unreach-call_true-termination.i unknown 0 wit inspect 21   380 250 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .47 43 error (2) 0 wit inspect .019 5.0
floats-cdfpl/newton_3_4_true-unreach-call_true-termination.i unknown 0 wit inspect 17   370 190 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 42 error (2) 0 wit inspect .018 4.9
floats-cdfpl/newton_3_5_true-unreach-call_true-termination.i unknown 0 wit inspect 18   370 190 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 41 error (2) 0 wit inspect .020 4.9
floats-cdfpl/sine_4_true-unreach-call_true-termination.i true 2 wit inspect 6.9 350 68 - 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 6.7 310 57 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    490 timeout 0 wit inspect 960     850  
floats-cdfpl/sine_6_true-unreach-call_true-termination.i true 2 wit inspect 7.2 350 69 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    660 timeout 0 wit inspect 960     820  
floats-cdfpl/sine_7_true-unreach-call_true-termination.i true 2 wit inspect 7.5 340 63 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 670    600 timeout 0 wit inspect 960     760  
floats-cdfpl/sine_8_true-unreach-call_true-termination.i true 2 wit inspect 6.3 320 54 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 580    540 timeout 0 wit inspect 960     830  
floats-cdfpl/square_4_true-unreach-call_true-termination.i true 2 wit inspect 6.4 350 58 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 680    580 true 2 wit inspect 650     860  
floats-cdfpl/square_5_true-unreach-call_true-termination.i true 2 wit inspect 6.1 330 56 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 520    510 true 2 wit inspect 540     730  
floats-cdfpl/square_6_true-unreach-call_true-termination.i true 2 wit inspect 6.0 320 54 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 280    500 true 2 wit inspect 410     790  
floats-cdfpl/square_7_true-unreach-call_true-termination.i true 2 wit inspect 6.6 330 54 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 830    490 true 2 wit inspect 180     720  
floats-cdfpl/square_8_true-unreach-call_true-termination.i true 2 wit inspect 6.3 340 49 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 60    360 true 2 wit inspect 130     600  
floats-cbmc-regression/float-div1_true-unreach-call.i unknown 0 wit inspect 5.0 290 49 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .024 4.9
floats-cbmc-regression/float-flags-simp1_true-unreach-call.i unknown 0 wit inspect 4.9 300 45 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 41 error (2) 0 wit inspect .028 4.9
floats-cbmc-regression/float-no-simp1_true-unreach-call_true-termination.i true 2 wit inspect 3.7 230 32 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.3  240 true 2 wit inspect 11     230  
floats-cbmc-regression/float-no-simp2_true-unreach-call.i unknown 0 wit inspect 3.5 260 32 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 45 error (2) 0 wit inspect .022 4.9
floats-cbmc-regression/float-no-simp3_true-unreach-call_true-termination.i true 2 wit inspect 3.8 230 34 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  240 true 2 wit inspect 8.9   230  
floats-cbmc-regression/float-no-simp4_true-unreach-call.i unknown 0 wit inspect 4.7 310 43 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .025 4.8
floats-cbmc-regression/float-no-simp6_true-unreach-call_true-termination.i true 2 wit inspect 3.7 240 33 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 12     290  
floats-cbmc-regression/float-no-simp7_true-unreach-call_true-termination.i true 2 wit inspect 3.6 230 33 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 11     250  
floats-cbmc-regression/float-no-simp8_true-unreach-call.i true 2 wit inspect 3.9 240 38 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0  260 true 2 wit inspect 12     300  
floats-cbmc-regression/float-rounding1_true-unreach-call.i unknown 0 wit inspect 4.1 270 41 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 44 error (2) 0 wit inspect .022 5.0
floats-cbmc-regression/float-to-double1_true-unreach-call.i unknown 0 wit inspect 3.8 240 37 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .019 4.9
floats-cbmc-regression/float-to-double2_true-unreach-call_true-termination.i true 2 wit inspect 3.7 230 38 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 8.9   240  
floats-cbmc-regression/float-zero-sum1_true-unreach-call_true-termination.i true 2 wit inspect 3.8 240 35 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  250 true 2 wit inspect 14     280  
floats-cbmc-regression/float11_true-unreach-call_true-termination.i true 2 wit inspect 3.4 320 40 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 10     240  
floats-cbmc-regression/float12_true-unreach-call_true-termination.i unknown 0 wit inspect 5.7 310 48 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .48 43 error (2) 0 wit inspect .019 4.9
floats-cbmc-regression/float13_true-unreach-call_true-termination.i true 2 wit inspect 3.8 240 38 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 11     250  
floats-cbmc-regression/float14_true-unreach-call.i unknown 0 wit inspect 3.6 240 32 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .43 44 error (2) 0 wit inspect .020 4.8
floats-cbmc-regression/float18_true-unreach-call.i true 2 wit inspect 3.8 240 33 - 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 unknown 0 wit inspect 3.7 250 34 - 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-cbmc-regression/float1_true-unreach-call_true-termination.i true 2 wit inspect 3.6 230 32 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 9.2   230  
floats-cbmc-regression/float20_true-unreach-call_true-termination.i false(unreach-call) -16 wit inspect 6.2 330 57 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  260 true 2 wit inspect 18     390  
floats-cbmc-regression/float21_true-unreach-call.i unknown 0 wit inspect 4.1 270 39 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .020 4.9
floats-cbmc-regression/float22_true-unreach-call_true-termination.i true 2 wit inspect 3.8 250 37 - wit inspect - wit inspect - wit inspect - wit inspect false(unreach-call) -16 wit inspect 4.9  280 true 2 wit inspect 340     1000  
floats-cbmc-regression/float2_true-unreach-call_true-termination.i true 2 wit inspect 3.6 230 32 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  240 true 2 wit inspect 11     270  
floats-cbmc-regression/float3_true-unreach-call_true-termination.i true 2 wit inspect 5.9 310 47 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  270 true 2 wit inspect 15     320  
floats-cbmc-regression/float4_true-unreach-call.i unknown 0 wit inspect 3.9 270 35 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .41 44 error (2) 0 wit inspect .019 5.0
floats-cbmc-regression/float5_true-unreach-call_true-termination.i true 2 wit inspect 6.8 330 63 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  260 true 2 wit inspect 31     280  
floats-cbmc-regression/float6_true-unreach-call_true-termination.i unknown 0 wit inspect 6.1 300 50 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .019 5.0
floats-cbmc-regression/float8_true-unreach-call.i unknown 0 wit inspect 4.7 280 38 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .023 4.8
floats-cbmc-regression/float_lib1_true-unreach-call.i unknown 0 wit inspect 3.2 210 32 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 41 error (2) 0 wit inspect .020 4.9
floats-cbmc-regression/float_lib2_true-unreach-call.i unknown 0 wit inspect 4.1 250 37 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .017 4.8
float-benchs/cast_float_ptr_false-unreach-call_true-termination.c unknown 0 wit inspect 5.0 290 44 error (invalid witness file) 0 wit inspect .59 44 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .86 47 error (invalid witness file) 0 wit inspect .0037 .26 - wit inspect - wit inspect
float-benchs/cast_union_loose_false-unreach-call_true-termination.c unknown 0 wit inspect 5.6 320 44 error (invalid witness file) 0 wit inspect .62 43 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .85 47 error (invalid witness file) 0 wit inspect .0035 .26 - wit inspect - wit inspect
float-benchs/cast_union_tight_false-unreach-call_true-termination.c unknown 0 wit inspect 5.1 310 41 error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .64 49 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
float-benchs/float_int_inv_square_false-unreach-call_true-termination.c unknown 0 wit inspect 6.0 320 48 error (invalid witness file) 0 wit inspect .42 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .69 50 error (invalid witness file) 0 wit inspect .0010 .26 - wit inspect - wit inspect
float-benchs/inv_Newton_false-unreach-call.c unknown 0 wit inspect 5.7 310 57 error (invalid witness file) 0 wit inspect .68 41 error (2) 0 wit inspect .041 4.9 error (invalid witness file) 0 wit inspect .69 50 error (invalid witness file) 0 wit inspect .0023 .26 - wit inspect - wit inspect
float-benchs/inv_square_false-unreach-call_true-termination.c unknown 0 wit inspect 5.4 310 51 error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .024 4.8 error (invalid witness file) 0 wit inspect .85 47 error (invalid witness file) 0 wit inspect .0011 .29 - wit inspect - wit inspect
float-benchs/nan_double_false-unreach-call_true-termination.c unknown 0 wit inspect 4.9 290 42 error (invalid witness file) 0 wit inspect .41 41 error (2) 0 wit inspect .023 4.9 error (invalid witness file) 0 wit inspect .84 47 error (invalid witness file) 0 wit inspect .0013 .27 - wit inspect - wit inspect
float-benchs/nan_float_false-unreach-call_true-termination.c unknown 0 wit inspect 4.6 290 46 error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .87 48 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
float-benchs/sin_interpolated_index_false-unreach-call_true-termination.c unknown 0 wit inspect 8.4 480 75 error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .022 5.0 error (invalid witness file) 0 wit inspect .65 49 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
float-benchs/sqrt_poly2_false-unreach-call.c unknown 0 wit inspect 6.4 330 51 error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .84 49 error (invalid witness file) 0 wit inspect .0039 .26 - wit inspect - wit inspect
float-benchs/Muller_Kahan_true-unreach-call_true-termination.c unknown 0 wit inspect 5.6 310 51 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 45 error (2) 0 wit inspect .021 4.9
float-benchs/Rump_double_true-unreach-call_true-termination.c true 2 wit inspect 4.0 250 38 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 25     970  
float-benchs/Rump_float_true-unreach-call_true-termination.c true 2 wit inspect 4.0 250 35 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 13     420  
float-benchs/addsub_double_exact_true-unreach-call_true-termination.c true 2 wit inspect 3.9 240 38 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 9.4   270  
float-benchs/addsub_float_exact_true-unreach-call_true-termination.c true 2 wit inspect 4.0 250 35 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  250 true 2 wit inspect 9.9   270  
float-benchs/addsub_float_inexact_true-unreach-call_true-termination.c true 2 wit inspect 3.9 240 41 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 12     250  
float-benchs/arctan_Pade_true-unreach-call_true-termination.c unknown 0 wit inspect 6.4 330 55 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 44 error (2) 0 wit inspect .021 4.9
float-benchs/bary_diverge_true-unreach-call_true-termination.c unknown 0 wit inspect 6.7 330 56 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .021 4.8
float-benchs/cast_float_union_true-unreach-call.c true 2 wit inspect 4.1 250 36 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.7  250 true 2 wit inspect 4.6   220  
float-benchs/cos_polynomial_true-unreach-call_true-termination.c unknown 0 wit inspect 6.5 320 59 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .018 4.9
float-benchs/divmul_buf_diverge_true-unreach-call_true-termination.c unknown 0 wit inspect 6.2 320 53 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .018 4.9
float-benchs/divmul_diverge_true-unreach-call_true-termination.c unknown 0 wit inspect 5.4 310 49 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .020 4.8
float-benchs/drift_tenth_true-unreach-call_true-termination.c true 2 wit inspect 4.0 240 37 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 14    330 true 2 wit inspect 380     660  
float-benchs/exp_loop_true-unreach-call.c unknown 0 wit inspect 6.4 310 53 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .45 43 error (2) 0 wit inspect .025 4.9
float-benchs/feedback_diverge_true-unreach-call_true-termination.c unknown 0 wit inspect 6.2 340 59 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .48 43 error (2) 0 wit inspect .021 4.8
float-benchs/filter1_true-unreach-call_true-termination.c unknown 0 wit inspect 6.1 320 56 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .47 44 error (2) 0 wit inspect .019 4.9
float-benchs/filter2_alt_true-unreach-call.c unknown 0 wit inspect 6.8 330 55 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .024 4.9
float-benchs/filter2_iterated_true-unreach-call.c unknown 0 wit inspect 6.7 350 58 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .019 4.9
float-benchs/filter2_reinit_true-unreach-call_true-termination.c unknown 0 wit inspect 5.8 300 54 - 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
float-benchs/filter2_set_true-unreach-call_true-termination.c unknown 0 wit inspect 7.2 350 58 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .019 4.8
float-benchs/filter2_true-unreach-call_true-termination.c unknown 0 wit inspect 5.6 300 47 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .035 5.0
float-benchs/filter_iir_true-unreach-call.c unknown 0 wit inspect 7.3 360 56 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .026 4.9
float-benchs/float_double_true-unreach-call_true-termination.c true 2 wit inspect 3.8 230 41 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 10     260  
float-benchs/image_filter_true-unreach-call.c unknown 0 wit inspect 10   640 86 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .48 43 error (2) 0 wit inspect .025 4.9
float-benchs/interpolation2_true-unreach-call_true-termination.c unknown 0 wit inspect 5.8 320 53 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 41 error (2) 0 wit inspect .024 5.0
float-benchs/interpolation_true-unreach-call_true-termination.c unknown 0 wit inspect 5.9 320 45 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .73 44 error (2) 0 wit inspect .020 5.0
float-benchs/inv_sqrt_Quake_true-unreach-call_true-termination.c unknown 0 wit inspect 5.9 320 50 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .025 4.8
float-benchs/inv_square_int_true-unreach-call_true-termination.c unknown 0 wit inspect 5.6 300 45 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .45 43 error (2) 0 wit inspect .019 4.8
float-benchs/inv_square_true-unreach-call_true-termination.c true 2 wit inspect 5.8 310 48 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  260 true 2 wit inspect 43     300  
float-benchs/loop_true-unreach-call.c unknown 0 wit inspect 5.3 300 44 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .39 43 error (2) 0 wit inspect .024 4.8
float-benchs/mea8000_true-unreach-call.c unknown 0 wit inspect 15   730 120 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 45 error (2) 0 wit inspect .021 4.9
float-benchs/nan_double_range_true-unreach-call_true-termination.c unknown 0 wit inspect 5.5 300 47 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .019 5.0
float-benchs/nan_float_range_true-unreach-call_true-termination.c unknown 0 wit inspect 5.0 300 42 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 42 error (2) 0 wit inspect .019 4.9
float-benchs/rlim_exit_true-unreach-call_true-termination.c unknown 0 wit inspect 5.7 320 51 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 42 error (2) 0 wit inspect .019 4.9
float-benchs/rlim_invariant_true-unreach-call_true-termination.c unknown 0 wit inspect 5.8 310 48 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .024 4.8
float-benchs/sin_interpolated_bigrange_loose_true-unreach-call_true-termination.c unknown 0 wit inspect 8.0 470 69 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 43 error (2) 0 wit inspect .019 4.9
float-benchs/sin_interpolated_bigrange_tight_true-unreach-call_true-termination.c unknown 0 wit inspect 8.2 480 74 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .41 43 error (2) 0 wit inspect .020 4.9
float-benchs/sin_interpolated_index_true-unreach-call_true-termination.c unknown 0 wit inspect 8.5 470 76 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 42 error (2) 0 wit inspect .021 4.9
float-benchs/sin_interpolated_negation_true-unreach-call.c unknown 0 wit inspect 11   520 90 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .019 4.8
float-benchs/sin_interpolated_smallrange_true-unreach-call.c unknown 0 wit inspect 8.4 470 69 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .019 4.8
float-benchs/sqrt_Householder_constant_true-unreach-call.c unknown 0 wit inspect 6.3 330 59 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .73 44 error (2) 0 wit inspect .023 4.9
float-benchs/sqrt_Householder_interval_true-unreach-call.c unknown 0 wit inspect 6.2 330 59 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 43 error (2) 0 wit inspect .021 4.9
float-benchs/sqrt_Householder_pseudoconstant_true-unreach-call.c unknown 0 wit inspect 6.2 320 59 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 41 error (2) 0 wit inspect .024 4.9
float-benchs/sqrt_Newton_pseudoconstant_true-unreach-call.c unknown 0 wit inspect 6.4 320 63 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 41 error (2) 0 wit inspect .019 5.0
float-benchs/sqrt_biNewton_pseudoconstant_true-unreach-call.c unknown 0 wit inspect 6.0 300 54 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .018 4.8
float-benchs/sqrt_poly_true-unreach-call_true-termination.c unknown 0 wit inspect 5.7 330 57 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .019 4.8
float-benchs/water_pid_true-unreach-call_true-termination.c unknown 0 wit inspect 5.5 300 45 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 45 error (2) 0 wit inspect .018 4.9
float-benchs/zonotope_2_true-unreach-call_true-termination.c unknown 0 wit inspect 5.6 300 46 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 44 error (2) 0 wit inspect .019 4.9
float-benchs/zonotope_3_true-unreach-call_true-termination.c unknown 0 wit inspect 5.5 320 52 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 44 error (2) 0 wit inspect .025 4.9
float-benchs/zonotope_loose_true-unreach-call_true-termination.c unknown 0 wit inspect 5.7 320 51 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 41 error (2) 0 wit inspect .018 4.8
float-benchs/zonotope_tight_true-unreach-call_true-termination.c unknown 0 wit inspect 5.5 320 51 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .41 44 error (2) 0 wit inspect .018 5.0
floats-esbmc-regression/Double_div_true-unreach-call.i unknown 0 wit inspect 5.2 300 46 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 42 error (2) 0 wit inspect .021 4.8
floats-esbmc-regression/Float_div_true-unreach-call.i unknown 0 wit inspect 5.2 290 44 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .72 41 error (2) 0 wit inspect .020 4.9
floats-esbmc-regression/ceil_nondet_true-unreach-call.i unknown 0 wit inspect 4.2 290 43 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 41 error (2) 0 wit inspect .023 5.0
floats-esbmc-regression/ceil_true-unreach-call.i unknown 0 wit inspect 3.8 250 38 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 41 error (2) 0 wit inspect .020 4.9
floats-esbmc-regression/copysign_true-unreach-call.i unknown 0 wit inspect 4.0 270 37 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .020 4.9
floats-esbmc-regression/digits_for_true-unreach-call.i unknown 0 wit inspect 2.9 200 32 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .72 41 error (2) 0 wit inspect .020 4.9
floats-esbmc-regression/digits_while_true-unreach-call.i unknown 0 wit inspect 2.9 200 27 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .45 43 error (2) 0 wit inspect .019 4.8
floats-esbmc-regression/fabs_true-unreach-call.i unknown 0 wit inspect 3.9 240 38 - 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
floats-esbmc-regression/fdim_true-unreach-call.i unknown 0 wit inspect 3.9 260 39 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .46 43 error (2) 0 wit inspect .020 4.9
floats-esbmc-regression/floor_nondet_true-unreach-call.i unknown 0 wit inspect 4.2 280 39 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .019 5.0
floats-esbmc-regression/floor_true-unreach-call.i unknown 0 wit inspect 4.0 260 34 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 42 error (2) 0 wit inspect .024 5.0
floats-esbmc-regression/fmax_true-unreach-call.i unknown 0 wit inspect 3.9 250 34 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 46 error (2) 0 wit inspect .020 4.8
floats-esbmc-regression/fmin_true-unreach-call.i unknown 0 wit inspect 3.8 250 38 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 41 error (2) 0 wit inspect .019 4.8
floats-esbmc-regression/fmod2_true-unreach-call.i unknown 0 wit inspect 3.9 270 36 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .020 4.9
floats-esbmc-regression/fmod3_true-unreach-call.i unknown 0 wit inspect 3.9 260 36 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 41 error (2) 0 wit inspect .022 4.8
floats-esbmc-regression/fmod_true-unreach-call.i true 2 wit inspect 3.8 240 34 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3  250 unknown 0 wit inspect 4.1   190  
floats-esbmc-regression/isgreater_true-unreach-call.i true 2 wit inspect 4.2 240 37 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  250 true 2 wit inspect 10     260  
floats-esbmc-regression/isgreaterequal_true-unreach-call.i true 2 wit inspect 4.0 240 38 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  260 true 2 wit inspect 9.8   270  
floats-esbmc-regression/isless_true-unreach-call.i true 2 wit inspect 4.1 240 34 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  260 true 2 wit inspect 11     270  
floats-esbmc-regression/islessequal_true-unreach-call.i true 2 wit inspect 3.8 250 39 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.9  250 true 2 wit inspect 11     280  
floats-esbmc-regression/islessgreater_true-unreach-call.i true 2 wit inspect 4.1 240 40 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  260 true 2 wit inspect 10     270  
floats-esbmc-regression/isunordered_true-unreach-call.i true 2 wit inspect 4.0 240 35 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  260 true 2 wit inspect 11     280  
floats-esbmc-regression/lrint_true-unreach-call.i unknown 0 wit inspect 4.5 300 38 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .022 4.8
floats-esbmc-regression/modf_true-unreach-call.i unknown 0 wit inspect 3.9 250 36 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .46 44 error (2) 0 wit inspect .025 4.8
floats-esbmc-regression/nan_true-unreach-call.i unknown 0 wit inspect 4.2 260 40 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .48 43 error (2) 0 wit inspect .018 5.0
floats-esbmc-regression/nearbyint2_true-unreach-call.i unknown 0 wit inspect 3.7 240 33 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .024 4.9
floats-esbmc-regression/nearbyint_true-unreach-call.i unknown 0 wit inspect 3.8 240 33 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .019 5.0
floats-esbmc-regression/remainder_true-unreach-call.i unknown 0 wit inspect 4.5 300 38 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .020 5.0
floats-esbmc-regression/rint2_true-unreach-call.i unknown 0 wit inspect 4.0 240 33 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .49 43 error (2) 0 wit inspect .025 4.8
floats-esbmc-regression/rint_true-unreach-call.i unknown 0 wit inspect 3.9 240 33 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 42 error (2) 0 wit inspect .024 4.8
floats-esbmc-regression/round_nondet_true-unreach-call.i unknown 0 wit inspect 3.9 290 36 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .47 43 error (2) 0 wit inspect .021 5.0
floats-esbmc-regression/round_true-unreach-call.i unknown 0 wit inspect 4.2 300 41 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 42 error (2) 0 wit inspect .021 4.9
floats-esbmc-regression/rounding_functions_true-unreach-call.i true 2 wit inspect 4.0 240 37 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.5  260 unknown 0 wit inspect 3.7   200  
floats-esbmc-regression/trunc_nondet_2_true-unreach-call.i unknown 0 wit inspect 4.0 260 39 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .41 43 error (2) 0 wit inspect .024 4.8
floats-esbmc-regression/trunc_nondet_true-unreach-call.i unknown 0 wit inspect 4.2 270 41 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .019 4.9
floats-esbmc-regression/trunc_true-unreach-call.i unknown 0 wit inspect 3.9 250 40 - 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-esbmc-regression/Double_div_bad_false-unreach-call.i unknown 0 wit inspect 5.4 300 45 error (invalid witness file) 0 wit inspect .70 45 error (2) 0 wit inspect .023 5.0 error (invalid witness file) 0 wit inspect .69 51 error (invalid witness file) 0 wit inspect .0035 .30 - wit inspect - wit inspect
floats-esbmc-regression/Float_div_bad_false-unreach-call.i unknown 0 wit inspect 5.3 300 44 error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .67 50 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
floats-esbmc-regression/digits_bad_for_false-unreach-call.i unknown 0 wit inspect 3.0 200 33 error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .023 5.0 error (invalid witness file) 0 wit inspect .66 49 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
floats-esbmc-regression/digits_bad_while_false-unreach-call.i unknown 0 wit inspect 2.9 200 28 error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .023 4.9 error (invalid witness file) 0 wit inspect .64 50 error (invalid witness file) 0 wit inspect .0014 .28 - 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 91 1100   53000 11000 31 10 810 5800 31 -254 430 4400 31 0 40 3300 31 -416 7.7 240 141 62 12000   21000 141 70 14000 25000
    correct results 59 107 370   17000 3500 10 10 530 3800 2 2 110 980 0 0 39 78 3800   12000 35 70 3000 14000
        correct true 48 96 280   13000 2600 0 0 0 0 39 78 3800   12000 35 70 3000 14000
        correct false 11 11 89   3900 860 10 10 530 3800 2 2 110 980 0 0 0 0
    correct-unconfimed results 2 0 22   710 230 0 0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0 0
        correct-unconfirmed false 2 0 22   710 230 0 0 0 0 0 0
    incorrect results 1 -16 6.2 330 57 0 8 -256 29 1800 0 13 -416 7.6 240 1 -16 4.9 280 0
        incorrect true 0 0 8 -256 29 1800 0 13 -416 7.6 240 0 0
        incorrect false 1 -16 6.2 330 57 0 0 0 0 1 -16 4.9 280 0
score (172 tasks, max score: 313) 91 10 -254 0 -416 62 70
Run set skink.sv-comp18.ReachSafety-Floats cpa-seq-validate-violation-witnesses-skink.sv-comp18-violation-witness.ReachSafety-Floats uautomizer-validate-violation-witnesses-skink.sv-comp18-violation-witness.ReachSafety-Floats cpa-witness2test-validate-violation-witnesses-skink.sv-comp18-violation-witness.ReachSafety-Floats fshell-witness2test-validate-violation-witnesses-skink.sv-comp18-violation-witness.ReachSafety-Floats cpa-seq-validate-correctness-witnesses-skink.sv-comp18-correctness-witness.ReachSafety-Floats uautomizer-validate-correctness-witnesses-skink.sv-comp18-correctness-witness.ReachSafety-Floats