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