Tool JBMC 5.10 (cbmc-5.10-1744-gdf5e3b8-dirty)
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:33:09 CET
Run set sv-comp19_prop-reachsafety_java.ReachSafety-Java
../sv-benchmarks/java/ status cpu (s) mem (MB) energy (J)
jayhorn-recursive/Ackermann01.yml 1.1  51 9.8
jayhorn-recursive/Addition.yml 880    7100 7400  
jayhorn-recursive/InfiniteLoop.yml 1.1  51 9.6
jayhorn-recursive/SatAckermann01.yml 880    270 6400  
jayhorn-recursive/SatAckermann02.yml 880    270 5500  
jayhorn-recursive/SatAckermann03.yml 880    270 5300  
jayhorn-recursive/SatAddition01.yml 880    2000 4700  
jayhorn-recursive/SatEvenOdd01.yml 880    390 8300  
jayhorn-recursive/SatFibonacci01.yml 880    160 5200  
jayhorn-recursive/SatFibonacci02.yml 2.0  51 19  
jayhorn-recursive/SatFibonacci03.yml 880    160 7500  
jayhorn-recursive/SatGcd.yml 880    2500 6700  
jayhorn-recursive/SatHanoi01.yml 880    210 6400  
jayhorn-recursive/SatMccarthy91.yml 880    210 4500  
jayhorn-recursive/SatMultCommutative01.yml 880    570 4600  
jayhorn-recursive/SatPrimes01.yml 880    220 5800  
jayhorn-recursive/UnsatAckermann01.yml 7.4  91 76  
jayhorn-recursive/UnsatAddition01.yml 1.0  51 9.3
jayhorn-recursive/UnsatAddition02.yml 880    11000 8900  
jayhorn-recursive/UnsatEvenOdd01.yml 1.0  51 9.9
jayhorn-recursive/UnsatFibonacci01.yml 2.6  54 28  
jayhorn-recursive/UnsatFibonacci02.yml 880    160 5500  
jayhorn-recursive/UnsatMccarthy91.yml 1.1  51 9.6
jbmc-regression/ArithmeticException1.yml 1.1  52 11  
jbmc-regression/ArithmeticException5.yml 1.4  50 13  
jbmc-regression/ArithmeticException6.yml 1.1  51 11  
jbmc-regression/ArrayIndexOutOfBoundsException1.yml .99 51 9.7
jbmc-regression/ArrayIndexOutOfBoundsException2.yml .99 51 10  
jbmc-regression/ArrayIndexOutOfBoundsException3.yml 1.0  51 9.7
jbmc-regression/BufferedReaderReadLine.yml 1.2  51 11  
jbmc-regression/CharSequenceBug.yml 1.1  51 10  
jbmc-regression/CharSequenceToString.yml 1.8  51 21  
jbmc-regression/ClassCastException1.yml 1.1  51 11  
jbmc-regression/ClassCastException2.yml 1.5  51 16  
jbmc-regression/ClassCastException3.yml 1.1  50 11  
jbmc-regression/Class_method1.yml 1.5  51 16  
jbmc-regression/Inheritance1.yml 1.6  51 16  
jbmc-regression/NegativeArraySizeException1.yml 1.0  51 8.5
jbmc-regression/NegativeArraySizeException2.yml 1.1  58 11  
jbmc-regression/NullPointerException1.yml 1.5  51 15  
jbmc-regression/NullPointerException2.yml 1.0  50 9.4
jbmc-regression/NullPointerException3.yml 1.0  51 9.0
jbmc-regression/NullPointerException4.yml 1.1  50 10  
jbmc-regression/RegexMatches01.yml 1.2  52 10  
jbmc-regression/RegexMatches02.yml 1.2  52 9.7
jbmc-regression/RegexSubstitution01.yml 99    8200 1200  
jbmc-regression/RegexSubstitution02.yml 120    13000 1300  
jbmc-regression/RegexSubstitution03.yml 2.7  110 30  
jbmc-regression/StaticCharMethods01.yml 2.3  53 32  
jbmc-regression/StaticCharMethods02.yml 1.7  64 17  
jbmc-regression/StaticCharMethods03.yml 1.6  56 22  
jbmc-regression/StaticCharMethods04.yml 1.2  52 12  
jbmc-regression/StaticCharMethods05.yml 2.7  73 27  
jbmc-regression/StaticCharMethods06.yml 4.3  62 48  
jbmc-regression/StringBuilderAppend01.yml 1.4  55 14  
jbmc-regression/StringBuilderAppend02.yml 880    170 12000  
jbmc-regression/StringBuilderCapLen01.yml 1.1  51 11  
jbmc-regression/StringBuilderCapLen02.yml 1.1  51 10  
jbmc-regression/StringBuilderCapLen03.yml 1.0  51 9.9
jbmc-regression/StringBuilderCapLen04.yml 1.0  50 11  
jbmc-regression/StringBuilderChars01.yml 7.7  450 110  
jbmc-regression/StringBuilderChars02.yml 1.1  51 12  
jbmc-regression/StringBuilderChars03.yml 1.0  51 8.9
jbmc-regression/StringBuilderChars04.yml 1.4  53 12  
jbmc-regression/StringBuilderChars05.yml 1.2  52 12  
jbmc-regression/StringBuilderChars06.yml 1.1  51 12  
jbmc-regression/StringBuilderConstructors01.yml 1.7  51 21  
jbmc-regression/StringBuilderConstructors02.yml 1.1  51 10  
jbmc-regression/StringBuilderInsertDelete01.yml 880    130 12000  
jbmc-regression/StringBuilderInsertDelete02.yml 880    120 13000  
jbmc-regression/StringBuilderInsertDelete03.yml 880    130 12000  
jbmc-regression/StringCompare01.yml 1.3  52 15  
jbmc-regression/StringCompare02.yml 1.0  51 11  
jbmc-regression/StringCompare03.yml 1.1  51 11  
jbmc-regression/StringCompare04.yml 1.2  60 12  
jbmc-regression/StringCompare05.yml 1.0  51 10  
jbmc-regression/StringConcatenation01.yml 10    100 130  
jbmc-regression/StringConcatenation02.yml 1.5  57 15  
jbmc-regression/StringConcatenation03.yml 1.2  53 13  
jbmc-regression/StringConcatenation04.yml 1.2  52 11  
jbmc-regression/StringConstructors01.yml 3.6  71 46  
jbmc-regression/StringConstructors02.yml 1.1  51 9.6
jbmc-regression/StringConstructors03.yml 1.2  52 13  
jbmc-regression/StringConstructors04.yml 1.7  52 19  
jbmc-regression/StringConstructors05.yml 2.5  57 28  
jbmc-regression/StringContains01.yml .99 51 11  
jbmc-regression/StringContains02.yml 1.0  51 11  
jbmc-regression/StringIndexMethods01.yml 6.5  81 68  
jbmc-regression/StringIndexMethods02.yml 1.2  51 11  
jbmc-regression/StringIndexMethods03.yml 1.1  59 10  
jbmc-regression/StringIndexMethods04.yml 1.1  52 11  
jbmc-regression/StringIndexMethods05.yml 1.1  51 11  
jbmc-regression/StringMiscellaneous01.yml 13    66 150  
jbmc-regression/StringMiscellaneous02.yml 1.0  59 8.9
jbmc-regression/StringMiscellaneous03.yml 1.7  67 19  
jbmc-regression/StringMiscellaneous04.yml 4.7  64 66  
jbmc-regression/StringStartEnd01.yml 3.6  65 39  
jbmc-regression/StringStartEnd02.yml 1.7  51 19  
jbmc-regression/StringStartEnd03.yml 1.9  55 20  
jbmc-regression/StringValueOf01.yml 2.2  110 28  
jbmc-regression/StringValueOf02.yml 2.1  92 20  
jbmc-regression/StringValueOf03.yml 2.9  110 33  
jbmc-regression/StringValueOf04.yml 1.1  51 10  
jbmc-regression/StringValueOf05.yml 1.3  52 13  
jbmc-regression/StringValueOf06.yml 1.1  51 10  
jbmc-regression/StringValueOf07.yml 1.7  54 20  
jbmc-regression/StringValueOf08.yml 2.1  160 22  
jbmc-regression/StringValueOf09.yml 1.9  160 21  
jbmc-regression/StringValueOf10.yml 1.1  51 10  
jbmc-regression/SubString01.yml 2.0  52 22  
jbmc-regression/SubString02.yml 1.2  52 11  
jbmc-regression/SubString03.yml 1.1  52 11  
jbmc-regression/TokenTest01.yml 86    790 1000  
jbmc-regression/TokenTest02.yml 260    13000 3500  
jbmc-regression/Validate01.yml 1.2  52 12  
jbmc-regression/Validate02.yml 1.2  51 11  
jbmc-regression/aastore_aaload1.yml 540    14000 6800  
jbmc-regression/array1.yml 230    14000 2900  
jbmc-regression/array2.yml 1.9  51 24  
jbmc-regression/arraylength1.yml 1.6  51 17  
jbmc-regression/arrayread1.yml 1.6  51 16  
jbmc-regression/assert1.yml 1.9  51 20  
jbmc-regression/assert2.yml 1.1  51 9.4
jbmc-regression/assert3.yml 1.0  51 11  
jbmc-regression/assert4.yml 1.1  51 9.9
jbmc-regression/assert5.yml 1.7  51 18  
jbmc-regression/assert6.yml 1.5  51 17  
jbmc-regression/astore_aload1.yml 9.4  120 110  
jbmc-regression/athrow1.yml 1.0  51 8.8
jbmc-regression/basic1.yml 1.5  51 17  
jbmc-regression/bitwise1.yml 1.5  51 16  
jbmc-regression/boolean1.yml 1.5  51 16  
jbmc-regression/boolean2.yml 1.6  51 17  
jbmc-regression/bug-test-gen-095.yml 1.2  51 11  
jbmc-regression/bug-test-gen-119-2.yml 3.0  53 34  
jbmc-regression/bug-test-gen-119.yml 1.8  51 18  
jbmc-regression/calc.yml 880    340 8900  
jbmc-regression/cast1.yml 1.9  52 22  
jbmc-regression/catch1.yml 1.5  51 17  
jbmc-regression/char1.yml 1.9  59 24  
jbmc-regression/charArray.yml 6.9  170 90  
jbmc-regression/classtest1.yml 1.4  50 15  
jbmc-regression/const1.yml 1.6  51 18  
jbmc-regression/constructor1.yml 1.6  52 16  
jbmc-regression/enum1.yml 1.9  51 21  
jbmc-regression/exceptions1.yml 1.1  51 10  
jbmc-regression/exceptions10.yml 1.1  51 10  
jbmc-regression/exceptions11.yml 1.0  51 9.8
jbmc-regression/exceptions12.yml 1.1  51 10  
jbmc-regression/exceptions13.yml 1.1  51 11  
jbmc-regression/exceptions14.yml 1.5  51 19  
jbmc-regression/exceptions15.yml 1.6  51 16  
jbmc-regression/exceptions16.yml 1.2  51 11  
jbmc-regression/exceptions18.yml 1.6  51 17  
jbmc-regression/exceptions2.yml 1.1  51 8.9
jbmc-regression/exceptions3.yml 1.0  51 9.9
jbmc-regression/exceptions4.yml 1.5  51 17  
jbmc-regression/exceptions5.yml 1.7  51 17  
jbmc-regression/exceptions6.yml 1.1  51 9.2
jbmc-regression/exceptions7.yml 1.1  51 9.7
jbmc-regression/exceptions8.yml 1.1  51 9.3
jbmc-regression/exceptions9.yml 1.6  51 17  
jbmc-regression/fcmpx_dcmpx1.yml 1.5  51 15  
jbmc-regression/iarith1.yml 1.5  51 17  
jbmc-regression/iarith2.yml 1.6  51 18  
jbmc-regression/if_acmp1.yml 1.6  52 22  
jbmc-regression/if_expr1.yml 1.6  51 18  
jbmc-regression/if_icmp1.yml 1.7  51 18  
jbmc-regression/ifxx1.yml 1.5  51 17  
jbmc-regression/instanceof1.yml 1.5  51 14  
jbmc-regression/instanceof2.yml 1.7  51 15  
jbmc-regression/instanceof3.yml 1.6  51 16  
jbmc-regression/instanceof4.yml 1.5  51 14  
jbmc-regression/instanceof5.yml 1.4  51 16  
jbmc-regression/instanceof6.yml 1.6  51 20  
jbmc-regression/instanceof7.yml 1.6  51 19  
jbmc-regression/instanceof8.yml 1.8  51 21  
jbmc-regression/interface1.yml 1.1  51 9.8
jbmc-regression/java_append_char.yml 1.9  56 21  
jbmc-regression/lazyloading4.yml 1.5  58 15  
jbmc-regression/list1.yml 50    190 600  
jbmc-regression/long1.yml 1.5  59 15  
jbmc-regression/lookupswitch1.yml 1.6  51 18  
jbmc-regression/multinewarray.yml 2.9  55 33  
jbmc-regression/overloading1.yml 1.5  51 14  
jbmc-regression/package1.yml 1.5  51 14  
jbmc-regression/putfield_getfield1.yml 1.5  51 15  
jbmc-regression/putstatic_getstatic1.yml 1.5  51 16  
jbmc-regression/recursion2.yml 1.8  51 20  
jbmc-regression/return1.yml 1.0  51 11  
jbmc-regression/return2.yml 1.1  51 11  
jbmc-regression/store_load1.yml 1.6  52 16  
jbmc-regression/swap1.yml 1.4  51 14  
jbmc-regression/synchronized.yml 1.5  51 15  
jbmc-regression/tableswitch1.yml 1.6  52 16  
jbmc-regression/uninitialised1.yml 1.5  51 16  
jbmc-regression/virtual1.yml 1.5  51 18  
jbmc-regression/virtual2.yml 1.0  51 12  
jbmc-regression/virtual4.yml 1.5  51 14  
jbmc-regression/virtual_function_unwinding.yml 1.6  51 16  
jpf-regression/ExDarko_false.yml 1.2  51 12  
jpf-regression/ExDarko_true.yml 1.9  52 23  
jpf-regression/ExException_false.yml 1.1  58 10  
jpf-regression/ExException_true.yml 1.7  51 21  
jpf-regression/ExGenSymExe_false.yml 1.1  51 10  
jpf-regression/ExGenSymExe_true.yml 1.7  51 18  
jpf-regression/ExLazy_false.yml 1.2  59 15  
jpf-regression/ExLazy_true.yml 1.6  51 17  
jpf-regression/ExMIT_false.yml 1.0  51 9.2
jpf-regression/ExMIT_true.yml 1.5  51 17  
jpf-regression/ExSymExe10_false.yml 1.1  51 11  
jpf-regression/ExSymExe10_true.yml 1.6  51 17  
jpf-regression/ExSymExe11_false.yml 1.1  51 9.8
jpf-regression/ExSymExe11_true.yml 1.6  51 16  
jpf-regression/ExSymExe12_false.yml 1.1  51 11  
jpf-regression/ExSymExe12_true.yml 1.8  51 18  
jpf-regression/ExSymExe13_false.yml 1.1  51 10  
jpf-regression/ExSymExe13_true.yml 1.7  52 19  
jpf-regression/ExSymExe14_false.yml 1.1  51 11  
jpf-regression/ExSymExe14_true.yml 1.7  51 19  
jpf-regression/ExSymExe15_false.yml 1.2  51 10  
jpf-regression/ExSymExe15_true.yml 1.6  51 21  
jpf-regression/ExSymExe16_false.yml 1.1  52 12  
jpf-regression/ExSymExe16_true.yml 1.6  51 17  
jpf-regression/ExSymExe17_false.yml 1.1  51 9.4
jpf-regression/ExSymExe17_true.yml 1.7  51 17  
jpf-regression/ExSymExe18_false.yml 1.2  51 9.8
jpf-regression/ExSymExe18_true.yml 1.6  51 17  
jpf-regression/ExSymExe19_false.yml 1.2  52 13  
jpf-regression/ExSymExe19_true.yml 1.7  51 16  
jpf-regression/ExSymExe1_false.yml 1.2  53 11  
jpf-regression/ExSymExe1_true.yml 1.5  51 16  
jpf-regression/ExSymExe20_false.yml 1.2  52 10  
jpf-regression/ExSymExe20_true.yml 1.6  51 20  
jpf-regression/ExSymExe21_false.yml 1.1  51 11  
jpf-regression/ExSymExe21_true.yml 1.6  51 19  
jpf-regression/ExSymExe25_false.yml 1.0  51 9.1
jpf-regression/ExSymExe25_true.yml 1.6  59 17  
jpf-regression/ExSymExe26_false.yml 1.2  53 12  
jpf-regression/ExSymExe26_true.yml 1.6  51 17  
jpf-regression/ExSymExe27_false.yml 1.1  51 11  
jpf-regression/ExSymExe27_true.yml 1.6  51 19  
jpf-regression/ExSymExe28_false.yml 1.1  51 8.6
jpf-regression/ExSymExe28_true.yml 1.6  59 15  
jpf-regression/ExSymExe29_false.yml 1.1  51 11  
jpf-regression/ExSymExe29_true.yml 1.6  51 19  
jpf-regression/ExSymExe2_false.yml 1.1  51 9.9
jpf-regression/ExSymExe2_true.yml 1.7  52 16  
jpf-regression/ExSymExe3_false.yml 1.1  51 10  
jpf-regression/ExSymExe3_true.yml 1.7  51 21  
jpf-regression/ExSymExe4_false.yml 1.2  51 11  
jpf-regression/ExSymExe4_true.yml 1.6  51 16  
jpf-regression/ExSymExe5_false.yml 1.1  51 12  
jpf-regression/ExSymExe5_true.yml 1.6  51 18  
jpf-regression/ExSymExe6_false.yml 1.1  61 11  
jpf-regression/ExSymExe6_true.yml 1.6  51 19  
jpf-regression/ExSymExe7_false.yml 1.1  52 11  
jpf-regression/ExSymExe7_true.yml 1.7  51 19  
jpf-regression/ExSymExe8_false.yml 1.1  51 12  
jpf-regression/ExSymExe8_true.yml 1.5  51 19  
jpf-regression/ExSymExe9_false.yml 1.1  51 9.7
jpf-regression/ExSymExe9_true.yml 1.6  51 17  
jpf-regression/ExSymExeArrays_false.yml 1.1  51 11  
jpf-regression/ExSymExeArrays_true.yml 1.6  51 17  
jpf-regression/ExSymExeBool_false.yml 1.2  51 10  
jpf-regression/ExSymExeBool_true.yml 1.5  51 15  
jpf-regression/ExSymExeComplexMath_false.yml 1.1  52 10  
jpf-regression/ExSymExeComplexMath_true.yml 1.6  52 18  
jpf-regression/ExSymExeD2I_false.yml 1.0  51 9.3
jpf-regression/ExSymExeD2I_true.yml 1.7  59 18  
jpf-regression/ExSymExeD2L_false.yml 1.0  51 8.9
jpf-regression/ExSymExeD2L_true.yml 1.6  51 18  
jpf-regression/ExSymExeF2I_false.yml .99 51 9.1
jpf-regression/ExSymExeF2I_true.yml 1.6  51 20  
jpf-regression/ExSymExeF2L_false.yml 1.1  51 9.6
jpf-regression/ExSymExeF2L_true.yml 1.7  51 20  
jpf-regression/ExSymExeFNEG_false.yml 1.1  51 12  
jpf-regression/ExSymExeFNEG_true.yml 1.6  51 20  
jpf-regression/ExSymExeGetStatic_false.yml 1.2  52 9.3
jpf-regression/ExSymExeGetStatic_true.yml 1.6  51 15  
jpf-regression/ExSymExeI2D_false.yml 1.1  51 10  
jpf-regression/ExSymExeI2D_true.yml 1.7  51 15  
jpf-regression/ExSymExeI2F_false.yml 1.1  51 8.7
jpf-regression/ExSymExeI2F_true.yml 1.6  52 16  
jpf-regression/ExSymExeLCMP_false.yml 1.0  51 9.6
jpf-regression/ExSymExeLCMP_true.yml 1.6  51 17  
jpf-regression/ExSymExeLongBytecodes_false.yml 1.0  51 10  
jpf-regression/ExSymExeLongBytecodes_true.yml 1.8  52 18  
jpf-regression/ExSymExeResearch_false.yml 1.0  51 11  
jpf-regression/ExSymExeResearch_true.yml 1.6  51 17  
jpf-regression/ExSymExeSimple_false.yml 1.1  51 12  
jpf-regression/ExSymExeSimple_true.yml 1.7  51 19  
jpf-regression/ExSymExeSuzette_false.yml 1.0  51 9.3
jpf-regression/ExSymExeSuzette_true.yml 1.6  51 18  
jpf-regression/ExSymExeSwitch_false.yml 1.0  51 11  
jpf-regression/ExSymExeSwitch_true.yml 1.6  51 16  
jpf-regression/ExSymExeTestAssignments_false.yml 1.0  51 10  
jpf-regression/ExSymExeTestAssignments_true.yml 1.5  51 16  
jpf-regression/ExSymExeTestClassFields_false.yml 1.1  59 11  
jpf-regression/ExSymExeTestClassFields_true.yml 1.6  51 15  
jpf-regression/ExSymExe_false.yml 1.2  52 11  
jpf-regression/ExSymExe_true.yml 1.6  53 16  
jpf-regression/TestLazy_false.yml 1.2  51 12  
jpf-regression/TestLazy_true.yml 1.7  51 20  
MinePump/spec1-5_product1.yml 5.3  93 61  
MinePump/spec1-5_product10.yml 5.3  94 58  
MinePump/spec1-5_product11.yml 130    560 1400  
MinePump/spec1-5_product12.yml 130    560 1500  
MinePump/spec1-5_product13.yml 5.5  93 72  
MinePump/spec1-5_product14.yml 5.4  92 66  
MinePump/spec1-5_product15.yml 150    600 1700  
MinePump/spec1-5_product16.yml 150    600 1700  
MinePump/spec1-5_product17.yml 5.4  93 63  
MinePump/spec1-5_product18.yml 5.4  92 64  
MinePump/spec1-5_product19.yml 150    590 1700  
MinePump/spec1-5_product2.yml 5.5  92 75  
MinePump/spec1-5_product20.yml 160    600 1800  
MinePump/spec1-5_product21.yml 5.6  95 65  
MinePump/spec1-5_product22.yml 5.6  94 68  
MinePump/spec1-5_product23.yml 180    650 1700  
MinePump/spec1-5_product24.yml 190    650 2100  
MinePump/spec1-5_product25.yml 5.3  92 64  
MinePump/spec1-5_product26.yml 5.6  92 75  
MinePump/spec1-5_product27.yml 150    600 1700  
MinePump/spec1-5_product28.yml 150    600 1800  
MinePump/spec1-5_product29.yml 5.4  93 65  
MinePump/spec1-5_product3.yml 130    550 1600  
MinePump/spec1-5_product30.yml 5.5  94 65  
MinePump/spec1-5_product31.yml 170    650 2000  
MinePump/spec1-5_product32.yml 180    650 1700  
MinePump/spec1-5_product33.yml 120    540 1300  
MinePump/spec1-5_product34.yml 120    540 1400  
MinePump/spec1-5_product35.yml 160    600 1700  
MinePump/spec1-5_product36.yml 160    610 1800  
MinePump/spec1-5_product37.yml 130    590 1600  
MinePump/spec1-5_product38.yml 140    580 1800  
MinePump/spec1-5_product39.yml 180    650 1600  
MinePump/spec1-5_product4.yml 130    570 1600  
MinePump/spec1-5_product40.yml 180    660 1800  
MinePump/spec1-5_product41.yml 120    560 1400  
MinePump/spec1-5_product42.yml 130    570 1400  
MinePump/spec1-5_product43.yml 160    640 2600  
MinePump/spec1-5_product44.yml 180    640 2000  
MinePump/spec1-5_product45.yml 150    600 2000  
MinePump/spec1-5_product46.yml 150    600 1700  
MinePump/spec1-5_product47.yml 200    690 2800  
MinePump/spec1-5_product48.yml 210    690 2700  
MinePump/spec1-5_product49.yml 130    580 1400  
MinePump/spec1-5_product5.yml 5.3  92 60  
MinePump/spec1-5_product50.yml 140    580 1600  
MinePump/spec1-5_product51.yml 180    650 1900  
MinePump/spec1-5_product52.yml 190    660 2100  
MinePump/spec1-5_product53.yml 160    620 2400  
MinePump/spec1-5_product54.yml 160    620 2200  
MinePump/spec1-5_product55.yml 230    710 2800  
MinePump/spec1-5_product56.yml 230    710 3100  
MinePump/spec1-5_product57.yml 250    610 2800  
MinePump/spec1-5_product58.yml 250    620 3000  
MinePump/spec1-5_product59.yml 340    700 3800  
MinePump/spec1-5_product6.yml 5.4  92 76  
MinePump/spec1-5_product60.yml 360    710 3900  
MinePump/spec1-5_product61.yml 310    650 3900  
MinePump/spec1-5_product62.yml 310    650 3900  
MinePump/spec1-5_product63.yml 450    750 4700  
MinePump/spec1-5_product64.yml 460    760 4800  
MinePump/spec1-5_product7.yml 150    590 1700  
MinePump/spec1-5_product8.yml 150    590 1700  
MinePump/spec1-5_product9.yml 5.2  91 67  
../sv-benchmarks/java/ status cpu (s) mem (MB) energy (J)
total 368 28000 140000 280000
    correct results 331 9700 47000 110000
        correct true 139 3100 14000 36000
        correct false 192 6600 33000 77000
    incorrect results 0
        incorrect true 0
        incorrect false 0
Run set sv-comp19_prop-reachsafety_java.ReachSafety-Java