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