Tool JayHorn 0.6-alpha
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.15.0-42-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33546 MB
Date of execution 2018-12-06 11:12:12 CET
Run set sv-comp19_prop-reachsafety_java.ReachSafety-Java
../sv-benchmarks/java/ status cpu (s) mem (MB) energy (J)
jayhorn-recursive/Ackermann01.yml 12   330 110
jayhorn-recursive/Addition.yml 5.9 330 52
jayhorn-recursive/InfiniteLoop.yml 3.2 140 27
jayhorn-recursive/SatAckermann01.yml 5.7 300 48
jayhorn-recursive/SatAckermann02.yml 13   520 96
jayhorn-recursive/SatAckermann03.yml 12   460 110
jayhorn-recursive/SatAddition01.yml 5.9 320 51
jayhorn-recursive/SatEvenOdd01.yml 900   3000 9300
jayhorn-recursive/SatFibonacci01.yml 6.7 350 59
jayhorn-recursive/SatFibonacci02.yml 19   790 130
jayhorn-recursive/SatFibonacci03.yml 25   870 160
jayhorn-recursive/SatGcd.yml 5.6 320 53
jayhorn-recursive/SatHanoi01.yml 900   2700 12000
jayhorn-recursive/SatMccarthy91.yml 6.2 340 51
jayhorn-recursive/SatMultCommutative01.yml 900   2500 9300
jayhorn-recursive/SatPrimes01.yml 9.6 370 68
jayhorn-recursive/UnsatAckermann01.yml 13   340 110
jayhorn-recursive/UnsatAddition01.yml 11   320 89
jayhorn-recursive/UnsatAddition02.yml 120   2500 990
jayhorn-recursive/UnsatEvenOdd01.yml 13   340 110
jayhorn-recursive/UnsatFibonacci01.yml 13   360 110
jayhorn-recursive/UnsatFibonacci02.yml 24   500 200
jayhorn-recursive/UnsatMccarthy91.yml 9.7 320 81
jbmc-regression/ArithmeticException1.yml 11   310 100
jbmc-regression/ArithmeticException5.yml 3.8 250 37
jbmc-regression/ArithmeticException6.yml 10   310 83
jbmc-regression/ArrayIndexOutOfBoundsException1.yml 14   430 110
jbmc-regression/ArrayIndexOutOfBoundsException2.yml 13   400 100
jbmc-regression/ArrayIndexOutOfBoundsException3.yml 17   440 150
jbmc-regression/BufferedReaderReadLine.yml 900   3400 9300
jbmc-regression/CharSequenceBug.yml 34   1000 300
jbmc-regression/CharSequenceToString.yml 52   1300 490
jbmc-regression/ClassCastException1.yml 12   350 98
jbmc-regression/ClassCastException2.yml 4.7 290 44
jbmc-regression/ClassCastException3.yml 14   440 110
jbmc-regression/Class_method1.yml 3.7 240 39
jbmc-regression/Inheritance1.yml 4.9 300 41
jbmc-regression/NegativeArraySizeException1.yml 7.7 300 70
jbmc-regression/NegativeArraySizeException2.yml 7.5 290 73
jbmc-regression/NullPointerException1.yml 3.2 140 31
jbmc-regression/NullPointerException2.yml 3.3 140 32
jbmc-regression/NullPointerException3.yml 3.3 150 32
jbmc-regression/NullPointerException4.yml 3.3 140 30
jbmc-regression/RegexMatches01.yml 900   3200 10000
jbmc-regression/RegexMatches02.yml 900   2900 9900
jbmc-regression/RegexSubstitution01.yml 900   3400 11000
jbmc-regression/RegexSubstitution02.yml 900   3000 11000
jbmc-regression/RegexSubstitution03.yml 900   3200 12000
jbmc-regression/StaticCharMethods01.yml 12   330 93
jbmc-regression/StaticCharMethods02.yml 32   970 300
jbmc-regression/StaticCharMethods03.yml 32   940 280
jbmc-regression/StaticCharMethods04.yml 8.1 320 75
jbmc-regression/StaticCharMethods05.yml 900   3200 9800
jbmc-regression/StaticCharMethods06.yml 33   950 280
jbmc-regression/StringBuilderAppend01.yml 900   3100 10000
jbmc-regression/StringBuilderAppend02.yml 900   3300 12000
jbmc-regression/StringBuilderCapLen01.yml 33   810 310
jbmc-regression/StringBuilderCapLen02.yml 68   1300 640
jbmc-regression/StringBuilderCapLen03.yml 42   1200 400
jbmc-regression/StringBuilderCapLen04.yml 42   1200 350
jbmc-regression/StringBuilderChars01.yml 900   3400 5800
jbmc-regression/StringBuilderChars02.yml 69   1300 740
jbmc-regression/StringBuilderChars03.yml 43   1300 410
jbmc-regression/StringBuilderChars04.yml 910   3400 5600
jbmc-regression/StringBuilderChars05.yml 84   1400 960
jbmc-regression/StringBuilderChars06.yml 120   1600 1500
jbmc-regression/StringBuilderConstructors01.yml 34   1000 310
jbmc-regression/StringBuilderConstructors02.yml 49   1400 430
jbmc-regression/StringBuilderInsertDelete01.yml 900   3100 9700
jbmc-regression/StringBuilderInsertDelete02.yml 900   3400 11000
jbmc-regression/StringBuilderInsertDelete03.yml 900   3400 11000
jbmc-regression/StringCompare01.yml 15   440 120
jbmc-regression/StringCompare02.yml 280   1700 3200
jbmc-regression/StringCompare03.yml 240   1700 3300
jbmc-regression/StringCompare04.yml 400   2100 4700
jbmc-regression/StringCompare05.yml 49   1300 500
jbmc-regression/StringConcatenation01.yml 900   3200 10000
jbmc-regression/StringConcatenation02.yml 900   3400 10000
jbmc-regression/StringConcatenation03.yml 900   2900 10000
jbmc-regression/StringConcatenation04.yml 140   1600 1600
jbmc-regression/StringConstructors01.yml 110   1600 1200
jbmc-regression/StringConstructors02.yml 40   1200 380
jbmc-regression/StringConstructors03.yml 900   3100 12000
jbmc-regression/StringConstructors04.yml 380   2100 4000
jbmc-regression/StringConstructors05.yml 160   1900 1600
jbmc-regression/StringContains01.yml 250   1700 2600
jbmc-regression/StringContains02.yml 33   1100 300
jbmc-regression/StringIndexMethods01.yml 14   320 120
jbmc-regression/StringIndexMethods02.yml 32   990 300
jbmc-regression/StringIndexMethods03.yml 34   990 310
jbmc-regression/StringIndexMethods04.yml 34   1100 320
jbmc-regression/StringIndexMethods05.yml 34   1100 290
jbmc-regression/StringMiscellaneous01.yml 110   1600 950
jbmc-regression/StringMiscellaneous02.yml 31   1000 270
jbmc-regression/StringMiscellaneous03.yml 450   2000 5400
jbmc-regression/StringMiscellaneous04.yml 900   2800 11000
jbmc-regression/StringStartEnd01.yml 42   870 350
jbmc-regression/StringStartEnd02.yml 900   3400 10000
jbmc-regression/StringStartEnd03.yml 900   3200 13000
jbmc-regression/StringValueOf01.yml 900   3400 7900
jbmc-regression/StringValueOf02.yml 460   2300 5100
jbmc-regression/StringValueOf03.yml 900   3400 8900
jbmc-regression/StringValueOf04.yml 11   340 91
jbmc-regression/StringValueOf05.yml 46   1300 470
jbmc-regression/StringValueOf06.yml 12   330 110
jbmc-regression/StringValueOf07.yml 46   1200 430
jbmc-regression/StringValueOf08.yml 54   1300 500
jbmc-regression/StringValueOf09.yml 52   1300 490
jbmc-regression/StringValueOf10.yml 450   2100 5400
jbmc-regression/SubString01.yml 17   450 140
jbmc-regression/SubString02.yml 51   1300 520
jbmc-regression/SubString03.yml 52   1300 460
jbmc-regression/TokenTest01.yml 900   3400 9000
jbmc-regression/TokenTest02.yml 900   3300 9800
jbmc-regression/Validate01.yml 18   470 150
jbmc-regression/Validate02.yml 900   2500 11000
jbmc-regression/aastore_aaload1.yml 910   3400 6500
jbmc-regression/array1.yml 900   2600 12000
jbmc-regression/array2.yml 18   450 150
jbmc-regression/arraylength1.yml 4.5 290 40
jbmc-regression/arrayread1.yml 4.8 300 45
jbmc-regression/assert1.yml 4.5 300 44
jbmc-regression/assert2.yml 7.9 300 70
jbmc-regression/assert3.yml 8.0 300 76
jbmc-regression/assert4.yml 8.0 310 77
jbmc-regression/assert5.yml 4.4 300 40
jbmc-regression/assert6.yml 4.2 300 37
jbmc-regression/astore_aload1.yml 900   4900 7000
jbmc-regression/athrow1.yml 11   320 96
jbmc-regression/basic1.yml 5.7 310 54
jbmc-regression/bitwise1.yml 8.6 320 76
jbmc-regression/boolean1.yml 3.7 240 34
jbmc-regression/boolean2.yml 5.3 320 46
jbmc-regression/bug-test-gen-095.yml 120   1600 1300
jbmc-regression/bug-test-gen-119-2.yml 12   340 98
jbmc-regression/bug-test-gen-119.yml 14   340 110
jbmc-regression/calc.yml 900   2400 11000
jbmc-regression/cast1.yml 57   1300 610
jbmc-regression/catch1.yml 4.9 290 41
jbmc-regression/char1.yml 33   950 260
jbmc-regression/charArray.yml 35   1100 300
jbmc-regression/classtest1.yml 4.2 170 38
jbmc-regression/const1.yml 3.9 250 39
jbmc-regression/constructor1.yml 19   480 160
jbmc-regression/enum1.yml 4.6 250 41
jbmc-regression/exceptions1.yml 44   1200 410
jbmc-regression/exceptions10.yml 16   460 130
jbmc-regression/exceptions11.yml 18   460 170
jbmc-regression/exceptions12.yml 15   450 120
jbmc-regression/exceptions13.yml 15   450 120
jbmc-regression/exceptions14.yml 5.1 310 45
jbmc-regression/exceptions15.yml 5.9 310 54
jbmc-regression/exceptions16.yml 12   330 100
jbmc-regression/exceptions18.yml 4.6 290 43
jbmc-regression/exceptions2.yml 12   320 90
jbmc-regression/exceptions3.yml 12   330 98
jbmc-regression/exceptions4.yml 5.1 310 50
jbmc-regression/exceptions5.yml 7.6 340 62
jbmc-regression/exceptions6.yml 4.5 170 36
jbmc-regression/exceptions7.yml 19   510 160
jbmc-regression/exceptions8.yml 18   470 160
jbmc-regression/exceptions9.yml 5.1 300 38
jbmc-regression/fcmpx_dcmpx1.yml 4.0 290 39
jbmc-regression/iarith1.yml 4.6 180 42
jbmc-regression/iarith2.yml 4.2 300 42
jbmc-regression/if_acmp1.yml 6.0 310 56
jbmc-regression/if_expr1.yml 5.1 330 46
jbmc-regression/if_icmp1.yml 5.3 320 49
jbmc-regression/ifxx1.yml 3.7 250 33
jbmc-regression/instanceof1.yml 4.0 250 43
jbmc-regression/instanceof2.yml 4.2 170 42
jbmc-regression/instanceof3.yml 3.8 250 39
jbmc-regression/instanceof4.yml 3.8 250 33
jbmc-regression/instanceof5.yml 4.3 170 41
jbmc-regression/instanceof6.yml 25   560 220
jbmc-regression/instanceof7.yml 28   660 230
jbmc-regression/instanceof8.yml 4.5 300 40
jbmc-regression/interface1.yml 12   340 110
jbmc-regression/java_append_char.yml 120   1600 1200
jbmc-regression/lazyloading4.yml 4.8 290 46
jbmc-regression/list1.yml 900   2700 11000
jbmc-regression/long1.yml 28   570 230
jbmc-regression/lookupswitch1.yml 6.9 350 62
jbmc-regression/multinewarray.yml 5.0 260 42
jbmc-regression/overloading1.yml 4.3 300 39
jbmc-regression/package1.yml 3.9 250 34
jbmc-regression/putfield_getfield1.yml 4.4 300 42
jbmc-regression/putstatic_getstatic1.yml 4.0 260 37
jbmc-regression/recursion2.yml 7.8 380 65
jbmc-regression/return1.yml 8.0 300 78
jbmc-regression/return2.yml 7.7 310 69
jbmc-regression/store_load1.yml 4.7 300 42
jbmc-regression/swap1.yml 9.7 330 84
jbmc-regression/synchronized.yml 7.6 300 75
jbmc-regression/tableswitch1.yml 6.6 340 53
jbmc-regression/uninitialised1.yml 4.0 240 40
jbmc-regression/virtual1.yml 4.3 300 44
jbmc-regression/virtual2.yml 9.9 320 95
jbmc-regression/virtual4.yml 4.6 310 39
jbmc-regression/virtual_function_unwinding.yml 5.8 310 49
jpf-regression/ExDarko_false.yml 87   1500 900
jpf-regression/ExDarko_true.yml 9.7 370 81
jpf-regression/ExException_false.yml 14   370 130
jpf-regression/ExException_true.yml 6.1 320 51
jpf-regression/ExGenSymExe_false.yml 69   1500 660
jpf-regression/ExGenSymExe_true.yml 78   1300 750
jpf-regression/ExLazy_false.yml 9.8 310 80
jpf-regression/ExLazy_true.yml 5.9 330 50
jpf-regression/ExMIT_false.yml 8.4 310 70
jpf-regression/ExMIT_true.yml 4.1 290 39
jpf-regression/ExSymExe10_false.yml 14   370 130
jpf-regression/ExSymExe10_true.yml 6.4 330 60
jpf-regression/ExSymExe11_false.yml 13   350 120
jpf-regression/ExSymExe11_true.yml 5.6 320 52
jpf-regression/ExSymExe12_false.yml 14   360 110
jpf-regression/ExSymExe12_true.yml 6.9 340 62
jpf-regression/ExSymExe13_false.yml 15   400 130
jpf-regression/ExSymExe13_true.yml 7.5 350 67
jpf-regression/ExSymExe14_false.yml 15   370 130
jpf-regression/ExSymExe14_true.yml 6.4 330 49
jpf-regression/ExSymExe15_false.yml 14   350 120
jpf-regression/ExSymExe15_true.yml 6.4 330 54
jpf-regression/ExSymExe16_false.yml 13   330 120
jpf-regression/ExSymExe16_true.yml 6.1 320 51
jpf-regression/ExSymExe17_false.yml 13   330 110
jpf-regression/ExSymExe17_true.yml 5.2 300 49
jpf-regression/ExSymExe18_false.yml 14   360 130
jpf-regression/ExSymExe18_true.yml 6.4 310 57
jpf-regression/ExSymExe19_false.yml 15   360 120
jpf-regression/ExSymExe19_true.yml 6.9 330 65
jpf-regression/ExSymExe1_false.yml 42   1100 260
jpf-regression/ExSymExe1_true.yml 5.2 310 51
jpf-regression/ExSymExe20_false.yml 23   480 210
jpf-regression/ExSymExe20_true.yml 6.0 320 51
jpf-regression/ExSymExe21_false.yml 17   420 140
jpf-regression/ExSymExe21_true.yml 5.5 310 48
jpf-regression/ExSymExe25_false.yml 15   350 130
jpf-regression/ExSymExe25_true.yml 5.6 320 50
jpf-regression/ExSymExe26_false.yml 21   410 170
jpf-regression/ExSymExe26_true.yml 5.3 310 48
jpf-regression/ExSymExe27_false.yml 14   340 110
jpf-regression/ExSymExe27_true.yml 5.4 310 50
jpf-regression/ExSymExe28_false.yml 14   340 110
jpf-regression/ExSymExe28_true.yml 5.4 310 45
jpf-regression/ExSymExe29_false.yml 40   1100 260
jpf-regression/ExSymExe29_true.yml 5.3 310 49
jpf-regression/ExSymExe2_false.yml 41   1200 280
jpf-regression/ExSymExe2_true.yml 5.3 310 48
jpf-regression/ExSymExe3_false.yml 15   340 120
jpf-regression/ExSymExe3_true.yml 5.1 310 49
jpf-regression/ExSymExe4_false.yml 38   1100 240
jpf-regression/ExSymExe4_true.yml 5.2 310 53
jpf-regression/ExSymExe5_false.yml 14   360 130
jpf-regression/ExSymExe5_true.yml 5.2 310 47
jpf-regression/ExSymExe6_false.yml 41   990 290
jpf-regression/ExSymExe6_true.yml 6.0 340 52
jpf-regression/ExSymExe7_false.yml 20   450 170
jpf-regression/ExSymExe7_true.yml 8.7 340 75
jpf-regression/ExSymExe8_false.yml 40   1100 280
jpf-regression/ExSymExe8_true.yml 5.5 320 46
jpf-regression/ExSymExe9_false.yml 14   330 130
jpf-regression/ExSymExe9_true.yml 5.2 300 53
jpf-regression/ExSymExeArrays_false.yml 20   490 150
jpf-regression/ExSymExeArrays_true.yml 23   590 210
jpf-regression/ExSymExeBool_false.yml 13   320 110
jpf-regression/ExSymExeBool_true.yml 5.1 300 43
jpf-regression/ExSymExeComplexMath_false.yml 14   420 120
jpf-regression/ExSymExeComplexMath_true.yml 15   430 120
jpf-regression/ExSymExeD2I_false.yml 16   440 120
jpf-regression/ExSymExeD2I_true.yml 6.3 310 58
jpf-regression/ExSymExeD2L_false.yml 21   550 170
jpf-regression/ExSymExeD2L_true.yml 6.0 310 47
jpf-regression/ExSymExeF2I_false.yml 15   450 130
jpf-regression/ExSymExeF2I_true.yml 6.2 310 59
jpf-regression/ExSymExeF2L_false.yml 48   1400 350
jpf-regression/ExSymExeF2L_true.yml 6.5 320 58
jpf-regression/ExSymExeFNEG_false.yml 18   470 150
jpf-regression/ExSymExeFNEG_true.yml 18   480 160
jpf-regression/ExSymExeGetStatic_false.yml 13   330 120
jpf-regression/ExSymExeGetStatic_true.yml 5.2 300 50
jpf-regression/ExSymExeI2D_false.yml 13   330 110
jpf-regression/ExSymExeI2D_true.yml 6.4 330 54
jpf-regression/ExSymExeI2F_false.yml 13   320 110
jpf-regression/ExSymExeI2F_true.yml 6.3 320 59
jpf-regression/ExSymExeLCMP_false.yml 13   320 100
jpf-regression/ExSymExeLCMP_true.yml 5.6 310 42
jpf-regression/ExSymExeLongBytecodes_false.yml 14   350 130
jpf-regression/ExSymExeLongBytecodes_true.yml 7.1 330 60
jpf-regression/ExSymExeResearch_false.yml 15   360 130
jpf-regression/ExSymExeResearch_true.yml 7.3 350 65
jpf-regression/ExSymExeSimple_false.yml 16   440 150
jpf-regression/ExSymExeSimple_true.yml 6.5 320 57
jpf-regression/ExSymExeSuzette_false.yml 15   370 130
jpf-regression/ExSymExeSuzette_true.yml 6.5 320 51
jpf-regression/ExSymExeSwitch_false.yml 9.8 320 89
jpf-regression/ExSymExeSwitch_true.yml 5.5 310 46
jpf-regression/ExSymExeTestAssignments_false.yml 9.8 310 91
jpf-regression/ExSymExeTestAssignments_true.yml 4.7 290 46
jpf-regression/ExSymExeTestClassFields_false.yml 13   320 110
jpf-regression/ExSymExeTestClassFields_true.yml 5.2 310 51
jpf-regression/ExSymExe_false.yml 13   330 100
jpf-regression/ExSymExe_true.yml 5.5 320 50
jpf-regression/TestLazy_false.yml 19   480 150
jpf-regression/TestLazy_true.yml 18   460 150
MinePump/spec1-5_product1.yml 900   3400 6600
MinePump/spec1-5_product10.yml 900   3400 5700
MinePump/spec1-5_product11.yml 900   3400 6500
MinePump/spec1-5_product12.yml 900   3500 6900
MinePump/spec1-5_product13.yml 900   3400 6700
MinePump/spec1-5_product14.yml 900   3400 6200
MinePump/spec1-5_product15.yml 900   3500 5800
MinePump/spec1-5_product16.yml 900   3400 6000
MinePump/spec1-5_product17.yml 900   3500 6500
MinePump/spec1-5_product18.yml 900   3500 6800
MinePump/spec1-5_product19.yml 910   3400 6500
MinePump/spec1-5_product2.yml 900   3400 6700
MinePump/spec1-5_product20.yml 900   3500 6800
MinePump/spec1-5_product21.yml 910   3500 6500
MinePump/spec1-5_product22.yml 900   3500 7000
MinePump/spec1-5_product23.yml 900   3500 5900
MinePump/spec1-5_product24.yml 910   3500 6100
MinePump/spec1-5_product25.yml 900   3400 6300
MinePump/spec1-5_product26.yml 900   3500 6200
MinePump/spec1-5_product27.yml 910   3500 6400
MinePump/spec1-5_product28.yml 910   3400 7200
MinePump/spec1-5_product29.yml 910   3400 6100
MinePump/spec1-5_product3.yml 900   3400 6700
MinePump/spec1-5_product30.yml 900   3500 5700
MinePump/spec1-5_product31.yml 910   3500 6100
MinePump/spec1-5_product32.yml 900   3400 6500
MinePump/spec1-5_product33.yml 900   3500 6200
MinePump/spec1-5_product34.yml 900   3400 6200
MinePump/spec1-5_product35.yml 900   3400 6000
MinePump/spec1-5_product36.yml 910   3500 5600
MinePump/spec1-5_product37.yml 910   3400 6000
MinePump/spec1-5_product38.yml 910   3500 6700
MinePump/spec1-5_product39.yml 910   3500 7100
MinePump/spec1-5_product4.yml 900   3400 6400
MinePump/spec1-5_product40.yml 910   3400 6300
MinePump/spec1-5_product41.yml 910   3500 5800
MinePump/spec1-5_product42.yml 900   3400 6500
MinePump/spec1-5_product43.yml 900   3400 6800
MinePump/spec1-5_product44.yml 900   3400 6900
MinePump/spec1-5_product45.yml 900   3500 7100
MinePump/spec1-5_product46.yml 910   3500 7400
MinePump/spec1-5_product47.yml 900   3500 6600
MinePump/spec1-5_product48.yml 900   3400 6500
MinePump/spec1-5_product49.yml 900   3500 6500
MinePump/spec1-5_product5.yml 900   3400 6500
MinePump/spec1-5_product50.yml 910   3500 6600
MinePump/spec1-5_product51.yml 910   3500 5800
MinePump/spec1-5_product52.yml 900   3400 6000
MinePump/spec1-5_product53.yml 900   3500 6400
MinePump/spec1-5_product54.yml 900   3400 6200
MinePump/spec1-5_product55.yml 910   3400 6000
MinePump/spec1-5_product56.yml 910   3400 6100
MinePump/spec1-5_product57.yml 910   3400 6000
MinePump/spec1-5_product58.yml 910   3500 5900
MinePump/spec1-5_product59.yml 900   3400 5100
MinePump/spec1-5_product6.yml 900   3400 5800
MinePump/spec1-5_product60.yml 900   3300 6800
MinePump/spec1-5_product61.yml 900   3500 6400
MinePump/spec1-5_product62.yml 910   3400 6400
MinePump/spec1-5_product63.yml 910   3400 6900
MinePump/spec1-5_product64.yml 910   3400 6500
MinePump/spec1-5_product7.yml 910   3500 6400
MinePump/spec1-5_product8.yml 910   3500 7000
MinePump/spec1-5_product9.yml 900   3400 6800
../sv-benchmarks/java/ status cpu (s) mem (MB) energy (J)
total 368 96000   480000 830000
    correct results 186 2100   72000 18000
        correct true 109 800   37000 7100
        correct false 77 1300   34000 11000
    incorrect results 2 120   2800 1100
        incorrect true 1 120   2500 990
        incorrect false 1 7.6 300 75
Run set sv-comp19_prop-reachsafety_java.ReachSafety-Java