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