Tool PeSCo 1.7-svn b8d6131600+ 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* [apollon004; apollon069; apollon137; apollon154] [apollon004; apollon006; apollon021; apollon061; apollon109; apollon155] 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 12:44:04 CET 2018-12-08 07:39:30 CET 2018-12-08 12:16:42 CET 2018-12-08 13:32:07 CET 2018-12-12 20:37:42 CET 2018-12-08 05:07:50 CET 2018-12-08 09:11:31 CET
Run set pesco.sv-comp19_prop-reachsafety.ReachSafety-Floats cpa-seq-validate-violation-witnesses-pesco.sv-comp19_prop-reachsafety.ReachSafety-Floats uautomizer-validate-violation-witnesses-pesco.sv-comp19_prop-reachsafety.ReachSafety-Floats cpa-witness2test-validate-violation-witnesses-pesco.sv-comp19_prop-reachsafety.ReachSafety-Floats fshell-witness2test-validate-violation-witnesses-pesco.sv-comp19_prop-reachsafety.ReachSafety-Floats cpa-seq-validate-correctness-witnesses-pesco.sv-comp19_prop-reachsafety.ReachSafety-Floats uautomizer-validate-correctness-witnesses-pesco.sv-comp19_prop-reachsafety.ReachSafety-Floats
Options -svcomp19-pesco -heap 10000M -stack 2048k -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/pesco.2018-12-06_1244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/pesco.2018-12-06_1244.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/pesco.2018-12-06_1244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/pesco.2018-12-06_1244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/pesco.2018-12-06_1244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/pesco.2018-12-06_1244.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 46 36   1200 360 .0082 0     false(unreach-call) 1 wit inspect 81    79    350 0   0   false(unreach-call) 1 --- inspect 33     28     670   .68 0   unknown 0 --- inspect 3.8  2.3  240 0     0     true -32 --- inspect .57   .57   20    .053 0      - --- inspect - --- inspect
floats-cdfpl/newton_1_5_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 62 53   1200 450 .0082 0     false(unreach-call) 1 wit inspect 67    65    350 0   0   timeout 0 --- inspect 97     92     690   1.3  0   unknown 0 --- inspect 3.6  2.1  250 0     0     true -32 --- inspect .57   .57   20    .053 0      - --- inspect - --- inspect
floats-cdfpl/newton_1_6_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 27 18   1200 180 .0082 0     false(unreach-call) 1 wit inspect 55    52    350 0   0   false(unreach-call) 1 --- inspect 73     67     690   .71 0   unknown 0 --- inspect 3.5  2.1  250 0     0     true -32 --- 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 26 18   1300 230 .0082 .090 false(unreach-call) 1 wit inspect 26    24    350 0   0   timeout 0 --- inspect 97     91     700   .78 0   unknown 0 --- inspect 3.6  2.1  240 0     0     true -32 --- inspect .59   .59   20    .053 0      - --- inspect - --- inspect
floats-cdfpl/newton_1_8_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 22 13   1200 170 .0082 0     false(unreach-call) 1 wit inspect 18    16    350 0   0   false(unreach-call) 1 --- inspect 28     23     680   .71 0   unknown 0 --- inspect 3.9  2.2  250 0     0     true -32 --- inspect .58   .58   20    .053 .0041 - --- inspect - --- inspect
floats-cdfpl/newton_2_6_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 35 25   1300 250 .0082 0     timeout 0 wit inspect 92    90    450 0   0   timeout 0 --- inspect 97     91     810   1.6  0   unknown 0 --- inspect 3.6  2.1  240 0     0     true -32 --- inspect .60   .60   20    .053 0      - --- inspect - --- inspect
floats-cdfpl/newton_2_7_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 33 23   1300 240 .0082 0     timeout 0 wit inspect 92    90    450 0   0   timeout 0 --- inspect 97     91     810   1.6  0   unknown 0 --- inspect 3.5  2.1  250 0     .098 true -32 --- inspect .58   .57   20    .053 0      - --- inspect - --- inspect
floats-cdfpl/newton_2_8_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 42 33   1300 350 .0082 0     false(unreach-call) 1 wit inspect 49    47    450 0   0   false(unreach-call) 1 --- inspect 40     35     820   .71 0   unknown 0 --- inspect 3.9  2.2  250 0     0     true -32 --- inspect .58   .57   20    .053 0      - --- inspect - --- inspect
floats-cdfpl/newton_3_6_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 410 400   1900 2900 .020  0     timeout 0 wit inspect 92    90    550 0   0   timeout 0 --- inspect 97     91     890   1.5  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/newton_3_7_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 300 290   2000 2000 .020  0     false(unreach-call) 1 wit inspect 68    66    550 0   0   false(unreach-call) 1 --- inspect 51     45     910   .68 0   false(unreach-call) 1 --- inspect 3.9  2.3  260 0     0     false(unreach-call) 1 --- inspect .58   .58   20    .053 0      - --- inspect - --- inspect
floats-cdfpl/newton_3_8_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 29 21   1500 210 .0082 0     timeout 0 wit inspect 92    90    550 0   0   timeout 0 --- inspect 97     90     920   1.6  0   unknown 0 --- inspect 3.6  2.1  240 0     0     true -32 --- inspect .57   .57   20    .053 0      - --- inspect - --- inspect
floats-cdfpl/sine_1_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 110 99   1400 1000 .012  0     false(unreach-call) 1 wit inspect 11    8.9  310 0   0   timeout 0 --- inspect 97     91     610   1.6  0   false(unreach-call) 1 --- inspect 3.5  2.0  250 0     0     false(unreach-call) 1 --- inspect .62   .62   20    .049 0      - --- inspect - --- inspect
floats-cdfpl/sine_2_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 21 12   1100 180 .0041 0     false(unreach-call) 1 wit inspect 56    55    320 0   0   timeout 0 --- inspect 97     91     570   .97 0   unknown 0 --- inspect 3.6  2.1  250 0     0     true -32 --- inspect .57   .57   20    .049 0      - --- inspect - --- inspect
floats-cdfpl/sine_3_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 45 37   1200 450 .0041 0     false(unreach-call) 1 wit inspect 52    50    320 0   0   timeout 0 --- inspect 97     91     600   1.6  0   unknown 0 --- inspect 3.8  2.2  250 0     0     true -32 --- inspect .57   .57   20    .049 0      - --- inspect - --- inspect
floats-cdfpl/square_1_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 29 19   1200 230 .0082 0     false(unreach-call) 1 wit inspect 12    9.6  310 0   0   timeout 0 --- inspect 97     91     450   1.8  0   false(unreach-call) 1 --- inspect 3.4  2.0  250 0     0     false(unreach-call) 1 --- inspect .57   .57   20    .049 0      - --- inspect - --- inspect
floats-cdfpl/square_2_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 200 190   1400 1500 .0082 0     false(unreach-call) 1 wit inspect 54    52    340 0   0   timeout 0 --- inspect 97     92     440   1.5  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/square_3_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 71 62   1300 620 .0082 0     false(unreach-call) 1 wit inspect 21    19    320 0   0   timeout 0 --- inspect 97     91     470   1.7  0   false(unreach-call) 1 --- inspect 4.2  2.4  250 0     0     false(unreach-call) 1 --- inspect .58   .58   20    .049 0      - --- inspect - --- inspect
floats-cdfpl/newton_1_1_true-unreach-call_true-termination.i timeout 0 wit inspect 900 890   1600 5800 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    590 0   0      timeout 0 --- inspect 960     950     970   1.7  0  
floats-cdfpl/newton_1_2_true-unreach-call_true-termination.i timeout 0 wit inspect 900 890   1600 6100 .0082 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 890   1600 6400 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    580 0   0      timeout 0 --- inspect 960     950     960   1.6  0  
floats-cdfpl/newton_2_1_true-unreach-call_true-termination.i timeout 0 wit inspect 900 890   1700 6600 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    540 0   0      timeout 0 --- inspect 960     950     890   .75 0  
floats-cdfpl/newton_2_2_true-unreach-call_true-termination.i timeout 0 wit inspect 900 890   2000 6500 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    840 0   0      timeout 0 --- inspect 960     950     960   .74 0  
floats-cdfpl/newton_2_3_true-unreach-call_true-termination.i timeout 0 wit inspect 900 890   1700 6100 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    530 0   0      timeout 0 --- inspect 960     950     1000   .73 0  
floats-cdfpl/newton_2_4_true-unreach-call_true-termination.i timeout 0 wit inspect 900 890   1700 6400 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    580 0   0      timeout 0 --- inspect 960     950     1100   .84 0  
floats-cdfpl/newton_2_5_true-unreach-call_true-termination.i timeout 0 wit inspect 900 890   1700 6800 .0082 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_3_1_true-unreach-call_true-termination.i timeout 0 wit inspect 900 890   1700 6700 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    590 0   0      timeout 0 --- inspect 960     950     1100   .80 0  
floats-cdfpl/newton_3_2_true-unreach-call_true-termination.i timeout 0 wit inspect 900 890   1700 6700 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    570 0   0      timeout 0 --- inspect 960     950     1100   .75 0  
floats-cdfpl/newton_3_3_true-unreach-call_true-termination.i timeout 0 wit inspect 900 890   1900 7200 .0082 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 890   1900 6100 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    700 0   0      timeout 0 --- inspect 960     950     1000   .88 0  
floats-cdfpl/newton_3_5_true-unreach-call_true-termination.i timeout 0 wit inspect 900 890   1700 8000 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    560 0   0      timeout 0 --- inspect 960     950     1000   .75 0  
floats-cdfpl/sine_4_true-unreach-call_true-termination.i timeout 0 wit inspect 900 890   1500 6600 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    500 0   0      timeout 0 --- inspect 960     950     790   1.4  0  
floats-cdfpl/sine_5_true-unreach-call_true-termination.i timeout 0 wit inspect 900 890   1500 7600 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    490 0   0      timeout 0 --- inspect 960     950     830   .81 0  
floats-cdfpl/sine_6_true-unreach-call_true-termination.i timeout 0 wit inspect 900 890   1700 4900 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    650 0   0      timeout 0 --- inspect 960     950     830   .75 0  
floats-cdfpl/sine_7_true-unreach-call_true-termination.i true 2 wit inspect 690 680   1600 5500 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 830    830    590 0   0      timeout 0 --- inspect 960     950     820   .75 0  
floats-cdfpl/sine_8_true-unreach-call_true-termination.i true 2 wit inspect 560 550   1600 4800 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 580    580    540 0   0      timeout 0 --- inspect 960     950     810   .72 0  
floats-cdfpl/square_4_true-unreach-call_true-termination.i true 2 wit inspect 540 530   1400 5000 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 700    700    570 0   0      timeout (true) 0 --- inspect 930     920     730   .71 0  
floats-cdfpl/square_5_true-unreach-call_true-termination.i true 2 wit inspect 450 440   1300 3100 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 530    530    510 0   0      timeout 0 --- inspect 960     950     770   .72 0  
floats-cdfpl/square_6_true-unreach-call_true-termination.i true 2 wit inspect 240 230   1300 1600 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 300    290    500 0   0      timeout 0 --- inspect 960     950     770   .76 0  
floats-cdfpl/square_7_true-unreach-call_true-termination.i true 2 wit inspect 750 740   1300 5700 0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    480 0   0      true 2 --- inspect 650     640     780   .71 0  
floats-cdfpl/square_8_true-unreach-call_true-termination.i true 2 wit inspect 65 57   1300 570 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 74    72    360 0   0      true 2 --- inspect 84     78     590   .71 0  
floats-cbmc-regression/float-div1_true-unreach-call.i true 2 wit inspect 17 5.0 1200 120 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.8  3.6  320 0   0      true 2 --- inspect 44     38     920   .65 0  
floats-cbmc-regression/float-flags-simp1_true-unreach-call.i true 2 wit inspect 31 10   2100 270 0      .090 - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 10    8.1  780 0   0      error (7) 0 --- inspect 13     7.6   280   .75 0  
floats-cbmc-regression/float-no-simp1_true-unreach-call_true-termination.i true 2 wit inspect 13 3.6 1100 88 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.7  2.1  250 0   0      true 2 --- inspect 13     7.6   300   .75 0  
floats-cbmc-regression/float-no-simp2_true-unreach-call.i true 2 wit inspect 25 13   1200 230 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 20    18    300 0   0      true 2 --- inspect 51     44     550   .68 0  
floats-cbmc-regression/float-no-simp3_true-unreach-call_true-termination.i true 2 wit inspect 12 3.5 1000 77 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-simp4_true-unreach-call.i true 2 --- inspect 15 4.1 1200 95 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .47 41 0   0      error (2) 0 --- inspect .022 .023 5.8 0    0  
floats-cbmc-regression/float-no-simp6_true-unreach-call_true-termination.i true 2 wit inspect 11 3.5 1100 90 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.7  2.1  250 0   0      true 2 --- inspect 14     8.8   310   .75 0  
floats-cbmc-regression/float-no-simp7_true-unreach-call_true-termination.i true 2 wit inspect 13 3.6 1000 84 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.0  2.3  250 0   0      true 2 --- inspect 14     8.1   300   .75 0  
floats-cbmc-regression/float-no-simp8_true-unreach-call.i true 2 wit inspect 14 4.1 1100 100 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.2  2.8  250 0   0      error (7) 0 --- inspect 13     7.8   290   .75 0  
floats-cbmc-regression/float-rounding1_true-unreach-call.i unknown 0 --- inspect 18 5.2 1300 140 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 42 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0  
floats-cbmc-regression/float-to-double1_true-unreach-call.i true 2 wit inspect 15 4.3 1200 120 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.1  2.8  260 0   0      true 2 --- inspect 32     26     450   .75 0  
floats-cbmc-regression/float-to-double2_true-unreach-call_true-termination.i true 2 wit inspect 13 3.6 1000 89 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.9  2.1  250 0   0      true 2 --- inspect 13     7.7   300   .75 0  
floats-cbmc-regression/float-zero-sum1_true-unreach-call_true-termination.i true 2 wit inspect 13 3.9 1200 100 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.7  2.1  250 0   0      true 2 --- inspect 15     8.6   300   .75 0  
floats-cbmc-regression/float11_true-unreach-call_true-termination.i true 2 wit inspect 13 3.6 1000 90 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.0  2.2  250 0   0      true 2 --- inspect 13     7.6   310   .75 0  
floats-cbmc-regression/float12_true-unreach-call_true-termination.i true 2 wit inspect 13 3.7 1000 91 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.3  2.5  260 0   0      true 2 --- inspect 21     15     290   .75 0  
floats-cbmc-regression/float13_true-unreach-call_true-termination.i true 2 wit inspect 13 3.6 1000 88 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.2  2.3  250 0   0      true 2 --- inspect 15     9.1   300   .75 0  
floats-cbmc-regression/float14_true-unreach-call.i true 2 wit inspect 14 4.1 1100 90 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.4  2.9  260 0   0      true 2 --- inspect 15     8.6   380   .71 0  
floats-cbmc-regression/float18_true-unreach-call.i true 2 wit inspect 12 3.9 1300 94 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 45    39    630 0   0      error (7) 0 --- inspect 12     6.4   290   .75 0  
floats-cbmc-regression/float19_true-unreach-call.i true 2 wit inspect 15 4.2 1200 120 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.6  2.5  260 0   0      true 2 --- inspect 16     9.0   390   .75 0  
floats-cbmc-regression/float1_true-unreach-call_true-termination.i true 2 wit inspect 12 3.6 1000 89 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.4  2.4  250 0   0      true 2 --- inspect 13     7.4   290   .75 0  
floats-cbmc-regression/float20_true-unreach-call_true-termination.i true 2 wit inspect 13 3.7 1000 85 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.6  2.5  250 0   0      true 2 --- inspect 20     15     370   .75 0  
floats-cbmc-regression/float21_true-unreach-call.i true 2 wit inspect 21 8.1 1200 160 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 9.1  6.8  290 0   0      true 2 --- inspect 67     59     570   .71 0  
floats-cbmc-regression/float22_true-unreach-call_true-termination.i true 2 --- inspect 15 4.4 1200 130 .0082 .090 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .45 41 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0  
floats-cbmc-regression/float2_true-unreach-call_true-termination.i true 2 wit inspect 12 3.6 1000 81 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.4  2.4  250 0   0      true 2 --- inspect 14     8.1   300   .75 0  
floats-cbmc-regression/float3_true-unreach-call_true-termination.i true 2 wit inspect 13 3.7 1000 98 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.0  2.3  270 0   0      true 2 --- inspect 17     11     310   .75 0  
floats-cbmc-regression/float4_true-unreach-call.i true 2 wit inspect 63 51   1200 690 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 66    64    330 0   0      true 2 --- inspect 93     85     590   .71 0  
floats-cbmc-regression/float5_true-unreach-call_true-termination.i true 2 wit inspect 13 3.8 1000 88 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.7  2.6  260 0   0      true 2 --- inspect 32     26     290   .75 0  
floats-cbmc-regression/float6_true-unreach-call_true-termination.i true 2 wit inspect 14 3.8 1100 90 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.5  2.5  250 0   0      true 2 --- inspect 15     8.8   310   .75 0  
floats-cbmc-regression/float8_true-unreach-call.i true 2 wit inspect 18 7.1 1200 160 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 9.0  6.7  270 0   0      true 2 --- inspect 15     9.3   400   .75 0  
floats-cbmc-regression/float_lib1_true-unreach-call.i true 2 wit inspect 15 4.8 1300 120 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.2  2.9  260 0   0      error (7) 0 --- inspect 11     6.9   280   .75 0  
floats-cbmc-regression/float_lib2_true-unreach-call.i true 2 wit inspect 14 4.2 1100 100 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.5  2.5  260 0   0      true 2 --- inspect 17     10     420   .75 0  
float-benchs/cast_float_ptr_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 12 3.9 1200 89 .0082 0     false(unreach-call) 1 wit inspect 3.9  2.2  260 0   0   false(unreach-call) 1 --- inspect 16     9.3   310   .75 0   unknown 0 --- inspect 3.5  2.1  250 0     0     true -32 --- inspect .57   .57   20    .049 0      - --- inspect - --- inspect
float-benchs/cast_union_loose_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 14 4.1 1100 110 .0082 0     false(unreach-call) 1 wit inspect 4.1  2.4  270 0   0   false(unreach-call) 1 --- inspect 13     8.7   310   .75 0   unknown 0 --- inspect 3.7  2.2  250 0     0     true -32 --- inspect .58   .58   20    .053 0      - --- inspect - --- inspect
float-benchs/cast_union_tight_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 12 3.9 1200 94 .0082 0     false(unreach-call) 1 wit inspect 4.3  2.5  260 0   0   false(unreach-call) 1 --- inspect 14     8.8   310   .71 0   unknown 0 --- inspect 3.7  2.1  250 0     0     true -32 --- inspect .59   .59   20    .049 0      - --- inspect - --- inspect
float-benchs/float_int_inv_square_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 12 3.7 1200 82 .0082 0     false(unreach-call) 1 wit inspect 3.9  2.2  260 0   0   false(unreach-call) 1 --- inspect 14     8.5   300   .71 0   unknown 0 --- inspect 3.6  2.1  250 0     0     true -32 --- inspect .58   .58   20    .049 0      - --- inspect - --- inspect
float-benchs/inv_Newton_false-unreach-call.c false(unreach-call) 1 wit inspect 14 5.5 1300 110 .012  0     false(unreach-call) 1 wit inspect 6.6  4.8  330 0   0   timeout 0 --- inspect 97     89     760   1.9  0   unknown 0 --- inspect 3.9  2.2  250 0     0     true -32 --- inspect .59   .59   20    .057 .0041 - --- inspect - --- inspect
float-benchs/inv_Newton_false-unreach-call.c.p+cfa-reducer.c false(unreach-call) 1 wit inspect 14 5.0 1300 110 .012  0     false(unreach-call) 1 wit inspect 6.1  4.3  340 0   0   timeout 0 --- inspect 97     89     770   1.7  0   unknown 0 --- inspect 3.8  2.2  250 0     0     true -32 --- inspect .58   .58   20    .057 0      - --- inspect - --- inspect
float-benchs/inv_square_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 14 4.0 1100 100 .0082 0     false(unreach-call) 1 wit inspect 4.0  2.3  260 0   0   false(unreach-call) 1 --- inspect 15     9.6   300   .71 0   unknown 0 --- inspect 4.0  2.3  250 0     0     true -32 --- inspect .58   .58   20    .049 0      - --- inspect - --- inspect
float-benchs/nan_double_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 13 3.9 1100 92 .0041 0     false(unreach-call) 1 wit inspect 4.0  2.3  260 0   0   false(unreach-call) 1 --- inspect 12     7.5   300   .68 0   unknown 0 --- inspect 3.6  2.1  240 0     0     true -32 --- inspect .58   .57   20    .045 0      - --- inspect - --- inspect
float-benchs/nan_float_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 13 3.8 1100 93 .0041 0     false(unreach-call) 1 wit inspect 4.0  2.3  250 0   0   false(unreach-call) 1 --- inspect 12     7.1   300   .68 0   unknown 0 --- inspect 4.1  2.4  250 0     0     true -32 --- inspect .64   .65   20    .045 0      - --- inspect - --- inspect
float-benchs/sin_interpolated_index_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 15 4.3 1200 120 0      0     false(unreach-call) 1 wit inspect 7.5  4.5  340 0   0   false(unreach-call) 1 --- inspect 28     19     990   .71 0   false(unreach-call) 1 --- inspect 4.7  2.6  270 0     0     false(unreach-call) 1 --- inspect .63   .63   20    .086 0      - --- inspect - --- inspect
float-benchs/sqrt_poly2_false-unreach-call.c false(unreach-call) 1 wit inspect 30 22   1400 280 .0082 0     false(unreach-call) 1 wit inspect 30    28    420 0   0   false(unreach-call) 1 --- inspect 20     14     590   .75 0   unknown 0 --- inspect 4.0  2.3  240 0     0     true -32 --- inspect .59   .58   20    .057 0      - --- inspect - --- inspect
float-benchs/Muller_Kahan_true-unreach-call.c.p+cfa-reducer.c true 2 wit inspect 15 4.2 1200 99 0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    1500 0   0      timeout 0 --- inspect 960     910     2500   .72 0  
float-benchs/Muller_Kahan_true-unreach-call_true-termination.c true 2 wit inspect 16 4.3 1200 110 0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    2400 0   0      timeout 0 --- inspect 960     900     3200   1.5  0  
float-benchs/Rump_double_true-unreach-call_true-termination.c true 2 wit inspect 13 3.6 1000 82 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.1  2.3  250 0   0      true 2 --- inspect 29     24     990   .75 0  
float-benchs/Rump_float_true-unreach-call_true-termination.c true 2 wit inspect 11 3.4 1200 88 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.5  2.0  250 0   0      true 2 --- inspect 19     12     420   .75 0  
float-benchs/addsub_double_exact_true-unreach-call_true-termination.c true 2 wit inspect 13 3.7 1000 87 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.1  2.3  250 0   0      true 2 --- inspect 16     9.3   290   .75 0  
float-benchs/addsub_float_exact_true-unreach-call_true-termination.c true 2 wit inspect 13 3.6 1000 92 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.5  2.0  250 0   0      true 2 --- inspect 13     8.0   290   .71 0  
float-benchs/addsub_float_inexact_true-unreach-call_true-termination.c true 2 wit inspect 13 3.6 1000 82 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.7  2.0  250 0   0      true 2 --- inspect 13     7.9   300   .75 0  
float-benchs/arctan_Pade_true-unreach-call_true-termination.c true 2 wit inspect 32 23   1400 280 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 37    35    500 0   0      error (7) 0 --- inspect 130     130     2600   .68 0  
float-benchs/bary_diverge_true-unreach-call_true-termination.c timeout 0 wit inspect 920 450   2600 8100 .012  0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    1200 0   0      timeout 0 --- inspect 960     950     2600   1.7  0  
float-benchs/cast_float_union_true-unreach-call.c true 2 wit inspect 13 3.8 1100 83 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.5  2.0  250 0   0      true 2 --- inspect 6.8   3.9   310   .62 0  
float-benchs/cos_polynomial_true-unreach-call_true-termination.c timeout 0 wit inspect 900 890   2500 6100 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    1300 0   0      timeout 0 --- inspect 960     950     2900   .84 0  
float-benchs/divmul_buf_diverge_true-unreach-call_true-termination.c timeout 0 wit inspect 910 440   4400 8900 0      0     - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 690    680    7000 0   0      timeout 0 --- inspect 960     830     1400   .72 0  
float-benchs/divmul_diverge_true-unreach-call_true-termination.c timeout 0 wit inspect 910 440   3000 8300 0      0     - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 510    500    7000 0   0      error (7) 0 --- inspect 12     6.6   290   .75 0  
float-benchs/drift_tenth_true-unreach-call.c.p+cfa-reducer.c true 2 wit inspect 110 98   1600 1600 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 31    28    450 0   0      true 2 --- inspect 550     540     690   .71 0  
float-benchs/drift_tenth_true-unreach-call_true-termination.c true 2 wit inspect 22 12   1200 210 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 28    25    430 0   0      true 2 --- inspect 290     280     700   .71 0  
float-benchs/exp_loop_true-unreach-call.c true 2 wit inspect 850 820   9700 8000 0      0     - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 550    530    7000 0   0      timeout 0 --- inspect 960     940     1100   .85 0  
float-benchs/feedback_diverge_true-unreach-call_true-termination.c timeout 0 wit inspect 960 480   5300 10000 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .69 .42 43 0   0      error (invalid witness file) 0 --- inspect 6.1   3.5   270   .65 0  
float-benchs/filter1_true-unreach-call.c.p+cfa-reducer.c true 2 wit inspect 30 7.6 1700 210 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 40    31    2100 0   0      timeout 0 --- inspect 960     950     1000   .82 0  
float-benchs/filter1_true-unreach-call.c.v+lhb-reducer.c true 2 wit inspect 49 17   2100 440 .016  0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 330    310    2600 0   0      true 2 --- inspect 530     520     830   .71 0  
float-benchs/filter1_true-unreach-call.c.v+nlh-reducer.c true 2 wit inspect 45 15   1700 410 .016  0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 220    200    2500 0   0      true 2 --- inspect 580     570     970   .71 0  
float-benchs/filter1_true-unreach-call_true-termination.c true 2 wit inspect 28 6.7 1400 200 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 9.0  6.6  420 0   0      timeout 0 --- inspect 960     930     1500   .72 0  
float-benchs/filter2_alt_true-unreach-call.c timeout 0 wit inspect 900 890   1900 7100 .012  0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    1000 0   0      timeout 0 --- inspect 960     950     950   .75 0  
float-benchs/filter2_iterated_true-unreach-call.c timeout 0 wit inspect 900 890   3000 8800 .016  0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    1600 0   0      error (7) 0 --- inspect 53     45     2200   .71 0  
float-benchs/filter2_reinit_true-unreach-call_true-termination.c timeout 0 wit inspect 960 490   4100 9600 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .68 .42 44 0   0      error (invalid witness file) 0 --- inspect 5.5   3.4   270   .65 0  
float-benchs/filter2_set_true-unreach-call_true-termination.c timeout 0 wit inspect 960 510   3500 10000 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .80 .49 43 0   0      error (invalid witness file) 0 --- inspect 5.6   3.1   260   .61 0  
float-benchs/filter2_true-unreach-call_true-termination.c timeout 0 wit inspect 960 480   3100 11000 .0082 .090 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .41 43 0   0      error (invalid witness file) 0 --- inspect 5.1   2.8   260   .65 0  
float-benchs/filter_iir_true-unreach-call.c true 2 wit inspect 13 3.9 1200 100 0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    3200 0   0      timeout 0 --- inspect 960     950     2800   1.6  0  
float-benchs/float_double_true-unreach-call_true-termination.c true 2 wit inspect 11 3.5 1200 86 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.8  2.1  250 0   0      true 2 --- inspect 14     8.7   300   .71 0  
float-benchs/image_filter_true-unreach-call.c out of memory 0 --- inspect 260 200   15000 2700 .95   0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .48 40 0   0      error (2) 0 --- inspect .020 .022 5.7 0    0  
float-benchs/interpolation2_true-unreach-call.c.p+cfa-reducer.c true 2 wit inspect 46 34   1500 560 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 560    560    630 0   0      timeout 0 --- inspect 960     950     1500   .73 0  
float-benchs/interpolation2_true-unreach-call.c.v+cfa-reducer.c true 2 wit inspect 290 280   1500 3900 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 110    110    620 0   0      timeout 0 --- inspect 960     950     1500   1.1  0  
float-benchs/interpolation2_true-unreach-call.c.v+nlh-reducer.c true 2 wit inspect 32 21   1400 350 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 66    63    600 0   0      timeout 0 --- inspect 960     950     1600   .87 0  
float-benchs/interpolation2_true-unreach-call_true-termination.c true 2 wit inspect 28 17   1400 260 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 50    47    590 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 24 11   1400 180 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 31    28    510 0   0      timeout 0 --- inspect 960     950     1500   .74 0  
float-benchs/interpolation_true-unreach-call.c.v+cfa-reducer.c true 2 wit inspect 32 20   1400 350 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 130    120    520 0   0      timeout 0 --- inspect 960     950     1500   .83 0  
float-benchs/interpolation_true-unreach-call.c.v+nlh-reducer.c true 2 wit inspect 27 15   1400 250 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 47    44    480 0   0      timeout 0 --- inspect 960     950     1500   .72 0  
float-benchs/interpolation_true-unreach-call_true-termination.c true 2 wit inspect 21 11   1300 170 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 31    28    520 0   0      timeout 0 --- inspect 960     950     2000   .77 0  
float-benchs/inv_Newton_true-unreach-call.c timeout 0 wit inspect 900 890   3500 8800 .012  0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    900    1300 0   0      true 2 --- inspect 86     79     620   .71 0  
float-benchs/inv_sqrt_Quake_true-unreach-call.c.v+cfa-reducer.c true 2 wit inspect 16 5.5 1200 120 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 7.7  5.6  310 0   0      true 2 --- inspect 92     83     1200   .71 0  
float-benchs/inv_sqrt_Quake_true-unreach-call_true-termination.c true 2 wit inspect 14 4.4 1100 110 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.5  2.8  280 0   0      true 2 --- inspect 81     75     520   .71 0  
float-benchs/inv_square_int_true-unreach-call_true-termination.c true 2 ---