Tool JayHorn 0.5.1 JBMC 5.9 (cbmc-5.9-3c2e55e) JPF rev 32
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host localhost
OS Linux 4.4.0-131-generic x86_64
System CPU: Intel Core i7-6700HQ CPU @ 2.60GHz with 8 cores, frequency: 3500 MHz, Turbo Boost enabled; RAM: 16014020 kB
Date of execution 2018-07-29 02:53:52 BST 2018-07-28 18:40:30 BST 2018-07-29 16:02:12 BST
Run set jayhorn.sv-comp18 jbmc.sv-comp18 jpf.sv-comp18
sv-benchmarks/java/ status cputime walltime memUsage status cputime walltime memUsage status cputime walltime memUsage
jbmc-regression/ArithmeticException1_false-assert.jar true 2.895s 1.657s 195948544 false(reach) 0.260s 0.273s 43819008 false(reach) 1.011s 0.595s 67473408
jbmc-regression/ArithmeticException5_true-assert.jar true 2.308s 1.345s 152911872 true 0.346s 0.365s 43417600 false(reach) 0.998s 0.612s 66256896
jbmc-regression/ArithmeticException6_false-assert.jar true 2.345s 1.346s 150769664 false(reach) 0.304s 0.328s 43786240 true 0.938s 0.584s 64716800
jbmc-regression/ArrayIndexOutOfBoundsException1_false-assert.jar false(reach) 4.108s 2.300s 197890048 false(reach) 0.297s 0.308s 44023808 true 1.011s 0.601s 66256896
jbmc-regression/ArrayIndexOutOfBoundsException2_false-assert.jar false(reach) 4.161s 2.296s 193990656 false(reach) 0.301s 0.316s 43749376 true 0.979s 0.590s 63488000
jbmc-regression/ArrayIndexOutOfBoundsException3_false-assert.jar false(reach) 5.137s 2.827s 230653952 false(reach) 0.311s 0.324s 43880448 true 0.918s 0.577s 64274432
jbmc-regression/BufferedReaderReadLine_false-assert.jar false(reach) 7.010s 3.658s 260804608 false(reach) 0.439s 0.447s 44457984 true 1.006s 0.616s 67321856
jbmc-regression/CharSequenceBug_false-assert.jar false(reach) 4.433s 2.416s 192462848 false(reach) 0.387s 0.402s 44269568 true 0.959s 0.597s 63365120
jbmc-regression/CharSequenceToString_true-assert.jar false(reach) 4.515s 2.493s 193818624 true 0.712s 0.731s 44658688 true 0.970s 0.580s 63336448
jbmc-regression/ClassCastException1_false-assert.jar false(reach) 3.961s 2.215s 194396160 false(reach) 0.328s 0.335s 44134400 false(reach) 1.000s 0.604s 64888832
jbmc-regression/ClassCastException2_true-assert.jar true 4.357s 2.356s 189190144 true 0.442s 0.456s 44097536 true 0.950s 0.581s 64630784
jbmc-regression/ClassCastException3_false-assert.jar false(reach) 3.969s 2.186s 192733184 false(reach) 0.297s 0.316s 43929600 false(reach) 0.950s 0.584s 64626688
jbmc-regression/Class_method1_true-assert.jar true 3.129s 1.754s 184451072 true 0.467s 0.486s 43941888 true 0.920s 0.568s 63279104
jbmc-regression/Inheritance1_true-assert.jar true 5.023s 2.652s 217104384 true 0.459s 0.471s 44077056 true 0.950s 0.578s 64221184
jbmc-regression/NegativeArraySizeException1_false-assert.jar true 2.399s 1.394s 153817088 false(reach) 0.291s 0.303s 43745280 false(reach) 0.961s 0.578s 64442368
jbmc-regression/NegativeArraySizeException2_false-assert.jar true 2.205s 1.305s 153120768 false(reach) 0.285s 0.312s 43921408 false(reach) 0.985s 0.605s 63938560
jbmc-regression/NullPointerException1_true-assert.jar unknown 1.303s 0.761s 116211712 true 0.431s 0.441s 43900928 false(reach) 0.952s 0.595s 63512576
jbmc-regression/NullPointerException2_false-assert.jar unknown 1.273s 0.736s 115384320 false(reach) 0.286s 0.294s 43929600 false(reach) 0.949s 0.575s 64266240
jbmc-regression/NullPointerException3_false-assert.jar unknown 1.325s 0.752s 115838976 false(reach) 0.266s 0.275s 43737088 false(reach) 0.973s 0.574s 63655936
jbmc-regression/NullPointerException4_false-assert.jar unknown 1.218s 0.700s 114372608 false(reach) 0.282s 0.296s 43929600 false(reach) 1.002s 0.613s 64077824
jbmc-regression/RegexMatches01_true-assert.jar false(reach) 5.222s 2.814s 195457024 false(reach) 38.274s 38.288s 237780992 true 1.001s 0.620s 63860736
jbmc-regression/RegexMatches02_false-assert.jar false(reach) 6.126s 3.235s 218169344 false(reach) 38.763s 38.780s 243040256 true 0.974s 0.603s 63315968
jbmc-regression/RegexSubstitution01_true-assert.jar false(reach) 10.211s 5.299s 412655616 true 4.537s 4.554s 117723136 true 1.038s 0.645s 65220608
jbmc-regression/RegexSubstitution02_false-assert.jar false(reach) 9.948s 5.200s 384372736 true 4.592s 4.612s 89309184 true 0.978s 0.598s 64528384
jbmc-regression/RegexSubstitution03_true-assert.jar false(reach) 7.912s 4.162s 297971712 true 1.741s 1.765s 49369088 true 1.068s 0.638s 65187840
jbmc-regression/StaticCharMethods01_true-assert.jar false(reach) 4.988s 2.604s 233947136 true 0.944s 0.966s 46419968 true 0.966s 0.579s 62652416
jbmc-regression/StaticCharMethods02_false-assert.jar false(reach) 5.032s 2.683s 210714624 false(reach) 1.094s 1.104s 53043200 true 0.960s 0.585s 63422464
jbmc-regression/StaticCharMethods03_false-assert.jar false(reach) 4.816s 2.622s 198123520 false(reach) 1.084s 1.096s 51294208 true 1.022s 0.632s 64135168
jbmc-regression/StaticCharMethods04_false-assert.jar false(reach) 4.843s 2.636s 200192000 false(reach) 1.046s 1.055s 51044352 true 0.906s 0.551s 63311872
jbmc-regression/StaticCharMethods05_false-assert.jar false(reach) 7.822s 4.077s 278511616 false(reach) 1.824s 1.833s 59617280 unknown 0.986s 0.598s 60248064
jbmc-regression/StaticCharMethods06_true-assert.jar false(reach) 6.272s 3.271s 237772800 true 2.687s 2.697s 53399552 true 1.008s 0.624s 64339968
jbmc-regression/StringBuilderAppend01_true-assert.jar false(reach) 15.775s 8.096s 521629696 unknown 874.936s 875.035s 63283200 true 1.008s 0.610s 65589248
jbmc-regression/StringBuilderAppend02_false-assert.jar false(reach) 16.517s 8.540s 539189248 unknown 874.962s 875.030s 129449984 true 1.007s 0.616s 63279104
jbmc-regression/StringBuilderCapLen01_true-assert.jar false(reach) 5.024s 2.724s 201596928 false(reach) 0.383s 0.388s 44445696 true 0.977s 0.593s 64712704
jbmc-regression/StringBuilderCapLen02_false-assert.jar false(reach) 5.417s 2.896s 202170368 false(reach) 0.338s 0.366s 44212224 true 0.942s 0.577s 65617920
jbmc-regression/StringBuilderCapLen03_false-assert.jar false(reach) 5.092s 2.694s 211800064 false(reach) 0.307s 0.326s 44081152 true 0.947s 0.582s 63275008
jbmc-regression/StringBuilderCapLen04_false-assert.jar false(reach) 5.273s 2.813s 207589376 false(reach) 0.306s 0.312s 44134400 true 0.940s 0.580s 62439424
jbmc-regression/StringBuilderChars01_true-assert.jar false(reach) 7.307s 3.812s 275435520 false(reach) 0.479s 0.490s 44728320 true 1.013s 0.604s 65175552
jbmc-regression/StringBuilderChars02_false-assert.jar false(reach) 5.234s 2.859s 202293248 false(reach) 0.328s 0.331s 44261376 true 0.973s 0.597s 63217664
jbmc-regression/StringBuilderChars03_false-assert.jar false(reach) 5.032s 2.754s 195198976 false(reach) 0.320s 0.330s 44077056 true 0.970s 0.601s 63328256
jbmc-regression/StringBuilderChars04_false-assert.jar false(reach) 7.555s 4.000s 268259328 false(reach) 2.058s 2.065s 53182464 true 0.989s 0.590s 64303104
jbmc-regression/StringBuilderChars05_false-assert.jar false(reach) 5.559s 3.003s 197734400 false(reach) 0.351s 0.367s 44204032 true 0.955s 0.586s 63377408
jbmc-regression/StringBuilderChars06_false-assert.jar false(reach) 5.771s 3.040s 214429696 false(reach) 0.347s 0.363s 44261376 true 0.923s 0.573s 63377408
jbmc-regression/StringBuilderConstructors01_true-assert.jar false(reach) 5.539s 2.960s 200265728 true 0.731s 0.747s 44924928 true 0.989s 0.617s 63533056
jbmc-regression/StringBuilderConstructors02_false-assert.jar false(reach) 5.782s 3.032s 216121344 false(reach) 0.371s 0.384s 44470272 true 0.974s 0.601s 64122880
jbmc-regression/StringBuilderInsertDelete01_true-assert.jar false(reach) 15.210s 7.869s 494309376 unknown 874.959s 875.036s 110702592 true 1.219s 0.734s 66805760
jbmc-regression/StringBuilderInsertDelete02_false-assert.jar false(reach) 9.589s 5.029s 357441536 unknown 874.935s 875.031s 105070592 true 1.069s 0.661s 63287296
jbmc-regression/StringBuilderInsertDelete03_false-assert.jar false(reach) 9.375s 4.863s 358379520 unknown 874.933s 875.022s 112689152 true 1.101s 0.693s 65011712
jbmc-regression/StringCompare01_true-assert.jar false(reach) 5.172s 2.818s 192585728 false(reach) 0.491s 0.506s 44924928 true 1.034s 0.633s 64724992
jbmc-regression/StringCompare02_false-assert.jar false(reach) 5.384s 2.839s 235458560 false(reach) 0.299s 0.322s 44187648 true 1.068s 0.649s 65601536
jbmc-regression/StringCompare03_false-assert.jar false(reach) 4.851s 2.597s 197275648 false(reach) 0.297s 0.308s 44134400 true 1.251s 0.758s 63311872
jbmc-regression/StringCompare04_false-assert.jar false(reach) 5.040s 2.706s 199389184 false(reach) 0.382s 0.391s 44605440 true 1.169s 0.710s 63926272
jbmc-regression/StringCompare05_false-assert.jar false(reach) 4.624s 2.523s 190091264 false(reach) 0.307s 0.311s 44007424 true 1.017s 0.611s 63873024
jbmc-regression/StringConcatenation01_true-assert.jar false(reach) 7.218s 3.821s 257482752 true 6.347s 6.357s 93097984 true 1.166s 0.708s 63787008
jbmc-regression/StringConcatenation02_false-assert.jar false(reach) 8.330s 4.336s 306331648 false(reach) 0.672s 0.688s 48984064 true 1.075s 0.664s 64266240
jbmc-regression/StringConcatenation03_false-assert.jar false(reach) 7.384s 3.920s 265039872 false(reach) 1.713s 1.726s 103763968 true 0.994s 0.609s 63090688
jbmc-regression/StringConcatenation04_false-assert.jar false(reach) 6.147s 3.229s 215842816 false(reach) 0.316s 0.329s 44265472 true 1.025s 0.636s 64749568
jbmc-regression/StringConstructors01_true-assert.jar false(reach) 11.549s 5.956s 336797696 false(reach) 0.378s 0.393s 44609536 true 1.057s 0.636s 64761856
jbmc-regression/StringConstructors02_false-assert.jar false(reach) 5.172s 2.776s 217108480 false(reach) 0.320s 0.339s 44204032 true 0.962s 0.604s 64311296
jbmc-regression/StringConstructors03_false-assert.jar false(reach) 7.000s 3.626s 253747200 false(reach) 0.402s 0.410s 44797952 true 0.924s 0.563s 63078400
jbmc-regression/StringConstructors04_false-assert.jar false(reach) 11.628s 6.022s 311443456 unknown 0.334s 0.350s 45457408 true 1.073s 0.638s 63614976
jbmc-regression/StringConstructors05_false-assert.jar false(reach) 11.061s 5.748s 307453952 false(reach) 0.349s 0.365s 44527616 true 0.970s 0.590s 63168512
jbmc-regression/StringContains01_false-assert.jar false(reach) 6.433s 3.386s 239173632 false(reach) 0.365s 0.384s 44265472 true 1.089s 0.659s 63569920
jbmc-regression/StringContains02_false-assert.jar false(reach) 4.544s 2.497s 192176128 false(reach) 0.313s 0.331s 44195840 true 1.102s 0.654s 63545344
jbmc-regression/StringIndexMethods01_true-assert.jar false(reach) 5.975s 3.126s 236871680 true 3.657s 3.674s 74919936 true 1.032s 0.625s 59584512
jbmc-regression/StringIndexMethods02_false-assert.jar false(reach) 4.588s 2.489s 191799296 false(reach) 0.289s 0.310s 44011520 true 0.966s 0.577s 63758336
jbmc-regression/StringIndexMethods03_false-assert.jar false(reach) 4.680s 2.573s 194117632 false(reach) 0.305s 0.312s 44007424 true 0.888s 0.539s 59273216
jbmc-regression/StringIndexMethods04_false-assert.jar false(reach) 5.429s 2.851s 227586048 false(reach) 0.326s 0.347s 43958272 true 0.959s 0.586s 64159744
jbmc-regression/StringIndexMethods05_false-assert.jar false(reach) 4.617s 2.527s 210472960 false(reach) 0.303s 0.311s 44077056 true 0.950s 0.587s 63389696
jbmc-regression/StringMiscellaneous01_true-assert.jar false(reach) 7.674s 3.990s 292941824 false(reach) 3.647s 3.664s 55812096 unknown 1.044s 0.626s 64917504
jbmc-regression/StringMiscellaneous02_false-assert.jar false(reach) 4.728s 2.562s 192233472 false(reach) 0.283s 0.299s 43941888 true 0.964s 0.591s 63442944
jbmc-regression/StringMiscellaneous03_false-assert.jar false(reach) 5.888s 3.145s 206323712 false(reach) 544.216s 544.288s 451305472 true 1.088s 0.657s 63492096
jbmc-regression/StringMiscellaneous04_true-assert.jar false(reach) 8.929s 4.701s 333737984 true 1.193s 1.206s 48758784 true 1.120s 0.686s 64425984
jbmc-regression/StringStartEnd01_true-assert.jar false(reach) 8.877s 4.635s 268394496 true 2.819s 2.835s 56639488 true 0.987s 0.607s 63467520
jbmc-regression/StringStartEnd02_false-assert.jar false(reach) 22.361s 11.586s 663404544 false(reach) 0.550s 0.571s 47136768 true 0.954s 0.578s 64020480
jbmc-regression/StringStartEnd03_false-assert.jar false(reach) 22.715s 11.756s 644952064 false(reach) 0.861s 0.869s 49045504 true 0.898s 0.555s 63242240
jbmc-regression/StringValueOf01_true-assert.jar false(reach) 12.622s 6.564s 424628224 false(reach) 1.325s 1.337s 82579456 true 0.947s 0.593s 64495616
jbmc-regression/StringValueOf02_false-assert.jar false(reach) 7.959s 4.181s 276004864 false(reach) 4.444s 4.451s 142090240 true 0.995s 0.602s 63070208
jbmc-regression/StringValueOf03_false-assert.jar false(reach) 7.782s 4.096s 274337792 false(reach) 3.939s 3.954s 141762560 true 0.972s 0.592s 62951424
jbmc-regression/StringValueOf04_false-assert.jar false(reach) 5.039s 2.723s 200253440 false(reach) 0.324s 0.327s 44339200 true 1.052s 0.629s 59379712
jbmc-regression/StringValueOf05_false-assert.jar false(reach) 5.092s 2.748s 198053888 false(reach) 0.506s 0.513s 47120384 true 1.022s 0.628s 63598592
jbmc-regression/StringValueOf06_false-assert.jar false(reach) 4.890s 2.629s 197648384 false(reach) 0.370s 0.390s 44658688 true 1.133s 0.698s 63795200
jbmc-regression/StringValueOf07_false-assert.jar false(reach) 6.252s 3.289s 202477568 false(reach) 0.728s 0.741s 49778688 true 1.016s 0.609s 64266240
jbmc-regression/StringValueOf08_false-assert.jar false(reach) 5.050s 2.739s 213417984 false(reach) 1.143s 1.149s 144334848 true 1.068s 0.653s 62828544
jbmc-regression/StringValueOf09_false-assert.jar false(reach) 5.216s 2.796s 199860224 false(reach) 1.214s 1.225s 142495744 true 1.203s 0.746s 63414272
jbmc-regression/StringValueOf10_false-assert.jar false(reach) 6.207s 3.260s 208719872 false(reach) 0.401s 0.409s 44670976 true 1.017s 0.596s 66785280
jbmc-regression/SubString01_true-assert.jar false(reach) 4.305s 2.345s 193499136 true 0.620s 0.640s 44740608 true 1.006s 0.613s 61132800
jbmc-regression/SubString02_false-assert.jar false(reach) 4.900s 2.643s 194637824 false(reach) 0.503s 0.519s 46829568 true 0.976s 0.595s 62668800
jbmc-regression/SubString03_false-assert.jar false(reach) 4.691s 2.566s 200167424 false(reach) 0.722s 0.736s 49635328 true 1.034s 0.623s 63971328
jbmc-regression/TokenTest01_true-assert.jar false(reach) 7.941s 4.155s 272359424 false(reach) 1.834s 1.847s 71712768 true 1.234s 0.726s 63672320
jbmc-regression/TokenTest02_false-assert.jar false(reach) 6.015s 3.139s 210284544 false(reach) 0.941s 0.950s 52002816 true 1.079s 0.675s 65687552
jbmc-regression/Validate01_true-assert.jar false(reach) 6.013s 3.223s 226123776 false(reach) 0.362s 0.366s 44724224 true 1.013s 0.624s 64069632
jbmc-regression/Validate02_false-assert.jar false(reach) 10.852s 5.663s 413720576 false(reach) 0.487s 0.497s 45314048 true 1.052s 0.628s 63213568
jbmc-regression/aastore_aaload1_true-assert.jar false(reach) 7.982s 4.129s 284807168 true 2.574s 2.583s 125952000 true 1.018s 0.617s 63844352
jbmc-regression/array1_true-assert.jar false(reach) 20.661s 10.644s 466837504 true 1.403s 1.411s 81711104 true 1.047s 0.626s 60456960
jbmc-regression/array2_true-assert.jar false(reach) 6.027s 3.190s 204107776 true 0.584s 0.599s 44486656 true 1.051s 0.628s 63545344
jbmc-regression/arraylength1_true-assert.jar true 3.345s 1.903s 183369728 true 0.441s 0.461s 43798528 true 0.979s 0.611s 62353408
jbmc-regression/arrayread1_true-assert.jar true 4.059s 2.227s 190038016 true 0.443s 0.459s 44015616 true 0.983s 0.614s 63045632
jbmc-regression/assert1_true-assert.jar true 4.154s 2.260s 189239296 true 0.602s 0.617s 44761088 true 0.946s 0.590s 64520192
jbmc-regression/assert2_false-assert.jar false(reach) 4.038s 2.161s 205291520 false(reach) 0.320s 0.330s 44662784 true 1.014s 0.610s 59965440
jbmc-regression/assert3_false-assert.jar false(reach) 3.498s 1.998s 188317696 false(reach) 0.269s 0.286s 44134400 true 1.065s 0.656s 63700992
jbmc-regression/assert4_false-assert.jar false(reach) 3.590s 1.996s 188686336 false(reach) 0.322s 0.342s 44605440 true 1.138s 0.668s 64696320
jbmc-regression/assert5_true-assert.jar true 2.979s 1.702s 159711232 true 0.545s 0.562s 44785664 true 1.075s 0.668s 66523136
jbmc-regression/assert6_true-assert.jar true 3.539s 1.901s 182214656 true 0.432s 0.441s 44212224 true 1.057s 0.659s 62881792
jbmc-regression/astore_aload1_true-assert.jar unknown 20.088s 11.277s 957603840 true 2.870s 2.889s 119648256 true 1.171s 0.693s 65265664
jbmc-regression/athrow1_false-assert.jar false(reach) 3.838s 2.127s 187592704 false(reach) 0.266s 0.276s 43880448 false(reach) 1.053s 0.634s 63684608
jbmc-regression/basic1_true-assert.jar false(reach) 4.811s 2.593s 192946176 true 0.406s 0.420s 44085248 false(reach) 1.046s 0.651s 64778240
jbmc-regression/bitwise1_true-assert.jar false(reach) 3.391s 1.901s 187183104 true 0.423s 0.440s 43876352 true 1.059s 0.629s 63475712
jbmc-regression/boolean1_true-assert.jar true 3.302s 1.865s 185270272 true 0.418s 0.431s 43986944 true 1.060s 0.647s 63361024
jbmc-regression/boolean2_true-assert.jar true 4.290s 2.391s 217210880 true 0.424s 0.437s 44015616 true 1.088s 0.650s 64864256
jbmc-regression/bug-test-gen-095_false-assert.jar false(reach) 5.514s 3.020s 220692480 false(reach) 0.370s 0.382s 44335104 true 0.987s 0.599s 63213568
jbmc-regression/bug-test-gen-119-2_true-assert.jar false(reach) 3.663s 2.023s 189829120 true 1.062s 1.076s 46579712 true 0.972s 0.590s 63791104
jbmc-regression/bug-test-gen-119_true-assert.jar false(reach) 5.358s 2.856s 214175744 true 0.642s 0.661s 44535808 true 0.937s 0.575s 63930368
jbmc-regression/calc_true-assert.jar false(reach) 5.702s 3.056s 214544384 unknown 874.934s 875.033s 300933120 true 0.996s 0.610s 63782912
jbmc-regression/cast1_true-assert.jar false(reach) 5.444s 2.907s 196247552 true 0.573s 0.590s 44802048 true 1.000s 0.593s 62935040
jbmc-regression/catch1_true-assert.jar true 4.113s 2.227s 189849600 true 0.403s 0.412s 43937792 true 0.971s 0.590s 63721472
jbmc-regression/char1_true-assert.jar false(reach) 4.608s 2.538s 194822144 true 0.839s 0.856s 45518848 true 1.094s 0.660s 63832064
jbmc-regression/charArray_true-assert.jar false(reach) 7.203s 3.731s 278130688 true 12.687s 12.708s 290705408 true 1.119s 0.673s 64217088
jbmc-regression/classtest1_true-assert.jar unknown 1.500s 0.867s 117346304 true 0.352s 0.363s 43462656 true 1.120s 0.684s 64053248
jbmc-regression/const1_true-assert.jar true 3.135s 1.783s 183631872 true 0.383s 0.406s 44032000 true 1.159s 0.699s 63520768
jbmc-regression/constructor1_true-assert.jar true 4.891s 2.581s 207736832 true 0.467s 0.484s 44232704 true 0.944s 0.597s 63733760
jbmc-regression/enum1_true-assert.jar true 3.299s 1.804s 169730048 true 0.550s 0.568s 44437504 true 0.993s 0.621s 64745472
jbmc-regression/exceptions10_false-assert.jar false(reach) 5.042s 2.696s 218632192 false(reach) 0.280s 0.295s 44015616 false(reach) 1.086s 0.641s 64512000
jbmc-regression/exceptions11_false-assert.jar false(reach) 5.433s 2.913s 212705280 false(reach) 0.293s 0.307s 44060672 false(reach) 1.058s 0.636s 65552384
jbmc-regression/exceptions12_false-assert.jar false(reach) 4.857s 2.647s 196812800 false(reach) 0.297s 0.310s 44064768 false(reach) 1.007s 0.605s 61628416
jbmc-regression/exceptions13_false-assert.jar false(reach) 4.646s 2.549s 192217088 false(reach) 0.279s 0.291s 44003328 false(reach) 1.064s 0.641s 64966656
jbmc-regression/exceptions14_true-assert.jar true 4.332s 2.374s 186040320 true 0.414s 0.433s 44011520 true 1.040s 0.621s 64950272
jbmc-regression/exceptions15_true-assert.jar true 4.537s 2.419s 208195584 true 0.416s 0.422s 44044288 true 1.007s 0.610s 63750144
jbmc-regression/exceptions16_false-assert.jar false(reach) 4.609s 2.455s 224395264 false(reach) 0.292s 0.310s 44011520 false(reach) 1.152s 0.706s 64139264
jbmc-regression/exceptions18_true-assert.jar true 4.640s 2.431s 228958208 true 0.425s 0.441s 44064768 true 0.938s 0.559s 63926272
jbmc-regression/exceptions1_false-assert.jar false(reach) 6.101s 3.277s 227753984 false(reach) 0.310s 0.321s 44220416 false(reach) 1.027s 0.618s 63823872
jbmc-regression/exceptions2_false-assert.jar false(reach) 4.548s 2.434s 212107264 false(reach) 0.261s 0.267s 43995136 false(reach) 0.958s 0.568s 63385600
jbmc-regression/exceptions3_false-assert.jar false(reach) 4.737s 2.501s 209870848 false(reach) 0.278s 0.290s 43937792 false(reach) 1.166s 0.720s 63582208
jbmc-regression/exceptions4_true-assert.jar false(reach) 5.488s 2.911s 215441408 true 0.408s 0.421s 44023808 true 0.977s 0.590s 64507904
jbmc-regression/exceptions5_true-assert.jar false(reach) 7.811s 4.076s 284098560 true 0.484s 0.495s 44257280 true 1.099s 0.659s 64147456
jbmc-regression/exceptions6_false-assert.jar unknown 1.735s 0.991s 118091776 false(reach) 0.273s 0.284s 44064768 false(reach) 1.028s 0.620s 64065536
jbmc-regression/exceptions7_false-assert.jar false(reach) 5.561s 2.967s 207888384 false(reach) 0.303s 0.326s 44015616 false(reach) 1.044s 0.636s 64593920
jbmc-regression/exceptions8_false-assert.jar false(reach) 5.010s 2.764s 219394048 false(reach) 0.292s 0.313s 44011520 false(reach) 1.111s 0.676s 64000000
jbmc-regression/exceptions9_true-assert.jar true 4.569s 2.474s 194043904 true 0.454s 0.474s 44183552 true 1.060s 0.637s 63549440
jbmc-regression/fcmpx_dcmpx1_true-assert.jar true 3.487s 1.907s 206888960 true 0.393s 0.402s 44208128 true 1.165s 0.690s 64303104
jbmc-regression/iarith1_true-assert.jar true 3.089s 1.728s 178200576 true 0.401s 0.414s 44056576 true 1.041s 0.628s 62971904
jbmc-regression/iarith2_true-assert.jar true 4.422s 2.365s 229605376 true 0.384s 0.405s 44392448 true 1.053s 0.645s 63590400
jbmc-regression/if_acmp1_true-assert.jar true 4.692s 2.551s 191856640 true 0.456s 0.473s 44511232 true 1.012s 0.624s 63639552
jbmc-regression/if_expr1_true-assert.jar false(reach) 4.157s 2.286s 191787008 true 0.464s 0.488s 44089344 unknown 1.004s 0.601s 64192512
jbmc-regression/if_icmp1_true-assert.jar true 4.143s 2.279s 209264640 true 0.494s 0.508s 44154880 true 0.977s 0.604s 65355776
jbmc-regression/ifxx1_true-assert.jar true 3.315s 1.832s 184729600 true 0.392s 0.406s 44064768 true 0.971s 0.592s 64409600
jbmc-regression/instanceof1_true-assert.jar false(reach) 4.019s 2.238s 189321216 true 0.427s 0.451s 43806720 false(reach) 1.019s 0.616s 63856640
jbmc-regression/instanceof2_true-assert.jar unknown 1.545s 0.876s 117239808 true 0.455s 0.471s 44109824 true 1.000s 0.606s 63676416
jbmc-regression/instanceof3_true-assert.jar false(reach) 3.513s 1.972s 193040384 true 0.430s 0.443s 43921408 true 0.971s 0.580s 63336448
jbmc-regression/instanceof4_true-assert.jar false(reach) 3.413s 1.945s 189906944 true 0.391s 0.399s 43958272 true 1.019s 0.629s 63651840
jbmc-regression/instanceof5_true-assert.jar unknown 1.435s 0.832s 115032064 true 0.390s 0.409s 43933696 true 0.907s 0.554s 64008192
jbmc-regression/instanceof6_true-assert.jar true 5.496s 2.903s 212459520 true 0.461s 0.476s 43999232 true 0.949s 0.568s 64438272
jbmc-regression/instanceof7_true-assert.jar true 7.639s 3.991s 281653248 true 0.476s 0.498s 44220416 true 0.894s 0.557s 63160320
jbmc-regression/instanceof8_true-assert.jar true 5.013s 2.699s 213549056 true 0.458s 0.467s 44195840 true 0.975s 0.599s 63492096
jbmc-regression/interface1_false-assert.jar false(reach) 4.731s 2.519s 210878464 false(reach) 0.244s 0.267s 43868160 false(reach) 0.929s 0.566s 59240448
jbmc-regression/java_append_char_false-assert.jar false(reach) 8.372s 4.326s 302731264 false(reach) 0.505s 0.517s 47542272 true 0.980s 0.594s 64524288
jbmc-regression/lazyloading4_true-assert.jar true 3.776s 2.104s 180375552 true 0.411s 0.427s 44113920 true 0.949s 0.588s 63328256
jbmc-regression/list1_true-assert.jar false(reach) 123.938s 99.626s 1655496704 true 0.858s 0.880s 44965888 true 0.986s 0.599s 63283200
jbmc-regression/long1_true-assert.jar false(reach) 5.396s 2.891s 197922816 true 0.418s 0.438s 44355584 true 0.948s 0.586s 63754240
jbmc-regression/lookupswitch1_true-assert.jar true 5.619s 3.025s 202194944 true 0.493s 0.513s 44441600 true 1.033s 0.621s 63934464
jbmc-regression/multinewarray_true-assert.jar timeout 901.042s 831.275s 2536374272 true 2.326s 2.341s 53940224 true 1.014s 0.606s 63885312
jbmc-regression/overloading1_true-assert.jar true 4.256s 2.261s 207065088 true 0.404s 0.422s 44064768 true 0.986s 0.599s 63410176
jbmc-regression/package1_true-assert.jar true 3.017s 1.689s 159297536 true 0.379s 0.395s 43819008 true 0.970s 0.583s 63483904
jbmc-regression/putfield_getfield1_true-assert.jar true 3.137s 1.740s 180244480 true 0.395s 0.413s 44068864 true 0.922s 0.550s 63311872
jbmc-regression/putstatic_getstatic1_true-assert.jar true 3.493s 1.952s 184373248 true 0.391s 0.413s 43876352 true 0.974s 0.587s 62955520
jbmc-regression/recursion2_true-assert.jar true 6.895s 3.659s 263294976 true 0.398s 0.415s 43896832 true 1.018s 0.616s 65081344
jbmc-regression/return1_false-assert.jar false(reach) 3.892s 2.167s 189419520 false(reach) 0.257s 0.274s 43868160 false(reach) 0.983s 0.596s 63610880
jbmc-regression/return2_false-assert.jar false(reach) 4.200s 2.332s 191774720 false(reach) 0.265s 0.285s 43925504 unknown 0.983s 0.596s 64217088
jbmc-regression/store_load1_true-assert.jar true 3.587s 1.976s 184655872 true 0.483s 0.499s 45191168 true 0.989s 0.601s 65409024
jbmc-regression/swap1_true-assert.jar false(reach) 3.814s 2.070s 208756736 true 0.388s 0.411s 43937792 true 0.912s 0.573s 63344640
jbmc-regression/synchronized_true-assert.jar false(reach) 3.035s 1.750s 179392512 false(reach) 0.243s 0.256s 43905024 true 0.979s 0.587s 64331776
jbmc-regression/tableswitch1_true-assert.jar true 5.617s 3.001s 200945664 true 0.503s 0.524s 44503040 true 1.032s 0.628s 64270336
jbmc-regression/uninitialised1_true-assert.jar true 3.853s 2.104s 187744256 true 0.390s 0.405s 44060672 true 0.971s 0.577s 62795776
jbmc-regression/virtual1_true-assert.jar true 2.331s 1.370s 151609344 true 0.422s 0.435s 43962368 true 0.943s 0.581s 63340544
jbmc-regression/virtual2_false-assert.jar false(reach) 3.649s 2.018s 187904000 false(reach) 0.269s 0.280s 44007424 false(reach) 0.931s 0.586s 64663552
jbmc-regression/virtual4_true-assert.jar true 3.993s 2.173s 189456384 true 0.411s 0.427s 43999232 true 0.986s 0.602s 64671744
jbmc-regression/virtual_function_unwinding_true-assert.jar true 4.658s 2.533s 190947328 true 0.411s 0.421s 44122112 true 1.029s 0.637s 64237568
jpf-regression/ExDarko_false-assert.jar false(reach) 6.511s 3.434s 221106176 false(reach) 0.396s 0.411s 44867584 false(reach) 0.946s 0.575s 63455232
jpf-regression/ExDarko_true-assert.jar false(reach) 8.653s 4.547s 274624512 true 0.587s 0.595s 44744704 true 0.943s 0.578s 65765376
jpf-regression/ExException_false-assert.jar false(reach) 5.062s 2.679s 209301504 false(reach) 0.250s 0.280s 44056576 unknown 1.001s 0.612s 63762432
jpf-regression/ExException_true-assert.jar false(reach) 4.289s 2.339s 191094784 true 0.458s 0.481s 44077056 true 0.981s 0.596s 63328256
jpf-regression/ExGenSymExe_false-assert.jar false(reach) 10.557s 5.454s 319942656 false(reach) 0.304s 0.327s 44195840 false(reach) 0.983s 0.583s 63672320
jpf-regression/ExGenSymExe_true-assert.jar true 9.878s 5.157s 292446208 true 0.459s 0.478s 44244992 true 0.953s 0.585s 63979520
jpf-regression/ExLazy_false-assert.jar false(reach) 4.559s 2.481s 210501632 false(reach) 0.266s 0.284s 43884544 true 0.953s 0.600s 62865408
jpf-regression/ExLazy_true-assert.jar true 4.090s 2.268s 190455808 true 0.426s 0.444s 44134400 true 0.979s 0.589s 63356928
jpf-regression/ExMIT_false-assert.jar false(reach) 3.200s 1.835s 186384384 false(reach) 0.258s 0.270s 43868160 true 0.977s 0.593s 63270912
jpf-regression/ExMIT_true-assert.jar true 3.462s 1.868s 206229504 true 0.392s 0.416s 44007424 true 0.966s 0.591s 63983616
jpf-regression/ExSymExe10_false-assert.jar false(reach) 6.258s 3.372s 234074112 false(reach) 0.282s 0.302s 44208128 false(reach) 0.975s 0.596s 65064960
jpf-regression/ExSymExe10_true-assert.jar false(reach) 5.934s 3.207s 213032960 true 0.448s 0.472s 44265472 true 0.990s 0.616s 63504384
jpf-regression/ExSymExe11_false-assert.jar false(reach) 6.256s 3.349s 244301824 false(reach) 0.275s 0.290s 44183552 false(reach) 0.999s 0.595s 64000000
jpf-regression/ExSymExe11_true-assert.jar false(reach) 7.158s 3.715s 296554496 true 0.446s 0.457s 44171264 true 0.977s 0.598s 65912832
jpf-regression/ExSymExe12_false-assert.jar false(reach) 6.215s 3.306s 223064064 false(reach) 0.291s 0.308s 44134400 false(reach) 0.929s 0.583s 64176128
jpf-regression/ExSymExe12_true-assert.jar false(reach) 6.199s 3.275s 236339200 true 0.493s 0.512s 44212224 true 1.005s 0.587s 63836160
jpf-regression/ExSymExe13_false-assert.jar false(reach) 6.229s 3.300s 225804288 false(reach) 0.279s 0.292s 44130304 false(reach) 0.960s 0.587s 61063168
jpf-regression/ExSymExe13_true-assert.jar false(reach) 6.464s 3.428s 262225920 true 0.496s 0.508s 44179456 true 0.975s 0.603s 63639552
jpf-regression/ExSymExe14_false-assert.jar false(reach) 6.022s 3.147s 219394048 false(reach) 0.288s 0.299s 44142592 false(reach) 0.969s 0.581s 63655936
jpf-regression/ExSymExe14_true-assert.jar false(reach) 6.053s 3.220s 212426752 true 0.494s 0.515s 44122112 true 0.911s 0.574s 63287296
jpf-regression/ExSymExe15_false-assert.jar false(reach) 5.793s 3.092s 207278080 false(reach) 0.291s 0.302s 44191744 false(reach) 1.009s 0.618s 65101824
jpf-regression/ExSymExe15_true-assert.jar false(reach) 5.727s 3.068s 211132416 true 0.486s 0.494s 44126208 true 0.975s 0.596s 64516096
jpf-regression/ExSymExe16_false-assert.jar false(reach) 6.069s 3.169s 219373568 false(reach) 0.272s 0.286s 44081152 false(reach) 0.971s 0.586s 64061440
jpf-regression/ExSymExe16_true-assert.jar false(reach) 5.683s 3.012s 218923008 true 0.444s 0.460s 44036096 true 1.011s 0.596s 63188992
jpf-regression/ExSymExe17_false-assert.jar false(reach) 5.551s 2.971s 200290304 false(reach) 0.299s 0.308s 44027904 false(reach) 0.979s 0.599s 63508480
jpf-regression/ExSymExe17_true-assert.jar false(reach) 5.407s 2.891s 198946816 true 0.448s 0.467s 44019712 true 0.981s 0.604s 63803392
jpf-regression/ExSymExe18_false-assert.jar false(reach) 6.600s 3.507s 236236800 false(reach) 0.290s 0.308s 44265472 false(reach) 0.928s 0.565s 63684608
jpf-regression/ExSymExe18_true-assert.jar false(reach) 5.736s 3.084s 201875456 true 0.453s 0.471s 43999232 true 0.978s 0.578s 64004096
jpf-regression/ExSymExe19_false-assert.jar false(reach) 6.130s 3.296s 223866880 false(reach) 0.274s 0.287s 44261376 false(reach) 0.984s 0.587s 61730816
jpf-regression/ExSymExe19_true-assert.jar false(reach) 6.044s 3.220s 223727616 true 0.479s 0.500s 44339200 true 0.979s 0.588s 64741376
jpf-regression/ExSymExe1_false-assert.jar false(reach) 7.379s 3.861s 267083776 false(reach) 0.300s 0.312s 44216320 false(reach) 0.980s 0.601s 59498496
jpf-regression/ExSymExe1_true-assert.jar false(reach) 6.156s 3.235s 215298048 true 0.451s 0.474s 44269568 true 0.960s 0.578s 63344640
jpf-regression/ExSymExe20_false-assert.jar false(reach) 6.664s 3.530s 242249728 false(reach) 0.289s 0.301s 44220416 false(reach) 0.996s 0.608s 63492096
jpf-regression/ExSymExe20_true-assert.jar false(reach) 6.237s 3.279s 222855168 true 0.447s 0.467s 44261376 true 0.978s 0.597s 63598592
jpf-regression/ExSymExe21_false-assert.jar false(reach) 6.965s 3.680s 262287360 false(reach) 0.274s 0.293s 44273664 false(reach) 0.956s 0.606s 64405504
jpf-regression/ExSymExe21_true-assert.jar false(reach) 6.062s 3.231s 227467264 true 0.446s 0.463s 44134400 true 0.966s 0.581s 63512576
jpf-regression/ExSymExe25_false-assert.jar false(reach) 6.867s 3.645s 244543488 false(reach) 0.291s 0.312s 44396544 false(reach) 1.011s 0.612s 64294912
jpf-regression/ExSymExe25_true-assert.jar false(reach) 5.964s 3.146s 216961024 true 0.433s 0.451s 44130304 true 0.988s 0.597s 64102400
jpf-regression/ExSymExe26_false-assert.jar false(reach) 7.107s 3.771s 243032064 false(reach) 0.272s 0.287s 44273664 false(reach) 1.044s 0.640s 66494464
jpf-regression/ExSymExe26_true-assert.jar false(reach) 7.198s 3.717s 264404992 true 0.441s 0.454s 44146688 true 0.974s 0.584s 63250432
jpf-regression/ExSymExe27_false-assert.jar false(reach) 7.019s 3.673s 248942592 false(reach) 0.277s 0.296s 44204032 true 0.912s 0.551s 65699840
jpf-regression/ExSymExe27_true-assert.jar false(reach) 5.698s 3.074s 205279232 true 0.446s 0.463s 44163072 true 0.995s 0.583s 63905792
jpf-regression/ExSymExe28_false-assert.jar false(reach) 9.241s 4.828s 269332480 false(reach) 0.303s 0.311s 44077056 true 1.008s 0.616s 63623168
jpf-regression/ExSymExe28_true-assert.jar false(reach) 6.598s 3.419s 267558912 true 0.443s 0.458s 44032000 true 0.987s 0.576s 63410176
jpf-regression/ExSymExe29_false-assert.jar false(reach) 8.802s 4.600s 268247040 false(reach) 0.288s 0.318s 44220416 false(reach) 0.991s 0.589s 64118784
jpf-regression/ExSymExe29_true-assert.jar false(reach) 6.229s 3.273s 234254336 true 0.449s 0.473s 44015616 true 0.958s 0.579s 63369216
jpf-regression/ExSymExe2_false-assert.jar false(reach) 8.390s 4.424s 263299072 false(reach) 0.296s 0.310s 44097536 false(reach) 1.022s 0.629s 63492096
jpf-regression/ExSymExe2_true-assert.jar false(reach) 5.495s 2.940s 201170944 true 0.442s 0.451s 44130304 true 0.965s 0.579s 58380288
jpf-regression/ExSymExe3_false-assert.jar false(reach) 8.767s 4.607s 269209600 false(reach) 0.282s 0.287s 44347392 false(reach) 0.938s 0.569s 63078400
jpf-regression/ExSymExe3_true-assert.jar false(reach) 5.829s 3.097s 204283904 true 0.442s 0.464s 44163072 true 0.969s 0.587s 63393792
jpf-regression/ExSymExe4_false-assert.jar false(reach) 9.861s 5.127s 315842560 false(reach) 0.272s 0.288s 44204032 false(reach) 1.023s 0.621s 64212992
jpf-regression/ExSymExe4_true-assert.jar false(reach) 5.700s 3.025s 201338880 true 0.446s 0.459s 44032000 true 0.974s 0.588s 63799296
jpf-regression/ExSymExe5_false-assert.jar false(reach) 8.189s 4.232s 302059520 false(reach) 0.292s 0.301s 44224512 false(reach) 0.978s 0.580s 59604992
jpf-regression/ExSymExe5_true-assert.jar false(reach) 5.999s 3.164s 214781952 true 0.445s 0.462s 44003328 true 0.970s 0.596s 63594496
jpf-regression/ExSymExe6_false-assert.jar true 5.335s 2.868s 202420224 false(reach) 0.243s 0.269s 44199936 unknown 1.002s 0.598s 63647744
jpf-regression/ExSymExe6_true-assert.jar false(reach) 5.745s 3.058s 200556544 true 0.441s 0.460s 44175360 true 1.004s 0.615s 63668224
jpf-regression/ExSymExe7_false-assert.jar false(reach) 7.606s 4.012s 267075584 false(reach) 0.287s 0.312s 44077056 true 0.952s 0.606s 63352832
jpf-regression/ExSymExe7_true-assert.jar false(reach) 6.911s 3.689s 241197056 true 0.488s 0.502s 44290048 true 0.941s 0.570s 65581056
jpf-regression/ExSymExe8_false-assert.jar false(reach) 8.679s 4.561s 270532608 false(reach) 0.299s 0.312s 44195840 true 0.986s 0.593s 63332352
jpf-regression/ExSymExe8_true-assert.jar false(reach) 6.171s 3.217s 224788480 true 0.449s 0.457s 44122112 true 0.957s 0.604s 63860736
jpf-regression/ExSymExe9_false-assert.jar false(reach) 5.950s 3.158s 215334912 false(reach) 0.286s 0.302s 44077056 false(reach) 1.001s 0.606s 64536576
jpf-regression/ExSymExe9_true-assert.jar false(reach) 6.071s 3.188s 230756352 true 0.450s 0.482s 44048384 true 0.951s 0.589s 64626688
jpf-regression/ExSymExeArrays_false-assert.jar unknown 4.984s 2.608s 284143616 false(reach) 0.279s 0.296s 44183552 false(reach) 1.013s 0.620s 63668224
jpf-regression/ExSymExeArrays_true-assert.jar unknown 4.048s 2.190s 199471104 true 0.475s 0.490s 44007424 true 1.020s 0.618s 63938560
jpf-regression/ExSymExeBool_false-assert.jar false(reach) 4.980s 2.670s 197795840 false(reach) 0.283s 0.295s 44003328 false(reach) 0.987s 0.594s 64106496
jpf-regression/ExSymExeBool_true-assert.jar false(reach) 5.283s 2.819s 195043328 true 0.434s 0.449s 44093440 true 0.964s 0.586s 63389696
jpf-regression/ExSymExeComplexMath_false-assert.jar false(reach) 5.384s 2.902s 200830976 false(reach) 0.264s 0.286s 45367296 false(reach) 1.009s 0.618s 60461056
jpf-regression/ExSymExeComplexMath_true-assert.jar false(reach) 5.872s 3.091s 202727424 true 0.441s 0.455s 45363200 true 0.987s 0.601s 63164416
jpf-regression/ExSymExeD2I_false-assert.jar false(reach) 7.071s 3.706s 257540096 false(reach) 0.267s 0.274s 43937792 false(reach) 0.989s 0.618s 64339968
jpf-regression/ExSymExeD2I_true-assert.jar false(reach) 7.048s 3.774s 260263936 true 0.423s 0.438s 44023808 true 0.945s 0.557s 63053824
jpf-regression/ExSymExeD2L_false-assert.jar false(reach) 7.226s 3.830s 261935104 false(reach) 0.286s 0.302s 44531712 false(reach) 0.951s 0.597s 63139840
jpf-regression/ExSymExeD2L_true-assert.jar false(reach) 5.063s 2.749s 200646656 true 0.463s 0.481s 44470272 true 1.035s 0.622s 64016384
jpf-regression/ExSymExeF2I_false-assert.jar false(reach) 7.193s 3.788s 260259840 false(reach) 0.272s 0.287s 44011520 false(reach) 0.940s 0.585s 64909312
jpf-regression/ExSymExeF2I_true-assert.jar false(reach) 7.302s 3.851s 258314240 true 0.426s 0.444s 44130304 true 0.958s 0.588s 63578112
jpf-regression/ExSymExeF2L_false-assert.jar false(reach) 7.284s 3.844s 258560000 false(reach) 0.277s 0.288s 44204032 false(reach) 0.991s 0.618s 64172032
jpf-regression/ExSymExeF2L_true-assert.jar false(reach) 5.123s 2.739s 194072576 true 0.482s 0.501s 44380160 true 1.022s 0.624s 63848448
jpf-regression/ExSymExeFNEG_false-assert.jar false(reach) 6.105s 3.276s 216502272 false(reach) 0.277s 0.288s 44085248 false(reach) 0.974s 0.583s 63926272
jpf-regression/ExSymExeFNEG_true-assert.jar false(reach) 4.896s 2.692s 194887680 true 0.479s 0.496s 44285952 true 0.963s 0.592s 64204800
jpf-regression/ExSymExeGetStatic_false-assert.jar false(reach) 5.347s 2.870s 198496256 false(reach) 0.252s 0.258s 43999232 false(reach) 0.951s 0.586s 59068416
jpf-regression/ExSymExeGetStatic_true-assert.jar false(reach) 5.481s 2.931s 198561792 true 0.424s 0.442s 44019712 true 0.962s 0.600s 63541248
jpf-regression/ExSymExeI2D_false-assert.jar false(reach) 6.154s 3.211s 234520576 false(reach) 0.271s 0.283s 44089344 false(reach) 0.992s 0.609s 64401408
jpf-regression/ExSymExeI2D_true-assert.jar false(reach) 4.563s 2.497s 193425408 true 0.480s 0.501s 44093440 true 0.973s 0.598s 64876544
jpf-regression/ExSymExeI2F_false-assert.jar false(reach) 5.234s 2.828s 197787648 false(reach) 0.260s 0.267s 44060672 false(reach) 1.015s 0.636s 64806912
jpf-regression/ExSymExeI2F_true-assert.jar false(reach) 4.694s 2.561s 193949696 true 0.449s 0.463s 44130304 true 0.974s 0.574s 64061440
jpf-regression/ExSymExeLCMP_false-assert.jar false(reach) 4.972s 2.715s 195244032 false(reach) 0.258s 0.274s 44048384 false(reach) 1.020s 0.618s 65400832
jpf-regression/ExSymExeLCMP_true-assert.jar false(reach) 5.046s 2.711s 198156288 true 0.455s 0.474s 44036096 true 0.929s 0.569s 65228800
jpf-regression/ExSymExeLongBytecodes_false-assert.jar false(reach) 5.585s 3.018s 209715200 false(reach) 0.309s 0.323s 44601344 false(reach) 1.025s 0.627s 64299008
jpf-regression/ExSymExeLongBytecodes_true-assert.jar false(reach) 5.699s 3.084s 197857280 true 0.566s 0.577s 44670976 true 0.976s 0.590s 63950848
jpf-regression/ExSymExeResearch_false-assert.jar false(reach) 6.347s 3.361s 256229376 false(reach) 0.285s 0.293s 44138496 false(reach) 0.913s 0.571s 64008192
jpf-regression/ExSymExeResearch_true-assert.jar false(reach) 4.913s 2.642s 190365696 true 0.474s 0.490s 44134400 true 0.999s 0.618s 63881216
jpf-regression/ExSymExeSimple_false-assert.jar false(reach) 5.462s 2.937s 195584000 false(reach) 0.290s 0.303s 44113920 false(reach) 0.948s 0.578s 64184320
jpf-regression/ExSymExeSimple_true-assert.jar false(reach) 6.508s 3.431s 224432128 true 0.496s 0.524s 44171264 true 0.978s 0.599s 63545344
jpf-regression/ExSymExeSuzette_false-assert.jar false(reach) 4.719s 2.549s 193175552 false(reach) 0.285s 0.293s 44146688 false(reach) 0.982s 0.616s 65081344
jpf-regression/ExSymExeSuzette_true-assert.jar true 4.341s 2.350s 189919232 true 0.464s 0.485s 44392448 true 0.973s 0.590s 63942656
jpf-regression/ExSymExeSwitch_false-assert.jar false(reach) 4.525s 2.460s 191508480 false(reach) 0.260s 0.268s 43933696 false(reach) 1.000s 0.614s 64630784
jpf-regression/ExSymExeSwitch_true-assert.jar false(reach) 4.820s 2.577s 209408000 true 0.492s 0.513s 44040192 true 0.960s 0.578s 63606784
jpf-regression/ExSymExeTestAssignments_false-assert.jar false(reach) 4.934s 2.596s 208805888 false(reach) 0.270s 0.290s 44126208 true 0.922s 0.562s 63336448
jpf-regression/ExSymExeTestAssignments_true-assert.jar false(reach) 4.515s 2.438s 209068032 true 0.405s 0.419s 43970560 true 0.997s 0.609s 63516672
jpf-regression/ExSymExeTestClassFields_false-assert.jar false(reach) 6.195s 3.242s 231325696 false(reach) 0.276s 0.293s 43868160 true 0.994s 0.593s 62873600
jpf-regression/ExSymExeTestClassFields_true-assert.jar false(reach) 4.974s 2.676s 194899968 true 0.427s 0.438s 43937792 true 0.975s 0.594s 63012864
jpf-regression/ExSymExe_false-assert.jar false(reach) 5.589s 2.937s 218521600 false(reach) 0.283s 0.292s 45432832 false(reach) 0.951s 0.582s 63926272
jpf-regression/ExSymExe_true-assert.jar false(reach) 5.050s 2.734s 192638976 true 0.415s 0.434s 45637632 true 0.964s 0.595s 60485632
jpf-regression/TestLazy_false-assert.jar false(reach) 4.934s 2.692s 191397888 false(reach) 0.301s 0.313s 44208128 false(reach) 0.992s 0.598s 64430080
jpf-regression/TestLazy_true-assert.jar false(reach) 6.169s 3.204s 254156800 true 0.500s 0.518s 44322816 true 0.967s 0.592s 63836160
jayhorn-recursive/Ackermann01_false-assert.jar false(reach) 4.688s 2.585s 187351040 unknown 875.064s 875.051s 777363456 false(reach) 1.004s 0.606s 64323584
jayhorn-recursive/Addition_true-assert.jar false(reach) 5.809s 3.048s 237727744 unknown 875.547s 875.032s 3249168384 true 1.117s 0.663s 71094272
jayhorn-recursive/InfiniteLoop_false-assert.jar unknown 1.226s 0.725s 114171904 false(reach) 0.234s 0.246s 44400640 timeout 900.250s 899.646s 64204800
jayhorn-recursive/SatAckermann01_true-assert.jar true 6.191s 3.279s 219680768 unknown 874.968s 875.043s 162394112 true 0.932s 0.563s 64102400
jayhorn-recursive/SatAckermann02_true-assert.jar timeout 900.744s 852.348s 2450558976 unknown 874.957s 875.032s 162361344 true 0.929s 0.576s 63262720
jayhorn-recursive/SatAckermann03_true-assert.jar true 11.785s 6.144s 335183872 unknown 874.941s 875.040s 151662592 true 0.956s 0.579s 64155648
jayhorn-recursive/SatAddition01_true-assert.jar true 4.957s 2.660s 193413120 unknown 876.109s 875.032s 6160928768 true 0.945s 0.580s 64040960
jayhorn-recursive/SatEvenOdd01_true-assert.jar timeout 900.536s 867.250s 1701531648 unknown 875.035s 875.035s 2337341440 true 0.971s 0.606s 61173760
jayhorn-recursive/SatFibonacci01_true-assert.jar true 5.634s 3.022s 219037696 unknown 874.960s 875.024s 125136896 true 0.969s 0.600s 63565824
jayhorn-recursive/SatFibonacci02_true-assert.jar unknown 14.468s 7.565s 383287296 true 0.533s 0.544s 44355584 true 0.991s 0.606s 64847872
jayhorn-recursive/SatFibonacci03_true-assert.jar unknown 15.948s 8.244s 367681536 unknown 874.967s 875.045s 125505536 true 0.993s 0.622s 63324160
jayhorn-recursive/SatGcd_true-assert.jar timeout 900.458s 869.290s 1178828800 unknown 875.076s 875.027s 1068912640 true 0.973s 0.592s 63705088
jayhorn-recursive/SatHanoi01_true-assert.jar false(reach) 8.831s 4.654s 270553088 unknown 874.936s 875.028s 119222272 true 0.973s 0.592s 64204800
jayhorn-recursive/SatMccarthy91_true-assert.jar true 5.986s 3.176s 222064640 unknown 874.944s 875.028s 148709376 true 0.984s 0.608s 63950848
jayhorn-recursive/SatMultCommutative01_true-assert.jar timeout 900.585s 861.210s 1717514240 unknown 875.006s 875.028s 250007552 true 0.942s 0.559s 64552960
jayhorn-recursive/SatPrimes01_true-assert.jar true 8.011s 4.195s 270929920 unknown 876.309s 875.034s 12642136064 true 1.039s 0.632s 64397312
jayhorn-recursive/UnsatAckermann01_false-assert.jar false(reach) 6.063s 3.179s 221933568 unknown 874.950s 875.038s 182509568 timeout 904.013s 456.257s 1138184192
jayhorn-recursive/UnsatAddition01_false-assert.jar false(reach) 4.798s 2.630s 213229568 false(reach) 17.042s 17.064s 574369792 unknown 171.439s 89.832s 1137905664
jayhorn-recursive/UnsatAddition02_false-assert.jar unknown 84.877s 62.432s 1533648896 unknown 876.185s 875.033s 8191352832 timeout 904.016s 456.480s 1145958400
jayhorn-recursive/UnsatEvenOdd01_false-assert.jar false(reach) 5.270s 2.782s 211591168 false(reach) 0.317s 0.329s 44650496 true 1.080s 0.647s 64143360
jayhorn-recursive/UnsatFibonacci01_false-assert.jar false(reach) 7.139s 3.704s 268984320 unknown 874.965s 875.035s 128679936 true 1.064s 0.663s 64020480
jayhorn-recursive/UnsatFibonacci02_false-assert.jar false(reach) 12.365s 6.392s 382595072 unknown 874.922s 875.023s 128651264 true 1.114s 0.654s 63246336
jayhorn-recursive/UnsatMccarthy91_false-assert.jar false(reach) 4.689s 2.499s 224600064 unknown 874.930s 875.031s 452280320 false(reach) 1.164s 0.715s 66564096
MinePump/spec1-5_product10_false-assert.jar timeout 900.821s 823.560s 2865393664 false(reach) 2.811s 2.833s 99360768 false(reach) 1.162s 0.691s 65163264
MinePump/spec1-5_product11_false-assert.jar unknown 678.975s 608.631s 2374897664 false(reach) 86.332s 86.347s 627404800 false(reach) 1.105s 0.653s 64937984
MinePump/spec1-5_product12_false-assert.jar false(reach) 552.377s 490.606s 2586324992 false(reach) 88.336s 88.362s 635265024 false(reach) 1.091s 0.663s 66691072
MinePump/spec1-5_product13_false-assert.jar timeout 900.975s 825.193s 2633707520 false(reach) 2.742s 2.762s 97415168 false(reach) 1.139s 0.683s 65241088
MinePump/spec1-5_product14_false-assert.jar timeout 900.997s 818.702s 2625343488 false(reach) 2.824s 2.845s 98799616 false(reach) 1.054s 0.646s 64212992
MinePump/spec1-5_product15_false-assert.jar false(reach) 494.693s 434.232s 2427555840 false(reach) 100.814s 100.836s 681979904 false(reach) 1.097s 0.678s 64733184
MinePump/spec1-5_product16_false-assert.jar timeout 900.958s 824.587s 2677272576 false(reach) 102.168s 102.186s 689602560 false(reach) 1.186s 0.708s 65994752
MinePump/spec1-5_product17_false-assert.jar unknown 64.967s 37.562s 1542676480 false(reach) 2.733s 2.752s 97656832 false(reach) 1.102s 0.674s 66985984
MinePump/spec1-5_product18_false-assert.jar timeout 901.238s 824.261s 2772615168 false(reach) 2.797s 2.806s 99139584 false(reach) 1.214s 0.723s 65146880
MinePump/spec1-5_product19_false-assert.jar false(reach) 677.775s 604.496s 2529198080 false(reach) 100.176s 100.214s 686297088 false(reach) 1.100s 0.686s 64962560
MinePump/spec1-5_product1_false-assert.jar false(reach) 99.023s 69.828s 1624469504 false(reach) 2.724s 2.741s 96104448 false(reach) 1.150s 0.698s 64299008
MinePump/spec1-5_product20_false-assert.jar unknown 735.211s 660.421s 2556596224 false(reach) 103.506s 103.532s 692539392 false(reach) 1.138s 0.693s 64655360
MinePump/spec1-5_product21_false-assert.jar timeout 901.042s 817.586s 2855927808 false(reach) 2.789s 2.802s 98160640 false(reach) 1.175s 0.692s 65032192
MinePump/spec1-5_product22_false-assert.jar false(reach) 551.029s 492.365s 2490531840 false(reach) 2.856s 2.869s 97935360 false(reach) 1.214s 0.722s 66772992
MinePump/spec1-5_product23_false-assert.jar false(reach) 587.162s 523.346s 2512027648 false(reach) 119.182s 119.211s 733818880 false(reach) 1.198s 0.706s 65048576
MinePump/spec1-5_product24_false-assert.jar timeout 901.944s 817.950s 3058163712 false(reach) 123.262s 123.285s 744325120 false(reach) 1.108s 0.671s 66109440
MinePump/spec1-5_product25_false-assert.jar timeout 901.015s 826.683s 2690502656 false(reach) 2.766s 2.778s 97198080 false(reach) 1.136s 0.684s 65617920
MinePump/spec1-5_product26_false-assert.jar timeout 900.176s 817.492s 2748788736 false(reach) 2.779s 2.789s 98435072 false(reach) 1.135s 0.691s 65359872
MinePump/spec1-5_product27_false-assert.jar false(reach) 652.589s 590.135s 2367148032 false(reach) 100.410s 100.433s 686370816 false(reach) 1.159s 0.700s 68345856
MinePump/spec1-5_product28_false-assert.jar false(reach) 782.349s 701.787s 2574823424 false(reach) 103.231s 103.275s 691531776 false(reach) 1.121s 0.686s 66654208
MinePump/spec1-5_product29_false-assert.jar timeout 900.996s 821.223s 2580332544 false(reach) 2.678s 2.690s 97058816 false(reach) 1.177s 0.704s 66318336
MinePump/spec1-5_product2_false-assert.jar false(reach) 570.059s 504.010s 2487775232 false(reach) 2.796s 2.813s 98533376 false(reach) 1.140s 0.692s 64987136
MinePump/spec1-5_product30_false-assert.jar unknown 64.647s 37.691s 1518444544 false(reach) 2.796s 2.801s 97648640 false(reach) 1.220s 0.722s 66306048
MinePump/spec1-5_product31_false-assert.jar false(reach) 695.438s 623.863s 2515615744 false(reach) 121.084s 121.110s 737738752 false(reach) 1.150s 0.676s 65196032
MinePump/spec1-5_product32_false-assert.jar false(reach) 523.459s 462.510s 2383286272 false(reach) 123.202s 123.220s 745545728 false(reach) 1.143s 0.699s 65454080
MinePump/spec1-5_product33_false-assert.jar false(reach) 857.800s 780.833s 2532900864 false(reach) 80.553s 80.575s 609067008 false(reach) 1.141s 0.693s 65019904
MinePump/spec1-5_product34_false-assert.jar timeout 901.035s 817.170s 2848976896 false(reach) 83.620s 83.636s 620589056 false(reach) 1.139s 0.658s 64679936
MinePump/spec1-5_product35_false-assert.jar false(reach) 697.830s 625.296s 2517204992 false(reach) 104.231s 104.254s 696414208 false(reach) 1.147s 0.697s 65155072
MinePump/spec1-5_product36_false-assert.jar false(reach) 560.144s 499.504s 2465787904 false(reach) 105.930s 105.947s 702509056 false(reach) 1.163s 0.716s 66420736
MinePump/spec1-5_product37_false-assert.jar timeout 900.165s 820.644s 3067101184 false(reach) 93.004s 93.024s 651923456 false(reach) 1.151s 0.692s 65105920
MinePump/spec1-5_product38_false-assert.jar timeout 901.149s 820.232s 2936037376 false(reach) 95.906s 95.924s 666243072 false(reach) 1.087s 0.637s 65679360
MinePump/spec1-5_product39_false-assert.jar false(reach) 613.993s 551.756s 2570129408 false(reach) 123.254s 123.286s 750075904 false(reach) 1.150s 0.689s 65138688
MinePump/spec1-5_product3_false-assert.jar false(reach) 707.726s 638.300s 2532605952 false(reach) 85.820s 85.841s 624455680 false(reach) 1.183s 0.700s 66101248
MinePump/spec1-5_product40_false-assert.jar false(reach) 686.830s 616.611s 2496233472 false(reach) 125.231s 125.258s 755154944 false(reach) 1.117s 0.697s 66146304
MinePump/spec1-5_product41_false-assert.jar false(reach) 569.054s 509.524s 2469847040 false(reach) 88.972s 89.004s 636436480 false(reach) 1.220s 0.739s 66551808
MinePump/spec1-5_product42_false-assert.jar timeout 901.160s 825.399s 2755801088 false(reach) 91.679s 91.709s 647262208 false(reach) 1.153s 0.685s 66760704
MinePump/spec1-5_product43_false-assert.jar unknown 668.991s 603.326s 2361135104 false(reach) 114.610s 114.648s 728621056 false(reach) 1.203s 0.713s 65138688
MinePump/spec1-5_product44_false-assert.jar false(reach) 565.677s 501.046s 2525184000 false(reach) 117.238s 117.271s 737746944 false(reach) 1.161s 0.697s 67837952
MinePump/spec1-5_product45_false-assert.jar timeout 901.023s 820.165s 2612703232 false(reach) 103.631s 103.650s 683634688 true 1.053s 0.623s 64929792
MinePump/spec1-5_product46_false-assert.jar false(reach) 645.138s 579.087s 2430275584 false(reach) 109.747s 109.767s 690769920 true 1.193s 0.705s 66166784
MinePump/spec1-5_product47_false-assert.jar false(reach) 852.900s 779.017s 2667712512 false(reach) 141.526s 141.561s 791474176 true 1.165s 0.699s 66146304
MinePump/spec1-5_product48_false-assert.jar false(reach) 617.859s 548.977s 2577022976 false(reach) 143.689s 143.720s 800915456 true 1.124s 0.676s 66162688
MinePump/spec1-5_product49_false-assert.jar timeout 901.198s 818.987s 2819674112 false(reach) 93.725s 93.742s 655880192 false(reach) 1.116s 0.687s 65064960
MinePump/spec1-5_product4_false-assert.jar timeout 901.067s 826.393s 2562981888 false(reach) 89.158s 89.180s 641437696 false(reach) 1.102s 0.667s 64192512
MinePump/spec1-5_product50_false-assert.jar false(reach) 516.009s 454.652s 2380922880 false(reach) 97.873s 97.891s 665755648 false(reach) 1.150s 0.705s 64802816
MinePump/spec1-5_product51_false-assert.jar timeout 901.095s 826.244s 2922082304 false(reach) 122.698s 122.717s 747036672 false(reach) 1.060s 0.655s 64516096
MinePump/spec1-5_product52_false-assert.jar false(reach) 608.786s 547.746s 2567835648 false(reach) 126.481s 126.504s 761430016 false(reach) 1.154s 0.705s 64700416
MinePump/spec1-5_product53_false-assert.jar false(reach) 562.874s 499.631s 2494967808 false(reach) 112.212s 112.230s 703995904 false(reach) 1.066s 0.630s 65339392
MinePump/spec1-5_product54_false-assert.jar false(reach) 562.986s 500.429s 2502438912 false(reach) 114.903s 114.926s 709705728 false(reach) 1.047s 0.637s 65134592
MinePump/spec1-5_product55_false-assert.jar false(reach) 689.989s 619.467s 2453901312 false(reach) 153.072s 153.109s 813412352 false(reach) 1.192s 0.702s 66879488
MinePump/spec1-5_product56_false-assert.jar timeout 901.101s 821.753s 3056783360 false(reach) 154.428s 154.453s 816648192 false(reach) 1.155s 0.692s 64548864
MinePump/spec1-5_product57_true-assert.jar false(reach) 664.082s 594.637s 2496380928 true 212.842s 212.876s 693190656 true 1.188s 0.711s 65265664
MinePump/spec1-5_product58_true-assert.jar timeout 900.125s 814.932s 3248152576 true 220.400s 220.440s 706199552 true 1.100s 0.666s 67686400
MinePump/spec1-5_product59_true-assert.jar false(reach) 613.348s 553.456s 2459967488 true 292.183s 292.224s 888954880 true 1.250s 0.769s 65597440
MinePump/spec1-5_product5_false-assert.jar false(reach) 660.515s 591.627s 2663403520 false(reach) 2.749s 2.772s 97333248 false(reach) 1.149s 0.704s 65859584
MinePump/spec1-5_product60_true-assert.jar false(reach) 721.386s 647.200s 2496598016 true 300.663s 300.704s 808890368 true 1.162s 0.705s 64540672
MinePump/spec1-5_product61_true-assert.jar false(reach) 813.352s 738.564s 2669887488 true 263.296s 263.348s 741523456 true 1.141s 0.692s 67375104
MinePump/spec1-5_product62_true-assert.jar false(reach) 575.803s 515.980s 2471698432 true 270.806s 270.851s 752189440 true 1.137s 0.691s 64315392
MinePump/spec1-5_product63_true-assert.jar timeout 900.960s 822.733s 2507763712 true 371.996s 372.054s 862433280 true 1.155s 0.682s 64716800
MinePump/spec1-5_product64_true-assert.jar false(reach) 589.159s 521.216s 2615582720 true 382.229s 382.283s 871108608 true 1.227s 0.741s 66318336
MinePump/spec1-5_product6_false-assert.jar timeout 900.232s 815.742s 3037171712 false(reach) 2.784s 2.795s 98766848 false(reach) 1.173s 0.720s 65875968
MinePump/spec1-5_product7_false-assert.jar false(reach) 568.459s 508.424s 2446778368 false(reach) 100.088s 100.114s 682782720 false(reach) 1.194s 0.720s 65765376
MinePump/spec1-5_product8_false-assert.jar false(reach) 709.501s 639.593s 2527936512 false(reach) 101.917s 101.944s 691400704 false(reach) 1.122s 0.664s 64548864
MinePump/spec1-5_product9_false-assert.jar timeout 901.077s 822.711s 2842873856 false(reach) 2.692s 2.704s 96624640 false(reach) 1.153s 0.685s 65056768
sv-benchmarks/java/ status cputime walltime memUsage status cputime walltime memUsage status cputime walltime memUsage
total tasks 368 51828.354 46281.280 245770743808 368 29396.949 29400.214 88279203840 368 3253.102 2129.051 26829410304
local summary 27503.268 46342.270 9182.980 29464.288 543.460 2172.815
    correct results 217 19538.615 17074.321 117056225280 331 7466.179 7471.890 50042761216 277 285.223 173.148 17791205376
        correct true 51 233.866 126.411 10348670976 138 2414.990 2417.504 12711149568 158 158.950 96.636 10105884672
        correct false 166 19304.749 16947.910 106707554304 193 5051.190 5054.386 37331611648 119 126.272 76.512 7685320704
    incorrect results 103 4695.067 3986.056 39280283648 11 52.008 52.148 804532224 81 82.142 50.059 5170966528
        incorrect true 5 15.179 8.569 856076288 1 4.592 4.612 89309184 77 78.127 47.585 4912562176
        incorrect false 98 4679.888 3977.487 38424207360 10 47.416 47.536 715223040 4 4.015 2.474 258404352
score (368 tasks, max score: 532) -1460 - - - 277 - - - -2093 - - -
Run set jayhorn.sv-comp18 jbmc.sv-comp18 jpf.sv-comp18