Tool DepthK DepthK version 3.0 - Fri Jan 6 18:14:20 AMT 2017 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 16:01:31 CET 2017-12-01 08:31:47 CET 2017-12-01 08:56:50 CET 2017-12-01 08:59:39 CET 2017-12-01 09:01:39 CET 2017-12-01 08:10:33 CET 2017-12-01 08:38:18 CET
Run set depthk.sv-comp18.ReachSafety-Floats cpa-seq-validate-violation-witnesses-depthk.sv-comp18-violation-witness.ReachSafety-Floats uautomizer-validate-violation-witnesses-depthk.sv-comp18-violation-witness.ReachSafety-Floats cpa-witness2test-validate-violation-witnesses-depthk.sv-comp18-violation-witness.ReachSafety-Floats fshell-witness2test-validate-violation-witnesses-depthk.sv-comp18-violation-witness.ReachSafety-Floats cpa-seq-validate-correctness-witnesses-depthk.sv-comp18-correctness-witness.ReachSafety-Floats uautomizer-validate-correctness-witnesses-depthk.sv-comp18-correctness-witness.ReachSafety-Floats
Options -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/depthk.2017-11-30_1601.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/depthk.2017-11-30_1601.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/depthk.2017-11-30_1601.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/depthk.2017-11-30_1601.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/depthk.2017-11-30_1601.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/depthk.2017-11-30_1601.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 unknown 0 wit inspect 890    400 7500   error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .021 4.8 error (invalid witness file) 0 wit inspect .88 50 error (invalid witness file) 0 wit inspect .0016 .29 - wit inspect - wit inspect
floats-cdfpl/newton_1_5_false-unreach-call_true-termination.i unknown 0 wit inspect 890    480 8000   error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .047 4.8 error (invalid witness file) 0 wit inspect .84 47 error (invalid witness file) 0 wit inspect .0014 .26 - wit inspect - wit inspect
floats-cdfpl/newton_1_6_false-unreach-call_true-termination.i unknown 0 wit inspect 890    400 7900   error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .88 49 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect - wit inspect
floats-cdfpl/newton_1_7_false-unreach-call_true-termination.i unknown 0 wit inspect 890    400 8700   error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .87 47 error (invalid witness file) 0 wit inspect .0014 .30 - wit inspect - wit inspect
floats-cdfpl/newton_1_8_false-unreach-call_true-termination.i unknown 0 wit inspect 890    460 7500   error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .85 49 error (invalid witness file) 0 wit inspect .0012 .34 - wit inspect - wit inspect
floats-cdfpl/newton_2_6_false-unreach-call_true-termination.i unknown 0 wit inspect 890    710 8400   error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .86 49 error (invalid witness file) 0 wit inspect .0011 .34 - wit inspect - wit inspect
floats-cdfpl/newton_2_7_false-unreach-call_true-termination.i unknown 0 wit inspect 890    700 9200   error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .020 5.0 error (invalid witness file) 0 wit inspect .85 47 error (invalid witness file) 0 wit inspect .0013 .30 - wit inspect - wit inspect
floats-cdfpl/newton_2_8_false-unreach-call_true-termination.i unknown 0 wit inspect 890    760 8100   error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .88 49 error (invalid witness file) 0 wit inspect .0013 .29 - wit inspect - wit inspect
floats-cdfpl/newton_3_6_false-unreach-call_true-termination.i unknown 0 wit inspect 890    1000 9100   error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .85 49 error (invalid witness file) 0 wit inspect .0012 .29 - wit inspect - wit inspect
floats-cdfpl/newton_3_7_false-unreach-call_true-termination.i unknown 0 wit inspect 890    1000 8100   error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .021 5.0 error (invalid witness file) 0 wit inspect .85 49 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
floats-cdfpl/newton_3_8_false-unreach-call_true-termination.i unknown 0 wit inspect 890    1100 6900   error (invalid witness file) 0 wit inspect .40 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .84 49 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
floats-cdfpl/sine_1_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 190    240 1600   true -32 wit inspect 2.9  260 true -32 wit inspect 4.6   210   unknown 0 wit inspect 2.8  180 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
floats-cdfpl/sine_2_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 97    200 970   true -32 wit inspect 3.0  260 true -32 wit inspect 5.7   280   unknown 0 wit inspect 2.8  180 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
floats-cdfpl/sine_3_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 65    180 620   true -32 wit inspect 2.9  250 true -32 wit inspect 4.4   210   unknown 0 wit inspect 2.8  180 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 570    210 4500   true -32 wit inspect 2.1  260 true -32 wit inspect 4.4   220   unknown 0 wit inspect 2.8  210 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
floats-cdfpl/square_2_false-unreach-call_true-termination.i unknown 0 wit inspect 890    250 9000   error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .88 49 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
floats-cdfpl/square_3_false-unreach-call_true-termination.i unknown 0 wit inspect 890    350 6400   error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .84 49 error (invalid witness file) 0 wit inspect .0014 .26 - wit inspect - wit inspect
floats-cdfpl/newton_1_1_true-unreach-call_true-termination.i unknown 0 wit inspect 890    410 8900   - 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-cdfpl/newton_1_2_true-unreach-call_true-termination.i unknown 0 wit inspect 890    400 8300   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 45 error (2) 0 wit inspect .025 4.8
floats-cdfpl/newton_1_3_true-unreach-call_true-termination.i unknown 0 wit inspect 890    400 8800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 45 error (2) 0 wit inspect .018 4.9
floats-cdfpl/newton_2_1_true-unreach-call_true-termination.i unknown 0 wit inspect 890    680 8600   - 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
floats-cdfpl/newton_2_2_true-unreach-call_true-termination.i unknown 0 wit inspect 890    700 9100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .019 4.8
floats-cdfpl/newton_2_3_true-unreach-call_true-termination.i unknown 0 wit inspect 890    710 9300   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .019 5.0
floats-cdfpl/newton_2_4_true-unreach-call_true-termination.i unknown 0 wit inspect 890    710 9500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 43 error (2) 0 wit inspect .018 4.9
floats-cdfpl/newton_2_5_true-unreach-call_true-termination.i unknown 0 wit inspect 890    760 8400   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .020 4.9
floats-cdfpl/newton_3_1_true-unreach-call_true-termination.i unknown 0 wit inspect 890    1000 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .019 4.9
floats-cdfpl/newton_3_2_true-unreach-call_true-termination.i unknown 0 wit inspect 890    1000 9000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .019 4.8
floats-cdfpl/newton_3_3_true-unreach-call_true-termination.i unknown 0 wit inspect 890    930 8900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 41 error (2) 0 wit inspect .019 4.9
floats-cdfpl/newton_3_4_true-unreach-call_true-termination.i unknown 0 wit inspect 890    990 9900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 43 error (2) 0 wit inspect .019 4.8
floats-cdfpl/newton_3_5_true-unreach-call_true-termination.i unknown 0 wit inspect 890    1200 7700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .020 4.9
floats-cdfpl/sine_4_true-unreach-call_true-termination.i unknown 0 wit inspect 890    310 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .022 4.8
floats-cdfpl/sine_5_true-unreach-call_true-termination.i unknown 0 wit inspect 890    310 9900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .019 4.8
floats-cdfpl/sine_6_true-unreach-call_true-termination.i unknown 0 wit inspect 890    320 7000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 44 error (2) 0 wit inspect .019 4.9
floats-cdfpl/sine_7_true-unreach-call_true-termination.i unknown 0 wit inspect 890    310 8100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .018 4.8
floats-cdfpl/sine_8_true-unreach-call_true-termination.i unknown 0 wit inspect 890    310 8400   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 41 error (2) 0 wit inspect .018 4.8
floats-cdfpl/square_4_true-unreach-call_true-termination.i unknown 0 wit inspect 890    250 7700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .018 4.9
floats-cdfpl/square_5_true-unreach-call_true-termination.i unknown 0 wit inspect 890    350 8900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .049 4.8
floats-cdfpl/square_6_true-unreach-call_true-termination.i unknown 0 wit inspect 890    260 6600   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .019 4.8
floats-cdfpl/square_7_true-unreach-call_true-termination.i unknown 0 wit inspect 890    350 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 43 error (2) 0 wit inspect .048 4.9
floats-cdfpl/square_8_true-unreach-call_true-termination.i unknown 0 wit inspect 890    200 9900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .73 43 error (2) 0 wit inspect .020 4.9
floats-cbmc-regression/float-div1_true-unreach-call.i true 2 wit inspect 37    370 370   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.9  320 true 2 wit inspect 33     600  
floats-cbmc-regression/float-flags-simp1_true-unreach-call.i true 2 wit inspect 25    2000 220   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 11    790 true 2 wit inspect 32     710  
floats-cbmc-regression/float-no-simp1_true-unreach-call_true-termination.i true 2 wit inspect 3.1  270 33   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 9.1   240  
floats-cbmc-regression/float-no-simp2_true-unreach-call.i true 2 wit inspect 300    330 3000   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 16    300 true 2 wit inspect 41     400  
floats-cbmc-regression/float-no-simp3_true-unreach-call_true-termination.i true 2 wit inspect 3.2  260 30   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 9.2   220  
floats-cbmc-regression/float-no-simp4_true-unreach-call.i true 2 wit inspect 6.3  310 66   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  260 true 2 wit inspect 37     580  
floats-cbmc-regression/float-no-simp6_true-unreach-call_true-termination.i true 2 wit inspect 3.2  250 28   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 11     290  
floats-cbmc-regression/float-no-simp7_true-unreach-call_true-termination.i true 2 wit inspect 3.1  260 33   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  250 true 2 wit inspect 9.5   250  
floats-cbmc-regression/float-no-simp8_true-unreach-call.i true 2 wit inspect 4.3  260 39   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  260 true 2 wit inspect 10     300  
floats-cbmc-regression/float-rounding1_true-unreach-call.i unknown 0 wit inspect 9.1  450 82   - wit inspect - wit inspect - wit inspect - wit inspect error 0 wit inspect 4.9  250 unknown 0 wit inspect 3.7   200  
floats-cbmc-regression/float-to-double1_true-unreach-call.i true 2 wit inspect 29    320 350   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.7  260 true 2 wit inspect 130     420  
floats-cbmc-regression/float-to-double2_true-unreach-call_true-termination.i true 2 wit inspect 3.1  260 32   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 9.8   240  
floats-cbmc-regression/float-zero-sum1_true-unreach-call_true-termination.i true 2 wit inspect 3.1  260 30   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 12     300  
floats-cbmc-regression/float11_true-unreach-call_true-termination.i true 2 wit inspect 3.4  250 33   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 7.1   250  
floats-cbmc-regression/float12_true-unreach-call_true-termination.i true 2 wit inspect 7.7  290 85   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  250 true 2 wit inspect 15     260  
floats-cbmc-regression/float13_true-unreach-call_true-termination.i true 2 wit inspect 3.2  250 27   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 11     320  
floats-cbmc-regression/float14_true-unreach-call.i true 2 wit inspect 4.3  270 40   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  250 true 2 wit inspect 9.1   290  
floats-cbmc-regression/float18_true-unreach-call.i true 2 wit inspect 18    270 270   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 25    410 unknown 0 wit inspect 3.6   200  
floats-cbmc-regression/float19_true-unreach-call.i true 2 wit inspect 7.3  300 78   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0  260 true 2 wit inspect 10     280  
floats-cbmc-regression/float1_true-unreach-call_true-termination.i true 2 wit inspect 3.1  260 30   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 9.0   230  
floats-cbmc-regression/float20_true-unreach-call_true-termination.i true 2 wit inspect 24    250 270   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 15     410  
floats-cbmc-regression/float21_true-unreach-call.i true 2 wit inspect 30    310 370   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.4  300 true 2 wit inspect 82     610  
floats-cbmc-regression/float22_true-unreach-call_true-termination.i unknown 0 wit inspect 18    51 260   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 41 error (2) 0 wit inspect .023 4.9
floats-cbmc-regression/float2_true-unreach-call_true-termination.i true 2 wit inspect 3.2  240 28   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  250 true 2 wit inspect 10     280  
floats-cbmc-regression/float3_true-unreach-call_true-termination.i true 2 wit inspect 7.5  250 85   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  270 true 2 wit inspect 13     330  
floats-cbmc-regression/float4_true-unreach-call.i true 2 wit inspect 310    590 3400   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 78    330 true 2 wit inspect 78     450  
floats-cbmc-regression/float5_true-unreach-call_true-termination.i true 2 wit inspect 16    260 240   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  260 true 2 wit inspect 26     280  
floats-cbmc-regression/float6_true-unreach-call_true-termination.i true 2 wit inspect 3.5  260 34   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  250 true 2 wit inspect 11     290  
floats-cbmc-regression/float8_true-unreach-call.i true 2 wit inspect 7.5  340 81   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.2  270 true 2 wit inspect 11     300  
floats-cbmc-regression/float_lib1_true-unreach-call.i unknown 0 wit inspect 3.9  150 47   - wit inspect - wit inspect - wit inspect - wit inspect error (parsing failed) 0 wit inspect 2.1  140 error (7) 0 wit inspect 9.8   260  
floats-cbmc-regression/float_lib2_true-unreach-call.i true 2 wit inspect 4.4  260 43   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  260 true 2 wit inspect 17     530  
float-benchs/cast_float_ptr_false-unreach-call_true-termination.c false(unreach-call) 0 wit inspect .41 48 4.8 assertion 0 wit inspect 2.3  160 true -32 wit inspect 5.0   230   assertion 0 wit inspect 2.7  180 error (2) 0 wit inspect .58   18    - wit inspect - wit inspect
float-benchs/cast_union_loose_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .51 49 5.5 true -32 wit inspect 3.2  250 true -32 wit inspect 4.6   220   unknown 0 wit inspect 3.0  180 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  48 14   true -32 wit inspect 3.0  260 true -32 wit inspect 3.4   230   unknown 0 wit inspect 3.0  210 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
float-benchs/float_int_inv_square_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 17    66 220   true -32 wit inspect 3.1  260 true -32 wit inspect 4.8   210   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
float-benchs/inv_Newton_false-unreach-call.c unknown 0 wit inspect 890    340 7300   error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .020 5.0 error (invalid witness file) 0 wit inspect .87 49 error (invalid witness file) 0 wit inspect .0011 .32 - wit inspect - wit inspect
float-benchs/inv_square_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .46 40 5.6 true -32 wit inspect 3.0  250 true -32 wit inspect 4.2   210   unknown 0 wit inspect 3.0  210 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
float-benchs/nan_double_false-unreach-call_true-termination.c false(unreach-call) 0 wit inspect .36 48 4.8 true -32 wit inspect 3.3  270 true -32 wit inspect 4.6   220   unknown 0 wit inspect 3.1  180 true -32 wit inspect .59   18    - wit inspect - wit inspect
float-benchs/nan_float_false-unreach-call_true-termination.c false(unreach-call) 0 wit inspect .35 48 5.0 true -32 wit inspect 2.9  260 true -32 wit inspect 4.5   210   unknown 0 wit inspect 2.8  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 110    410 1100   true -32 wit inspect 3.8  260 true -32 wit inspect 6.3   400   unknown 0 wit inspect 3.1  210 false(unreach-call) 1 wit inspect .66   18    - wit inspect - wit inspect
float-benchs/sqrt_poly2_false-unreach-call.c false(unreach-call) 1 wit inspect 290    340 2800   assertion 0 wit inspect 2.3  160 true -32 wit inspect 5.1   230   assertion 0 wit inspect 2.6  170 false(unreach-call) 1 wit inspect .61   18    - wit inspect - wit inspect
float-benchs/Muller_Kahan_true-unreach-call_true-termination.c unknown 0 wit inspect 890    1200 6700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .042 4.8
float-benchs/Rump_double_true-unreach-call_true-termination.c true 2 wit inspect 3.3  300 30   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 23     990  
float-benchs/Rump_float_true-unreach-call_true-termination.c true 2 wit inspect 3.1  270 29   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 14     430  
float-benchs/addsub_double_exact_true-unreach-call_true-termination.c true 2 wit inspect 3.1  270 28   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 9.5   270  
float-benchs/addsub_float_exact_true-unreach-call_true-termination.c true 2 wit inspect 3.1  260 29   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 9.9   250  
float-benchs/addsub_float_inexact_true-unreach-call_true-termination.c true 2 wit inspect 3.0  260 27   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  250 true 2 wit inspect 9.1   250  
float-benchs/arctan_Pade_true-unreach-call_true-termination.c unknown 0 wit inspect 890    1100 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .019 5.0
float-benchs/bary_diverge_true-unreach-call_true-termination.c unknown 0 wit inspect 890    260 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .018 4.8
float-benchs/cast_float_union_true-unreach-call.c true 2 wit inspect 3.1  250 32   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  240 true 2 wit inspect 4.6   220  
float-benchs/cos_polynomial_true-unreach-call_true-termination.c unknown 0 wit inspect 890    610 8200   - 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 890    270 9500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .018 4.9
float-benchs/divmul_diverge_true-unreach-call_true-termination.c unknown 0 wit inspect 890    270 13000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .50 41 error (2) 0 wit inspect .019 5.0
float-benchs/drift_tenth_true-unreach-call_true-termination.c unknown 0 wit inspect 890    490 7700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 44 error (2) 0 wit inspect .018 4.8
float-benchs/exp_loop_true-unreach-call.c unknown 0 wit inspect 890    410 8100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .037 5.0
float-benchs/feedback_diverge_true-unreach-call_true-termination.c unknown 0 wit inspect 890    330 8200   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .018 4.9
float-benchs/filter1_true-unreach-call_true-termination.c unknown 0 wit inspect 890    280 8400   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .018 5.0
float-benchs/filter2_alt_true-unreach-call.c unknown 0 wit inspect 890    230 9700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .018 5.0
float-benchs/filter2_iterated_true-unreach-call.c unknown 0 wit inspect 900    6500 8200   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 44 error (2) 0 wit inspect .019 4.8
float-benchs/filter2_reinit_true-unreach-call_true-termination.c unknown 0 wit inspect 890    250 9500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 43 error (2) 0 wit inspect .018 4.8
float-benchs/filter2_set_true-unreach-call_true-termination.c unknown 0 wit inspect 890    450 7500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 43 error (2) 0 wit inspect .019 5.0
float-benchs/filter2_true-unreach-call_true-termination.c unknown 0 wit inspect 890    550 8500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 42 error (2) 0 wit inspect .019 4.9
float-benchs/filter_iir_true-unreach-call.c unknown 0 wit inspect 890    750 8400   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 42 error (2) 0 wit inspect .018 5.0
float-benchs/float_double_true-unreach-call_true-termination.c true 2 wit inspect 3.1  250 30   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 9.4   260  
float-benchs/image_filter_true-unreach-call.c unknown 0 wit inspect 890    3100 7200   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .020 4.9
float-benchs/interpolation2_true-unreach-call_true-termination.c unknown 0 wit inspect 630    320 7200   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    590 timeout 0 wit inspect 960     760  
float-benchs/interpolation_true-unreach-call_true-termination.c unknown 0 wit inspect 130    310 1400   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 14    370 timeout 0 wit inspect 960     870  
float-benchs/inv_sqrt_Quake_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 320    270 3100   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  260 true 2 wit inspect 150     940  
float-benchs/inv_square_int_true-unreach-call_true-termination.c true 2 wit inspect 27    300 360   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  260 true 2 wit inspect 16     310  
float-benchs/inv_square_true-unreach-call_true-termination.c true 2 wit inspect 5.2  280 56   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  260 true 2 wit inspect 58     370  
float-benchs/loop_true-unreach-call.c unknown 0 wit inspect 890    320 10000   - 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/mea8000_true-unreach-call.c unknown 0 wit inspect 890    1900 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 44 error (2) 0 wit inspect .018 4.9
float-benchs/nan_double_range_true-unreach-call_true-termination.c true 2 wit inspect 3.6  280 37   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 9.1   240  
float-benchs/nan_float_range_true-unreach-call_true-termination.c true 2 wit inspect 3.6  270 35   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  260 true 2 wit inspect 11     260  
float-benchs/rlim_exit_true-unreach-call_true-termination.c unknown 0 wit inspect 890    200 9900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .78 43 error (2) 0 wit inspect .018 5.0
float-benchs/rlim_invariant_true-unreach-call_true-termination.c unknown 0 wit inspect 890    440 8600   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.9  310 error (7) 0 wit inspect 440     780  
float-benchs/sin_interpolated_bigrange_loose_true-unreach-call_true-termination.c unknown 0 wit inspect 890    1700 5600   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 43 error (2) 0 wit inspect .019 4.8
float-benchs/sin_interpolated_bigrange_tight_true-unreach-call_true-termination.c unknown 0 wit inspect 890    1700 6900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 44 error (2) 0 wit inspect .021 4.8
float-benchs/sin_interpolated_index_true-unreach-call_true-termination.c unknown 0 wit inspect 890    490 6100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 44 error (2) 0 wit inspect .019 4.8
float-benchs/sin_interpolated_negation_true-unreach-call.c unknown 0 wit inspect 890    2100 6800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 44 error (2) 0 wit inspect .018 4.8
float-benchs/sin_interpolated_smallrange_true-unreach-call.c unknown 0 wit inspect 890    1800 6100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 43 error (2) 0 wit inspect .019 5.0
float-benchs/sqrt_Householder_constant_true-unreach-call.c unknown 0 wit inspect 890    1000 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .72 44 error (2) 0 wit inspect .019 4.9
float-benchs/sqrt_Householder_interval_true-unreach-call.c unknown 0 wit inspect 890    620 7700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .50 42 error (2) 0 wit inspect .019 4.9
float-benchs/sqrt_Householder_pseudoconstant_true-unreach-call.c unknown 0 wit inspect 890    1200 7200   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .020 5.0
float-benchs/sqrt_Newton_pseudoconstant_true-unreach-call.c unknown 0 wit inspect 890    1100 7200   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .019 4.9
float-benchs/sqrt_biNewton_pseudoconstant_true-unreach-call.c unknown 0 wit inspect 890    1400 7000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .019 4.9
float-benchs/sqrt_poly_true-unreach-call_true-termination.c unknown 0 wit inspect 890    500 6900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .018 4.8
float-benchs/water_pid_true-unreach-call_true-termination.c unknown 0 wit inspect 890    580 7600   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 41 error (2) 0 wit inspect .019 4.9
float-benchs/zonotope_2_true-unreach-call_true-termination.c unknown 0 wit inspect 45    76 610   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 43 error (2) 0 wit inspect .019 4.8
float-benchs/zonotope_3_true-unreach-call_true-termination.c true 2 wit inspect 200    2300 2000   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.7  340 timeout 0 wit inspect 960     5100  
float-benchs/zonotope_loose_true-unreach-call_true-termination.c true 2 wit inspect 90    350 890   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.1  310 true 2 wit inspect 110     940  
float-benchs/zonotope_tight_true-unreach-call_true-termination.c true 2 wit inspect 110    350 960   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.1  310 true 2 wit inspect 110     950  
floats-esbmc-regression/Double_div_true-unreach-call.i unknown 0 wit inspect 890    260 8000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 44 error (2) 0 wit inspect .019 4.8
floats-esbmc-regression/Float_div_true-unreach-call.i unknown 0 wit inspect 890    610 12000   - 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/ceil_nondet_true-unreach-call.i unknown 0 wit inspect 17    460 170   - wit inspect - wit inspect - wit inspect - wit inspect error 0 wit inspect 4.3  260 unknown 0 wit inspect 9.1   270  
floats-esbmc-regression/ceil_true-unreach-call.i true 2 wit inspect 4.3  270 48   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  260 unknown 0 wit inspect 3.7   210  
floats-esbmc-regression/copysign_true-unreach-call.i true 2 wit inspect 4.5  270 48   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  250 unknown 0 wit inspect 3.8   210  
floats-esbmc-regression/digits_for_true-unreach-call.i false(unreach-call) -16 wit inspect 19    76 280   - wit inspect - wit inspect - wit inspect - wit inspect assertion 0 wit inspect 4.0  270 true 2 wit inspect 5.2   250  
floats-esbmc-regression/digits_while_true-unreach-call.i false(unreach-call) -16 wit inspect 19    76 230   - wit inspect - wit inspect - wit inspect - wit inspect assertion 0 wit inspect 4.0  260 true 2 wit inspect 5.3   320  
floats-esbmc-regression/fabs_true-unreach-call.i true 2 wit inspect 5.8  300 59   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3  260 true 2 wit inspect 9.6   280  
floats-esbmc-regression/fdim_true-unreach-call.i true 2 wit inspect 4.2  260 45   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.9  250 unknown 0 wit inspect 3.4   200  
floats-esbmc-regression/floor_nondet_true-unreach-call.i unknown 0 wit inspect 14    440 160   - wit inspect - wit inspect - wit inspect - wit inspect error 0 wit inspect 5.2  260 unknown 0 wit inspect 7.3   210  
floats-esbmc-regression/floor_true-unreach-call.i true 2 wit inspect 4.3  270 44   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  260 unknown 0 wit inspect 3.8   200  
floats-esbmc-regression/fmax_true-unreach-call.i true 2 wit inspect 4.2  260 44   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  260 true 2 wit inspect 9.1   260  
floats-esbmc-regression/fmin_true-unreach-call.i true 2 wit inspect 4.1  270 39   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  260 true 2 wit inspect 6.1   280  
floats-esbmc-regression/fmod2_true-unreach-call.i false(unreach-call) -16 wit inspect 5.0  280 46   - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 4.8  270 unknown 0 wit inspect 7.1   210  
floats-esbmc-regression/fmod3_true-unreach-call.i false(unreach-call) -16 wit inspect 5.1  280 52   - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 3.9  270 unknown 0 wit inspect 11     210  
floats-esbmc-regression/fmod_true-unreach-call.i true 2 wit inspect 4.3  260 40   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  260 unknown 0 wit inspect 3.7   200  
floats-esbmc-regression/isgreater_true-unreach-call.i true 2 wit inspect 4.2  270 37   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0  260 true 2 wit inspect 8.6   270  
floats-esbmc-regression/isgreaterequal_true-unreach-call.i true 2 wit inspect 4.3  270 49   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.7  260 true 2 wit inspect 8.9   280  
floats-esbmc-regression/isless_true-unreach-call.i true 2 wit inspect 4.2  260 41   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.1  260 true 2 wit inspect 9.3   280  
floats-esbmc-regression/islessequal_true-unreach-call.i true 2 wit inspect 4.1  260 39   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.7  260 true 2 wit inspect 8.5   270  
floats-esbmc-regression/islessgreater_true-unreach-call.i true 2 wit inspect 4.3  280 45   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  260 true 2 wit inspect 9.2   270  
floats-esbmc-regression/isunordered_true-unreach-call.i true 2 wit inspect 4.2  270 44   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.9  260 true 2 wit inspect 10     260  
floats-esbmc-regression/lrint_true-unreach-call.i unknown 0 wit inspect 8.8  430 84   - wit inspect - wit inspect - wit inspect - wit inspect error 0 wit inspect 4.1  260 unknown 0 wit inspect 3.6   200  
floats-esbmc-regression/modf_true-unreach-call.i true 2 wit inspect 4.4  270 44   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.5  260 unknown 0 wit inspect 3.8   200  
floats-esbmc-regression/nan_true-unreach-call.i true 2 wit inspect 4.2  270 44   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  250 true 2 wit inspect 10     280  
floats-esbmc-regression/nearbyint2_true-unreach-call.i unknown 0 wit inspect 9.2  450 91   - wit inspect - wit inspect - wit inspect - wit inspect error 0 wit inspect 4.2  260 unknown 0 wit inspect 3.8   210  
floats-esbmc-regression/nearbyint_true-unreach-call.i unknown 0 wit inspect 11    470 100   - wit inspect - wit inspect - wit inspect - wit inspect error 0 wit inspect 5.9  290 unknown 0 wit inspect 3.7   200  
floats-esbmc-regression/remainder_true-unreach-call.i true 2 wit inspect 4.5  270 48   - 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/rint2_true-unreach-call.i unknown 0 wit inspect 9.4  450 83   - wit inspect - wit inspect - wit inspect - wit inspect error 0 wit inspect 4.1  260 unknown 0 wit inspect 3.7   200  
floats-esbmc-regression/rint_true-unreach-call.i unknown 0 wit inspect 12    470 98   - wit inspect - wit inspect - wit inspect - wit inspect error 0 wit inspect 5.6  290 unknown 0 wit inspect 3.8   200  
floats-esbmc-regression/round_nondet_true-unreach-call.i unknown 0 wit inspect 17    450 180   - wit inspect - wit inspect - wit inspect - wit inspect error 0 wit inspect 4.0  260 unknown 0 wit inspect 7.4   200  
floats-esbmc-regression/round_true-unreach-call.i true 2 wit inspect 4.8  260 47   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.7  250 unknown 0 wit inspect 3.9   210  
floats-esbmc-regression/rounding_functions_true-unreach-call.i true 2 wit inspect 5.1  260 52   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8  260 unknown 0 wit inspect 3.7   200  
floats-esbmc-regression/trunc_nondet_2_true-unreach-call.i unknown 0 wit inspect 890    97 12000   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.2  270 unknown 0 wit inspect 7.4   200  
floats-esbmc-regression/trunc_nondet_true-unreach-call.i unknown 0 wit inspect 12    450 100   - wit inspect - wit inspect - wit inspect - wit inspect error 0 wit inspect 4.5  250 unknown 0 wit inspect 8.1   210  
floats-esbmc-regression/trunc_true-unreach-call.i true 2 wit inspect 4.4  270 38   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.5  270 unknown 0 wit inspect 3.8   200  
floats-esbmc-regression/Double_div_bad_false-unreach-call.i unknown 0 wit inspect 890    630 8100   error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .023 4.9 error (invalid witness file) 0 wit inspect .85 49 error (invalid witness file) 0 wit inspect .0011 .34 - wit inspect - wit inspect
floats-esbmc-regression/Float_div_bad_false-unreach-call.i unknown 0 wit inspect 890    690 8800   error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .81 49 error (invalid witness file) 0 wit inspect .0014 .26 - wit inspect - wit inspect
floats-esbmc-regression/digits_bad_for_false-unreach-call.i false(unreach-call) 0 wit inspect 19    76 280   assertion 0 wit inspect 4.1  290 true -32 wit inspect 5.2   240   unknown 0 wit inspect 3.7  220 true -32 wit inspect .63   19    - wit inspect - wit inspect
floats-esbmc-regression/digits_bad_while_false-unreach-call.i false(unreach-call) 0 wit inspect 19    76 240   assertion 0 wit inspect 3.8  270 true -32 wit inspect 5.5   320   unknown 0 wit inspect 3.6  220 true -32 wit inspect .63   19    - 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 54 71000 87000 680000 31 -352 54 4400 31 -480 72 3700 31 0 58 3700 31 -118 9.0 280 141 132 1400 25000 141 106 4800 33000
    correct results 72 134 2800 23000 27000 0 0 0 10 10 6.0 180 66 132 400 18000 53 106 1300 20000
        correct true 62 124 1400 21000 15000 0 0 0 0 66 132 400 18000 53 106 1300 20000
        correct false 10 10 1300 1800 12000 0 0 0 10 10 6.0 180 0 0
    correct-unconfimed results 5 0 40 300 540 0 0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0 0
        correct-unconfirmed false 5 0 40 300 540 0 0 0 0 0 0
    incorrect results 5 -80 370 980 3700 11 -352 33 2800 15 -480 72 3600 0 4 -128 2.4 75 0 0
        incorrect true 0 11 -352 33 2800 15 -480 72 3600 0 4 -128 2.4 75 0 0
        incorrect false 5 -80 370 980 3700 0 0 0 0 0 0
score (172 tasks, max score: 313) 54 -352 -480 0 -118 132 106
Run set depthk.sv-comp18.ReachSafety-Floats cpa-seq-validate-violation-witnesses-depthk.sv-comp18-violation-witness.ReachSafety-Floats uautomizer-validate-violation-witnesses-depthk.sv-comp18-violation-witness.ReachSafety-Floats cpa-witness2test-validate-violation-witnesses-depthk.sv-comp18-violation-witness.ReachSafety-Floats fshell-witness2test-validate-violation-witnesses-depthk.sv-comp18-violation-witness.ReachSafety-Floats cpa-seq-validate-correctness-witnesses-depthk.sv-comp18-correctness-witness.ReachSafety-Floats uautomizer-validate-correctness-witnesses-depthk.sv-comp18-correctness-witness.ReachSafety-Floats