Tool 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-05 05:46:16 CET 2018-12-06 09:44:44 CET 2018-12-06 10:50:29 CET 2018-12-06 10:57:45 CET 2018-12-12 19:32:16 CET 2018-12-06 08:37:23 CET 2018-12-06 09:52:34 CET
Run set cpa-seq.sv-comp19_prop-reachsafety.ReachSafety-Floats cpa-seq-validate-violation-witnesses-cpa-seq.sv-comp19_prop-reachsafety.ReachSafety-Floats uautomizer-validate-violation-witnesses-cpa-seq.sv-comp19_prop-reachsafety.ReachSafety-Floats cpa-witness2test-validate-violation-witnesses-cpa-seq.sv-comp19_prop-reachsafety.ReachSafety-Floats fshell-witness2test-validate-violation-witnesses-cpa-seq.sv-comp19_prop-reachsafety.ReachSafety-Floats cpa-seq-validate-correctness-witnesses-cpa-seq.sv-comp19_prop-reachsafety.ReachSafety-Floats uautomizer-validate-correctness-witnesses-cpa-seq.sv-comp19_prop-reachsafety.ReachSafety-Floats
Options -svcomp19 -heap 10000M -benchmark -timelimit 900s -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/cpa-seq.2018-12-05_0546.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cpa-seq.2018-12-05_0546.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/cpa-seq.2018-12-05_0546.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/cpa-seq.2018-12-05_0546.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/cpa-seq.2018-12-05_0546.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cpa-seq.2018-12-05_0546.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 false(unreach-call) 1 wit inspect 74   72   450 650 0      0     false(unreach-call) 1 wit inspect 53    51    350 0   0   false(unreach-call) 1 --- inspect 33     28     680   .68 0   false(unreach-call) 1 --- inspect 3.8  2.2  250 0   0    false(unreach-call) 1 --- inspect .58   .58   20    .053 0      - --- inspect - --- inspect
floats-cdfpl/newton_1_5_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 57   56   440 410 0      0     false(unreach-call) 1 wit inspect 12    10    350 0   0   timeout 0 --- inspect 97     91     700   1.1  0   false(unreach-call) 1 --- inspect 3.8  2.2  250 0   0    false(unreach-call) 1 --- inspect .58   .58   20    .053 0      - --- inspect - --- inspect
floats-cdfpl/newton_1_6_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 44   43   450 360 0      0     false(unreach-call) 1 wit inspect 39    37    350 0   0   false(unreach-call) 1 --- inspect 68     63     690   .68 0   false(unreach-call) 1 --- inspect 3.9  2.3  250 0   0    false(unreach-call) 1 --- inspect .57   .57   20    .053 0      - --- inspect - --- inspect
floats-cdfpl/newton_1_7_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 22   20   440 210 0      0     false(unreach-call) 1 wit inspect 11    9.4  350 0   0   timeout 0 --- inspect 97     92     700   .68 0   false(unreach-call) 1 --- inspect 3.9  2.3  250 0   0    false(unreach-call) 1 --- inspect .60   .60   20    .053 0      - --- inspect - --- inspect
floats-cdfpl/newton_1_8_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 16   14   440 130 0      0     false(unreach-call) 1 wit inspect 10    8.6  350 0   0   false(unreach-call) 1 --- inspect 27     22     680   .71 0   false(unreach-call) 1 --- inspect 3.5  2.1  250 0   0    false(unreach-call) 1 --- inspect .58   .58   20    .053 0      - --- inspect - --- inspect
floats-cdfpl/newton_2_6_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 140   140   610 1100 0      0     timeout 0 wit inspect 92    90    450 0   0   timeout 0 --- inspect 97     92     820   .78 0   false(unreach-call) 1 --- inspect 3.9  2.3  250 0   0    false(unreach-call) 1 --- inspect .58   .58   20    .053 0      - --- inspect - --- inspect
floats-cdfpl/newton_2_7_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 84   83   600 590 0      0     false(unreach-call) 1 wit inspect 69    68    450 0   0   timeout 0 --- inspect 97     91     800   .72 0   false(unreach-call) 1 --- inspect 3.6  2.1  250 0   0    false(unreach-call) 1 --- inspect .58   .58   20    .053 0      - --- inspect - --- inspect
floats-cdfpl/newton_2_8_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 43   41   610 310 0      0     false(unreach-call) 1 wit inspect 21    19    450 0   0   false(unreach-call) 1 --- inspect 37     31     820   .71 0   false(unreach-call) 1 --- inspect 3.8  2.2  250 0   0    false(unreach-call) 1 --- inspect .58   .59   20    .053 0      - --- inspect - --- inspect
floats-cdfpl/newton_3_6_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 300   300   780 1900 0      0     timeout 0 wit inspect 92    89    550 0   0   timeout 0 --- inspect 97     90     890   .72 0   false(unreach-call) 1 --- inspect 3.9  2.3  250 0   0    false(unreach-call) 1 --- inspect .58   .58   20    .053 0      - --- inspect - --- inspect
floats-cdfpl/newton_3_7_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 200   200   780 1300 0      0     false(unreach-call) 1 wit inspect 74    72    550 0   0   false(unreach-call) 1 --- inspect 53     47     920   .71 0   false(unreach-call) 1 --- inspect 3.9  2.3  250 0   0    false(unreach-call) 1 --- inspect .61   .60   20    .053 0      - --- inspect - --- inspect
floats-cdfpl/newton_3_8_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 170   170   780 980 0      0     timeout 0 wit inspect 92    90    550 0   0   timeout 0 --- inspect 97     91     930   .75 0   false(unreach-call) 1 --- inspect 4.0  2.3  250 0   0    false(unreach-call) 1 --- inspect .61   .61   20    .053 0      - --- inspect - --- inspect
floats-cdfpl/sine_1_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 9.0 7.2 380 110 0      0     false(unreach-call) 1 wit inspect 12    9.7  310 0   0   timeout 0 --- inspect 97     92     610   1.1  0   false(unreach-call) 1 --- inspect 3.7  2.1  250 0   0    false(unreach-call) 1 --- inspect .58   .58   20    .049 0      - --- inspect - --- inspect
floats-cdfpl/sine_2_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 45   44   410 390 0      0     false(unreach-call) 1 wit inspect 58    56    330 0   0   timeout 0 --- inspect 97     91     570   .68 0   false(unreach-call) 1 --- inspect 3.6  2.1  250 0   0    false(unreach-call) 1 --- inspect .57   .57   20    .049 0      - --- inspect - --- inspect
floats-cdfpl/sine_3_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 270   270   540 2700 0      0     false(unreach-call) 1 wit inspect 8.9  7.2  300 0   0   timeout 0 --- inspect 97     91     610   .73 0   false(unreach-call) 1 --- inspect 3.8  2.2  250 0   0    false(unreach-call) 1 --- inspect .58   .58   20    .049 0      - --- inspect - --- inspect
floats-cdfpl/square_1_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 18   16   400 150 0      0     false(unreach-call) 1 wit inspect 11    8.9  310 0   0   false(unreach-call) 1 --- inspect 87     82     450   .71 0   false(unreach-call) 1 --- inspect 3.7  2.1  240 0   0    false(unreach-call) 1 --- inspect .60   .60   20    .049 0      - --- inspect - --- inspect
floats-cdfpl/square_2_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 180   180   590 1800 0      0     false(unreach-call) 1 wit inspect 52    50    340 0   0   timeout (false(unreach-call)) 0 --- inspect 96     91     450   .68 0   false(unreach-call) 1 --- inspect 3.7  2.2  250 0   0    false(unreach-call) 1 --- inspect .57   .57   20    .049 0      - --- inspect - --- inspect
floats-cdfpl/square_3_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 62   60   430 560 0      0     false(unreach-call) 1 wit inspect 21    19    330 0   0   timeout 0 --- inspect 97     91     460   1.1  0   false(unreach-call) 1 --- inspect 3.6  2.1  250 0   0    false(unreach-call) 1 --- inspect .58   .58   20    .049 .0041 - --- inspect - --- inspect
floats-cdfpl/newton_1_1_true-unreach-call_true-termination.i timeout 0 wit inspect 900   900   620 5800 0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    580 0   0   timeout 0 --- inspect 960     950     980   .72 0  
floats-cdfpl/newton_1_2_true-unreach-call_true-termination.i timeout 0 wit inspect 900   900   600 6700 0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    580 0   0   timeout 0 --- inspect 960     950     780   .72 0  
floats-cdfpl/newton_1_3_true-unreach-call_true-termination.i timeout 0 wit inspect 900   900   610 6100 0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    580 0   0   timeout 0 --- inspect 960     950     970   .89 0  
floats-cdfpl/newton_2_1_true-unreach-call_true-termination.i timeout 0 wit inspect 900   900   540 7300 0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    550 0   0   timeout 0 --- inspect 960     950     890   .74 0  
floats-cdfpl/newton_2_2_true-unreach-call_true-termination.i timeout 0 wit inspect 900   900   860 8000 0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    830 0   0   timeout 0 --- inspect 960     950     970   2.1  0  
floats-cdfpl/newton_2_3_true-unreach-call_true-termination.i timeout 0 wit inspect 900   900   550 6300 0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    520 0   0   timeout 0 --- inspect 960     950     1000   .80 0  
floats-cdfpl/newton_2_4_true-unreach-call_true-termination.i timeout 0 wit inspect 900   900   620 8600 0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    580 0   0   timeout 0 --- inspect 960     950     1100   1.3  0  
floats-cdfpl/newton_2_5_true-unreach-call_true-termination.i timeout 0 wit inspect 900   900   610 8500 0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    560 0   0   timeout 0 --- inspect 960     950     900   1.1  0  
floats-cdfpl/newton_3_1_true-unreach-call_true-termination.i timeout 0 wit inspect 900   900   610 6000 0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    590 0   0   timeout 0 --- inspect 960     950     1100   .72 0  
floats-cdfpl/newton_3_2_true-unreach-call_true-termination.i timeout 0 wit inspect 900   900   570 6900 0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    570 0   0   timeout 0 --- inspect 960     950     1100   2.5  0  
floats-cdfpl/newton_3_3_true-unreach-call_true-termination.i timeout 0 wit inspect 900   900   700 6500 0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    680 0   0   timeout 0 --- inspect 960     950     1100   .71 0  
floats-cdfpl/newton_3_4_true-unreach-call_true-termination.i timeout 0 wit inspect 900   900   710 7200 0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    700 0   0   timeout 0 --- inspect 960     950     1000   .97 0  
floats-cdfpl/newton_3_5_true-unreach-call_true-termination.i timeout 0 wit inspect 900   900   570 7400 0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    560 0   0   timeout 0 --- inspect 960     950     1000   1.6  0  
floats-cdfpl/sine_4_true-unreach-call_true-termination.i timeout 0 wit inspect 900   900   500 5300 0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    500 0   0   timeout 0 --- inspect 960     950     790   .72 0  
floats-cdfpl/sine_5_true-unreach-call_true-termination.i timeout 0 wit inspect 900   900   500 6700 0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    490 0   0   timeout 0 --- inspect 960     950     830   .72 0  
floats-cdfpl/sine_6_true-unreach-call_true-termination.i timeout 0 wit inspect 900   900   650 7600 0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    650 0   0   timeout 0 --- inspect 960     950     830   2.0  0  
floats-cdfpl/sine_7_true-unreach-call_true-termination.i true 2 wit inspect 590   590   590 4800 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 760    760    590 0   0   timeout 0 --- inspect 960     950     830   1.6  0  
floats-cdfpl/sine_8_true-unreach-call_true-termination.i true 2 wit inspect 460   460   550 4100 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 540    540    540 0   0   timeout 0 --- inspect 960     950     820   .75 0  
floats-cdfpl/square_4_true-unreach-call_true-termination.i true 2 wit inspect 540   530   570 3900 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 660    650    570 0   0   timeout (true) 0 --- inspect 910     900     790   .71 0  
floats-cdfpl/square_5_true-unreach-call_true-termination.i true 2 wit inspect 430   430   510 2900 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 490    490    510 0   0   timeout 0 --- inspect 960     950     760   1.7  0  
floats-cdfpl/square_6_true-unreach-call_true-termination.i true 2 wit inspect 220   220   500 1600 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 280    280    500 0   0   timeout 0 --- inspect 960     950     760   .72 0  
floats-cdfpl/square_7_true-unreach-call_true-termination.i true 2 wit inspect 760   750   490 6700 0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    480 0   0   true 2 --- inspect 650     640     790   .71 0  
floats-cdfpl/square_8_true-unreach-call_true-termination.i true 2 wit inspect 56   54   370 500 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 73    71    360 0   0   true 2 --- inspect 82     76     610   .71 0  
floats-cbmc-regression/float-div1_true-unreach-call.i true 2 wit inspect 4.9 2.3 350 41 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 6.6  4.0  320 0   0   true 2 --- inspect 48     40     950   .68 0  
floats-cbmc-regression/float-flags-simp1_true-unreach-call.i true 2 wit inspect 10   6.8 800 110 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 13    10    780 0   0   error (7) 0 --- inspect 12     7.5   280   .75 0  
floats-cbmc-regression/float-no-simp1_true-unreach-call_true-termination.i true 2 wit inspect 2.8 1.3 250 27 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.3  1.9  250 0   0   true 2 --- inspect 15     9.2   290   .71 0  
floats-cbmc-regression/float-no-simp2_true-unreach-call.i true 2 wit inspect 13   10   330 120 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 27    24    300 0   0   true 2 --- inspect 52     44     550   .71 0  
floats-cbmc-regression/float-no-simp3_true-unreach-call_true-termination.i true 2 wit inspect 2.9 1.3 250 30 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.2  2.4  250 0   0   true 2 --- inspect 12     6.9   300   .75 0  
floats-cbmc-regression/float-no-simp4_true-unreach-call.i true 2 wit inspect 4.4 1.7 300 42 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.7  3.2  260 0   0   true 2 --- inspect 19     11     440   .75 0  
floats-cbmc-regression/float-no-simp6_true-unreach-call_true-termination.i true 2 wit inspect 3.0 1.3 250 30 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.2  2.3  250 0   0   true 2 --- inspect 14     9.1   300   .75 0  
floats-cbmc-regression/float-no-simp7_true-unreach-call_true-termination.i true 2 wit inspect 2.9 1.3 250 26 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.3  1.9  250 0   0   true 2 --- inspect 13     7.5   300   .75 0  
floats-cbmc-regression/float-no-simp8_true-unreach-call.i true 2 wit inspect 4.1 1.6 290 37 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.6  2.5  260 0   0   error (7) 0 --- inspect 14     8.1   290   .71 0  
floats-cbmc-regression/float-rounding1_true-unreach-call.i error 0 wit inspect 4.0 1.6 270 33 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error 0 wit inspect 5.5  3.1  260 0   0   unknown 0 --- inspect 7.3   4.4   280   .66 0  
floats-cbmc-regression/float-to-double1_true-unreach-call.i true 2 wit inspect 4.0 1.6 290 39 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.8  2.7  260 0   0   true 2 --- inspect 35     28     460   .71 0  
floats-cbmc-regression/float-to-double2_true-unreach-call_true-termination.i true 2 wit inspect 2.7 1.2 250 25 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.6  2.6  250 0   0   true 2 --- inspect 13     8.0   290   .71 0  
floats-cbmc-regression/float-zero-sum1_true-unreach-call_true-termination.i true 2 wit inspect 3.0 1.3 250 27 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.7  2.0  250 0   0   true 2 --- inspect 13     7.6   300   .68 0  
floats-cbmc-regression/float11_true-unreach-call_true-termination.i true 2 wit inspect 2.9 1.3 260 28 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.8  2.6  250 0   0   true 2 --- inspect 13     8.5   300   .75 0  
floats-cbmc-regression/float12_true-unreach-call_true-termination.i true 2 wit inspect 2.8 1.3 260 27 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.4  1.9  250 0   0   true 2 --- inspect 18     13     300   .71 0  
floats-cbmc-regression/float13_true-unreach-call_true-termination.i true 2 wit inspect 3.0 1.3 250 26 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.7  2.0  250 0   0   true 2 --- inspect 17     10     310   .75 0  
floats-cbmc-regression/float14_true-unreach-call.i true 2 wit inspect 4.2 1.6 280 43 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.5  2.5  260 0   0   true 2 --- inspect 15     9.1   390   .68 0  
floats-cbmc-regression/float18_true-unreach-call.i error 0 --- inspect 4.0 1.5 280 33 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .38 41 0   0   error (2) 0 --- inspect .020 .022 5.7 0    0  
floats-cbmc-regression/float19_true-unreach-call.i true 2 wit inspect 4.2 1.6 290 40 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.6  2.5  260 0   0   true 2 --- inspect 19     11     390   .71 0  
floats-cbmc-regression/float1_true-unreach-call_true-termination.i true 2 wit inspect 2.9 1.3 250 28 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.4  1.9  250 0   0   true 2 --- inspect 14     7.8   290   .75 0  
floats-cbmc-regression/float20_true-unreach-call_true-termination.i true 2 wit inspect 3.0 1.3 260 30 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.4  2.0  250 0   0   true 2 --- inspect 21     15     380   .68 0  
floats-cbmc-regression/float21_true-unreach-call.i true 2 wit inspect 7.8 5.3 330 83 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 8.3  6.2  300 0   0   true 2 --- inspect 78     71     590   .71 0  
floats-cbmc-regression/float22_true-unreach-call_true-termination.i true 2 wit inspect 3.2 1.5 270 29 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.7  2.1  270 0   0   true 2 --- inspect 200     190     760   .71 0  
floats-cbmc-regression/float2_true-unreach-call_true-termination.i true 2 wit inspect 2.9 1.3 260 30 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.3  1.9  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 3.0 1.4 280 29 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.5  2.5  270 0   0   true 2 --- inspect 18     12     320   .75 0  
floats-cbmc-regression/float4_true-unreach-call.i true 2 wit inspect 51   49   360 670 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 89    87    330 0   0   true 2 --- inspect 93     85     580   .71 0  
floats-cbmc-regression/float5_true-unreach-call_true-termination.i true 2 wit inspect 3.1 1.4 260 29 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.8  2.1  260 0   0   true 2 --- inspect 26     21     300   .68 0  
floats-cbmc-regression/float6_true-unreach-call_true-termination.i true 2 wit inspect 3.1 1.4 260 33 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.1  2.3  250 0   0   true 2 --- inspect 16     9.3   300   .75 0  
floats-cbmc-regression/float8_true-unreach-call.i true 2 wit inspect 7.0 4.5 300 79 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 10    7.4  270 0   0   true 2 --- inspect 16     9.2   390   .71 0  
floats-cbmc-regression/float_lib1_true-unreach-call.i true 2 wit inspect 4.2 1.7 260 40 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.7  3.0  260 0   0   error (7) 0 --- inspect 12     6.4   280   .71 0  
floats-cbmc-regression/float_lib2_true-unreach-call.i true 2 wit inspect 4.2 1.6 290 43 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.3  2.4  260 0   0   true 2 --- inspect 17     9.5   420   .75 0  
float-benchs/cast_float_ptr_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.1 1.4 270 29 0      0     false(unreach-call) 1 wit inspect 4.1  2.3  260 0   0   false(unreach-call) 1 --- inspect 16     9.5   310   .71 0   true -32 --- inspect 3.8  2.2  250 0   0    true -32 --- inspect .59   .59   20    .057 0      - --- inspect - --- inspect
float-benchs/cast_union_loose_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.3 1.5 280 35 0      0     false(unreach-call) 1 wit inspect 4.9  2.8  270 0   0   false(unreach-call) 1 --- inspect 14     8.3   310   .75 0   true -32 --- inspect 3.8  2.2  250 0   0    true -32 --- inspect .61   .61   20    .057 0      - --- inspect - --- inspect
float-benchs/cast_union_tight_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.2 1.5 290 29 0      0     false(unreach-call) 1 wit inspect 5.2  2.9  270 0   0   false(unreach-call) 1 --- inspect 14     8.2   310   .71 0   true -32 --- inspect 3.7  2.1  250 0   0    true -32 --- inspect .57   .57   20    .049 0      - --- inspect - --- inspect
float-benchs/float_int_inv_square_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.1 1.4 280 32 0      0     false(unreach-call) 1 wit inspect 4.1  2.3  260 0   0   false(unreach-call) 1 --- inspect 14     8.4   300   .71 0   false(unreach-call) 1 --- inspect 3.7  2.2  250 0   0    false(unreach-call) 1 --- inspect .60   .60   20    .057 0      - --- inspect - --- inspect
float-benchs/inv_Newton_false-unreach-call.c false(unreach-call) 1 wit inspect 5.4 3.3 350 60 .012  0     false(unreach-call) 1 wit inspect 6.6  4.8  340 0   0   timeout 0 --- inspect 97     90     770   1.0  0   unknown 0 --- inspect 4.0  2.3  240 0   0    true -32 --- inspect .61   .61   20    .057 .0041 - --- inspect - --- inspect
float-benchs/inv_Newton_false-unreach-call.c.p+cfa-reducer.c false(unreach-call) 1 wit inspect 4.7 2.5 350 45 .012  0     false(unreach-call) 1 wit inspect 5.7  3.9  340 0   0   timeout 0 --- inspect 97     89     770   .84 0   unknown 0 --- inspect 3.8  2.2  250 0   0    true -32 --- inspect .59   .59   21    .057 0      - --- inspect - --- inspect
float-benchs/inv_square_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.1 1.5 280 33 0      0     false(unreach-call) 1 wit inspect 4.3  2.4  260 0   0   false(unreach-call) 1 --- inspect 13     8.3   300   .71 0   false(unreach-call) 1 --- inspect 3.8  2.2  250 0   0    false(unreach-call) 1 --- inspect .62   .62   20    .057 0      - --- inspect - --- inspect
float-benchs/nan_double_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.9 1.3 260 27 0      0     false(unreach-call) 1 wit inspect 4.3  2.4  260 0   0   false(unreach-call) 1 --- inspect 12     7.4   300   .68 0   unknown 0 --- inspect 3.5  2.1  250 0   0    true -32 --- inspect .57   .57   20    .045 0      - --- inspect - --- inspect
float-benchs/nan_float_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.8 1.3 270 26 0      0     false(unreach-call) 1 wit inspect 4.0  2.2  260 0   0   false(unreach-call) 1 --- inspect 13     7.1   300   .71 0   unknown 0 --- inspect 3.8  2.2  250 0   0    true -32 --- inspect .59   .59   20    .045 0      - --- inspect - --- inspect
float-benchs/sin_interpolated_index_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 5.5 2.3 420 51 0      0     false(unreach-call) 1 wit inspect 7.3  4.5  310 0   0   false(unreach-call) 1 --- inspect 33     22     1000   .75 0   false(unreach-call) 1 --- inspect 4.3  2.5  250 0   0    false(unreach-call) 1 --- inspect .63   .63   20    .086 .020  - --- inspect - --- inspect
float-benchs/sqrt_poly2_false-unreach-call.c false(unreach-call) 1 wit inspect 15   13   570 160 0      0     false(unreach-call) 1 wit inspect 8.3  5.9  390 0   0   false(unreach-call) 1 --- inspect 20     14     590   .71 0   false(unreach-call) 1 --- inspect 4.1  2.3  250 0   0    false(unreach-call) 1 --- inspect .60   .60   20    .066 0      - --- inspect - --- inspect
float-benchs/Muller_Kahan_true-unreach-call.c.p+cfa-reducer.c true 2 wit inspect 3.7 1.4 260 31 0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    1500 0   0   timeout 0 --- inspect 960     910     2400   1.7  0  
float-benchs/Muller_Kahan_true-unreach-call_true-termination.c true 2 wit inspect 3.8 1.4 260 39 0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    2400 0   0   timeout 0 --- inspect 960     890     3200   .69 0  
float-benchs/Rump_double_true-unreach-call_true-termination.c true 2 wit inspect 2.9 1.3 250 25 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.9  2.2  250 0   0   true 2 --- inspect 29     23     990   .75 0  
float-benchs/Rump_float_true-unreach-call_true-termination.c true 2 wit inspect 2.9 1.3 260 25 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.4  1.9  250 0   0   true 2 --- inspect 16     10     430   .71 0  
float-benchs/addsub_double_exact_true-unreach-call_true-termination.c true 2 wit inspect 2.8 1.3 260 28 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.6  2.1  250 0   0   true 2 --- inspect 13     7.8   300   .71 0  
float-benchs/addsub_float_exact_true-unreach-call_true-termination.c true 2 wit inspect 2.8 1.3 250 24 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.5  2.0  250 0   0   true 2 --- inspect 14     7.8   300   .75 0  
float-benchs/addsub_float_inexact_true-unreach-call_true-termination.c true 2 wit inspect 2.9 1.3 260 27 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.9  2.2  250 0   0   true 2 --- inspect 13     7.5   300   .71 0  
float-benchs/arctan_Pade_true-unreach-call_true-termination.c true 2 wit inspect 22   20   500 260 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 36    34    500 0   0   error (7) 0 --- inspect 140     130     2600   .71 0  
float-benchs/bary_diverge_true-unreach-call_true-termination.c timeout 0 wit inspect 910   450   3100 9000 .025  0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    1200 0   0   timeout 0 --- inspect 960     950     2700   .72 0  
float-benchs/cast_float_union_true-unreach-call.c true 2 wit inspect 3.0 1.3 250 28 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.5  1.9  250 0   0   true 2 --- inspect 6.7   4.2   300   .66 0  
float-benchs/cos_polynomial_true-unreach-call_true-termination.c timeout 0 wit inspect 900   900   1500 9000 0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    1200 0   0   timeout 0 --- inspect 960     950     3000   1.6  0  
float-benchs/divmul_buf_diverge_true-unreach-call_true-termination.c timeout 0 wit inspect 960   890   4500 6900 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .41 43 0   0   error (invalid witness file) 0 --- inspect 5.2   2.9   270   .65 0  
float-benchs/divmul_diverge_true-unreach-call_true-termination.c timeout 0 wit inspect 970   890   4300 8200 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 42 0   0   error (invalid witness file) 0 --- inspect 5.1   2.8   260   .65 0  
float-benchs/drift_tenth_true-unreach-call.c.p+cfa-reducer.c true 2 wit inspect 2.8 1.2 240 28 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 28    26    430 0   0   true 2 --- inspect 420     410     690   .68 0  
float-benchs/drift_tenth_true-unreach-call_true-termination.c true 2 wit inspect 2.7 1.2 250 28 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 32    28    420 0   0   true 2 --- inspect 270     260     670   .71 0  
float-benchs/exp_loop_true-unreach-call.c true 2 wit inspect 840   820   8700 7900 .025  0     - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 580    560    7000 0   0   timeout 0 --- inspect 960     940     1300   1.8  0  
float-benchs/feedback_diverge_true-unreach-call_true-termination.c timeout 0 wit inspect 970   890   4800 8100 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .38 43 0   0   error (invalid witness file) 0 --- inspect 5.8   3.1   270   .61 0  
float-benchs/filter1_true-unreach-call.c.p+cfa-reducer.c true 2 wit inspect 20   5.8 890 170 .025  0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 35    26    1700 0   0   timeout 0 --- inspect 960     950     1000   .80 0  
float-benchs/filter1_true-unreach-call.c.v+lhb-reducer.c true 2 wit inspect 31   8.7 1100 230 .025  0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 250    230    2500 0   0   true 2 --- inspect 540     530     860   .71 0  
float-benchs/filter1_true-unreach-call.c.v+nlh-reducer.c true 2 wit inspect 28   6.8 900 220 .025  0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 65    56    2000 0   0   true 2 --- inspect 490     480     890   .71 0  
float-benchs/filter1_true-unreach-call_true-termination.c true 2 wit inspect 20   5.7 880 170 .016  0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 8.7  6.4  420 0   0   timeout 0 --- inspect 960     940     1600   .72 0  
float-benchs/filter2_alt_true-unreach-call.c timeout 0 wit inspect 900   900   1100 10000 .025  0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    1000 0   0   timeout 0 --- inspect 960     950     1100   .75 0  
float-benchs/filter2_iterated_true-unreach-call.c timeout 0 wit inspect 900   890   2200 10000 .033  0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    1600 0   0   error (7) 0 --- inspect 46     39     2200   .68 0  
float-benchs/filter2_reinit_true-unreach-call_true-termination.c timeout 0 wit inspect 960   480   3300 10000 .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .40 43 0   0   error (invalid witness file) 0 --- inspect 5.1   3.2   260   .65 0  
float-benchs/filter2_set_true-unreach-call_true-termination.c timeout 0 wit inspect 960   490   3700 12000 .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .38 42 0   0   error (invalid witness file) 0 --- inspect 5.5   2.9   270   .61 0  
float-benchs/filter2_true-unreach-call_true-termination.c timeout 0 wit inspect 960   480   2900 11000 .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .40 43 0   0   error (invalid witness file) 0 --- inspect 5.4   2.9   260   .65 0  
float-benchs/filter_iir_true-unreach-call.c true 2 wit inspect 3.7 1.3 300 29 0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    3400 0   0   timeout 0 --- inspect 960     950     3000   .75 0  
float-benchs/float_double_true-unreach-call_true-termination.c true 2 wit inspect 2.8 1.3 250 27 0      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  
float-benchs/image_filter_true-unreach-call.c out of memory 0 --- inspect 330   310   15000 3900 2.1    0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .70 .42 40 0   0   error (2) 0 --- inspect .022 .024 5.6 0    0  
float-benchs/interpolation2_true-unreach-call.c.p+cfa-reducer.c true 2 wit inspect 24   19   660 260 .016  0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 520    520    630 0   0   timeout 0 --- inspect 960     950     1500   1.5  0  
float-benchs/interpolation2_true-unreach-call.c.v+cfa-reducer.c true 2 wit inspect 270   260   790 3500 .016  0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 86    83    620 0   0   timeout 0 --- inspect 960     950     1500   .72 0  
float-benchs/interpolation2_true-unreach-call.c.v+nlh-reducer.c true 2 wit inspect 25   19   490 280 .016  0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 54    51    580 0   0   timeout 0 --- inspect 960     950     1600   .72 0  
float-benchs/interpolation2_true-unreach-call_true-termination.c true 2 wit inspect 23   18   620 240 .016  0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 58    56    590 0   0   timeout 0 --- inspect 960     950     1600   .72 0  
float-benchs/interpolation_true-unreach-call.c.p+cfa-reducer.c true 2 wit inspect 16   10   610 140 .016  0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 33    30    510 0   0   timeout 0 --- inspect 960     950     1500   1.9  0  
float-benchs/interpolation_true-unreach-call.c.v+cfa-reducer.c true 2 wit inspect 23   18   580 250 .016  0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 120    120    510 0   0   timeout 0 --- inspect 960     950     1400   .74 0  
float-benchs/interpolation_true-unreach-call.c.v+nlh-reducer.c true 2 wit inspect 19   13   460 250 .016  .029 - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 43    40    480 0   0   timeout 0 --- inspect 960     950     1400   1.6  0  
float-benchs/interpolation_true-unreach-call_true-termination.c true 2 wit inspect 14   9.4 550 140 .016  0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 33    29    520 0   0   timeout 0 --- inspect 960     950     1900   1.1  0  
float-benchs/inv_Newton_true-unreach-call.c timeout 0 wit inspect 900   900   2500 8600 .025  0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    1300 0   0   true 2 --- inspect 90     82     620   .71 0  
float-benchs/inv_sqrt_Quake_true-unreach-call.c.v+cfa-reducer.c true 2 wit inspect 4.6 2.9 310 43 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 6.4  4.7  320 0   0   true 2 --- inspect 88     81     1200   .68 0  
float-benchs/inv_sqrt_Quake_true-unreach-call_true-termination.c true 2 wit inspect 3.4 1.8 280 33 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.2  3.2  280 0   0   true 2 ---