Tool SMACK 1.9.3 CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a CPA-witness2test 1.7-svn 29852 CProver witness2test 0.1 CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a
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.15.0-42-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33546 MB
Date of execution 2018-12-07 19:13:55 CET 2018-12-08 22:05:35 CET 2018-12-08 23:40:49 CET 2018-12-08 23:45:33 CET 2018-12-12 21:01:56 CET 2018-12-08 20:48:05 CET 2018-12-08 22:13:47 CET
Run set smack.sv-comp19_prop-reachsafety.ReachSafety-Floats cpa-seq-validate-violation-witnesses-smack.sv-comp19_prop-reachsafety.ReachSafety-Floats uautomizer-validate-violation-witnesses-smack.sv-comp19_prop-reachsafety.ReachSafety-Floats cpa-witness2test-validate-violation-witnesses-smack.sv-comp19_prop-reachsafety.ReachSafety-Floats fshell-witness2test-validate-violation-witnesses-smack.sv-comp19_prop-reachsafety.ReachSafety-Floats cpa-seq-validate-correctness-witnesses-smack.sv-comp19_prop-reachsafety.ReachSafety-Floats uautomizer-validate-correctness-witnesses-smack.sv-comp19_prop-reachsafety.ReachSafety-Floats
Options -w error-witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -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 -witness ../../results-verified/smack.2018-12-07_1913.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/smack.2018-12-07_1913.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true -witness ../../results-verified/smack.2018-12-07_1913.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/smack.2018-12-07_1913.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/smack.2018-12-07_1913.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/smack.2018-12-07_1913.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB)
floats-cdfpl/newton_1_4_false-unreach-call_true-termination.i timeout 0 --- inspect 880    930    1100 7300   .92 0      error (invalid witness file) 0 --- inspect .61 .38 42 0   0     error (2) 0 --- inspect .021 .021 5.6 0    0    error (invalid witness file) 0 --- inspect .94 .60 48 0   0      error (invalid witness file) 0 --- inspect .0047 .0062 .53 0      0      - --- inspect - --- inspect
floats-cdfpl/newton_1_5_false-unreach-call_true-termination.i timeout 0 --- inspect 880    930    1200 6000   .92 0      error (invalid witness file) 0 --- inspect .76 .46 42 0   0     error (2) 0 --- inspect .021 .022 5.6 0    0    error (invalid witness file) 0 --- inspect .95 .63 47 0   0      error (invalid witness file) 0 --- inspect .0047 .0057 .53 0      0      - --- inspect - --- inspect
floats-cdfpl/newton_1_6_false-unreach-call_true-termination.i timeout 0 --- inspect 880    930    970 6900   .91 0      error (invalid witness file) 0 --- inspect .62 .39 41 0   0     error (2) 0 --- inspect .021 .021 5.6 0    0    error (invalid witness file) 0 --- inspect .94 .61 48 0   0      error (invalid witness file) 0 --- inspect .0016 .0018 .40 0      0      - --- inspect - --- inspect
floats-cdfpl/newton_1_7_false-unreach-call_true-termination.i timeout 0 --- inspect 880    930    960 6500   .92 0      error (invalid witness file) 0 --- inspect .65 .40 40 0   0     error (2) 0 --- inspect .031 .032 5.6 0    0    error (invalid witness file) 0 --- inspect 1.0  .66 47 0   0      error (invalid witness file) 0 --- inspect .0017 .0021 .53 0      0      - --- inspect - --- inspect
floats-cdfpl/newton_1_8_false-unreach-call_true-termination.i timeout 0 --- inspect 880    930    1400 5300   .91 0      error (invalid witness file) 0 --- inspect .58 .36 40 0   0     error (2) 0 --- inspect .021 .021 5.6 0    0    error (invalid witness file) 0 --- inspect .95 .61 46 0   0      error (invalid witness file) 0 --- inspect .0045 .0055 .53 0      0      - --- inspect - --- inspect
floats-cdfpl/newton_2_6_false-unreach-call_true-termination.i timeout 0 --- inspect 880    930    2100 6400   .91 0      error (invalid witness file) 0 --- inspect .59 .37 40 0   0     error (2) 0 --- inspect .020 .022 5.7 0    0    error (invalid witness file) 0 --- inspect .96 .63 48 0   0      error (invalid witness file) 0 --- inspect .0058 .0075 .53 0      0      - --- inspect - --- inspect
floats-cdfpl/newton_2_7_false-unreach-call_true-termination.i timeout 0 --- inspect 880    930    1500 6800   .91 0      error (invalid witness file) 0 --- inspect .73 .45 41 0   0     error (2) 0 --- inspect .021 .021 5.6 0    0    error (invalid witness file) 0 --- inspect .94 .61 47 0   0      error (invalid witness file) 0 --- inspect .0054 .0082 .53 0      0      - --- inspect - --- inspect
floats-cdfpl/newton_2_8_false-unreach-call_true-termination.i timeout 0 --- inspect 880    930    2100 6000   .91 0      error (invalid witness file) 0 --- inspect .63 .38 41 0   0     error (2) 0 --- inspect .021 .022 5.6 0    0    error (invalid witness file) 0 --- inspect 1.0  .63 47 0   0      error (invalid witness file) 0 --- inspect .0025 .0034 .54 0      0      - --- inspect - --- inspect
floats-cdfpl/newton_3_6_false-unreach-call_true-termination.i timeout 0 --- inspect 880    930    3200 6800   .93 0      error (invalid witness file) 0 --- inspect .75 .47 41 0   0     error (2) 0 --- inspect .021 .021 5.6 0    0    error (invalid witness file) 0 --- inspect .96 .61 47 0   0      error (invalid witness file) 0 --- inspect .0021 .0026 .53 0      0      - --- inspect - --- inspect
floats-cdfpl/newton_3_7_false-unreach-call_true-termination.i timeout 0 --- inspect 880    930    2100 6800   .93 0      error (invalid witness file) 0 --- inspect .74 .46 41 0   0     error (2) 0 --- inspect .020 .020 5.6 0    0    error (invalid witness file) 0 --- inspect .95 .61 47 0   0      error (invalid witness file) 0 --- inspect .0019 .0025 .52 0      0      - --- inspect - --- inspect
floats-cdfpl/newton_3_8_false-unreach-call_true-termination.i timeout 0 --- inspect 880    930    2800 5800   .93 0      error (invalid witness file) 0 --- inspect .56 .35 40 0   0     error (2) 0 --- inspect .021 .022 5.6 0    0    error (invalid witness file) 0 --- inspect .93 .61 49 0   0      error (invalid witness file) 0 --- inspect .0048 .0058 .53 0      0      - --- inspect - --- inspect
floats-cdfpl/sine_1_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 750    750    700 6300   .90 0      error (invalid witness file) 0 --- inspect 2.9  1.6  200 0   0     timeout 0 --- inspect 97     92     600   .71 0    error (invalid witness file) 0 --- inspect 3.1  1.8  200 0   .029  error (1) 0 --- inspect .52   .52   20    .0041 0      - --- inspect - --- inspect
floats-cdfpl/sine_2_false-unreach-call_true-termination.i timeout 0 --- inspect 880    930    610 6600   .89 0      error (invalid witness file) 0 --- inspect .70 .44 40 0   0     error (2) 0 --- inspect .020 .021 5.6 0    0    error (invalid witness file) 0 --- inspect .94 .62 46 0   0      error (invalid witness file) 0 --- inspect .0051 .0063 .53 0      0      - --- inspect - --- inspect
floats-cdfpl/sine_3_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 680    680    530 5100   .89 0      error (invalid witness file) 0 --- inspect 2.9  1.6  200 0   0     timeout 0 --- inspect 97     92     610   1.6  0    error (invalid witness file) 0 --- inspect 3.0  1.8  210 0   0      error (1) 0 --- inspect .52   .52   20    .0041 0      - --- inspect - --- inspect
floats-cdfpl/square_1_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 390    390    200 2700   .88 0      error (invalid witness file) 0 --- inspect 2.7  1.5  200 0   0     timeout (false(unreach-call)) 0 --- inspect 93     87     440   .71 0    error (invalid witness file) 0 --- inspect 3.1  1.8  200 0   0      error (1) 0 --- inspect .51   .51   20    .0041 0      - --- inspect - --- inspect
floats-cdfpl/square_2_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 830    830    280 6700   .88 0      error (invalid witness file) 0 --- inspect 3.3  1.9  200 0   0     timeout (false(unreach-call)) 0 --- inspect 92     87     440   .71 0    error (invalid witness file) 0 --- inspect 3.0  1.7  200 0   0      error (1) 0 --- inspect .55   .54   20    .0041 0      - --- inspect - --- inspect
floats-cdfpl/square_3_false-unreach-call_true-termination.i timeout 0 --- inspect 880    930    280 9500   .89 0      error (invalid witness file) 0 --- inspect .58 .36 41 0   0     error (2) 0 --- inspect .020 .021 5.6 0    0    error (invalid witness file) 0 --- inspect 1.0  .65 47 0   0      error (invalid witness file) 0 --- inspect .0017 .0028 .53 0      0      - --- inspect - --- inspect
floats-cdfpl/newton_1_1_true-unreach-call_true-termination.i timeout 0 --- inspect 880    930    1600 6700   .92 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .35 40 0   0      error (2) 0 --- inspect .028 .029 5.6 0    0     
floats-cdfpl/newton_1_2_true-unreach-call_true-termination.i timeout 0 --- inspect 880    930    990 6600   .91 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .44 41 0   0      error (2) 0 --- inspect .020 .022 5.6 0    0     
floats-cdfpl/newton_1_3_true-unreach-call_true-termination.i timeout 0 --- inspect 880    930    1200 6400   .91 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 41 0   0      error (2) 0 --- inspect .027 .027 5.6 0    0     
floats-cdfpl/newton_2_1_true-unreach-call_true-termination.i timeout 0 --- inspect 880    930    1500 7900   .91 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .67 .43 41 0   0      error (2) 0 --- inspect .020 .021 5.6 0    0     
floats-cdfpl/newton_2_2_true-unreach-call_true-termination.i timeout 0 --- inspect 880    930    2500 5700   .91 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .47 43 0   0      error (2) 0 --- inspect .035 .035 5.6 0    0     
floats-cdfpl/newton_2_3_true-unreach-call_true-termination.i timeout 0 --- inspect 880    930    2600 5200   .91 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .38 41 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0     
floats-cdfpl/newton_2_4_true-unreach-call_true-termination.i timeout 0 --- inspect 880    930    1500 5200   .91 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .47 41 0   0      error (2) 0 --- inspect .024 .025 5.7 0    0     
floats-cdfpl/newton_2_5_true-unreach-call_true-termination.i timeout 0 --- inspect 880    930    1800 7000   .92 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .48 40 0   0      error (2) 0 --- inspect .026 .027 5.6 0    0     
floats-cdfpl/newton_3_1_true-unreach-call_true-termination.i timeout 0 --- inspect 880    930    3300 5400   .93 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .47 41 0   0      error (2) 0 --- inspect .023 .024 5.6 0    0     
floats-cdfpl/newton_3_2_true-unreach-call_true-termination.i timeout 0 --- inspect 880    930    2300 7100   .93 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .46 42 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0     
floats-cdfpl/newton_3_3_true-unreach-call_true-termination.i timeout 0 --- inspect 880    930    3500 6000   .93 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .46 41 0   0      error (2) 0 --- inspect .026 .027 5.6 0    0     
floats-cdfpl/newton_3_4_true-unreach-call_true-termination.i timeout 0 --- inspect 880    930    2800 11000   .93 .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .45 42 0   0      error (2) 0 --- inspect .027 .027 5.7 0    0     
floats-cdfpl/newton_3_5_true-unreach-call_true-termination.i timeout 0 --- inspect 880    930    2400 5600   .93 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .46 40 0   0      error (2) 0 --- inspect .019 .020 5.6 0    0     
floats-cdfpl/sine_4_true-unreach-call_true-termination.i timeout 0 --- inspect 880    930    620 5300   .90 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .44 40 0   0      error (2) 0 --- inspect .023 .023 5.6 0    0     
floats-cdfpl/sine_5_true-unreach-call_true-termination.i timeout 0 --- inspect 880    930    600 6500   .90 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .46 42 0   0      error (2) 0 --- inspect .027 .027 5.6 0    0     
floats-cdfpl/sine_6_true-unreach-call_true-termination.i timeout 0 --- inspect 880    930    600 6500   .89 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .47 40 0   0      error (2) 0 --- inspect .027 .028 5.7 0    0     
floats-cdfpl/sine_7_true-unreach-call_true-termination.i timeout 0 --- inspect 880    930    630 6000   .89 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .48 41 0   0      error (2) 0 --- inspect .027 .027 5.6 0    0     
floats-cdfpl/sine_8_true-unreach-call_true-termination.i timeout 0 --- inspect 880    930    720 6500   .90 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .45 41 0   0      error (2) 0 --- inspect .021 .021 5.6 0    0     
floats-cdfpl/square_4_true-unreach-call_true-termination.i timeout 0 --- inspect 880    930    370 7800   .90 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .81 .49 40 0   0      error (2) 0 --- inspect .026 .026 5.6 0    0     
floats-cdfpl/square_5_true-unreach-call_true-termination.i timeout 0 --- inspect 880    930    370 9700   .89 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .43 40 0   0      error (2) 0 --- inspect .025 .025 5.6 0    0     
floats-cdfpl/square_6_true-unreach-call_true-termination.i timeout 0 --- inspect 880    930    560 7700   .89 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .35 42 0   0      error (2) 0 --- inspect .040 .042 5.7 0    .029 
floats-cdfpl/square_7_true-unreach-call_true-termination.i timeout 0 --- inspect 880    930    370 9200   .90 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .37 40 0   0      error (2) 0 --- inspect .021 .023 5.6 0    0     
floats-cdfpl/square_8_true-unreach-call_true-termination.i timeout 0 --- inspect 880    930    370 7200   .90 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .45 40 0   0      error (2) 0 --- inspect .026 .028 5.6 0    0     
floats-cbmc-regression/float-div1_true-unreach-call.i true 2 wit inspect 37    37    250 440   .98 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 6.7  4.1  320 0   .19   true 2 --- inspect 43     37     950   .68 0     
floats-cbmc-regression/float-flags-simp1_true-unreach-call.i true 2 wit inspect 290    290    590 1900   1.5  2.1    - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 13    9.9  780 0   0      error (7) 0 --- inspect 16     9.0   290   .75 0     
floats-cbmc-regression/float-no-simp1_true-unreach-call_true-termination.i true 2 wit inspect 2.5  2.7  74 31   .87 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.4  2.4  250 0   0      true 2 --- inspect 13     8.0   290   .75 0     
floats-cbmc-regression/float-no-simp2_true-unreach-call.i true 2 wit inspect 91    91    190 1100   .96 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 19    16    300 0   0      true 2 --- inspect 52     44     540   .68 0     
floats-cbmc-regression/float-no-simp3_true-unreach-call_true-termination.i true 2 wit inspect 2.5  2.7  74 33   .86 2.1    - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.4  2.5  250 0   0      true 2 --- inspect 14     8.4   300   .75 0     
floats-cbmc-regression/float-no-simp4_true-unreach-call.i true 2 wit inspect 7.6  7.9  290 77   1.2  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.8  2.6  270 0   0      true 2 --- inspect 20     12     440   .68 0     
floats-cbmc-regression/float-no-simp6_true-unreach-call_true-termination.i true 2 wit inspect 2.6  2.7  73 28   .88 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.3  1.9  250 0   0      true 2 --- inspect 15     8.8   310   .71 0     
floats-cbmc-regression/float-no-simp7_true-unreach-call_true-termination.i true 2 wit inspect 2.6  2.7  72 34   .87 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.9  2.2  250 0   0      true 2 --- inspect 15     8.9   300   .75 0     
floats-cbmc-regression/float-no-simp8_true-unreach-call.i true 2 wit inspect 2.6  2.7  73 32   .92 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.4  2.9  260 0   0      error (7) 0 --- inspect 15     8.2   290   .75 .0082
floats-cbmc-regression/float-rounding1_true-unreach-call.i true 2 wit inspect 2.7  2.7  79 32   .96 0      - --- inspect - --- inspect - --- inspect - --- inspect error 0 wit inspect 6.0  3.3  260 0   0      unknown 0 --- inspect 7.8   4.3   280   .66 0     
floats-cbmc-regression/float-to-double1_true-unreach-call.i true 2 wit inspect 2.9  3.2  130 42   .96 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.7  3.2  260 0   0      true 2 --- inspect 35     28     450   .75 0     
floats-cbmc-regression/float-to-double2_true-unreach-call_true-termination.i true 2 wit inspect 2.5  2.7  73 31   .86 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.5  2.6  250 0   0      true 2 --- inspect 17     9.6   300   .75 0     
floats-cbmc-regression/float-zero-sum1_true-unreach-call_true-termination.i true 2 wit inspect 2.5  2.7  74 36   .87 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.6  2.5  250 0   0      true 2 --- inspect 13     7.5   300   .68 0     
floats-cbmc-regression/float11_true-unreach-call_true-termination.i true 2 wit inspect 2.5  2.7  72 31   .86 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.7  2.0  250 0   0      true 2 --- inspect 14     8.4   300   .75 0     
floats-cbmc-regression/float12_true-unreach-call_true-termination.i true 2 wit inspect 4.2  4.2  100 53   .88 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.3  2.4  250 0   0      true 2 --- inspect 22     15     300   .75 0     
floats-cbmc-regression/float13_true-unreach-call_true-termination.i true 2 wit inspect 2.5  2.7  74 29   .90 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.6  2.6  250 0   0      true 2 --- inspect 14     8.9   310   .75 0     
floats-cbmc-regression/float14_true-unreach-call.i true 2 wit inspect 2.6  2.8  87 35   .95 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.2  2.3  260 0   0      true 2 --- inspect 21     12     390   .75 0     
floats-cbmc-regression/float18_true-unreach-call.i true 2 wit inspect 2.5  2.7  72 33   .93 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 45    39    620 0   0      error (7) 0 --- inspect 15     8.4   290   .75 .0082
floats-cbmc-regression/float19_true-unreach-call.i true 2 wit inspect 3.0  3.3  100 36   .95 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.4  2.9  260 0   0      true 2 --- inspect 18     11     390   .75 0     
floats-cbmc-regression/float1_true-unreach-call_true-termination.i true 2 wit inspect 2.6  2.7  80 32   .87 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.0  2.2  250 0   0      true 2 --- inspect 15     9.0   300   .75 0     
floats-cbmc-regression/float20_true-unreach-call_true-termination.i true 2 wit inspect 8.0  8.2  140 93   .91 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.0  2.3  250 0   0      true 2 --- inspect 20     14     380   .75 0     
floats-cbmc-regression/float21_true-unreach-call.i true 2 wit inspect 120    120    450 940   1.0  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 11    8.1  300 0   0      true 2 --- inspect 74     64     570   .71 0     
floats-cbmc-regression/float22_true-unreach-call_true-termination.i true 2 wit inspect 5.1  5.3  110 71   1.0  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.0  2.9  270 0   0      true 2 --- inspect 200     180     740   .68 0     
floats-cbmc-regression/float2_true-unreach-call_true-termination.i true 2 wit inspect 2.5  2.7  72 32   .87 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.4  1.9  250 0   0      true 2 --- inspect 18     11     310   .75 0     
floats-cbmc-regression/float3_true-unreach-call_true-termination.i true 2 wit inspect 4.2  4.2  120 56   .90 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.5  2.0  270 0   .30   true 2 --- inspect 16     10     320   .75 0     
floats-cbmc-regression/float4_true-unreach-call.i true 2 wit inspect 88    88    190 1100   1.0  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 92    89    330 0   0      true 2 --- inspect 99     89     590   .71 0     
floats-cbmc-regression/float5_true-unreach-call_true-termination.i true 2 wit inspect 5.5  5.7  97 67   .88 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.2  2.9  260 0   0      true 2 --- inspect 31     24     300   .75 0     
floats-cbmc-regression/float6_true-unreach-call_true-termination.i true 2 wit inspect 2.7  2.8  78 33   .97 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.9  2.7  250 0   0      true 2 --- inspect 18     10     310   .75 0     
floats-cbmc-regression/float8_true-unreach-call.i true 2 wit inspect 2.6  2.7  73 34   .93 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 9.4  7.0  270 0   0      true 2 --- inspect 16     9.5   390   .75 0     
floats-cbmc-regression/float_lib1_true-unreach-call.i true 2 wit inspect 2.8  2.8  80 32   1.0  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 6.0  3.3  260 0   0      error (7) 0 --- inspect 12     7.2   290   .68 0     
floats-cbmc-regression/float_lib2_true-unreach-call.i true 2 wit inspect 9.3  9.2  290 110   .97 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.8  2.6  260 0   .029  true 2 --- inspect 17     9.6   430   .68 0     
float-benchs/cast_float_ptr_false-unreach-call_true-termination.c false(unreach-call) 0 wit inspect 3.9  4.2  88 57   .91 0      error (invalid witness file) 0 --- inspect 3.0  1.7  200 0   0     false(unreach-call) 1 --- inspect 18     10     320   .68 0    error (invalid witness file) 0 --- inspect 3.6  2.1  210 0   0      error (1) 0 --- inspect .51   .52   20    .0041 .0041 - --- inspect - --- inspect
float-benchs/cast_union_loose_false-unreach-call_true-termination.c false(unreach-call) 0 wit inspect 4.7  4.8  94 59   .91 0      error (invalid witness file) 0 --- inspect 3.0  1.7  200 0   0     false(unreach-call) 1 --- inspect 14     8.1   320   .68 0    error (invalid witness file) 0 --- inspect 3.2  1.8  200 0   0      error (1) 0 --- inspect .53   .53   20    .0041 0      - --- inspect - --- inspect
float-benchs/cast_union_tight_false-unreach-call_true-termination.c false(unreach-call) 0 wit inspect 4.3  4.2  100 57   .91 0      error (invalid witness file) 0 --- inspect 2.6  1.4  200 0   0     false(unreach-call) 1 --- inspect 13     7.6   310   .75 0    error (invalid witness file) 0 --- inspect 3.2  1.9  200 0   .0041 error (1) 0 --- inspect .51   .51   20    .0041 0      - --- inspect - --- inspect
float-benchs/float_int_inv_square_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 4.0  4.2  89 48   .88 0      false(unreach-call) 1 wit inspect 3.9  2.2  260 0   0     false(unreach-call) 1 --- inspect 13     7.6   300   .68 0    false(unreach-call) 1 --- inspect 3.8  2.2  250 0   0      error (2) 0 --- inspect .56   .56   20    .037  .0041 - --- inspect - --- inspect
float-benchs/inv_Newton_false-unreach-call.c timeout 0 --- inspect 880    930    810 8800   .93 0      error (invalid witness file) 0 --- inspect .60 .36 42 0   0     error (2) 0 --- inspect .020 .020 5.6 0    0    error (invalid witness file) 0 --- inspect .91 .60 47 0   0      error (invalid witness file) 0 --- inspect .0015 .0019 .41 0      0      - --- inspect - --- inspect
float-benchs/inv_Newton_false-unreach-call.c.p+cfa-reducer.c timeout 0 --- inspect 880    930    650 8900   .93 0      error (invalid witness file) 0 --- inspect .74 .46 40 0   0     error (2) 0 --- inspect .021 .022 5.6 0    0    error (invalid witness file) 0 --- inspect 1.1  .71 47 0   0      error (invalid witness file) 0 --- inspect .0054 .0074 .41 0      0      - --- inspect - --- inspect
float-benchs/inv_square_false-unreach-call_true-termination.c false(unreach-call) 0 wit inspect 3.5  3.7  81 45   .88 0      error (invalid witness file) 0 --- inspect 2.8  1.6  200 0   0     false(unreach-call) 1 --- inspect 13     8.0   300   .71 0    error (invalid witness file) 0 --- inspect 2.9  1.7  210 0   0      error (1) 0 --- inspect .54   .54   20    .0041 0      - --- inspect - --- inspect
float-benchs/nan_double_false-unreach-call_true-termination.c false(unreach-call) 0 wit inspect 3.2  3.2  72 35   .87 0      error (invalid witness file) 0 --- inspect 2.5  1.4  190 0   0     false(unreach-call) 1 --- inspect 12     7.6   290   .68 0    error (invalid witness file) 0 --- inspect 2.9  1.7  200 0   0      error (1) 0 --- inspect .51   .51   20    .0041 0      - --- inspect - --- inspect
float-benchs/nan_float_false-unreach-call_true-termination.c false(unreach-call) 0 wit inspect 3.2  3.2  72 39   .87 0      error (invalid witness file) 0 --- inspect 2.6  1.5  200 0   0     false(unreach-call) 1 --- inspect 15     9.2   290   .75 0    error (invalid witness file) 0 --- inspect 2.9  1.7  210 0   0      error (1) 0 --- inspect .51   .51   20    .0041 0      - --- inspect - --- inspect
float-benchs/sin_interpolated_index_false-unreach-call_true-termination.c timeout 0 --- inspect 880    930    3200 7100   1.0  0      error (invalid witness file) 0 --- inspect .71 .44 40 0   0     error (2) 0 --- inspect .020 .020 5.6 0    0    error (invalid witness file) 0 --- inspect 1.1  .71 47 0   .094  error (invalid witness file) 0 --- inspect .0021 .0027 .53 0      0      - --- inspect - --- inspect
float-benchs/sqrt_poly2_false-unreach-call.c timeout 0 --- inspect 880    930    480 6000   .93 0      error (invalid witness file) 0 --- inspect .60 .37 42 0   0     error (2) 0 --- inspect .021 .023 5.7 0    0    error (invalid witness file) 0 --- inspect 1.1  .70 47 0   0      error (invalid witness file) 0 --- inspect .0048 .0058 .40 0      0      - --- inspect - --- inspect
float-benchs/Muller_Kahan_true-unreach-call.c.p+cfa-reducer.c out of memory 0 --- inspect 35    34    15000 410   2.2  .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .46 41 0   0      error (2) 0 --- inspect .027 .028 5.7 0    0     
float-benchs/Muller_Kahan_true-unreach-call_true-termination.c out of memory 0 --- inspect 36    35    15000 390   1.5  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .79 .49 41 0   0      error (2) 0 --- inspect .026 .028 5.7 0    .029 
float-benchs/Rump_double_true-unreach-call_true-termination.c true 2 wit inspect 270    270    740 2400   .91 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.2  2.4  250 0   0      true 2 --- inspect 30     24     990   .75 0     
float-benchs/Rump_float_true-unreach-call_true-termination.c true 2 wit inspect 95    95    280 840   .90 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.4  2.4  250 0   0      true 2 --- inspect 18     11     430   .75 0     
float-benchs/addsub_double_exact_true-unreach-call_true-termination.c true 2 wit inspect 2.6  2.7  82 33   .87 .0041 - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.4  2.5  250 0   0      true 2 --- inspect 20     12     290   .75 0     
float-benchs/addsub_float_exact_true-unreach-call_true-termination.c true 2 wit inspect 2.6  2.7  75 38   .87 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.4  2.9  250 0   0      true 2 --- inspect 15     9.1   300   .68 0     
float-benchs/addsub_float_inexact_true-unreach-call_true-termination.c true 2 wit inspect 2.6  2.7  75 32   .87 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.8  2.1  250 0   0      true 2 --- inspect 15     8.5   290   .75 0     
float-benchs/arctan_Pade_true-unreach-call_true-termination.c timeout 0 --- inspect 880    930    4400 7100   .92 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .45 42 0   0      error (2) 0 --- inspect .020 .021 5.6 0    0     
float-benchs/bary_diverge_true-unreach-call_true-termination.c timeout 0 --- inspect 880    930    410 6900   .95 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .47 40 0   0      error (2) 0 --- inspect .026 .026 5.6 0    0     
float-benchs/cast_float_union_true-unreach-call.c true 2 wit inspect 2.6  2.7  74 32   .90 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.4  1.9  250 0   0      true 2 --- inspect 8.3   4.6   300   .66 0     
float-benchs/cos_polynomial_true-unreach-call_true-termination.c timeout 0 --- inspect 880    930    640 5400   .94 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .36 41 0   0      error (2) 0 --- inspect .026 .027 5.6 0    0     
float-benchs/divmul_buf_diverge_true-unreach-call_true-termination.c timeout 0 --- inspect 880    930    640 7500   .92 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .68 .41 41 0   0      error (2) 0 --- inspect .021 .023 5.6 0    0     
float-benchs/divmul_diverge_true-unreach-call_true-termination.c timeout 0 --- inspect 880    930    490 8000   .91 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .83 .49 41 0   0      error (2) 0 --- inspect .026 .027 5.6 0    0     
float-benchs/drift_tenth_true-unreach-call.c.p+cfa-reducer.c true 2 wit inspect 2.5  2.7  74 34   .87 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 30    27    400 0   0      true 2 --- inspect 250     240     640   .71 0     
float-benchs/drift_tenth_true-unreach-call_true-termination.c true 2 wit inspect 2.5  2.7  72 34   .88 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 27    23    410 0   0      true 2 --- inspect 450     440     720   .68 0     
float-benchs/exp_loop_true-unreach-call.c timeout 0 --- inspect 880    930    640 7500   .96 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .46 42 0   0      error (2) 0 --- inspect .020 .020 5.6 0    0     
float-benchs/feedback_diverge_true-unreach-call_true-termination.c timeout 0 --- inspect 880    930    640 8100   .91 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 41 0   0      error (2) 0 --- inspect .025 .026 5.6 0    0     
float-benchs/filter1_true-unreach-call.c.p+cfa-reducer.c timeout 0 --- inspect 880    930    500 8100   .92 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .99 .60 41 0   0      error (2) 0 --- inspect .022 .022 5.6 0    0     
float-benchs/filter1_true-unreach-call.c.v+lhb-reducer.c timeout 0 --- inspect 880    930    640 6800   .97 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .47 41 0   0      error (2) 0 --- inspect .026 .027 5.6 0    0     
float-benchs/filter1_true-unreach-call.c.v+nlh-reducer.c timeout 0 --- inspect 880    930    460 8100   .97 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .48 40 0   0      error (2) 0 --- inspect .020 .021 5.6 0    0     
float-benchs/filter1_true-unreach-call_true-termination.c timeout 0 --- inspect 880    930    780 11000   .91 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .46 40 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0     
float-benchs/filter2_alt_true-unreach-call.c timeout 0 --- inspect 880    930    360 8000   .94 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .40 41 0   0      error (2) 0 --- inspect .025 .026 5.6 0    0     
float-benchs/filter2_iterated_true-unreach-call.c timeout 0 --- inspect 880    930    8300 13000   1.0  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .44 41 0   0      error (2) 0 --- inspect .026 .028 5.7 0    0     
float-benchs/filter2_reinit_true-unreach-call_true-termination.c timeout 0 --- inspect 880    930    710 8000   .94 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .80 .48 41 0   0      error (2) 0 --- inspect .022 .023 5.7 0    0     
float-benchs/filter2_set_true-unreach-call_true-termination.c timeout 0 --- inspect 880    930    580 7700   .96 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 41 0   0      error (2) 0 --- inspect .024 .026 5.7 0    0     
float-benchs/filter2_true-unreach-call_true-termination.c timeout 0 --- inspect 880    930    600 7600   .93 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .91 .56 42 0   0      error (2) 0 --- inspect .024 .024 5.6 0    0     
float-benchs/filter_iir_true-unreach-call.c timeout 0 --- inspect 880    930    680 7200   .95 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .48 41 0   0      error (2) 0 --- inspect .026 .028 5.6 0    0     
float-benchs/float_double_true-unreach-call_true-termination.c true 2 wit inspect 2.5  2.7  77 30   .87 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.3  2.4  250 0   0      true 2 --- inspect 12     7.9   290   .75 0     
float-benchs/image_filter_true-unreach-call.c out of memory 0 --- inspect 68    67    15000 500   1.9  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .45 40 0   0      error (2) 0 --- inspect .028 .028 5.5 0    0     
float-benchs/interpolation2_true-unreach-call.c.p+cfa-reducer.c true 2 wit inspect 190    190    240 2200   .95 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    640 0   0      timeout 0 --- inspect 960     950     1500   1.1  0     
float-benchs/interpolation2_true-unreach-call.c.v+cfa-reducer.c true 2 wit inspect 190    190    210 2000   .95 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 78    75    570 0   0      timeout 0 --- inspect 960     950     1600   .72 0     
float-benchs/interpolation2_true-unreach-call.c.v+nlh-reducer.c true 2 wit inspect 230    230    220 2100   .97 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 44    42    450 0   0      timeout 0 --- inspect 960     950     1600   .72 0     
float-benchs/interpolation2_true-unreach-call_true-termination.c true 2 wit inspect 190    190    220 2500   .95 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 52    49    560 0   0      timeout 0 --- inspect 960     950     1500   .72 0     
float-benchs/interpolation_true-unreach-call.c.p+cfa-reducer.c true 2 wit inspect 70    71    160 710   .94 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 37    34    480 0   0      timeout 0 --- inspect 960     950     1400   .72 0     
float-benchs/interpolation_true-unreach-call.c.v+cfa-reducer.c true 2 wit inspect 84    84    210 790   .94 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 77    74    470 0   .0041 timeout 0 --- inspect 960     950     1400   .73 0     
float-benchs/interpolation_true-unreach-call.c.v+nlh-reducer.c true 2 wit inspect 100    100    200 1200   .95 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 32    29    400 0   0      timeout 0 --- inspect 960     950     1500   .72 0     
float-benchs/interpolation_true-unreach-call_true-termination.c true 2 wit inspect 77    77    150 1200   .93 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 22    20    480 0   0      timeout 0 --- inspect 960     950     1600   .71 0     
float-benchs/inv_Newton_true-unreach-call.c timeout 0 --- inspect 880    930    800 7800   .93 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .68 .42 41 0   0      error (2) 0 --- inspect .024 .025 5.7 0    0     
float-benchs/inv_sqrt_Quake_true-unreach-call.c.v+cfa-reducer.c true 2 wit inspect 720    720    340 5300   .92 1.9    - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 7.3  5.4  310 0   0      true 2 --- inspect 84     77     780   .68 7.2   
float-benchs/inv_sqrt_Quake_true-unreach-call_true-termination.c true 2 wit inspect 150    150    170 1600   .90 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.8  3.1  280 0   0      true 2 --- inspect 88     80     520   .71 0     
float-benchs/inv_square_int_true-unreach-call_true-termination.c true 2 wit inspect 4.1  4.2  89 52   .88 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.0  2.9  260 0   0      true 2 --- inspect 25     19     340   .75 0     
float-benchs/inv_square_true-unreach-call_true-termination.c true 2 wit inspect 3.9  4.2  81 51   .88 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.1  2.3  260 0   0      true 2 --- inspect 75     68     350   .71 0     
float-benchs/loop_true-unreach-call.c true 2 wit inspect 880    880    480 7800   .90 0      - --- inspect - ---