Tool DIVINE 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-06 11:06:04 CET 2018-12-08 03:24:14 CET 2018-12-08 05:17:35 CET 2018-12-08 06:43:53 CET 2018-12-12 20:24:22 CET 2018-12-08 01:45:35 CET 2018-12-08 04:38:54 CET
Run set divine-smt.sv-comp19_prop-reachsafety.ReachSafety-Floats cpa-seq-validate-violation-witnesses-divine-smt.sv-comp19_prop-reachsafety.ReachSafety-Floats uautomizer-validate-violation-witnesses-divine-smt.sv-comp19_prop-reachsafety.ReachSafety-Floats cpa-witness2test-validate-violation-witnesses-divine-smt.sv-comp19_prop-reachsafety.ReachSafety-Floats fshell-witness2test-validate-violation-witnesses-divine-smt.sv-comp19_prop-reachsafety.ReachSafety-Floats cpa-seq-validate-correctness-witnesses-divine-smt.sv-comp19_prop-reachsafety.ReachSafety-Floats uautomizer-validate-correctness-witnesses-divine-smt.sv-comp19_prop-reachsafety.ReachSafety-Floats
Options -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/divine-smt.2018-12-06_1106.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/divine-smt.2018-12-06_1106.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/divine-smt.2018-12-06_1106.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/divine-smt.2018-12-06_1106.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/divine-smt.2018-12-06_1106.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/divine-smt.2018-12-06_1106.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 unknown 0 --- inspect 8.3 8.3 430 110 0   0   error (invalid witness file) 0 --- inspect .62 .38 40 0   0    error (2) 0 --- inspect .028 .029 5.6 0    0   error (invalid witness file) 0 --- inspect 1.0  .67 46 0   0      error (invalid witness file) 0 --- inspect .0031 .0049 .53 0     0      - --- inspect - --- inspect
floats-cdfpl/newton_1_5_false-unreach-call_true-termination.i unknown 0 --- inspect 8.3 8.3 430 110 0   0   error (invalid witness file) 0 --- inspect .79 .48 40 0   0    error (2) 0 --- inspect .022 .023 5.6 0    0   error (invalid witness file) 0 --- inspect .90 .59 47 0   0      error (invalid witness file) 0 --- inspect .0033 .0038 .40 0     0      - --- inspect - --- inspect
floats-cdfpl/newton_1_6_false-unreach-call_true-termination.i unknown 0 --- inspect 8.3 8.3 430 95 0   0   error (invalid witness file) 0 --- inspect .78 .48 41 0   0    error (2) 0 --- inspect .024 .024 5.6 0    0   error (invalid witness file) 0 --- inspect 1.3  .79 46 0   0      error (invalid witness file) 0 --- inspect .0048 .0060 .54 0     0      - --- inspect - --- inspect
floats-cdfpl/newton_1_7_false-unreach-call_true-termination.i unknown 0 --- inspect 8.2 8.2 430 91 0   0   error (invalid witness file) 0 --- inspect .61 .37 41 0   0    error (2) 0 --- inspect .021 .022 5.6 0    0   error (invalid witness file) 0 --- inspect .93 .60 47 0   0      error (invalid witness file) 0 --- inspect .0034 .0044 .53 0     0      - --- inspect - --- inspect
floats-cdfpl/newton_1_8_false-unreach-call_true-termination.i unknown 0 --- inspect 8.5 8.5 430 110 0   0   error (invalid witness file) 0 --- inspect .73 .44 41 0   0    error (2) 0 --- inspect .031 .033 5.8 0    0   error (invalid witness file) 0 --- inspect 1.2  .81 46 0   0      error (invalid witness file) 0 --- inspect .0050 .0063 .53 0     0      - --- inspect - --- inspect
floats-cdfpl/newton_2_6_false-unreach-call_true-termination.i unknown 0 --- inspect 8.3 8.3 430 110 0   0   error (invalid witness file) 0 --- inspect .65 .40 40 0   0    error (2) 0 --- inspect .026 .028 5.7 0    0   error (invalid witness file) 0 --- inspect 1.2  .76 48 0   0      error (invalid witness file) 0 --- inspect .0058 .0073 .52 0     0      - --- inspect - --- inspect
floats-cdfpl/newton_2_7_false-unreach-call_true-termination.i unknown 0 --- inspect 8.4 8.4 430 100 0   0   error (invalid witness file) 0 --- inspect .67 .40 41 0   0    error (2) 0 --- inspect .025 .026 5.6 0    0   error (invalid witness file) 0 --- inspect 1.1  .69 48 0   0      error (invalid witness file) 0 --- inspect .0055 .0074 .53 0     0      - --- inspect - --- inspect
floats-cdfpl/newton_2_8_false-unreach-call_true-termination.i unknown 0 --- inspect 8.5 8.5 430 100 0   0   error (invalid witness file) 0 --- inspect .75 .45 41 0   0    error (2) 0 --- inspect .028 .028 5.6 0    0   error (invalid witness file) 0 --- inspect .97 .64 46 0   0      error (invalid witness file) 0 --- inspect .0052 .0064 .53 0     0      - --- inspect - --- inspect
floats-cdfpl/newton_3_6_false-unreach-call_true-termination.i unknown 0 --- inspect 8.2 8.2 430 120 0   0   error (invalid witness file) 0 --- inspect .68 .43 40 0   0    error (2) 0 --- inspect .022 .022 5.6 0    0   error (invalid witness file) 0 --- inspect 1.2  .79 47 0   0      error (invalid witness file) 0 --- inspect .0015 .0019 .53 0     0      - --- inspect - --- inspect
floats-cdfpl/newton_3_7_false-unreach-call_true-termination.i unknown 0 --- inspect 8.4 8.5 430 100 0   0   error (invalid witness file) 0 --- inspect .76 .46 40 0   0    error (2) 0 --- inspect .022 .023 5.7 0    0   error (invalid witness file) 0 --- inspect .98 .63 47 0   0      error (invalid witness file) 0 --- inspect .0055 .0088 .53 0     0      - --- inspect - --- inspect
floats-cdfpl/newton_3_8_false-unreach-call_true-termination.i unknown 0 --- inspect 8.4 8.4 430 130 0   0   error (invalid witness file) 0 --- inspect .66 .39 41 0   0    error (2) 0 --- inspect .027 .028 5.6 0    0   error (invalid witness file) 0 --- inspect 1.2  .77 47 0   0      error (invalid witness file) 0 --- inspect .0042 .0053 .53 0     0      - --- inspect - --- inspect
floats-cdfpl/sine_1_false-unreach-call_true-termination.i unknown 0 --- inspect 8.3 8.4 430 110 0   0   error (invalid witness file) 0 --- inspect .57 .35 41 0   0    error (2) 0 --- inspect .026 .027 5.6 0    0   error (invalid witness file) 0 --- inspect 1.2  .76 46 0   0      error (invalid witness file) 0 --- inspect .0018 .0024 .54 0     0      - --- inspect - --- inspect
floats-cdfpl/sine_2_false-unreach-call_true-termination.i unknown 0 --- inspect 8.3 8.3 430 110 0   0   error (invalid witness file) 0 --- inspect .68 .43 40 0   0    error (2) 0 --- inspect .027 .028 5.6 0    0   error (invalid witness file) 0 --- inspect .95 .61 47 0   0      error (invalid witness file) 0 --- inspect .0036 .0052 .41 0     0      - --- inspect - --- inspect
floats-cdfpl/sine_3_false-unreach-call_true-termination.i unknown 0 --- inspect 8.3 8.3 430 110 0   0   error (invalid witness file) 0 --- inspect .62 .40 40 0   0    error (2) 0 --- inspect .026 .028 5.7 0    0   error (invalid witness file) 0 --- inspect .94 .62 47 0   0      error (invalid witness file) 0 --- inspect .0054 .0075 .41 0     0      - --- inspect - --- inspect
floats-cdfpl/square_1_false-unreach-call_true-termination.i unknown 0 --- inspect 8.2 8.2 430 110 0   0   error (invalid witness file) 0 --- inspect .58 .35 40 0   0    error (2) 0 --- inspect .021 .022 5.6 0    0   error (invalid witness file) 0 --- inspect .99 .63 49 0   0      error (invalid witness file) 0 --- inspect .0047 .0058 .41 0     0      - --- inspect - --- inspect
floats-cdfpl/square_2_false-unreach-call_true-termination.i unknown 0 --- inspect 8.4 8.4 430 100 0   0   error (invalid witness file) 0 --- inspect .62 .38 42 0   0    error (2) 0 --- inspect .027 .029 5.6 0    0   error (invalid witness file) 0 --- inspect 1.3  .85 49 0   0      error (invalid witness file) 0 --- inspect .0050 .0062 .52 0     0      - --- inspect - --- inspect
floats-cdfpl/square_3_false-unreach-call_true-termination.i unknown 0 --- inspect 8.3 8.3 430 120 0   0   error (invalid witness file) 0 --- inspect .77 .47 41 0   0    error (2) 0 --- inspect .028 .028 5.6 0    0   error (invalid witness file) 0 --- inspect 1.1  .71 47 0   0      error (invalid witness file) 0 --- inspect .0053 .0081 .54 0     0      - --- inspect - --- inspect
floats-cdfpl/newton_1_1_true-unreach-call_true-termination.i unknown 0 --- inspect 8.6 8.7 430 110 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .39 40 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0     
floats-cdfpl/newton_1_2_true-unreach-call_true-termination.i unknown 0 --- inspect 8.3 8.3 430 100 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .40 43 0   0      error (2) 0 --- inspect .019 .020 5.6 0    0     
floats-cdfpl/newton_1_3_true-unreach-call_true-termination.i unknown 0 --- inspect 8.3 8.4 430 110 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .38 40 0   0      error (2) 0 --- inspect .022 .024 5.6 0    0     
floats-cdfpl/newton_2_1_true-unreach-call_true-termination.i unknown 0 --- inspect 8.4 8.4 430 110 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .48 41 0   0      error (2) 0 --- inspect .022 .023 5.6 0    0     
floats-cdfpl/newton_2_2_true-unreach-call_true-termination.i unknown 0 --- inspect 8.2 8.3 430 88 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .70 .44 40 0   0      error (2) 0 --- inspect .021 .023 5.6 0    0     
floats-cdfpl/newton_2_3_true-unreach-call_true-termination.i unknown 0 --- inspect 8.3 8.3 430 98 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .68 .42 41 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0     
floats-cdfpl/newton_2_4_true-unreach-call_true-termination.i unknown 0 --- inspect 8.3 8.3 430 96 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .42 41 0   0      error (2) 0 --- inspect .027 .028 5.5 0    0     
floats-cdfpl/newton_2_5_true-unreach-call_true-termination.i unknown 0 --- inspect 8.2 8.2 430 100 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .45 41 0   0      error (2) 0 --- inspect .024 .026 5.8 0    0     
floats-cdfpl/newton_3_1_true-unreach-call_true-termination.i unknown 0 --- inspect 8.3 8.4 430 100 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .36 40 0   0      error (2) 0 --- inspect .026 .027 5.6 0    0     
floats-cdfpl/newton_3_2_true-unreach-call_true-termination.i unknown 0 --- inspect 8.3 8.4 430 100 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .36 40 0   0      error (2) 0 --- inspect .026 .027 5.6 0    0     
floats-cdfpl/newton_3_3_true-unreach-call_true-termination.i unknown 0 --- inspect 8.3 8.3 430 100 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 41 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0     
floats-cdfpl/newton_3_4_true-unreach-call_true-termination.i unknown 0 --- inspect 8.4 8.4 430 97 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .47 41 0   0      error (2) 0 --- inspect .020 .021 5.7 0    0     
floats-cdfpl/newton_3_5_true-unreach-call_true-termination.i unknown 0 --- inspect 8.4 8.4 430 110 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .47 40 0   0      error (2) 0 --- inspect .027 .028 5.6 0    0     
floats-cdfpl/sine_4_true-unreach-call_true-termination.i unknown 0 --- inspect 8.4 8.4 430 120 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 40 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0     
floats-cdfpl/sine_5_true-unreach-call_true-termination.i unknown 0 --- inspect 8.6 8.6 430 99 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .45 40 0   0      error (2) 0 --- inspect .021 .021 5.6 0    0     
floats-cdfpl/sine_6_true-unreach-call_true-termination.i unknown 0 --- inspect 8.5 8.6 430 120 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 41 0   0      error (2) 0 --- inspect .022 .023 5.6 0    0     
floats-cdfpl/sine_7_true-unreach-call_true-termination.i unknown 0 --- inspect 8.2 8.2 430 94 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 40 0   0      error (2) 0 --- inspect .022 .022 5.6 0    0     
floats-cdfpl/sine_8_true-unreach-call_true-termination.i unknown 0 --- inspect 8.3 8.3 430 110 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .41 40 0   0      error (2) 0 --- inspect .026 .026 5.6 0    0     
floats-cdfpl/square_4_true-unreach-call_true-termination.i unknown 0 --- inspect 8.3 8.3 430 90 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .45 40 0   0      error (2) 0 --- inspect .022 .023 5.6 0    0     
floats-cdfpl/square_5_true-unreach-call_true-termination.i unknown 0 --- inspect 8.4 8.4 430 120 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .41 40 0   0      error (2) 0 --- inspect .021 .022 5.7 0    0     
floats-cdfpl/square_6_true-unreach-call_true-termination.i unknown 0 --- inspect 8.2 8.2 430 110 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .45 41 0   0      error (2) 0 --- inspect .021 .023 5.6 0    0     
floats-cdfpl/square_7_true-unreach-call_true-termination.i unknown 0 --- inspect 8.4 8.5 430 100 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .47 41 0   0      error (2) 0 --- inspect .025 .034 5.6 0    0     
floats-cdfpl/square_8_true-unreach-call_true-termination.i unknown 0 --- inspect 8.2 8.3 430 110 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .44 40 0   0      error (2) 0 --- inspect .027 .029 5.6 0    0     
floats-cbmc-regression/float-div1_true-unreach-call.i unknown 0 --- inspect 8.2 8.2 430 120 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .35 40 0   0      error (2) 0 --- inspect .030 .031 5.5 0    0     
floats-cbmc-regression/float-flags-simp1_true-unreach-call.i unknown 0 --- inspect 8.4 8.4 430 110 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .80 .48 41 0   0      error (2) 0 --- inspect .025 .026 5.7 0    0     
floats-cbmc-regression/float-no-simp1_true-unreach-call_true-termination.i true 2 wit inspect 8.0 8.0 370 130 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.6  2.0  250 0   0      true 2 --- inspect 13     8.3   290   .68 0     
floats-cbmc-regression/float-no-simp2_true-unreach-call.i error - divine failed with exitcode 1 0 --- inspect 1.7 1.7 200 21 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .38 40 0   0      error (2) 0 --- inspect .026 .027 5.8 0    0     
floats-cbmc-regression/float-no-simp3_true-unreach-call_true-termination.i true 2 wit inspect 8.1 8.1 370 120 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.5  2.0  250 0   0      true 2 --- inspect 13     7.3   300   .75 0     
floats-cbmc-regression/float-no-simp4_true-unreach-call.i error - divine failed with exitcode 1 0 --- inspect 1.7 1.7 200 24 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .69 .41 41 0   0      error (2) 0 --- inspect .026 .027 5.6 0    0     
floats-cbmc-regression/float-no-simp6_true-unreach-call_true-termination.i true 2 wit inspect 8.1 8.1 370 92 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.6  2.0  250 0   0      true 2 --- inspect 15     8.8   300   .75 0     
floats-cbmc-regression/float-no-simp7_true-unreach-call_true-termination.i true 2 wit inspect 8.0 8.1 370 86 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.5  2.0  250 0   0      true 2 --- inspect 16     9.1   300   .75 0     
floats-cbmc-regression/float-no-simp8_true-unreach-call.i unknown 0 --- inspect 8.3 8.3 430 140 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .46 40 0   0      error (2) 0 --- inspect .023 .025 5.6 0    0     
floats-cbmc-regression/float-rounding1_true-unreach-call.i unknown 0 --- inspect 8.3 8.3 430 100 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .44 40 0   0      error (2) 0 --- inspect .021 .023 5.6 0    0     
floats-cbmc-regression/float-to-double1_true-unreach-call.i unknown 0 --- inspect 8.2 8.2 430 100 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .46 40 0   0      error (2) 0 --- inspect .028 .029 5.6 0    0     
floats-cbmc-regression/float-to-double2_true-unreach-call_true-termination.i true 2 wit inspect 8.1 8.1 370 96 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.3  2.4  250 0   0      true 2 --- inspect 16     9.0   300   .75 0     
floats-cbmc-regression/float-zero-sum1_true-unreach-call_true-termination.i true 2 wit inspect 8.0 8.0 370 93 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.2  2.3  250 0   0      true 2 --- inspect 14     8.0   300   .71 0     
floats-cbmc-regression/float11_true-unreach-call_true-termination.i true 2 wit inspect 8.1 8.1 370 120 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.1  2.3  250 0   0      true 2 --- inspect 17     9.9   300   .75 0     
floats-cbmc-regression/float12_true-unreach-call_true-termination.i error - divine failed with signal 11 0 --- inspect 1.7 1.7 200 21 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .39 40 0   0      error (2) 0 --- inspect .027 .028 5.6 0    0     
floats-cbmc-regression/float13_true-unreach-call_true-termination.i true 2 wit inspect 8.2 8.3 370 99 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.5  2.5  250 0   0      true 2 --- inspect 14     7.9   300   .75 0     
floats-cbmc-regression/float14_true-unreach-call.i unknown 0 --- inspect 8.4 8.4 430 110 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .44 40 0   0      error (2) 0 --- inspect .024 .025 5.6 0    0     
floats-cbmc-regression/float18_true-unreach-call.i unknown 0 --- inspect 8.4 8.4 430 110 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .39 43 0   0      error (2) 0 --- inspect .020 .021 5.6 0    0     
floats-cbmc-regression/float19_true-unreach-call.i unknown 0 --- inspect 8.4 8.4 430 120 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .46 40 0   0      error (2) 0 --- inspect .027 .028 5.6 0    0     
floats-cbmc-regression/float1_true-unreach-call_true-termination.i true 2 wit inspect 8.0 8.1 370 89 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.4  2.0  250 0   0      true 2 --- inspect 13     7.7   300   .71 0     
floats-cbmc-regression/float20_true-unreach-call_true-termination.i unknown 0 --- inspect 8.2 8.2 430 97 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 40 0   0      error (2) 0 --- inspect .026 .026 5.7 0    0     
floats-cbmc-regression/float21_true-unreach-call.i unknown 0 --- inspect 8.4 8.5 430 100 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .39 40 0   0      error (2) 0 --- inspect .026 .028 5.7 0    0     
floats-cbmc-regression/float22_true-unreach-call_true-termination.i true 2 wit inspect 8.2 8.2 370 99 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.0  2.3  270 0   0      true 2 --- inspect 210     200     720   .71 0     
floats-cbmc-regression/float2_true-unreach-call_true-termination.i true 2 wit inspect 8.1 8.1 370 96 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.8  2.2  250 0   0      true 2 --- inspect 14     8.0   310   .75 0     
floats-cbmc-regression/float3_true-unreach-call_true-termination.i true 2 wit inspect 8.3 8.4 370 100 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.6  2.1  270 0   0      true 2 --- inspect 21     13     320   .71 0     
floats-cbmc-regression/float4_true-unreach-call.i unknown 0 --- inspect 8.4 8.4 430 110 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .43 41 0   0      error (2) 0 --- inspect .026 .026 5.6 0    0     
floats-cbmc-regression/float5_true-unreach-call_true-termination.i unknown 0 --- inspect 8.2 8.3 430 98 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .43 41 0   0      error (2) 0 --- inspect .021 .022 5.8 0    0     
floats-cbmc-regression/float6_true-unreach-call_true-termination.i unknown 0 --- inspect 8.4 8.4 430 93 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .81 .48 42 0   0      error (2) 0 --- inspect .027 .029 5.6 0    0     
floats-cbmc-regression/float8_true-unreach-call.i error - divine failed with exitcode 1 0 --- inspect 1.7 1.7 200 20 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .46 41 0   0      error (2) 0 --- inspect .027 .027 5.6 0    0     
floats-cbmc-regression/float_lib1_true-unreach-call.i unknown 0 --- inspect 8.3 8.3 430 94 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .45 40 0   0      error (2) 0 --- inspect .026 .027 5.6 0    0     
floats-cbmc-regression/float_lib2_true-unreach-call.i unknown 0 --- inspect 8.2 8.2 430 110 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .69 .41 41 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0     
float-benchs/cast_float_ptr_false-unreach-call_true-termination.c unknown 0 --- inspect 8.2 8.3 430 100 0   0   error (invalid witness file) 0 --- inspect .62 .39 41 0   0    error (2) 0 --- inspect .020 .021 5.6 0    0   error (invalid witness file) 0 --- inspect 1.3  .82 48 0   0      error (invalid witness file) 0 --- inspect .0043 .0068 .52 0     0      - --- inspect - --- inspect
float-benchs/cast_union_loose_false-unreach-call_true-termination.c error - unexpected error: memory error in userspace 0 --- inspect 8.5 8.5 430 110 0   0   error (invalid witness file) 0 --- inspect .68 .42 41 0   0    error (2) 0 --- inspect .026 .027 5.6 0    0   error (invalid witness file) 0 --- inspect 1.2  .76 47 0   0      error (invalid witness file) 0 --- inspect .0061 .0079 .53 0     0      - --- inspect - --- inspect
float-benchs/cast_union_tight_false-unreach-call_true-termination.c error - divine failed with signal 11 0 --- inspect 1.7 1.7 200 24 0   0   error (invalid witness file) 0 --- inspect .60 .39 41 0   0    error (2) 0 --- inspect .025 .026 5.6 0    0   error (invalid witness file) 0 --- inspect 1.2  .80 47 0   0      error (invalid witness file) 0 --- inspect .0054 .0065 .52 0     0      - --- inspect - --- inspect
float-benchs/float_int_inv_square_false-unreach-call_true-termination.c error - divine failed with signal 11 0 --- inspect 1.7 1.7 200 22 0   0   error (invalid witness file) 0 --- inspect .80 .49 41 0   0    error (2) 0 --- inspect .028 .029 5.6 0    0   error (invalid witness file) 0 --- inspect .94 .62 47 0   0      error (invalid witness file) 0 --- inspect .0037 .0066 .53 0     0      - --- inspect - --- inspect
float-benchs/inv_Newton_false-unreach-call.c unknown 0 --- inspect 8.5 8.5 430 110 0   0   error (invalid witness file) 0 --- inspect .74 .46 41 0   0    error (2) 0 --- inspect .026 .027 5.5 0    0   error (invalid witness file) 0 --- inspect 1.0  .65 47 0   0      error (invalid witness file) 0 --- inspect .0057 .0080 .54 0     0      - --- inspect - --- inspect
float-benchs/inv_Newton_false-unreach-call.c.p+cfa-reducer.c unknown 0 --- inspect 8.2 8.2 430 100 0   0   error (invalid witness file) 0 --- inspect .64 .40 40 0   0    error (2) 0 --- inspect .024 .024 5.6 0    0   error (invalid witness file) 0 --- inspect 1.1  .71 48 0   0      error (invalid witness file) 0 --- inspect .0017 .0022 .54 0     0      - --- inspect - --- inspect
float-benchs/inv_square_false-unreach-call_true-termination.c unknown 0 --- inspect 8.3 8.3 430 110 0   0   error (invalid witness file) 0 --- inspect .75 .45 40 0   0    error (2) 0 --- inspect .024 .025 5.6 0    0   error (invalid witness file) 0 --- inspect 1.2  .75 47 0   0      error (invalid witness file) 0 --- inspect .0058 .0068 .53 0     0      - --- inspect - --- inspect
float-benchs/nan_double_false-unreach-call_true-termination.c unknown 0 --- inspect 8.3 8.3 430 100 0   0   error (invalid witness file) 0 --- inspect .64 .39 42 0   0    error (2) 0 --- inspect .027 .028 5.7 0    0   error (invalid witness file) 0 --- inspect .92 .60 47 0   0      error (invalid witness file) 0 --- inspect .0059 .0076 .53 0     0      - --- inspect - --- inspect
float-benchs/nan_float_false-unreach-call_true-termination.c unknown 0 --- inspect 8.3 8.4 430 100 0   0   error (invalid witness file) 0 --- inspect .75 .47 41 0   0    error (2) 0 --- inspect .026 .027 5.6 0    0   error (invalid witness file) 0 --- inspect 1.3  .81 47 0   0      error (invalid witness file) 0 --- inspect .0070 .0094 .54 0     0      - --- inspect - --- inspect
float-benchs/sin_interpolated_index_false-unreach-call_true-termination.c unknown 0 --- inspect 8.4 8.5 430 100 0   0   error (invalid witness file) 0 --- inspect .65 .40 41 0   0    error (2) 0 --- inspect .026 .028 5.6 0    0   error (invalid witness file) 0 --- inspect .97 .61 47 0   0      error (invalid witness file) 0 --- inspect .0057 .0070 .40 0     0      - --- inspect - --- inspect
float-benchs/sqrt_poly2_false-unreach-call.c unknown 0 --- inspect 8.4 8.4 430 96 0   0   error (invalid witness file) 0 --- inspect .76 .46 41 0   0    error (2) 0 --- inspect .032 .033 5.6 0    0   error (invalid witness file) 0 --- inspect 1.2  .77 46 0   0      error (invalid witness file) 0 --- inspect .0019 .0025 .40 0     0      - --- inspect - --- inspect
float-benchs/Muller_Kahan_true-unreach-call.c.p+cfa-reducer.c true 2 wit inspect 8.1 8.1 370 130 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    1500 0   0      timeout 0 --- inspect 960     900     2400   1.6  0     
float-benchs/Muller_Kahan_true-unreach-call_true-termination.c true 2 wit inspect 8.2 8.2 370 110 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    1600 0   0      timeout 0 --- inspect 960     900     4500   .71 0     
float-benchs/Rump_double_true-unreach-call_true-termination.c true 2 wit inspect 8.1 8.1 370 100 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.3  2.4  250 0   0      true 2 --- inspect 25     20     1000   .71 0     
float-benchs/Rump_float_true-unreach-call_true-termination.c true 2 wit inspect 8.0 8.0 370 94 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.4  1.9  250 0   0      true 2 --- inspect 19     13     430   .75 0     
float-benchs/addsub_double_exact_true-unreach-call_true-termination.c true 2 wit inspect 8.2 8.2 370 100 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.3  2.4  250 0   0      true 2 --- inspect 16     9.8   300   .68 0     
float-benchs/addsub_float_exact_true-unreach-call_true-termination.c true 2 wit inspect 8.1 8.1 370 97 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.5  2.5  250 0   0      true 2 --- inspect 13     7.8   300   .75 0     
float-benchs/addsub_float_inexact_true-unreach-call_true-termination.c true 2 wit inspect 8.1 8.1 370 100 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.4  2.0  250 0   0      true 2 --- inspect 16     9.5   300   .75 0     
float-benchs/arctan_Pade_true-unreach-call_true-termination.c unknown 0 --- inspect 8.4 8.4 430 100 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .39 40 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0     
float-benchs/bary_diverge_true-unreach-call_true-termination.c unknown 0 --- inspect 8.3 8.3 430 110 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .68 .41 41 0   0      error (2) 0 --- inspect .027 .028 5.7 0    0     
float-benchs/cast_float_union_true-unreach-call.c unknown 0 --- inspect 8.4 8.4 430 130 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .84 .51 42 0   0      error (2) 0 --- inspect .027 .028 5.8 0    0     
float-benchs/cos_polynomial_true-unreach-call_true-termination.c unknown 0 --- inspect 8.4 8.4 430 100 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .45 41 0   0      error (2) 0 --- inspect .024 .025 5.6 0    0     
float-benchs/divmul_buf_diverge_true-unreach-call_true-termination.c unknown 0 --- inspect 8.3 8.3 430 130 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .67 .42 40 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0     
float-benchs/divmul_diverge_true-unreach-call_true-termination.c unknown 0 --- inspect 8.5 8.5 430 100 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 40 0   0      error (2) 0 --- inspect .023 .023 5.6 0    0     
float-benchs/drift_tenth_true-unreach-call.c.p+cfa-reducer.c true 2 wit inspect 8.1 8.1 370 110 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 29    26    410 0   0      true 2 --- inspect 270     260     640   .71 0     
float-benchs/drift_tenth_true-unreach-call_true-termination.c true 2 wit inspect 8.1 8.1 370 110 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 27    24    410 0   0      true 2 --- inspect 780     770     780   .68 0     
float-benchs/exp_loop_true-unreach-call.c unknown 0 --- inspect 8.5 8.5 430 120 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .38 40 0   0      error (2) 0 --- inspect .024 .025 5.6 0    0     
float-benchs/feedback_diverge_true-unreach-call_true-termination.c unknown 0 --- inspect 8.3 8.3 430 100 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 40 0   0      error (2) 0 --- inspect .022 .023 5.6 0    0     
float-benchs/filter1_true-unreach-call.c.p+cfa-reducer.c unknown 0 --- inspect 8.4 8.4 430 110 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .38 40 0   0      error (2) 0 --- inspect .024 .026 5.6 0    0     
float-benchs/filter1_true-unreach-call.c.v+lhb-reducer.c unknown 0 --- inspect 8.4 8.5 430 100 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .46 40 0   0      error (2) 0 --- inspect .022 .022 5.6 0    0     
float-benchs/filter1_true-unreach-call.c.v+nlh-reducer.c unknown 0 --- inspect 8.2 8.2 430 100 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .57 .35 40 0   0      error (2) 0 --- inspect .025 .026 5.6 0    0     
float-benchs/filter1_true-unreach-call_true-termination.c unknown 0 --- inspect 8.5 8.5 430 100 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .46 40 0   0      error (2) 0 --- inspect .023 .025 5.7 0    0     
float-benchs/filter2_alt_true-unreach-call.c unknown 0 --- inspect 8.3 8.3 430 93 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 40 0   0      error (2) 0 --- inspect .027 .027 5.6 0    0     
float-benchs/filter2_iterated_true-unreach-call.c true 2 wit inspect 8.1 8.1 370 97 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    1600 0   0      error (7) 0 --- inspect 46     40     2200   .71 0     
float-benchs/filter2_reinit_true-unreach-call_true-termination.c unknown 0 --- inspect 8.4 8.4 430 100 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .67 .41 41 0   0      error (2) 0 --- inspect .024 .025 5.6 0    0     
float-benchs/filter2_set_true-unreach-call_true-termination.c unknown 0 --- inspect 8.3 8.3 430 92 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .68 .41 40 0   0      error (2) 0 --- inspect .021 .023 5.7 0    0     
float-benchs/filter2_true-unreach-call_true-termination.c unknown 0 --- inspect 8.4 8.4 430 110 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .67 .40 40 0   0      error (2) 0 --- inspect .026 .034 5.6 0    0     
float-benchs/filter_iir_true-unreach-call.c unknown 0 --- inspect 8.2 8.3 430 100 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .67 .43 40 0   0      error (2) 0 --- inspect .027 .027 5.7 0    0     
float-benchs/float_double_true-unreach-call_true-termination.c true 2 wit inspect 8.1 8.1 370 110 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.2  2.3  250 0   0      true 2 --- inspect 13     8.2   300   .68 0     
float-benchs/image_filter_true-unreach-call.c unknown 0 --- inspect 8.4 8.4 430 120 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .41 41 0   0      error (2) 0 --- inspect .026 .027 5.6 0    0     
float-benchs/interpolation2_true-unreach-call.c.p+cfa-reducer.c unknown 0 --- inspect 8.1 8.1 430 110 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .44 41 0   0      error (2) 0 --- inspect .027 .028 5.7 0    0     
float-benchs/interpolation2_true-unreach-call.c.v+cfa-reducer.c unknown 0 --- inspect 8.3 8.3 430 100 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 40 0   0      error (2) 0 --- inspect .022 .023 5.6 0    0     
float-benchs/interpolation2_true-unreach-call.c.v+nlh-reducer.c unknown 0 --- inspect 8.2 8.2 430 100 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .43 40 0   0      error (2) 0 --- inspect .026 .027 5.7 0    0     
float-benchs/interpolation2_true-unreach-call_true-termination.c unknown 0 --- inspect 8.2 8.3 430 130 0   3.2 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .45 43 0   0      error (2) 0 --- inspect .020 .021 5.6 0    0     
float-benchs/interpolation_true-unreach-call.c.p+cfa-reducer.c unknown 0 --- inspect 8.5 8.5 430 120 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .37 43 0   0      error (2) 0 --- inspect .025 .025 5.5 0    0     
float-benchs/interpolation_true-unreach-call.c.v+cfa-reducer.c unknown 0 --- inspect 8.5 8.5 430 110 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .46 41 0   0      error (2) 0 --- inspect .027 .028 5.6 0    0     
float-benchs/interpolation_true-unreach-call.c.v+nlh-reducer.c unknown 0 --- inspect 8.4 8.4 430 90 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .67 .42 40 0   0      error (2) 0 --- inspect .021 .023 5.6 0    0     
float-benchs/interpolation_true-unreach-call_true-termination.c unknown 0 --- inspect 8.4 8.4 430 94 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 42 0   0      error (2) 0 --- inspect .022 .024 5.7 0    0     
float-benchs/inv_Newton_true-unreach-call.c unknown 0 --- inspect 8.4 8.4 430 100 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .46 41 0   0      error (2) 0 --- inspect .024 .025 5.6 0    0     
float-benchs/inv_sqrt_Quake_true-unreach-call.c.v+cfa-reducer.c unknown 0 --- inspect 8.3 8.3 430 120 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .46 41 0   0      error (2) 0 --- inspect .021 .022 5.7 0    0     
float-benchs/inv_sqrt_Quake_true-unreach-call_true-termination.c unknown 0 --- inspect 8.4 8.4 430 100 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .46 41 0   0      error (2) 0 --- inspect .027 .027 5.6 0    0     
float-benchs/inv_square_int_true-unreach-call_true-termination.c error - divine failed with signal 11 0 --- inspect 1.8 1.8 200 22 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .39 40 0   0      error (2) 0 --- inspect .027 .028 5.7 0    0     
float-benchs/inv_square_true-unreach-call_true-termination.c unknown 0 --- inspect 8.3 8.3 430 110 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .38 42 0   0      error (2) 0 --- inspect .022 .024 5.7 0    0     
float-benchs/loop_true-unreach-call.c true 2 wit inspect 450   120   2300 4300 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    2000 0   0      true 2 --- inspect 170     160     400   .71 0     
float-benchs/mea8000_true-unreach-call.c error - divine failed with exitcode 1 0 --- inspect 1.3 1.3 170 17 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .44 42 0   0      error (2) 0 --- inspect .021 .023 5.7 0    0     
float-benchs/nan_double_range_true-unreach-call_true-termination.c unknown 0 --- inspect 8.4 8.4 430 110 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 ---