Tool ULTIMATE Kojak f7c3ed31
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-59-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB
Date of execution 2017-01-13 13:05:01 CET [[ 2017-01-15 02:11:27 CET ]] [[ 2017-01-15 04:07:55 CET ]] [[ 2017-01-15 02:33:46 CET ]] [[ 2017-01-15 04:34:07 CET ]]
Run set sv-comp17.ReachSafety-Floats
Options [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ukojak.2017-01-13_1305.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ukojak.2017-01-13_1305.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ukojak.2017-01-13_1305.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ukojak.2017-01-13_1305.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]
../../sv-benchmarks/c/ verifier status score witness inspect witness cpu (s) wall (s) energy (J) mem (MB) blkio-w (MB) blkio-r (MB) validator cpachecker violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator cpachecker correctness t<900s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer correctness t<900s status cpu (s) wall (s) energy (J) mem (MB)
floats-cdfpl/newton_1_4_false-unreach-call.i error 0 wit inspect 85   79   730 1100 2.5 0      error (invalid witness file) .47 .32 4.2 39 error (invalid witness file) 6.1 3.2 110 290 - -
floats-cdfpl/newton_1_5_false-unreach-call.i error 0 wit inspect 84   77   860 1100 2.5 0      error (invalid witness file) .57 .37 8.0 40 error (invalid witness file) 6.3 3.3 130 300 - -
floats-cdfpl/newton_1_6_false-unreach-call.i error 0 wit inspect 79   73   580 1100 2.5 0      error (invalid witness file) .53 .33 9.2 43 error (invalid witness file) 6.0 3.2 100 300 - -
floats-cdfpl/newton_1_7_false-unreach-call.i error 0 wit inspect 82   76   810 1000 2.5 0      error (invalid witness file) .53 .34 7.9 42 error (invalid witness file) 6.0 3.2 120 300 - -
floats-cdfpl/newton_1_8_false-unreach-call.i error 0 wit inspect 80   74   840 1000 2.5 0      error (invalid witness file) .53 .36 12   43 error (invalid witness file) 5.6 3.0 81 290 - -
floats-cdfpl/newton_2_6_false-unreach-call.i error 0 wit inspect 70   64   650 1400 2.5 0      error (invalid witness file) .56 .37 12   42 error (invalid witness file) 6.0 3.2 120 300 - -
floats-cdfpl/newton_2_7_false-unreach-call.i error 0 wit inspect 67   61   590 1400 2.5 0      error (invalid witness file) .62 .40 8.1 39 error (invalid witness file) 5.4 2.9 81 290 - -
floats-cdfpl/newton_2_8_false-unreach-call.i error 0 wit inspect 75   69   690 1400 2.5 0      error (invalid witness file) .52 .34 10   41 error (invalid witness file) 5.8 3.1 120 300 - -
floats-cdfpl/newton_3_6_false-unreach-call.i error 0 wit inspect 88   81   700 1900 2.5 0      error (invalid witness file) .49 .32 5.4 40 error (invalid witness file) 6.2 3.3 130 300 - -
floats-cdfpl/newton_3_7_false-unreach-call.i error 0 wit inspect 77   71   590 2000 2.5 0      error (invalid witness file) .50 .32 10   42 error (invalid witness file) 6.0 3.1 130 300 - -
floats-cdfpl/newton_3_8_false-unreach-call.i error 0 wit inspect 74   67   520 2000 2.5 0      error (invalid witness file) .49 .31 7.0 39 error (invalid witness file) 5.4 2.9 110 300 - -
floats-cdfpl/sine_1_false-unreach-call.i error 0 wit inspect 31   25   280 570 2.6 0      error (invalid witness file) .53 .35 8.1 39 error (invalid witness file) 5.9 3.2 120 300 - -
floats-cdfpl/sine_2_false-unreach-call.i error 0 wit inspect 31   25   280 560 2.6 0      error (invalid witness file) .53 .33 11   40 error (invalid witness file) 5.9 3.2 86 290 - -
floats-cdfpl/sine_3_false-unreach-call.i error 0 wit inspect 31   25   230 580 2.6 0      error (invalid witness file) .59 .38 11   43 error (invalid witness file) 5.9 3.1 120 300 - -
floats-cdfpl/square_1_false-unreach-call.i error 0 wit inspect 30   23   210 330 2.6 0      error (invalid witness file) .53 .33 11   40 error (invalid witness file) 5.9 3.2 120 300 - -
floats-cdfpl/square_2_false-unreach-call.i error 0 wit inspect 29   23   290 320 2.6 0      error (invalid witness file) .52 .32 12   42 error (invalid witness file) 6.6 3.5 87 310 - -
floats-cdfpl/square_3_false-unreach-call.i error 0 wit inspect 29   23   220 320 2.6 0      error (invalid witness file) .66 .43 7.2 40 error (invalid witness file) 6.3 3.3 130 320 - -
floats-cdfpl/newton_1_1_true-unreach-call.i error 0 wit inspect 82   75   630 1100 2.5 0      - - error (invalid witness file) .64 .41 7.6 43 error (invalid witness file) 6.3 3.4 98 300
floats-cdfpl/newton_1_2_true-unreach-call.i error 0 wit inspect 80   73   600 1100 2.5 0      - - error (invalid witness file) .69 .42 8.0 39 error (invalid witness file) 7.0 3.7 130 300
floats-cdfpl/newton_1_3_true-unreach-call.i error 0 wit inspect 78   71   600 1000 2.5 0      - - error (invalid witness file) .52 .34 11   39 error (invalid witness file) 5.6 3.0 110 300
floats-cdfpl/newton_2_1_true-unreach-call.i error 0 wit inspect 77   71   600 1400 2.5 0      - - error (invalid witness file) .56 .37 8.5 40 error (invalid witness file) 6.0 3.2 120 300
floats-cdfpl/newton_2_2_true-unreach-call.i error 0 wit inspect 66   59   500 1500 2.5 0      - - error (invalid witness file) .52 .35 7.3 40 error (invalid witness file) 6.3 3.4 100 320
floats-cdfpl/newton_2_3_true-unreach-call.i error 0 wit inspect 72   66   550 1500 2.5 .17   - - error (invalid witness file) .61 .38 7.1 39 error (invalid witness file) 6.3 3.3 140 310
floats-cdfpl/newton_2_4_true-unreach-call.i error 0 wit inspect 67   61   550 1500 2.5 0      - - error (invalid witness file) .54 .37 10   40 error (invalid witness file) 5.9 3.1 100 310
floats-cdfpl/newton_2_5_true-unreach-call.i error 0 wit inspect 73   67   650 1500 2.5 0      - - error (invalid witness file) .70 .44 7.6 42 error (invalid witness file) 6.1 3.2 110 300
floats-cdfpl/newton_3_1_true-unreach-call.i error 0 wit inspect 77   70   600 2000 2.5 0      - - error (invalid witness file) .55 .34 9.8 40 error (invalid witness file) 5.8 3.1 94 300
floats-cdfpl/newton_3_2_true-unreach-call.i error 0 wit inspect 67   60   610 1800 2.5 0      - - error (invalid witness file) .50 .32 7.8 39 error (invalid witness file) 6.7 3.6 82 290
floats-cdfpl/newton_3_3_true-unreach-call.i error 0 wit inspect 79   71   630 2000 2.5 0      - - error (invalid witness file) .53 .35 11   40 error (invalid witness file) 6.0 3.2 95 300
floats-cdfpl/newton_3_4_true-unreach-call.i error 0 wit inspect 76   69   620 1900 2.5 0      - - error (invalid witness file) .50 .32 12   40 error (invalid witness file) 6.1 3.2 130 300
floats-cdfpl/newton_3_5_true-unreach-call.i error 0 wit inspect 80   73   800 1900 2.5 0      - - error (invalid witness file) .70 .46 8.6 40 error (invalid witness file) 6.6 3.5 130 300
floats-cdfpl/sine_4_true-unreach-call.i error 0 wit inspect 31   25   230 580 2.6 0      - - error (invalid witness file) .52 .33 13   39 error (invalid witness file) 5.9 3.2 97 300
floats-cdfpl/sine_5_true-unreach-call.i error 0 wit inspect 31   25   250 560 2.6 0      - - error (invalid witness file) .54 .35 6.8 39 error (invalid witness file) 5.8 3.1 110 290
floats-cdfpl/sine_6_true-unreach-call.i error 0 wit inspect 31   25   270 570 2.6 0      - - error (invalid witness file) .64 .41 9.2 40 error (invalid witness file) 6.1 3.3 120 300
floats-cdfpl/sine_7_true-unreach-call.i error 0 wit inspect 31   25   270 550 2.6 0      - - error (invalid witness file) .57 .35 9.6 39 error (invalid witness file) 6.4 3.4 100 310
floats-cdfpl/sine_8_true-unreach-call.i error 0 wit inspect 31   25   240 560 2.6 0      - - error (invalid witness file) .54 .35 12   41 error (invalid witness file) 6.4 3.4 63 300
floats-cdfpl/square_4_true-unreach-call.i error 0 wit inspect 29   23   280 330 2.6 0      - - error (invalid witness file) .67 .43 6.4 39 error (invalid witness file) 6.0 3.2 96 310
floats-cdfpl/square_5_true-unreach-call.i error 0 wit inspect 30   23   290 320 2.6 0      - - error (invalid witness file) .54 .34 14   42 error (invalid witness file) 5.7 3.0 96 290
floats-cdfpl/square_6_true-unreach-call.i error 0 wit inspect 29   23   250 320 2.6 0      - - error (invalid witness file) .50 .32 11   39 error (invalid witness file) 5.5 2.9 78 290
floats-cdfpl/square_7_true-unreach-call.i error 0 wit inspect 31   23   270 340 2.6 0      - - error (invalid witness file) .53 .33 13   40 error (invalid witness file) 7.4 3.9 120 310
floats-cdfpl/square_8_true-unreach-call.i error 0 wit inspect 29   23   300 330 2.6 0      - - error (invalid witness file) .65 .41 7.7 40 error (invalid witness file) 5.8 3.0 110 300
floats-cbmc-regression/float-div1_true-unreach-call.i error 0 wit inspect 50   43   420 390 2.5 0      - - error (invalid witness file) .51 .32 6.6 41 error (invalid witness file) 6.1 3.2 120 290
floats-cbmc-regression/float-flags-simp1_true-unreach-call.i true 2 wit inspect 18   7.0 150 530 2.9 0      - - true 15    10    180   680 true 35   23   560 720
floats-cbmc-regression/float-no-simp1_true-unreach-call.i error 0 wit inspect 4.9 1.5 35 320 2.5 0      - - error (invalid witness file) .65 .41 8.5 40 error (invalid witness file) 6.2 3.3 120 300
floats-cbmc-regression/float-no-simp2_true-unreach-call.i error 0 wit inspect 33   25   370 370 2.6 0      - - error (invalid witness file) .65 .42 7.5 39 error (invalid witness file) 6.2 3.3 120 300
floats-cbmc-regression/float-no-simp3_true-unreach-call.i error 0 wit inspect 5.0 1.6 42 310 2.5 0      - - error (invalid witness file) .48 .30 10   39 error (invalid witness file) 6.1 3.2 120 300
floats-cbmc-regression/float-no-simp4_true-unreach-call.i true 2 wit inspect 14   4.7 110 480 2.7 0      - - true 6.0  3.2  130   280 true 23   14   380 510
floats-cbmc-regression/float-no-simp6_true-unreach-call.i true 2 wit inspect 13   7.0 120 320 2.6 0      - - true 3.7  2.1  65   260 true 14   7.4 210 320
floats-cbmc-regression/float-no-simp7_true-unreach-call.i true 2 wit inspect 10   3.6 89 330 2.6 0      - - true 4.2  2.3  45   250 true 13   6.9 240 320
floats-cbmc-regression/float-no-simp8_true-unreach-call.i true 2 wit inspect 10   3.8 89 310 2.6 0      - - true 5.5  3.0  88   270 true 14   7.4 210 300
floats-cbmc-regression/float-rounding1_true-unreach-call.i unknown 0 wit inspect 5.0 1.6 42 300 2.5 0      - - error (invalid witness file) .57 .37 10   39 error (invalid witness file) 6.2 3.3 120 300
floats-cbmc-regression/float-to-double1_true-unreach-call.i true 2 wit inspect 19   13   210 300 2.6 0      - - true 5.1  2.8  89   270 true 110   110   1300 470
floats-cbmc-regression/float-to-double2_true-unreach-call.i true 2 wit inspect 11   3.2 79 360 2.6 0      - - true 4.1  2.2  50   260 true 12   6.4 190 320
floats-cbmc-regression/float-zero-sum1_true-unreach-call.i unknown 0 wit inspect 4.7 1.5 34 300 2.5 .012  - - error (invalid witness file) .50 .34 4.8 40 error (invalid witness file) 5.8 3.1 120 300
floats-cbmc-regression/float11_true-unreach-call.i true 2 wit inspect 11   3.5 80 340 2.6 0      - - true 3.5  2.0  65   260 true 13   6.9 180 310
floats-cbmc-regression/float12_true-unreach-call.i true 2 wit inspect 19   12   270 320 2.6 0      - - true 3.9  2.2  58   260 true 19   13   240 310
floats-cbmc-regression/float13_true-unreach-call.i true 2 wit inspect 12   4.0 97 350 2.6 0      - - true 3.6  2.1  80   250 true 13   7.2 240 320
floats-cbmc-regression/float14_true-unreach-call.i true 2 wit inspect 10   3.7 79 300 2.6 0      - - true 6.2  3.4  65   270 true 14   7.7 260 300
floats-cbmc-regression/float18_true-unreach-call.i unknown 0 wit inspect 5.2 1.6 42 310 2.5 0      - - error (invalid witness file) .64 .42 7.4 40 error (invalid witness file) 6.0 3.2 100 310
floats-cbmc-regression/float19_true-unreach-call.i true 2 wit inspect 11   4.5 87 300 2.6 0      - - true 5.2  2.8  94   270 true 14   7.9 150 300
floats-cbmc-regression/float1_true-unreach-call.i error 0 wit inspect 4.9 1.6 39 300 2.5 0      - - error (invalid witness file) .68 .43 7.2 40 error (invalid witness file) 6.0 3.2 92 320
floats-cbmc-regression/float20_true-unreach-call.i error 0 wit inspect 22   16   270 330 2.6 0      - - error (invalid witness file) .67 .43 7.4 40 error (invalid witness file) 5.9 3.1 81 300
floats-cbmc-regression/float21_true-unreach-call.i true 2 wit inspect 51   42   640 580 2.6 0      - - true 5.8  3.3  120   300 true 69   61   880 610
floats-cbmc-regression/float22_true-unreach-call.i unknown 0 wit inspect 12   3.8 93 350 2.6 0      - - error (invalid witness file) .62 .40 8.2 40 error (invalid witness file) 6.0 3.1 92 300
floats-cbmc-regression/float2_true-unreach-call.i true 2 wit inspect 11   4.0 90 330 2.6 0      - - true 3.9  2.2  53   260 true 14   7.5 270 330
floats-cbmc-regression/float3_true-unreach-call.i true 2 wit inspect 16   8.6 140 340 2.6 0      - - true 3.6  2.1  77   280 true 20   14   390 340
floats-cbmc-regression/float4_true-unreach-call.i error 0 wit inspect 77   69   960 430 2.5 0      - - error (invalid witness file) .59 .37 12   44 error (invalid witness file) 7.2 3.8 97 290
floats-cbmc-regression/float5_true-unreach-call.i true 2 wit inspect 48   42   600 310 2.5 0      - - true 3.5  2.0  46   280 true 31   25   430 320
floats-cbmc-regression/float6_true-unreach-call.i true 2 wit inspect 17   7.9 160 450 2.6 0      - - true 5.3  3.0  54   270 true 13   7.3 240 310
floats-cbmc-regression/float7_true-unreach-call.i unknown 0 wit inspect 5.6 1.6 47 330 2.5 0      - - error (invalid witness file) .64 .41 7.7 41 error (invalid witness file) 5.8 3.1 110 290
floats-cbmc-regression/float8_true-unreach-call.i true 2 wit inspect 9.3 3.1 70 300 2.6 0      - - true 5.5  3.3  110   280 true 15   8.0 250 320
floats-cbmc-regression/float_lib1_true-unreach-call.i true 2 wit inspect 16   6.2 150 510 2.6 0      - - true 5.9  3.2  94   270 error 12   6.3 160 300
floats-cbmc-regression/float_lib2_true-unreach-call.i true 2 wit inspect 20   11   200 520 2.6 0      - - true 5.4  2.9  94   270 true 17   9.4 220 450
float-benchs/cast_float_ptr_false-unreach-call.c unknown 0 wit inspect 4.7 1.5 34 300 2.5 0      error (invalid witness file) .63 .40 7.1 40 error (invalid witness file) 6.0 3.2 130 300 - -
float-benchs/cast_union_loose_false-unreach-call.c unknown 0 wit inspect 4.8 1.6 35 300 2.5 0      error (invalid witness file) .59 .37 8.8 39 error (invalid witness file) 6.1 3.3 120 290 - -
float-benchs/cast_union_tight_false-unreach-call.c unknown 0 wit inspect 5.1 1.5 42 300 2.5 0      error (invalid witness file) .54 .37 11   43 error (invalid witness file) 5.5 2.9 110 290 - -
float-benchs/float_int_inv_square_false-unreach-call.c false(unreach-call) 1 wit inspect 16   8.5 140 350 2.6 0      false(unreach-call) 4.2  2.4  50   290 false(unreach-call) 14   7.7 220 330 - -
float-benchs/inv_square_false-unreach-call.c false(unreach-call) 1 wit inspect 12   5.1 140 320 2.6 0      false(unreach-call) 4.6  2.6  42   290 false(unreach-call) 12   6.6 110 310 - -
float-benchs/nan_double_false-unreach-call.c false(unreach-call) 1 wit inspect 9.1 3.1 68 320 2.6 0      false(unreach-call) 3.7  2.1  45   280 false(unreach-call) 7.0 3.7 130 320 - -
float-benchs/nan_float_false-unreach-call.c false(unreach-call) 1 wit inspect 8.8 3.0 76 320 2.6 0      false(unreach-call) 3.5  2.0  48   280 false(unreach-call) 6.6 3.6 120 310 - -
float-benchs/sin_interpolated_index_false-unreach-call.c error 0 wit inspect 5.3 1.6 40 320 2.5 0      error (invalid witness file) .69 .43 8.2 39 error (invalid witness file) 6.7 3.5 130 300 - -
float-benchs/sqrt_poly2_false-unreach-call.c error 0 wit inspect 8.8 2.7 77 320 2.6 0      error (invalid witness file) .49 .32 8.6 41 error (invalid witness file) 6.3 3.3 120 300 - -
float-benchs/Muller_Kahan_true-unreach-call.c error 0 wit inspect 300   260   2500 2400 2.5 0      - - error (invalid witness file) .66 .42 9.0 39 error (invalid witness file) 5.6 3.0 130 290
float-benchs/Rump_double_true-unreach-call.c error 0 wit inspect 24   17   180 1500 2.6 0      - - error (invalid witness file) .52 .33 12   41 error (invalid witness file) 5.8 3.1 100 300
float-benchs/Rump_float_true-unreach-call.c error 0 wit inspect 21   14   150 540 2.6 0      - - error (invalid witness file) .54 .35 10   41 error (invalid witness file) 6.2 3.2 97 300
float-benchs/addsub_double_exact_true-unreach-call.c error 0 wit inspect 19   13   230 320 2.6 0      - - error (invalid witness file) .54 .35 10   40 error (invalid witness file) 6.0 3.2 86 300
float-benchs/addsub_float_exact_true-unreach-call.c true 2 wit inspect 9.9 3.8 85 320 2.6 0      - - true 4.3  2.4  48   260 true 12   6.6 170 310
float-benchs/addsub_float_inexact_true-unreach-call.c true 2 wit inspect 11   3.7 94 330 2.6 0      - - true 3.8  2.1  58   260 true 12   6.7 150 310
float-benchs/arctan_Pade_true-unreach-call.c error 0 wit inspect 54   47   380 810 2.5 0      - - error (invalid witness file) .53 .35 9.2 39 error (invalid witness file) 5.7 3.0 66 290
float-benchs/bary_diverge_true-unreach-call.c error 0 wit inspect 5.0 1.6 37 300 2.5 0      - - error (invalid witness file) .49 .32 11   39 error (invalid witness file) 6.2 3.2 120 290
float-benchs/cast_float_union_true-unreach-call.c error 0 wit inspect 8.0 2.7 63 300 2.6 0      - - error (invalid witness file) .51 .32 13   42 error (invalid witness file) 5.8 3.1 86 290
float-benchs/cos_polynomial_true-unreach-call.c error 0 wit inspect 150   150   1100 960 2.5 0      - - error (invalid witness file) .53 .33 13   40 error (invalid witness file) 5.5 2.9 47 300
float-benchs/divmul_buf_diverge_true-unreach-call.c timeout 0 wit inspect 900   720   12000 3900 2.3 0      - - error (invalid witness file) .48 .33 9.7 39 error (invalid witness file) 5.8 3.1 86 290
float-benchs/divmul_diverge_true-unreach-call.c timeout 0 wit inspect 900   730   12000 4100 2.3 0      - - error (invalid witness file) .55 .35 12   42 error (invalid witness file) 6.1 3.2 86 310
float-benchs/drift_tenth_true-unreach-call.c timeout 0 wit inspect 900   890   8900 650 2.5 0      - - error (invalid witness file) .52 .33 14   40 error (invalid witness file) 6.3 3.3 120 310
float-benchs/exp_loop_true-unreach-call.c error 0 wit inspect 190   180   2000 630 2.5 0      - - error (invalid witness file) .51 .33 9.0 39 error (invalid witness file) 6.1 3.2 120 290
float-benchs/feedback_diverge_true-unreach-call.c timeout 0 wit inspect 900   730   13000 3700 2.3 0      - - error (invalid witness file) .59 .38 5.8 41 error (invalid witness file) 5.8 3.1 120 290
float-benchs/filter1_true-unreach-call.c error 0 wit inspect 61   55   570 390 2.5 0      - - error (invalid witness file) .59 .38 11   42 error (invalid witness file) 6.0 3.2 120 300
float-benchs/filter2_alt_true-unreach-call.c error 0 wit inspect 35   28   450 340 2.6 0      - - error (invalid witness file) .68 .41 8.7 40 error (invalid witness file) 6.4 3.4 110 320
float-benchs/filter2_iterated_true-unreach-call.c error 0 wit inspect 24   17   320 2200 2.6 0      - - error (invalid witness file) .66 .42 8.5 40 error (invalid witness file) 5.8 3.1 68 300
float-benchs/filter2_reinit_true-unreach-call.c error 0 wit inspect 50   44   460 410 2.5 0      - - error (invalid witness file) .63 .40 7.7 39 error (invalid witness file) 6.0 3.2 110 310
float-benchs/filter2_set_true-unreach-call.c error 0 wit inspect 31   24   230 510 2.6 0      - - error (invalid witness file) .51 .32 10   40 error (invalid witness file) 6.1 3.3 130 290
float-benchs/filter2_true-unreach-call.c error 0 wit inspect 30   23   300 390 2.6 0      - - error (invalid witness file) .53 .33 10   40 error (invalid witness file) 6.7 3.6 130 310
float-benchs/filter_iir_true-unreach-call.c unknown 0 wit inspect 4.7 1.5 39 300 2.5 0      - - error (invalid witness file) .56 .36 10   42 error (invalid witness file) 5.5 3.0 110 290
float-benchs/float_double_true-unreach-call.c true 2 wit inspect 10   3.4 79 320 2.6 0      - - true 3.3  1.8  65   260 true 13   7.1 190 310
float-benchs/image_filter_true-unreach-call.c unknown 0 wit inspect 4.8 1.6 42 300 2.5 0      - - error (invalid witness file) .68 .43 8.3 43 error (invalid witness file) 6.2 3.4 110 300
float-benchs/interpolation2_true-unreach-call.c error 0 wit inspect 69   62   670 370 2.5 0      - - error (invalid witness file) .51 .32 10   39 error (invalid witness file) 5.4 2.9 58 290
float-benchs/interpolation_true-unreach-call.c error 0 wit inspect 52   45   500 330 2.5 0      - - error (invalid witness file) .63 .40 7.9 39 error (invalid witness file) 6.7 3.5 76 320
float-benchs/inv_sqrt_Quake_true-unreach-call.c unknown 0 wit inspect 6.0 1.6 47 340 2.5 0      - - error (invalid witness file) .50 .31 8.3 40 error (invalid witness file) 6.1 3.2 130 300
float-benchs/inv_square_int_true-unreach-call.c true 2 wit inspect 13   6.1 120 340 2.6 0      - - true 3.7  2.1  71   270 true 21   15   400 330
float-benchs/inv_square_true-unreach-call.c true 2 wit inspect 15   8.8 150 320 2.6 .16   - - true 3.9  2.2  68   280 true 55   49   1000 320
float-benchs/loop_true-unreach-call.c error 0 wit inspect 74   67   850 410 2.5 0      - - error (invalid witness file) .66 .43 9.5 45 error (invalid witness file) 6.2 3.2 110 290
float-benchs/mea8000_true-unreach-call.c unknown 0 wit inspect 5.0 1.5 36 310 2.5 0      - - error (invalid witness file) .62 .41 8.7 40 error (invalid witness file) 6.3 3.3 140 300
float-benchs/nan_double_range_true-unreach-call.c true 2 wit inspect 9.9 3.1 75 350 2.6 0      - - true 3.6  2.0  72   260 true 12   6.6 180 310
float-benchs/nan_float_range_true-unreach-call.c true 2 wit inspect 10   3.6 93 310 2.6 0      - - true 3.6  2.0  81   260 true 15   8.8 280 310
float-benchs/rlim_exit_true-unreach-call.c timeout 0 wit inspect 900   730   15000 4900 2.3 0      - - error (invalid witness file) .63 .41 9.0 42 error (invalid witness file) 5.9 3.1 110 300
float-benchs/rlim_invariant_true-unreach-call.c error 0 wit inspect 73   65   820 430 2.5 0      - - error (invalid witness file) .58 .37 11   40 error (invalid witness file) 5.7 3.0 110 300
float-benchs/sin_interpolated_bigrange_loose_true-unreach-call.c error 0 wit inspect 6.3 1.7 51 350 2.5 0      - - error (invalid witness file) .64 .41 8.0 41 error (invalid witness file) 6.8 3.6 130 310
float-benchs/sin_interpolated_bigrange_tight_true-unreach-call.c error 0 wit inspect 5.5 1.6 40 310 2.5 0      - - error (invalid witness file) .62 .40 9.0 40 error (invalid witness file) 6.0 3.2 120 300
float-benchs/sin_interpolated_index_true-unreach-call.c error 0 wit inspect 5.9 1.7 43 330 2.5 0      - - error (invalid witness file) .58 .36 9.1 39 error (invalid witness file) 6.3 3.4 130 300
float-benchs/sin_interpolated_negation_true-unreach-call.c error 0 wit inspect 5.5 1.7 42 320 2.5 0      - - error (invalid witness file) .55 .35 11   41 error (invalid witness file) 6.1 3.2 120 300
float-benchs/sin_interpolated_smallrange_true-unreach-call.c error 0 wit inspect 5.5 1.6 43 330 2.5 0      - - error (invalid witness file) .65 .42 8.7 41 error (invalid witness file) 6.1 3.3 120 300
float-benchs/sqrt_Householder_constant_true-unreach-call.c error 0 wit inspect 110   100   880 1500 2.5 0      - - error (invalid witness file) .61 .38 9.4 40 error (invalid witness file) 5.8 3.1 84 300
float-benchs/sqrt_Householder_interval_true-unreach-call.c error 0 wit inspect 120   110   1000 1500 2.5 0      - - error (invalid witness file) .67 .42 7.5 40 error (invalid witness file) 5.7 3.0 110 290
float-benchs/sqrt_Householder_pseudoconstant_true-unreach-call.c error 0 wit inspect 130   130   1200 1900 2.5 0      - - error (invalid witness file) .50 .32 11   40 error (invalid witness file) 6.3 3.4 130 300
float-benchs/sqrt_Newton_pseudoconstant_true-unreach-call.c error 0 wit inspect 130   120   1100 1700 2.5 0      - - error (invalid witness file) .65 .40 7.8 40 error (invalid witness file) 5.7 3.0 75 300
float-benchs/sqrt_biNewton_pseudoconstant_true-unreach-call.c error 0 wit inspect 130   130   1300 1700 2.5 0      - - error (invalid witness file) .64 .41 11   44 error (invalid witness file) 6.1 3.2 66 300
float-benchs/sqrt_poly_true-unreach-call.c error 0 wit inspect 98   91   1000 760 2.5 0      - - error (invalid witness file) .49 .32 13   39 error (invalid witness file) 5.7 3.0 110 300
float-benchs/water_pid_true-unreach-call.c error 0 wit inspect 34   27   260 1200 2.6 0      - - error (invalid witness file) .50 .32 7.6 41 error (invalid witness file) 5.7 3.1 120 300
float-benchs/zonotope_2_true-unreach-call.c timeout 0 wit inspect 900   890   8200 860 2.5 0      - - error (invalid witness file) .52 .33 9.6 40 error (invalid witness file) 5.9 3.1 100 300
float-benchs/zonotope_3_true-unreach-call.c timeout 0 wit inspect 900   760   12000 5300 2.3 0      - - error (invalid witness file) .66 .41 9.0 42 error (invalid witness file) 6.2 3.3 110 300
float-benchs/zonotope_loose_true-unreach-call.c error 0 wit inspect 84   78   830 690 2.5 0      - - error (invalid witness file) .65 .42 7.6 40 error (invalid witness file) 5.7 3.0 83 290
float-benchs/zonotope_tight_true-unreach-call.c error 0 wit inspect 75   69   670 710 2.5 0      - - error (invalid witness file) .52 .32 12   42 error (invalid witness file) 5.7 3.0 88 290
floats-esbmc-regression/Double_div_true-unreach-call.i error 0 wit inspect 38   31   370 710 2.6 0      - - error (invalid witness file) .67 .43 7.7 40 error (invalid witness file) 6.0 3.2 93 300
floats-esbmc-regression/Float_div_true-unreach-call.i error 0 wit inspect 72   65   640 410 2.5 0      - - error (invalid witness file) .57 .37 9.9 40 error (invalid witness file) 6.1 3.2 99 310
floats-esbmc-regression/ceil_nondet_true-unreach-call.i unknown 0 wit inspect 8.4 2.7 67 300 2.6 0      - - error (invalid witness file) .52 .33 12   40 error (invalid witness file) 6.1 3.2 120 290
floats-esbmc-regression/ceil_true-unreach-call.i unknown 0 wit inspect 4.8 1.5 41 300 2.5 0      - - error (invalid witness file) .71 .45 8.5 43 error (invalid witness file) 5.9 3.2 110 290
floats-esbmc-regression/copysign_true-unreach-call.i unknown 0 wit inspect 4.9 1.6 40 300 2.5 0      - - error (invalid witness file) .55 .35 10   41 error (invalid witness file) 6.2 3.3 91 300
floats-esbmc-regression/digits_for_true-unreach-call.i error 0 wit inspect 4.7 1.5 39 310 2.5 0      - - error (invalid witness file) .72 .45 7.3 40 error (invalid witness file) 5.4 3.0 84 300
floats-esbmc-regression/digits_while_true-unreach-call.i error 0 wit inspect 5.1 1.6 39 310 2.5 0      - - error (invalid witness file) .63 .41 8.0 39 error (invalid witness file) 6.2 3.2 120 300
floats-esbmc-regression/fabs_true-unreach-call.i true 2 wit inspect 9.4 3.0 70 310 2.6 0      - - true 5.6  3.0  96   270 true 13   6.9 180 300
floats-esbmc-regression/fdim_true-unreach-call.i unknown 0 wit inspect 5.0 1.6 38 300 2.5 0      - - error (invalid witness file) .63 .40 9.0 39 error (invalid witness file) 6.0 3.2 120 300
floats-esbmc-regression/floor_nondet_true-unreach-call.i unknown 0 wit inspect 8.4 2.7 65 310 2.6 0      - - error (invalid witness file) .59 .38 9.7 40 error (invalid witness file) 6.0 3.2 130 300
floats-esbmc-regression/floor_true-unreach-call.i unknown 0 wit inspect 5.1 1.7 38 300 2.5 0      - - error (invalid witness file) .59 .38 10   42 error (invalid witness file) 5.7 3.0 64 300
floats-esbmc-regression/fmax_true-unreach-call.i unknown 0 wit inspect 4.9 1.5 34 330 2.5 0      - - error (invalid witness file) .68 .41 6.4 40 error (invalid witness file) 5.7 3.1 74 300
floats-esbmc-regression/fmin_true-unreach-call.i unknown 0 wit inspect 5.4 1.6 39 300 2.5 0      - - error (invalid witness file) .50 .32 12   42 error (invalid witness file) 6.2 3.3 96 300
floats-esbmc-regression/fmod2_true-unreach-call.i unknown 0 wit inspect 8.8 2.8 70 320 2.6 0      - - error (invalid witness file) .69 .44 8.0 40 error (invalid witness file) 6.3 3.3 120 300
floats-esbmc-regression/fmod3_true-unreach-call.i unknown 0 wit inspect 8.4 2.7 66 310 2.6 0      - - error (invalid witness file) .50 .33 11   40 error (invalid witness file) 6.7 3.5 140 320
floats-esbmc-regression/fmod_true-unreach-call.i unknown 0 wit inspect 5.5 1.7 38 300 2.5 0      - - error (invalid witness file) .50 .33 12   39 error (invalid witness file) 6.6 3.5 120 310
floats-esbmc-regression/isgreater_true-unreach-call.i error 0 wit inspect 8.3 2.7 75 300 2.6 0      - - error (invalid witness file) .59 .37 8.2 41 error (invalid witness file) 6.6 3.5 110 320
floats-esbmc-regression/isgreaterequal_true-unreach-call.i error 0 wit inspect 8.2 2.7 62 310 2.6 0      - - error (invalid witness file) .59 .39 9.8 40 error (invalid witness file) 6.6 3.5 80 300
floats-esbmc-regression/isless_true-unreach-call.i error 0 wit inspect 8.8 2.8 67 310 2.6 0      - - error (invalid witness file) .50 .33 12   39 error (invalid witness file) 5.8 3.1 120 300
floats-esbmc-regression/islessequal_true-unreach-call.i error 0 wit inspect 9.7 2.8 78 350 2.6 0      - - error (invalid witness file) .61 .37 7.4 39 error (invalid witness file) 5.9 3.1 57 310
floats-esbmc-regression/islessgreater_true-unreach-call.i error 0 wit inspect 8.6 2.8 76 320 2.6 0      - - error (invalid witness file) .70 .43 8.8 42 error (invalid witness file) 6.2 3.3 110 300
floats-esbmc-regression/isunordered_true-unreach-call.i error 0 wit inspect 8.8 2.7 62 320 2.6 0      - - error (invalid witness file) .54 .36 8.6 40 error (invalid witness file) 6.3 3.4 130 300
floats-esbmc-regression/lrint_true-unreach-call.i unknown 0 wit inspect 5.5 1.6 45 320 2.5 0      - - error (invalid witness file) .53 .33 12   40 error (invalid witness file) 5.9 3.1 63 310
floats-esbmc-regression/modf_true-unreach-call.i unknown 0 wit inspect 4.9 1.5 35 310 2.5 0      - - error (invalid witness file) .54 .34 10   40 error (invalid witness file) 6.0 3.2 120 300
floats-esbmc-regression/nan_true-unreach-call.i true 2 wit inspect 11   4.0 82 310 2.6 0      - - true 5.3  2.9  88   270 true 13   7.1 220 300
floats-esbmc-regression/nearbyint2_true-unreach-call.i unknown 0 wit inspect 5.0 1.6 37 300 2.5 0      - - error (invalid witness file) .61 .38 10   40 error (invalid witness file) 6.1 3.2 130 300
floats-esbmc-regression/nearbyint_true-unreach-call.i unknown 0 wit inspect 5.1 1.6 37 320 2.5 0      - - error (invalid witness file) .62 .40 7.1 39 error (invalid witness file) 7.2 3.8 140 310
floats-esbmc-regression/remainder_true-unreach-call.i unknown 0 wit inspect 5.2 1.6 40 320 2.5 0      - - error (invalid witness file) .64 .40 5.4 40 error (invalid witness file) 6.7 3.5 110 320
floats-esbmc-regression/rint2_true-unreach-call.i unknown 0 wit inspect 5.0 1.5 39 300 2.5 0      - - error (invalid witness file) .57 .37 7.6 41 error (invalid witness file) 5.9 3.1 110 300
floats-esbmc-regression/rint_true-unreach-call.i unknown 0 wit inspect 5.2 1.6 42 300 2.5 0      - - error (invalid witness file) .74 .48 9.2 40 error (invalid witness file) 5.9 3.2 95 290
floats-esbmc-regression/round_nondet_true-unreach-call.i unknown 0 wit inspect 9.1 2.8 74 320 2.6 0      - - error (invalid witness file) .68 .42 8.7 40 error (invalid witness file) 6.3 3.3 110 300
floats-esbmc-regression/round_true-unreach-call.i unknown 0 wit inspect 5.2 1.5 42 300 2.5 0      - - error (invalid witness file) .52 .33 13   40 error (invalid witness file) 6.5 3.5 120 300
floats-esbmc-regression/rounding_functions_true-unreach-call.i unknown 0 wit inspect 5.0 1.5 40 300 2.5 0      - - error (invalid witness file) .53 .34 9.2 41 error (invalid witness file) 6.1 3.2 110 300
floats-esbmc-regression/trunc_nondet_2_true-unreach-call.i unknown 0 wit inspect 9.6 2.8 82 330 2.6 0      - - error (invalid witness file) .56 .36 10   42 error (invalid witness file) 7.1 3.7 140 310
floats-esbmc-regression/trunc_nondet_true-unreach-call.i unknown 0 wit inspect 9.3 2.7 78 330 2.6 .0082 - - error (invalid witness file) .53 .34 12   40 error (invalid witness file) 6.2 3.3 110 300
floats-esbmc-regression/trunc_true-unreach-call.i unknown 0 wit inspect 5.4 1.6 39 320 2.5 0      - - error (invalid witness file) .54 .35 11   41 error (invalid witness file) 5.9 3.1 92 300
floats-esbmc-regression/Double_div_bad_false-unreach-call.i error 0 wit inspect 60   53   670 860 2.5 0      error (invalid witness file) .54 .35 12   41 error (invalid witness file) 5.9 3.2 120 300 - -
floats-esbmc-regression/Float_div_bad_false-unreach-call.i error 0 wit inspect 79   72   760 450 2.5 0      error (invalid witness file) .51 .33 9.4 40 error (invalid witness file) 5.1 2.8 84 290 - -
floats-esbmc-regression/digits_bad_for_false-unreach-call.i error 0 wit inspect 5.2 1.5 40 310 2.5 0      error (invalid witness file) .56 .37 7.0 39 error (invalid witness file) 5.3 2.8 69 300 - -
floats-esbmc-regression/digits_bad_while_false-unreach-call.i error 0 wit inspect 4.9 1.5 38 310 2.5 0      error (invalid witness file) .48 .31 11   39 error (invalid witness file) 6.1 3.2 110 300 - -
../../sv-benchmarks/c/ verifier status score witness inspect witness cpu (s) wall (s) energy (J) mem (MB) blkio-w (MB) blkio-r (MB) validator cpachecker violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator cpachecker correctness t<900s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer correctness t<900s status cpu (s) wall (s) energy (J) mem (MB)
total 172 62 12000 10000 130000 120000 440 .35 172 30 18   420 2200   172 190 100 3500 9000   172 210 120 3400 13000   172 1300 830 22000 44000  
    correct results 33 62 490 250 4800 12000 85 .16 4 16 9.1 190 1100   4 40 22 590 1300   29 140 81 2300 8200   28 650 470 9800 10000  
        correct true 29 58 450 230 4400 10000 75 .16 0 0 0   0 0   0 0 0 0 0   29 140 81 2300 8200   28 650 470 9800 10000  
        correct false 4 4 45 20 420 1300 10 0    4 16 9.1 190 1100   4 40 22 590 1300   0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 0
        correct-unconfirmed true 0
        correct-unconfirmed false 0
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (172 tasks, max score: 314) 62
Run set sv-comp17.ReachSafety-Floats