Tool 2LS 0.5.0 BLAST 2.7.3 CBMC 5.6 Ceagle Ceagle 1.3 @ 53cfa89 CPAchecker 1.6.1-svn 23987 CPAchecker 1.6.1-svn 24048 DepthK DepthK version 3.0 - Fri Jan 6 18:14:20 AMT 2017 ESBMC ESBMC version 3.1 64-bit x86_64 linux SMACK+Corral 1.7.2 symbiotic KLEE:7f3c74aa-dg:96e851cf-symbiotic:69a1d8e6-minisat:3db58943-stp:39fa956f-LLVMInstrumentation:f750b24a ULTIMATE Automizer f7c3ed31 ULTIMATE Kojak f7c3ed31 ULTIMATE Taipan f7c3ed31 VeriAbs
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-57-generic [Linux 4.4.0-57-generic; Linux 4.4.0-59-generic] Linux 4.4.0-59-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB
Date of execution 2017-01-10 17:21:21 CET [[ 2017-01-14 18:00:17 CET ]] [[ 2017-01-14 20:02:31 CET ]] [[ 2017-01-14 18:18:08 CET ]] [[ 2017-01-14 20:29:39 CET ]] 2017-01-10 17:21:21 CET [[ 2017-01-14 18:00:17 CET ]] [[ 2017-01-14 19:51:44 CET ]] [[ 2017-01-14 18:06:48 CET ]] [[ 2017-01-14 19:59:41 CET ]] 2017-01-10 17:21:21 CET [[ 2017-01-14 18:00:17 CET ]] [[ 2017-01-14 19:57:11 CET ]] [[ 2017-01-14 18:18:10 CET ]] [[ 2017-01-14 20:00:30 CET ]] 2017-01-10 17:21:21 CET [[ 2017-01-14 18:00:17 CET ]] [[ 2017-01-14 19:52:12 CET ]] [[ 2017-01-14 18:07:02 CET ]] [[ 2017-01-14 19:59:19 CET ]] 2017-01-10 20:44:08 CET [[ 2017-01-14 18:01:01 CET ]] [[ 2017-01-14 20:09:29 CET ]] [[ 2017-01-14 18:26:00 CET ]] [[ 2017-01-14 20:41:28 CET ]] 2017-01-10 22:04:57 CET [[ 2017-01-14 18:01:27 CET ]] [[ 2017-01-14 20:11:29 CET ]] [[ 2017-01-14 18:28:10 CET ]] [[ 2017-01-14 20:42:56 CET ]] 2017-01-11 11:18:39 CET [[ 2017-01-14 21:32:33 CET ]] [[ 2017-01-14 22:21:46 CET ]] [[ 2017-01-14 21:35:07 CET ]] [[ 2017-01-14 22:35:09 CET ]] 2017-01-11 11:24:16 CET [[ 2017-01-14 21:58:42 CET ]] [[ 2017-01-14 22:27:33 CET ]] [[ 2017-01-14 22:07:52 CET ]] [[ 2017-01-14 22:42:14 CET ]] 2017-01-11 11:31:18 CET [[ 2017-01-14 22:07:55 CET ]] [[ 2017-01-14 22:45:22 CET ]] [[ 2017-01-14 22:11:49 CET ]] [[ 2017-01-14 23:12:14 CET ]] 2017-01-11 15:09:43 CET [[ 2017-01-14 22:26:56 CET ]] [[ 2017-01-14 23:59:25 CET ]] [[ 2017-01-14 22:42:14 CET ]] [[ 2017-01-15 00:15:34 CET ]] 2017-01-11 16:16:17 CET [[ 2017-01-14 22:37:08 CET ]] [[ 2017-01-15 00:13:18 CET ]] [[ 2017-01-14 22:52:42 CET ]] [[ 2017-01-15 00:24:59 CET ]] 2017-01-12 12:02:41 CET [[ 2017-01-14 22:52:01 CET ]] [[ 2017-01-15 00:27:39 CET ]] [[ 2017-01-14 23:20:04 CET ]] [[ 2017-01-15 00:48:54 CET ]] 2017-01-13 11:09:55 CET [[ 2017-01-15 01:36:45 CET ]] [[ 2017-01-15 02:12:47 CET ]] [[ 2017-01-15 01:38:53 CET ]] [[ 2017-01-15 02:35:07 CET ]] 2017-01-13 11:10:58 CET [[ 2017-01-15 02:01:54 CET ]] [[ 2017-01-15 02:34:25 CET ]] [[ 2017-01-15 02:04:28 CET ]] [[ 2017-01-15 03:02:21 CET ]] 2017-01-13 12:41:58 CET [[ 2017-01-15 02:09:41 CET ]] [[ 2017-01-15 04:03:21 CET ]] [[ 2017-01-15 02:31:54 CET ]] [[ 2017-01-15 04:27:36 CET ]] 2017-01-13 13:05:01 CET [[ 2017-01-15 02:11:27 CET ]] [[ 2017-01-15 04:07:55 CET ]] [[ 2017-01-15 02:33:46 CET ]] [[ 2017-01-15 04:34:07 CET ]] 2017-01-14 09:46:18 CET [[ 2017-01-15 02:18:39 CET ]] [[ 2017-01-15 04:12:25 CET ]] [[ 2017-01-15 02:37:40 CET ]] [[ 2017-01-15 04:38:18 CET ]] 2017-01-14 09:46:18 CET [[ 2017-01-15 04:55:34 CET ]] [[ 2017-01-15 05:46:09 CET ]] [[ 2017-01-15 05:17:25 CET ]] [[ 2017-01-15 05:48:02 CET ]]
Run set 2ls.sv-comp17.ReachSafety-Arrays blast.sv-comp17.ReachSafety-Arrays cbmc.sv-comp17.ReachSafety-Arrays ceagle.sv-comp17.ReachSafety-Arrays cpa-bam-bnb.sv-comp17.ReachSafety-Arrays cpa-kind.sv-comp17.ReachSafety-Arrays cpa-seq.sv-comp17.ReachSafety-Arrays depthk.sv-comp17.ReachSafety-Arrays esbmc.sv-comp17.ReachSafety-Arrays esbmc-falsi.sv-comp17.ReachSafety-Arrays esbmc-incr.sv-comp17.ReachSafety-Arrays esbmc-kind.sv-comp17.ReachSafety-Arrays smack.sv-comp17.ReachSafety-Arrays symbiotic4.sv-comp17.ReachSafety-Arrays uautomizer.sv-comp17.ReachSafety-Arrays ukojak.sv-comp17.ReachSafety-Arrays utaipan.sv-comp17.ReachSafety-Arrays veriabs.sv-comp17.ReachSafety-Arrays
Options --graphml-witness witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/2ls.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/2ls.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/2ls.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/2ls.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] -alias empty -enable-recursion -noprofile -cref -sv-comp -lattice -include-lattice symb -nosserr -svcomp-witness error-witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/blast.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/blast.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/blast.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/blast.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] --graphml-witness witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cbmc.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cbmc.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cbmc.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cbmc.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] --compiler clang-3.7 [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ceagle.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ceagle.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ceagle.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ceagle.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] -sv-comp17-bam-bnb -disable-java-assertions -heap 10000m [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-bam-bnb.2017-01-10_2044.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-bam-bnb.2017-01-10_2044.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-bam-bnb.2017-01-10_2044.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-bam-bnb.2017-01-10_2044.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] -sv-comp17-k-induction -heap 10000M -disable-java-assertions [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-kind.2017-01-10_2204.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-kind.2017-01-10_2204.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-kind.2017-01-10_2204.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-kind.2017-01-10_2204.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] -sv-comp17 -heap 10000M -disable-java-assertions [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-seq.2017-01-11_1118.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-seq.2017-01-11_1118.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-seq.2017-01-11_1118.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-seq.2017-01-11_1118.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/depthk.2017-01-11_1124.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/depthk.2017-01-11_1124.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/depthk.2017-01-11_1124.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/depthk.2017-01-11_1124.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] -s fixed [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc.2017-01-11_1131.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc.2017-01-11_1131.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc.2017-01-11_1131.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc.2017-01-11_1131.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] -s falsi [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-falsi.2017-01-11_1509.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-falsi.2017-01-11_1509.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-falsi.2017-01-11_1509.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-falsi.2017-01-11_1509.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] -s incr [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-incr.2017-01-11_1616.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-incr.2017-01-11_1616.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-incr.2017-01-11_1616.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-incr.2017-01-11_1616.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] -s kinduction [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-kind.2017-01-12_1202.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-kind.2017-01-12_1202.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-kind.2017-01-12_1202.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-kind.2017-01-12_1202.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] -w error-witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/smack.2017-01-13_1109.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/smack.2017-01-13_1109.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/smack.2017-01-13_1109.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/smack.2017-01-13_1109.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] --witness witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/symbiotic4.2017-01-13_1110.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/symbiotic4.2017-01-13_1110.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/symbiotic4.2017-01-13_1110.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/symbiotic4.2017-01-13_1110.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/uautomizer.2017-01-13_1241.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/uautomizer.2017-01-13_1241.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/uautomizer.2017-01-13_1241.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/uautomizer.2017-01-13_1241.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ukojak.2017-01-13_1305.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ukojak.2017-01-13_1305.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ukojak.2017-01-13_1305.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ukojak.2017-01-13_1305.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/utaipan.2017-01-14_0946.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/utaipan.2017-01-14_0946.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/utaipan.2017-01-14_0946.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/utaipan.2017-01-14_0946.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/veriabs.2017-01-14_0946.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/veriabs.2017-01-14_0946.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/veriabs.2017-01-14_0946.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/veriabs.2017-01-14_0946.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]
../../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score
array-examples/data_structures_set_multi_proc_false-unreach-call_ground.i out of memory 41   15000 470 0 exception (gremlins) 180     160   2000    0 error (1) 130    14000 1700   0 false(unreach-call) .058 11   .41 1 error 2.6 280 21 0 timeout 900   4400 11000 0 timeout 900 4300 12000 0 timeout 900 750 13000 0 out of memory 64    15000 860   0 timeout 900    230 12000   0 timeout 900     590 2500    0 timeout 900     1100 11000    0 false(unreach-call) 2.7 85 29 1 false(unreach-call) 2.5  300   28   1 timeout 900   5600 12000 0 timeout 900   5200 12000 0 timeout 900   5300 14000 0 out of memory 43   15000 530 0
array-examples/sorting_bubblesort_false-unreach-call2_ground.i out of memory 38   15000 530 0 exception (gremlins) 40     64   410    0 out of memory 22    15000 250   0 false(unreach-call) 24     8.3 250    1 error 2.5 280 24 0 timeout 900   2400 11000 0 timeout 900 1400 13000 0 unknown 46 160 640 0 out of memory 150    15000 1100   0 timeout 900    970 11000   0 out of memory 360     15000 4400    0 timeout 900     500 9000    0 false(unreach-call) 2.2 94 25 1 timeout (timeout) 900    4200   9700   0 timeout 900   2500 13000 0 timeout 900   4400 12000 0 timeout 900   2200 12000 0 out of memory 440   15000 5700 0
array-examples/sorting_bubblesort_false-unreach-call_ground.i out of memory 38   15000 540 0 exception (gremlins) 40     66   470    0 out of memory 22    15000 290   0 false(unreach-call) 18     11   230    1 error 2.4 270 21 0 timeout 900   2100 11000 0 timeout 900 1400 14000 0 unknown 46 160 610 0 out of memory 140    15000 1100   0 timeout 900    970 10000   0 out of memory 360     15000 5100    0 timeout 900     450 7700    0 false(unreach-call) 2.2 90 27 1 timeout (timeout) 900    4200   9300   0 timeout 900   2300 14000 0 timeout 900   3900 13000 0 timeout 900   2100 14000 0 out of memory 430   15000 4900 0
array-examples/sorting_selectionsort_false-unreach-call2_ground.i out of memory 39   15000 540 0 exception (gremlins) 170     54   1700    0 error (134) 58    13000 760   0 false(unreach-call) .067 11   .36 1 error 2.4 260 20 0 timeout 900   2300 12000 0 timeout 900 2200 13000 0 unknown 890 330 10000 0 out of memory 34    15000 320   0 timeout 900    530 11000   0 out of memory 280     15000 3200    0 timeout 900     400 8600    0 false(unreach-call) 18   560 230 1 error 340    71   3500   0 timeout 900   2400 13000 0 timeout 900   3400 14000 0 timeout 900   2400 13000 0 out of memory 110   15000 1100 0
array-examples/sorting_selectionsort_false-unreach-call_ground.i out of memory 40   15000 520 0 timeout 900     270   9800    0 error (134) 70    13000 910   0 false(unreach-call) .056 13   .56 1 error 2.5 280 22 0 timeout 900   2100 13000 0 timeout 900 2200 10000 0 unknown 890 330 8200 0 out of memory 34    15000 310   0 timeout 900    530 11000   0 out of memory 280     15000 3200    0 timeout 900     430 7600    0 false(unreach-call) 120   650 1400 1 error 340    70   3300   0 timeout 900   3000 13000 0 timeout 900   2600 12000 0 timeout 900   2600 12000 0 out of memory 110   15000 1200 0
array-examples/standard_allDiff2_false-unreach-call_ground.i out of memory 220   15000 1900 0 timeout 900     390   11000    0 error (1) 410    10000 2400   0 false(unreach-call) 9.2   11   130    1 error 2.5 280 23 0 timeout 900   2100 12000 0 timeout 900 2200 11000 0 unknown 900 1500 9300 0 out of memory 40    15000 440   0 timeout 900    4500 11000   0 timeout 900     7500 11000    0 timeout 900     5900 10000    0 false(unreach-call) 20   130 240 1 false(unreach-call) 1.0  150   13   1 timeout 900   5700 15000 0 timeout 900   2300 13000 0 timeout 900   5400 13000 0 out of memory 170   15000 1900 0
array-examples/standard_copy1_false-unreach-call_ground.i timeout 900   13000 12000 0 exception (gremlins) 28     66   290    0 out of memory 130    15000 1700   0 false(unreach-call) .053 9.3 .31 1 error 2.3 270 20 0 timeout 900   2200 14000 0 timeout 900 2200 12000 0 unknown 79 100 1000 0 false(unreach-call) 310    670 4000   1 timeout 900    1300 1600   0 out of memory 280     15000 3600    0 out of memory 280     15000 3300    0 false(unreach-call) 1.8 83 25 1 false(unreach-call) 1.8  230   21   1 timeout 900   2300 14000 0 timeout 900   3500 14000 0 timeout 900   1800 13000 0 false(unreach-call) 5.5 220 44 1
array-examples/standard_copy2_false-unreach-call_ground.i out of memory 38   15000 510 0 exception (gremlins) 95     77   1000    0 out of memory 83    15000 1000   0 false(unreach-call) .082 11   .33 1 error 2.3 270 22 0 timeout 900   2200 12000 0 timeout 900 2200 12000 0 unknown 890 190 9700 0 false(unreach-call) 490    820 5800   1 timeout 900    5300 12000   0 out of memory 290     15000 3400    0 timeout 900     330 2100    0 false(unreach-call) 1.8 77 26 1 false(unreach-call) 4.6  560   50   1 timeout 900   3300 13000 0 timeout 900   3400 13000 0 timeout 900   2400 12000 0 false(unreach-call) 5.8 220 43 1
array-examples/standard_copy3_false-unreach-call_ground.i out of memory 39   15000 560 0 exception (gremlins) 290     110   3500    0 out of memory 94    15000 1500   0 false(unreach-call) .052 11   .43 1 error 2.5 270 22 0 timeout 900   2100 13000 0 timeout 900 2400 12000 0 unknown 890 200 10000 0 false(unreach-call) 660    970 8500   1 timeout 900    5200 11000   0 out of memory 290     15000 3800    0 timeout 900     680 10000    0 false(unreach-call) 1.9 80 23 1 false(unreach-call) 5.9  840   64   1 timeout 900   4200 12000 0 timeout 900   3600 12000 0 timeout 900   3500 14000 0 false(unreach-call) 6.0 220 46 1
array-examples/standard_copy4_false-unreach-call_ground.i out of memory 38   15000 610 0 timeout 900     250   9800    0 out of memory 100    15000 1400   0 false(unreach-call) .044 8.2 .41 1 error 2.4 260 23 0 timeout 900   2300 12000 0 timeout 900 2400 11000 0 unknown 890 190 11000 0 false(unreach-call) 810    1100 11000   1 timeout 900    5300 12000   0 out of memory 290     15000 3500    0 timeout 900     660 10000    0 false(unreach-call) 2.0 85 25 1 false(unreach-call) 7.4  1100   84   1 timeout 900   4900 15000 0 timeout 900   4300 12000 0 timeout 900   5000 13000 0 false(unreach-call) 6.0 220 60 1
array-examples/standard_copy5_false-unreach-call_ground.i out of memory 39   15000 550 0 timeout 850     290   10000    0 out of memory 120    15000 1500   0 false(unreach-call) .076 8.3 .33 1 error 2.5 260 22 0 timeout 900   2300 12000 0 timeout 900 2400 11000 0 unknown 900 210 11000 0 false(unreach-call) 890    1200 10000   1 timeout 900    5300 11000   0 out of memory 280     15000 3700    0 timeout 900     830 8300    0 false(unreach-call) 2.0 83 28 1 false(unreach-call) 8.7  1400   110   1 timeout 900   5000 13000 0 timeout 900   3800 13000 0 timeout 900   5100 13000 0 false(unreach-call) 6.2 230 48 1
array-examples/standard_copy6_false-unreach-call_ground.i out of memory 39   15000 570 0 timeout 900     500   8400    0 error (134) 93    15000 1200   0 false(unreach-call) .053 8.4 .38 1 error 2.4 260 21 0 timeout 900   2100 12000 0 timeout 900 2200 13000 0 unknown 890 240 9300 0 false(unreach-call) 890    1200 12000   1 timeout 900    5300 12000   0 out of memory 290     15000 3900    0 timeout 900     730 9700    0 false(unreach-call) 2.1 88 26 1 false(unreach-call) 10    1700   130   1 timeout 900   5100 14000 0 timeout 900   4800 13000 0 timeout 900   5300 13000 0 false(unreach-call) 6.3 220 49 1
array-examples/standard_copy7_false-unreach-call_ground.i out of memory 39   15000 470 0 timeout 900     610   8100    0 out of memory 100    15000 1600   0 false(unreach-call) .050 11   .41 1 error 2.4 270 22 0 timeout 900   2000 12000 0 timeout 900 3500 12000 0 unknown 900 270 9700 0 false(unreach-call) 900    1300 10000   1 timeout 900    5300 14000   0 out of memory 290     15000 3500    0 timeout 900     750 10000    0 false(unreach-call) 2.2 91 27 1 false(unreach-call) 11    1900   170   1 timeout 900   5200 13000 0 timeout 900   2900 15000 0 timeout 900   5200 14000 0 false(unreach-call) 6.9 220 50 1
array-examples/standard_copy8_false-unreach-call_ground.i out of memory 39   15000 460 0 timeout 900     590   8600    0 error (134) 82    14000 1200   0 false(unreach-call) .062 12   .45 1 error 2.4 270 21 0 timeout 900   2300 11000 0 timeout 900 2200 13000 0 unknown 900 300 9900 0 false(unreach-call) 890    1400 10000   1 timeout 900    5300 13000   0 out of memory 280     15000 3700    0 timeout 900     840 12000    0 false(unreach-call) 2.3 93 25 1 false(unreach-call) 13    2200   160   1 timeout 900   5100 12000 0 timeout 900   2400 12000 0 timeout 900   5300 14000 0 false(unreach-call) 7.1 220 59 1
array-examples/standard_copy9_false-unreach-call_ground.i out of memory 38   15000 530 0 timeout 900     610   8000    0 error (134) 89    14000 1400   0 false(unreach-call) .055 11   .46 1 error 2.5 270 23 0 timeout 900   2100 15000 0 timeout 900 3500 11000 0 unknown 900 330 9200 0 false(unreach-call) 890    1400 9800   1 timeout 900    5300 12000   0 out of memory 290     15000 4700    0 timeout 900     820 8700    0 false(unreach-call) 2.3 93 28 1 false(unreach-call) 14    2500   160   1 timeout 900   5100 12000 0 timeout 900   3600 13000 0 timeout 900   5300 12000 0 false(unreach-call) 7.1 220 60 1
array-examples/standard_copyInitSum2_false-unreach-call_ground.i out of memory 41   15000 520 0 timeout 900     480   8500    0 out of memory 78    15000 1200   0 false(unreach-call) .049 8.6 .37 1 error 2.5 280 23 0 timeout 900   1900 12000 0 timeout 900 730 11000 0 unknown 890 240 9900 0 false(unreach-call) 340    680 4200   1 timeout 900    5900 12000   0 out of memory 270     15000 3500    0 timeout 900     670 8600    0 false(unreach-call) 1.9 84 29 1 false(unreach-call) 2.6  560   35   1 timeout 900   4100 13000 0 timeout 900   2500 12000 0 timeout 900   3300 13000 0 false(unreach-call) 6.0 220 46 1
array-examples/standard_init1_false-unreach-call_ground.i timeout 900   9800 11000 0 timeout 900     230   9900    0 out of memory 130    15000 1800   0 false(unreach-call) .061 11   .45 1 error 2.6 280 26 0 timeout 900   2100 12000 0 timeout 900 740 12000 0 timeout 900 770 13000 0 false(unreach-call) 160    530 1800   1 timeout 900    5800 11000   0 out of memory 260     15000 3400    0 timeout 900     560 10000    0 false(unreach-call) 1.7 77 23 1 false(unreach-call) 1.4  280   18   1 timeout 900   2400 15000 0 timeout 900   2500 13000 0 timeout 900   1700 12000 0 false(unreach-call) 5.6 220 43 1
array-examples/standard_init2_false-unreach-call_ground.i out of memory 43   15000 550 0 timeout 900     410   11000    0 out of memory 67    15000 880   0 false(unreach-call) .056 13   .47 1 error 2.6 280 26 0 timeout 900   2100 11000 0 timeout 900 720 12000 0 timeout 900 800 12000 0 false(unreach-call) 490    790 6000   1 timeout 900    5900 11000   0 out of memory 270     15000 3200    0 timeout 900     660 10000    0 false(unreach-call) 1.7 85 23 1 false(unreach-call) 2.7  560   33   1 timeout 900   2500 13000 0 timeout 900   3900 15000 0 timeout 900   2300 11000 0 false(unreach-call) 5.6 220 49 1
array-examples/standard_init3_false-unreach-call_ground.i out of memory 42   15000 570 0 timeout 900     290   11000    0 out of memory 70    15000 910   0 false(unreach-call) .051 11   .42 1 error 2.5 280 21 0 timeout 900   2000 13000 0 timeout 900 760 12000 0 timeout 900 710 14000 0 false(unreach-call) 790    1100 11000   1 timeout 900    5900 12000   0 out of memory 270     15000 3900    0 timeout 900     540 9900    0 false(unreach-call) 1.8 86 23 1 false(unreach-call) 3.9  840   49   1 timeout 900   2700 13000 0 timeout 900   4100 12000 0 timeout 900   2500 13000 0 false(unreach-call) 5.6 230 44 1
array-examples/standard_init4_false-unreach-call_ground.i out of memory 42   15000 540 0 timeout 900     290   9800    0 out of memory 73    15000 890   0 false(unreach-call) .090 49   .97 1 error 2.4 260 21 0 timeout 900   2100 13000 0 timeout 900 780 13000 0 timeout 900 750 11000 0 false(unreach-call) 900    1200 12000   1 timeout 900    5800 11000   0 out of memory 260     15000 3700    0 timeout 900     690 9300    0 false(unreach-call) 1.8 82 23 1 false(unreach-call) 5.1  1100   52   1 timeout 900   3500 13000 0 timeout 900   3700 12000 0 timeout 900   3200 14000 0 false(unreach-call) 6.1 220 43 1
array-examples/standard_init5_false-unreach-call_ground.i out of memory 42   15000 540 0 timeout 900     290   8900    0 out of memory 76    15000 990   0 false(unreach-call) .077 11   .28 1 error 2.4 260 21 0 timeout 900   2300 12000 0 timeout 900 730 12000 0 unknown 900 230 9400 0 false(unreach-call) 890    1300 12000   1 timeout 900    5900 12000   0 out of memory 260     15000 4100    0 timeout 900     650 9000    0 false(unreach-call) 1.8 79 21 1 false(unreach-call) 6.5  1400   82   1 timeout 900   3800 14000 0 timeout 900   3100 12000 0 timeout 900   3800 13000 0 false(unreach-call) 6.3 220 48 1
array-examples/standard_init6_false-unreach-call_ground.i out of memory 42   15000 500 0 timeout 900     290   10000    0 out of memory 79    15000 1000   0 false(unreach-call) .051 8.3 .38 1 error 2.6 280 23 0 timeout 900   1900 12000 0 timeout 900 850 11000 0 unknown 890 240 11000 0 false(unreach-call) 900    1400 10000   1 timeout 900    5800 11000   0 out of memory 260     15000 3900    0 timeout 900     770 8200    0 false(unreach-call) 1.8 86 22 1 false(unreach-call) 7.7  1700   93   1 timeout 900   5100 14000 0 timeout 900   3100 14000 0 timeout 900   5000 13000 0 false(unreach-call) 6.4 220 47 1
array-examples/standard_init7_false-unreach-call_ground.i out of memory 42   15000 620 0 timeout 900     290   9700    0 out of memory 55    15000 720   0 false(unreach-call) .063 11   .46 1 error 2.6 270 20 0 timeout 900   1800 12000 0 timeout 900 800 14000 0 unknown 890 270 11000 0 false(unreach-call) 890    1500 10000   1 timeout 900    5900 12000   0 out of memory 260     15000 3700    0 timeout 900     450 1900    0 false(unreach-call) 1.9 80 25 1 false(unreach-call) 8.5  1900   97   1 timeout 900   5100 12000 0 timeout 900   4200 12000 0 timeout 900   5000 14000 0 false(unreach-call) 6.6 220 49 1
array-examples/standard_init8_false-unreach-call_ground.i out of memory 42   15000 600 0 timeout 900     280   12000    0 out of memory 57    15000 800   0 false(unreach-call) .075 11   .39 1 error 2.6 270 25 0 timeout 900   2100 13000 0 timeout 900 760 11000 0 unknown 900 290 8200 0 false(unreach-call) 890    1600 10000   1 timeout 900    6000 14000   0 out of memory 260     15000 3400    0 timeout 900     890 11000    0 false(unreach-call) 1.9 78 26 1 false(unreach-call) 9.9  2200   120   1 timeout 900   5100 14000 0 timeout 900   4500 13000 0 timeout 900   5300 13000 0 false(unreach-call) 6.9 220 52 1
array-examples/standard_init9_false-unreach-call_ground.i out of memory 42   15000 570 0 timeout 900     300   8800    0 out of memory 59    15000 920   0 false(unreach-call) .052 8.4 .35 1 error 2.5 270 21 0 timeout 900   2000 14000 0 timeout 900 760 11000 0 unknown 900 320 8400 0 false(unreach-call) 890    1800 12000   1 timeout 900    5900 11000   0 out of memory 260     15000 3800    0 timeout 900     740 8900    0 false(unreach-call) 1.9 81 26 1 false(unreach-call) 11    2500   130   1 timeout 900   5300 11000 0 timeout 900   4000 15000 0 timeout 900   5200 15000 0 false(unreach-call) 6.8 220 61 1
array-examples/standard_minInArray_false-unreach-call_ground.i out of memory 320   15000 3300 0 exception (gremlins) 42     65   490    0 error (42) 850    1300 3500   0 false(unreach-call) .049 11   .44 1 error 2.5 280 20 0 timeout 900   2300 11000 0 timeout 900 2200 13000 0 unknown 97 120 1400 0 false(unreach-call) 33    1300 380   1 timeout 900    530 9500   0 out of memory 290     15000 3900    0 out of memory 660     15000 8100    0 false(unreach-call) 1.9 90 23 1 error .50 100   5.8 0 timeout 900   2300 12000 0 timeout 900   2800 14000 0 timeout 900   1900 14000 0 unknown 270   1100 2800 0
array-examples/standard_partition_false-unreach-call_ground.i out of memory 40   15000 510 0 timeout 900     230   9100    0 error (134) 68    14000 810   0 false(unreach-call) .046 8.2 .38 1 error 2.5 280 21 0 timeout 900   2300 12000 0 timeout 900 2200 12000 0 timeout 900 2200 11000 0 false(unreach-call) 890    12000 10000   1 timeout 900    1100 11000   0 out of memory 330     15000 3700    0 timeout 900     630 8800    0 false(unreach-call) 2.0 91 29 1 timeout (timeout) 900    12000   8900   0 timeout 900   3000 12000 0 timeout 900   3800 12000 0 timeout 900   3100 12000 0 out of memory 35   15000 450 0
array-examples/standard_running_false-unreach-call.i out of memory 42   15000 580 0 timeout 900     310   11000    0 out of memory 94    15000 1300   0 false(unreach-call) .052 13   .60 1 error 2.6 280 21 0 timeout 900   2500 12000 0 timeout 900 2200 12000 0 unknown 890 310 11000 0 false(unreach-call) 900    1400 13000   1 out of memory 470    15000 6200   0 out of memory 840     15000 2300    0 timeout 900     730 9500    0 false(unreach-call) 2.3 100 23 1 error 1.2  160   14   0 timeout 900   3300 15000 0 timeout 900   3100 14000 0 timeout 900   2900 13000 0 out of memory 99   15000 1000 0
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i out of memory 41   15000 600 0 true .080 17   .49 2 error (42) 850    1500 4300   0 true .055 11   .47 2 error 2.7 280 22 0 true 3.9 280 26 2 true 160 2200 1900 2 unknown 900 1200 12000 0 out of memory 61    15000 610   0 timeout 900    11000 13000   0 out of memory 540     15000 6500    0 timeout 900     1200 8800    0 true 2.3 100 27 2 true .16 9.6 1.7 2 true 7.1 340 57 2 timeout 900   2200 12000 0 true 7.0 350 54 2 out of memory 43   15000 560 0
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i out of memory 41   15000 560 0 timeout 900     430   11000    0 error (134) 26    13000 340   0 true .068 11   .42 2 error 2.5 280 23 0 timeout 900   4000 12000 0 timeout 900 3700 12000 0 unknown 900 260 8300 0 out of memory 63    15000 760   0 timeout 900    230 12000   0 timeout 900     1100 8900    0 timeout 900     1300 9800    0 true 880   220 9900 2 timeout (timeout) 900    1300   10000   0 timeout 900   5300 14000 0 timeout 900   5200 13000 0 timeout 900   5400 12000 0 out of memory 41   15000 510 0
array-examples/relax_true-unreach-call.i false(unreach-call) 5.7 170 48 -16 false(unreach-call) 35     39   360    -16 error (42) 850    4800 3300   0 unknown .031 8.2 .14 0 error 7.6 410 57 0 timeout 950   3800 9200 0 timeout 900 4900 8000 0 unknown 890 190 11000 0 true 890    3200 10000   2 timeout 900    540 7200   0 timeout 900     240 2400    0 timeout 900     490 7700    0 true 880   370 11000 2 unknown 150    54   1600   0 timeout 900   1100 13000 0 timeout 900   540 11000 0 timeout 900   730 11000 0 unknown 570   13000 5300 0
array-examples/sanfoundry_02_true-unreach-call_ground.i out of memory 320   15000 3100 0 exception (gremlins) 110     54   1100    0 error (42) 850    2300 3500   0 true .047 8.5 .49 2 error 2.4 270 24 0 timeout 900   2200 12000 0 timeout 900 2200 12000 0 unknown 310 180 3700 0 timeout 900    440 10000   0 timeout 900    740 11000   0 out of memory 450     15000 5900    0 timeout 900     6400 11000    0 true 1.5 77 21 2 error 320    120   2300   0 timeout 900   2200 15000 0 timeout 900   3900 14000 0 timeout 900   2000 12000 0 unknown 800   6700 8200 0
array-examples/sanfoundry_10_true-unreach-call_ground.i timeout 900   15000 11000 0 timeout 900     290   12000    0 error (134) 28    13000 370   0 true .067 13   .37 2 timeout 900   4200 8800 0 segmentation fault 31   1200 200 0 timeout 900 5700 11000 0 unknown 900 180 9800 0 true 900    2600 13000   2 timeout 900    10000 8600   0 timeout 900     920 9100    0 timeout 900     1000 10000    0 true 4.2 91 60 2 timeout (timeout) 900    940   10000   0 timeout 900   1400 12000 0 timeout 900   1300 11000 0 timeout 900   1500 12000 0 true 650   880 7000 2
array-examples/sanfoundry_24_true-unreach-call.i true 41   5500 520 2 true .49  22   2.8  2 error (42) 850    4200 9300   0 unknown .027 7.8 .11 0 error 2.7 270 24 0 timeout 900   3900 11000 0 timeout 900 3900 13000 0 timeout 900 3900 12000 0 true 40    1700 560   2 out of memory 900    15000 12000   0 out of memory 470     15000 6400    0 true .081 23 .99 2 true 880   310 12000 2 timeout (timeout) 900    6400   7900   0 true 8.0 370 67 2 true 6.7 320 55 2 true 6.7 350 52 2 true 650   880 6200 2
array-examples/sanfoundry_27_true-unreach-call_ground.i out of memory 330   15000 3500 0 exception (gremlins) 160     150   1800    0 error (42) 850    1200 3500   0 true .11  8.3 .30 2 error 2.5 280 20 0 timeout 900   2200 12000 0 timeout 900 2200 12000 0 unknown 120 120 1500 0 timeout 900    360 10000   0 timeout 900    530 10000   0 out of memory 290     15000 3500    0 timeout 900     14000 12000    0 true 1.8 77 20 2 error .47 97   5.8 0 timeout 900   2300 13000 0 timeout 900   3200 14000 0 timeout 900   2000 15000 0 true 650   920 6900 2
array-examples/sanfoundry_43_true-unreach-call_ground.i out of memory 39   15000 470 0 true .090 15   .62 2 out of memory 110    15000 1600   0 true .12  11   .35 2 true 2.7 280 25 2 true 2.9 270 24 2 true 93 2300 1200 2 unknown 52 100 760 0 true .80 65 8.4 2 timeout 900    4300 11000   0 timeout 900     10000 13000    0 true .090 23 1.0  2 true 1.2 69 14 2 true .16 9.3 1.5 2 true 5.6 320 43 2 true 5.9 320 47 2 true 7.3 350 54 2 true 6.4 280 43 2
array-examples/sorting_bubblesort_true-unreach-call_ground.i out of memory 38   15000 470 0 exception (gremlins) 39     64   470    0 out of memory 19    15000 240   0 true 26     12   300    2 error 2.5 280 21 0 timeout 900   2400 12000 0 timeout 900 2200 13000 0 unknown 46 160 630 0 out of memory 150    15000 1000   0 timeout 900    970 10000   0 out of memory 360     15000 4700    0 timeout 900     490 9700    0 true 23   140 260 2 timeout (timeout) 900    4200   9200   0 timeout 900   2400 12000 0 timeout 900   3000 13000 0 timeout 900   2300 12000 0 out of memory 370   15000 4400 0
array-examples/sorting_selectionsort_true-unreach-call_ground.i out of memory 39   15000 520 0 timeout 900     180   11000    0 error (134) 70    13000 890   0 true .45  11   5.2  2 error 2.6 280 21 0 timeout 900   2100 14000 0 timeout 900 2200 11000 0 unknown 890 380 8900 0 out of memory 34    15000 330   0 timeout 900    530 11000   0 out of memory 280     15000 3600    0 timeout 900     410 8300    0 timeout 880   770 9900 0 error 330    69   3200   0 timeout 900   3200 13000 0 timeout 900   3800 14000 0 timeout 900   2700 13000 0 out of memory 110   15000 1100 0
array-examples/standard_compareModified_true-unreach-call_ground.i out of memory 42   15000 670 0 exception (gremlins) 200     110   2200    0 error (1) 140    15000 2100   0 true .048 8.2 .42 2 error 2.6 280 24 0 timeout 900   2300 14000 0 timeout 900 2200 13000 0 unknown 890 220 11000 0 true 29    2300 440   2 timeout 900    490 11000   0 out of memory 290     15000 3900    0 timeout 900     780 10000    0 true 1.4 75 20 2 error 100    170   680   0 timeout 900   2600 13000 0 timeout 900   4900 12000 0 timeout 900   2100 12000 0 true 650   900 6900 2
array-examples/standard_compare_true-unreach-call_ground.i out of memory 190   15000 2000 0 timeout 900     200   9500    0 error (42) 850    1400 3700   0 true .070 11   .39 2 error 2.6 290 22 0 timeout 900   3700 12000 0 timeout 900 2400 11000 0 unknown 110 170 1300 0 true 13    1200 160   2 timeout 900    530 9900   0 out of memory 290     15000 4200    0 out of memory 350     15000 4600    0 true 1.7 74 21 2 error 100    170   780   0 timeout 900   2700 12000 0 timeout 900   2500 13000 0 timeout 900   2000 13000 0 true 640   860 6600 2
array-examples/standard_copy1_true-unreach-call_ground.i timeout 900   14000 9100 0 exception (gremlins) 27     66   310    0 out of memory 130    15000 1500   0 true .056 8.4 .40 2 error 2.4 270 20 0 timeout 900   2200 11000 0 timeout 900 2400 14000 0 unknown 900 200 9200 0 true 3.9  420 52   2 timeout 900    5200 12000   0 out of memory 290     15000 3900    0 timeout 900     650 9500    0 true 1.6 82 29 2 true 1.1  100   16   2 timeout 900   3700 14000 0 timeout 900   3500 14000 0 timeout 900   1900 13000 0 true 640   850 7000 2
array-examples/standard_copy2_true-unreach-call_ground.i out of memory 38   15000 630 0 exception (gremlins) 96     79   1400    0 out of memory 83    15000 1100   0 true .051 8.2 .34 2 error 2.3 260 23 0 timeout 900   3700 14000 0 timeout 900 2200 11000 0 unknown 900 260 8400 0 true 4.1  450 46   2 timeout 900    5200 11000   0 out of memory 290     15000 3800    0 timeout 900     630 10000    0 true 1.8 78 20 2 true 1.5  120   22   2 timeout 900   3400 12000 0 timeout 900   3700 15000 0 timeout 900   2800 13000 0 true 650   880 6900 2
array-examples/standard_copy3_true-unreach-call_ground.i out of memory 39   15000 480 0 exception (gremlins) 290     120   3300    0 out of memory 94    15000 1400   0 true .059 8.5 .39 2 error 2.5 270 21 0 timeout 900   2200 11000 0 timeout 900 2200 13000 0 unknown 890 300 9300 0 true 4.2  470 48   2 timeout 900    5200 12000   0 out of memory 290     15000 3500    0 timeout 900     640 10000    0 true 1.8 83 20 2 true 1.8  140   21   2 timeout 900   3800 14000 0 timeout 900   4000 11000 0 timeout 900   3500 13000 0 true 680   880 7700 2
array-examples/standard_copy4_true-unreach-call_ground.i out of memory 39   15000 510 0 timeout 900     250   9300    0 out of memory 110    15000 1500   0 true .053 8.4 .36 2 error 2.4 270 23 0 timeout 900   2300 13000 0 timeout 900 3500 11000 0 unknown 890 330 10000 0 true 4.3  500 54   2 timeout 900    5300 11000   0 out of memory 290     15000 3700    0 timeout 900     370 1600    0 true 1.9 87 25 2 true 2.2  160   29   2 timeout 900   4400 14000 0 timeout 900   4500 12000 0 timeout 900   4900 12000 0 true 670   900 6800 2
array-examples/standard_copy5_true-unreach-call_ground.i out of memory 39   15000 520 0 timeout 900     300   10000    0 out of memory 120    15000 1800   0 true .075 13   .45 2 error 2.5 270 22 0 timeout 900   2200 11000 0 timeout 900 2200 12000 0 unknown 890 270 9700 0 true 4.5  520 52   2 timeout 900    5300 12000   0 out of memory 280     15000 3700    0 timeout 900     660 9000    0 true 2.0 87 26 2 true 2.5  180   34   2 timeout 900   4900 14000 0 timeout 900   3000 13000 0 timeout 900   5100 15000 0 true 680   940 7000 2
array-examples/standard_copy6_true-unreach-call_ground.i out of memory 39   15000 470 0 timeout 900     500   11000    0 error (134) 92    15000 1300   0 true .063 11   .34 2 error 2.6 260 22 0 timeout 900   2400 13000 0 timeout 900 2400 11000 0 unknown 890 270 8400 0 true 4.7  550 55   2 timeout 900    5300 13000   0 out of memory 280     15000 3800    0 timeout 900     640 9000    0 true 2.1 90 28 2 true 2.8  200   35   2 timeout 900   5100 13000 0 timeout 900   3600 13000 0 timeout 900   5300 13000 0 true 840   980 8900 2
array-examples/standard_copy7_true-unreach-call_ground.i out of memory 44   15000 510 0 timeout 900     610   8400    0 out of memory 100    15000 1400   0 true .047 8.3 .34 2 error 2.4 260 21 0 timeout 900   3700 11000 0 timeout 900 2200 12000 0 unknown 890 310 8900 0 true 4.8  570 63   2 timeout 900    5300 11000   0 out of memory 280     15000 4200    0 timeout 900     680 9100    0 true 2.2 94 28 2 true 3.2  230   49   2 timeout 900   5200 14000 0 timeout 900   3900 12000 0 timeout 900   5200 14000 0 true 890   1000 9200 2
array-examples/standard_copy8_true-unreach-call_ground.i out of memory 38   15000 520 0 timeout 900     610   9600    0 error (134) 82    14000 1100   0 true .078 11   .34 2 error 2.5 260 23 0 timeout 900   2500 13000 0 timeout 900 2200 14000 0 unknown 890 400 12000 0 true 5.0  600 58   2 timeout 900    5200 13000   0 out of memory 290     15000 3800    0 timeout 900     730 9800    0 true 2.5 92 28 2 true 3.5  250   47   2 timeout 900   5000 12000 0 timeout 900   3800 14000 0 timeout 900   5200 13000 0 true 900   990 8800 2
array-examples/standard_copy9_true-unreach-call_ground.i out of memory 39   15000 560 0 timeout 900     610   11000    0 error (134) 89    14000 1200   0 true .082 11   .45 2 error 2.4 270 25 0 timeout 900   1900 14000 0 timeout 900 2200 10000 0 unknown 890 340 7600 0 true 5.2  620 70   2 timeout 900    5300 12000   0 out of memory 290     15000 4200    0 timeout 900     680 8200    0 true 2.5 100 30 2 true 3.9  270   50   2 timeout 900   5100 13000 0 timeout 900   3400 12000 0 timeout 900   5300 14000 0 out of memory 760   15000 11000 0
array-examples/standard_copyInitSum2_true-unreach-call_ground.i out of memory 41   15000 580 0 timeout 900     480   9200    0 out of memory 78    15000 1000   0 true .051 11   .42 2 error 2.5 280 23 0 timeout 900   2000 12000 0 timeout 900 690 14000 0 unknown 900 160 10000 0 true 4.3  470 50   2 timeout 900    5900 11000   0 out of memory 270     15000 3200    0 timeout 900     310 2400    0 true 2.1 83 28 2 true 1.4  98   17   2 timeout 900   3500 12000 0 timeout 900   3300 12000 0 timeout 900   3400 13000 0 true 670   890 8000 2
array-examples/standard_copyInitSum3_true-unreach-call_ground.i out of memory 41   15000 540 0 timeout 900     460   9400    0 out of memory 81    15000 1000   0 true .061 11   .33 2 error 2.5 280 22 0 timeout 900   2000 13000 0 timeout 900 780 12000 0 unknown 890 220 12000 0 true 4.4  490 48   2 timeout 900    4800 9400   0 out of memory 270     15000 3700    0 timeout 900     580 9800    0 true 2.5 88 35 2 true 1.8  120   29   2 timeout 900   4400 12000 0 timeout 900   3800 14000 0 timeout 900   4100 13000 0 true 660   910 6700 2
array-examples/standard_copyInitSum_true-unreach-call_ground.i out of memory 40   15000 520 0 timeout 900     480   9800    0 out of memory 78    15000 1000   0 true .058 8.5 .32 2 error 2.5 280 22 0 timeout 900   3700 12000 0 timeout 900 780 13000 0 unknown 890 180 8100 0 true 4.3  470 55   2 timeout 900    5800 11000   0 out of memory 270     15000 4100    0 timeout 900     500 8300    0 true 2.0 81 24 2 true 1.5  130   19   2 timeout 900   3300 11000 0 timeout 900   2600 13000 0 timeout 900   3100 12000 0 true 650   890 7200 2
array-examples/standard_copyInit_true-unreach-call_ground.i out of memory 41   15000 510 0 timeout 900     470   9800    0 out of memory 74    15000 970   0 true .052 8.4 .39 2 error 2.7 280 21 0 timeout 900   1800 12000 0 timeout 900 750 11000 0 unknown 890 220 11000 0 true 4.1  450 56   2 timeout 900    5900 11000   0 out of memory 260     15000 3200    0 timeout 900     550 9800    0 true 1.7 78 22 2 true 1.1  79   14   2 timeout 900   2900 13000 0 timeout 900   2700 14000 0 timeout 900   2300 12000 0 true 650   850 6600 2
array-examples/standard_find_true-unreach-call_ground.i timeout 900   12000 9400 0 timeout 900     280   11000    0 out of memory 130    15000 1600   0 true .046 11   .54 2 error 2.6 280 24 0 timeout 900   1900 12000 0 timeout 900 2400 12000 0 timeout 900 2200 11000 0 true 15    900 220   2 timeout 900    9400 10000   0 out of memory 260     15000 3700    0 timeout 900     600 10000    0 true 2.4 81 27 2 timeout (timeout) 900    88   10000   0 timeout 900   2900 13000 0 timeout 900   3800 11000 0 timeout 900   2100 11000 0 true 650   920 6900 2
array-examples/standard_init1_true-unreach-call_ground.i timeout 900   9800 9600 0 timeout 900     230   8200    0 out of memory 130    15000 1600   0 true .053 11   .42 2 error 2.5 280 24 0 timeout 900   2100 13000 0 timeout 900 820 11000 0 timeout 900 730 11000 0 true 3.9  420 47   2 timeout 900    5800 13000   0 out of memory 270     15000 3400    0 timeout 900     520 9700    0 true 1.5 74 19 2 true .84 67   13   2 timeout 900   3400 12000 0 timeout 900   3400 13000 0 timeout 900   1700 13000 0 true 640   860 7100 2
array-examples/standard_init2_true-unreach-call_ground.i out of memory 43   15000 570 0 timeout 900     400   11000    0 out of memory 67    15000 760   0 true .058 8.2 .32 2 error 2.6 280 22 0 timeout 900   2200 12000 0 timeout 900 690 10000 0 timeout 900 730 11000 0 true 4.1  440 51   2 timeout 900    5800 11000   0 out of memory 270     15000 3800    0 timeout 900     560 9700    0 true 1.6 86 22 2 true 1.0  77   12   2 timeout 900   2400 13000 0 timeout 900   4000 13000 0 timeout 900   2000 12000 0 true 640   890 6300 2
array-examples/standard_init3_true-unreach-call_ground.i out of memory 42   15000 630 0 timeout 900     290   9900    0 out of memory 70    15000 970   0 true .10  11   .34 2 error 2.4 260 22 0 timeout 900   1900 13000 0 timeout 900 710 11000 0 timeout 900 790 11000 0 true 4.1  470 50   2 timeout 900    5800 12000   0 out of memory 260     15000 3900    0 timeout 900     620 8900    0 true 1.7 78 22 2 true 1.2  93   17   2 timeout 900   2800 11000 0 timeout 900   3100 13000 0 timeout 900   2700 13000 0 true 650   870 7500 2
array-examples/standard_init4_true-unreach-call_ground.i out of memory 42   15000 550 0 timeout 900     290   12000    0 out of memory 73    15000 950   0 true .067 8.4 .36 2 error 2.5 270 20 0 timeout 900   2000 12000 0 timeout 900 900 12000 0 timeout 900 740 12000 0 true 4.3  490 50   2 timeout 900    5800 11000   0 out of memory 260     15000 3300    0 timeout 900     410 1900    0 true 1.8 75 21 2 true 1.4  110   17   2 timeout 900   3700 13000 0 timeout 900   4900 15000 0 timeout 900   3600 14000 0 true 650   890 6500 2
array-examples/standard_init5_true-unreach-call_ground.i out of memory 42   15000 540 0 timeout 900     290   12000    0 out of memory 76    15000 1100   0 true .073 13   .43 2 error 2.5 280 21 0 timeout 900   2100 13000 0 timeout 900 720 13000 0 unknown 890 210 9600 0 true 4.4  510 51   2 timeout 900    5700 12000   0 out of memory 260     15000 3400    0 timeout 900     790 11000    0 true 1.9 78 23 2 true 1.6  130   20   2 timeout 900   4100 14000 0 timeout 900   3400 14000 0 timeout 900   3800 11000 0 true 650   930 7100 2
array-examples/standard_init6_true-unreach-call_ground.i out of memory 42   15000 580 0 timeout 900     290   8700    0 out of memory 79    15000 990   0 true .049 8.2 .39 2 error 2.5 260 20 0 timeout 900   2100 12000 0 timeout 900 770 13000 0 unknown 890 240 12000 0 true 4.5  540 52   2 timeout 900    5800 11000   0 out of memory 260     15000 3300    0 timeout 900     790 8400    0 true 1.9 83 23 2 true 1.8  140   34   2 timeout 900   5000 13000 0 timeout 900   3200 12000 0 timeout 900   5100 12000 0 true 650   960 6100 2
array-examples/standard_init7_true-unreach-call_ground.i out of memory 42   15000 480 0 timeout 900     290   9500    0 out of memory 55    15000 720   0 true .054 11   .42 2 error 2.4 260 21 0 timeout 900   2000 13000 0 timeout 900 730 13000 0 unknown 890 270 9200 0 true 4.7  560 57   2 timeout 900    5700 11000   0 out of memory 260     15000 3900    0 timeout 900     750 12000    0 true 2.0 84 24 2 true 2.1  160   28   2 timeout 900   5000 13000 0 timeout 900   3700 14000 0 timeout 900   5200 13000 0 true 660   940 6500 2
array-examples/standard_init8_true-unreach-call_ground.i out of memory 42   15000 620 0 timeout 900     280   11000    0 out of memory 57    15000 710   0 true .058 13   .52 2 error 2.5 280 22 0 timeout 900   2300 13000 0 timeout 900 740 12000 0 unknown 890 290 12000 0 true 4.7  580 70   2 timeout 900    5800 13000   0 out of memory 270     15000 3400    0 timeout 900     770 10000    0 true 2.0 86 24 2 true 2.2  180   33   2 timeout 900   5300 13000 0 timeout 900   3300 13000 0 timeout 900   5300 14000 0 true 660   1000 6800 2
array-examples/standard_init9_true-unreach-call_ground.i out of memory 43   15000 510 0 timeout 900     300   12000    0 out of memory 59    15000 750   0 true .087 11   .41 2 error 2.8 280 22 0 timeout 900   3600 11000 0 timeout 900 740 11000 0 unknown 900 320 9700 0 true 4.9  610 54   2 timeout 900    5800 12000   0 out of memory 270     15000 3400    0 timeout 900     480 2300    0 true 2.1 81 27 2 true 2.5  200   37   2 timeout 900   5100 14000 0 timeout 900   3700 13000 0 timeout 900   5300 14000 0 true 660   1000 6800 2
array-examples/standard_maxInArray_true-unreach-call_ground.i out of memory 400   15000 4600 0 timeout 900     390   11000    0 error (42) 850    1300 4500   0 true .078 13   .39 2 error 2.5 280 21 0 timeout 900   2700 13000 0 timeout 900 2200 11000 0 unknown 120 150 1600 0 timeout 900    310 10000   0 timeout 900    530 10000   0 out of memory 290     15000 3400    0 timeout 900     5000 1800    0 true 1.9 73 24 2 error .47 98   5.8 0 timeout 900   2400 13000 0 timeout 900   3200 14000 0 timeout 900   2000 14000 0 true 640   900 6800 2
array-examples/standard_minInArray_true-unreach-call_ground.i out of memory 330   15000 3200 0 timeout 900     270   13000    0 error (42) 850    1200 3900   0 true .067 11   .36 2 error 2.5 280 19 0 timeout 900   2500 12000 0 timeout 900 2200 14000 0 unknown 100 120 1500 0 timeout 900    350 11000   0 timeout 900    540 11000   0 out of memory 290     15000 3500    0 out of memory 720     15000 10000    0 true 1.9 73 24 2 error .52 100   6.9 0 timeout 900   2200 12000 0 timeout 900   3800 13000 0 timeout 900   1900 13000 0 true 640   870 5900 2
array-examples/standard_palindrome_true-unreach-call_ground.i timeout 900   13000 10000 0 timeout 900     500   10000    0 out of memory 130    15000 1800   0 true .059 13   .36 2 error 2.5 270 23 0 timeout 900   2100 13000 0 timeout 900 2200 11000 0 unknown 890 160 9200 0 true 4.0  420 49   2 timeout 900    4400 11000   0 out of memory 330     15000 3900    0 timeout 900     510 8600    0 true 1.4 81 18 2 true .67 57   9.9 2 timeout 900   2600 13000 0 timeout 900   3000 12000 0 timeout 900   2000 12000 0 true 640   840 6000 2
array-examples/standard_partial_init_true-unreach-call_ground.i out of memory 40   15000 520 0 exception (gremlins) 300     160   3800    0 error (134) 91    13000 1100   0 true .074 11   .40 2 error 2.4 270 21 0 timeout 900   2500 15000 0 timeout 900 1400 13000 0 timeout 900 1400 11000 0 timeout 900    2300 6600   0 timeout 900    1100 9600   0 out of memory 330     15000 3800    0 timeout 900     330 2600    0 true 120   100 1700 2 timeout (timeout) 900    3900   8400   0 timeout 900   2700 14000 0 timeout 900   4400 14000 0 timeout 900   2200 12000 0 true 650   960 6700 2
array-examples/standard_partition_original_true-unreach-call_ground.i out of memory 37   15000 480 0 exception (gremlins) 52     64   560    0 error (134) 77    14000 940   0 true .092 8.2 .31 2 error 2.6 280 21 0 timeout 900   2600 12000 0 timeout 900 2200 11000 0 timeout 900 2300 12000 0 timeout 900    2200 9600   0 out of memory 500    15000 6500   0 out of memory 200     15000 2600    0 timeout 900     600 12000    0 true 64   95 820 2 out of memory 16    15000   170   0 timeout 900   2300 12000 0 timeout 900   4100 13000 0 timeout 900   2200 11000 0 true 650   900 6700 2
array-examples/standard_partition_true-unreach-call_ground.i out of memory 40   15000 520 0 timeout 900     160   10000    0 error (134) 68    14000 860   0 true .098 11   .31 2 error 2.5 280 21 0 timeout 900   2500 14000 0 timeout 900 2200 11000 0 unknown 890 250 9200 0 timeout 900    1700 9200   0 timeout 900    1100 9900   0 out of memory 330     15000 4000    0 timeout 900     760 8500    0 true 21   86 330 2 timeout (timeout) 900    12000   10000   0 timeout 900   3100 14000 0 timeout 900   2500 13000 0 timeout 900   2800 14000 0 true 650   870 6500 2
array-examples/standard_password_true-unreach-call_ground.i out of memory 190   15000 2300 0 timeout 900     290   11000    0 error (42) 850    1400 4100   0 true .071 11   .39 2 error 2.6 280 23 0 timeout 900   2400 14000 0 timeout 900 2200 9900 0 unknown 110 170 1400 0 true 13    1200 160   2 timeout 900    540 9300   0 out of memory 290     15000 3400    0 timeout 900     10000 1700    0 true 1.7 82 20 2 error 94    170   610   0 timeout 900   2700 13000 0 timeout 900   2100 13000 0 timeout 900   2300 12000 0 true 640   860 6800 2
array-examples/standard_reverse_true-unreach-call_ground.i timeout 900   14000 12000 0 exception (gremlins) 29     66   320    0 out of memory 130    15000 1800   0 true .053 13   .44 2 error 2.4 260 23 0 timeout 900   2200 11000 0 timeout 900 2200 11000 0 unknown 890 180 9300 0 false(unreach-call) 440    680 5700   -16 timeout 900    4600 13000   0 out of memory 320     15000 4100    0 timeout 900     700 10000    0 true 1.7 80 25 2 true 1.2  100   15   2 timeout 900   2600 14000 0 timeout 900   3600 13000 0 timeout 900   2000 12000 0 true 640   830 7500 2
array-examples/standard_running_true-unreach-call.i out of memory 42   15000 500 0 timeout 900     310   11000    0 out of memory 94    15000 1300   0 true .077 11   .39 2 error 2.6 280 20 0 timeout 900   2600 12000 0 timeout 900 2200 12000 0 unknown 890 260 9400 0 timeout 900    1200 9700   0 out of memory 460    15000 6200   0 out of memory 190     15000 2600    0 timeout 900     730 10000    0 true 1.7 71 25 2 error 1.3  220   17   0 timeout 900   3100 13000 0 timeout 900   2800 13000 0 timeout 900   3100 12000 0 true 640   870 6900 2
array-examples/standard_sentinel_true-unreach-call_true-termination.i out of memory 320   15000 3600 0 false(unreach-call) .27  21   1.6  -16 error (42) 850    3900 11000   0 true .066 11   .41 2 error 2.4 260 23 0 timeout 900   3800 12000 0 timeout 900 2400 13000 0 unknown 100 75 1300 0 true 14    140 190   2 timeout 900    2400 12000   0 timeout 900     4100 10000    0 timeout 900     6200 10000    0 true 1.6 86 20 2 timeout (timeout) 900    460   9200   0 true 8.3 420 64 2 true 6.6 320 56 2 true 9.6 480 71 2 true 640   770 6600 2
array-examples/standard_seq_init_true-unreach-call_ground.i timeout 900   13000 11000 0 exception (gremlins) 28     63   310    0 out of memory 130    15000 1700   0 true .091 8.1 .23 2 error 2.5 280 22 0 timeout 900   3700 14000 0 timeout 900 800 12000 0 timeout 900 740 12000 0 true 3.9  420 46   2 timeout 900    4300 15000   0 out of memory 310     15000 3900    0 timeout 900     560 9700    0 true 1.7 79 22 2 true .93 61   13   2 timeout 900   2100 14000 0 timeout 900   2400 11000 0 timeout 900   1800 14000 0 out of memory 250   15000 2500 0
array-examples/standard_strcmp_true-unreach-call_ground.i false(unreach-call) 84   10000 830 -16 timeout 740     520   9500    0 error (42) 850    3300 4200   0 true .058 11   .47 2 error 2.6 280 24 0 timeout 900   3700 12000 0 timeout 900 3500 11000 0 unknown 120 130 1400 0 true 5.6  550 70   2 out of memory 710    15000 11000   0 out of memory 400     15000 6000    0 timeout 900     7400 13000    0 true 1.7 74 20 2 timeout (timeout) 900    670   8700   0 timeout 900   5300 11000 0 timeout 900   5200 12000 0 timeout 900   4300 12000 0 true 640   880 6800 2
array-examples/standard_strcpy_original_true-unreach-call.i out of memory 40   15000 480 0 exception (gremlins) 32     64   340    0 out of memory 79    15000 1200   0 unknown .027 7.9 .12 0 error 2.4 260 21 0 timeout 900   2000 12000 0 timeout 900 2400 9900 0 timeout 900 2200 12000 0 true 890    1200 12000   2 timeout 900    9700 10000   0 out of memory 260     15000 3400    0 timeout 900     450 8600    0 true 6.1 97 77 2 timeout (timeout) 900    89   11000   0 timeout 900   2800 12000 0 timeout 900   4700 13000 0 timeout 900   1900 12000 0 out of memory 240   15000 1900 0
array-examples/standard_strcpy_true-unreach-call_ground.i out of memory 40   15000 530 0 exception (gremlins) 33     63   360    0 out of memory 79    15000 960   0 unknown .043 7.7 .11 0 error 2.4 260 24 0 timeout 900   2000 12000 0 timeout 900 2200 12000 0 unknown 890 300 9900 0 timeout 900    1200 13000   0 timeout 900    9600 9600   0 out of memory 260     15000 3800    0 timeout 900     490 13000    0 true 4.2 90 64 2 timeout (timeout) 900    88   12000   0 timeout 900   2700 13000 0 timeout 900   3200 15000 0 timeout 900   2000 14000 0 true 650   920 6700 2
array-examples/standard_two_index_01_true-unreach-call.i timeout 900   5600 11000 0 exception (gremlins) .18  23   .98 0 out of memory 160    15000 2100   0 true .046 11   .51 2 error 2.4 280 20 0 timeout 900   2100 13000 0 timeout 900 2200 11000 0 unknown 890 230 12000 0 true 4.4  480 51   2 timeout 900    4200 11000   0 out of memory 260     15000 3900    0 timeout 900     670 9600    0 timeout 880   900 13000 0 true .24 18   3.2 2 timeout 900   1500 12000 0 timeout 900   2800 12000 0 timeout 900   1500 11000 0 true 640   860 7100 2
array-examples/standard_two_index_02_true-unreach-call.i timeout 900   14000 11000 0 timeout 900     700   9200    0 out of memory 130    15000 1600   0 true .050 8.2 .38 2 error 2.4 260 22 0 timeout 900   2300 12000 0 timeout 900 2200 12000 0 unknown 890 210 8800 0 true 4.4  490 61   2 timeout 900    1000 2300   0 out of memory 260     15000 3400    0 timeout 900     830 11000    0 true 1.5 79 19 2 true .74 58   8.6 2 timeout 900   1500 11000 0 timeout 900   4200 12000 0 timeout 900   1500 13000 0 true 640   850 6700 2
array-examples/standard_two_index_03_true-unreach-call.i timeout 900   5700 9800 0 timeout 900     690   9500    0 out of memory 160    15000 2000   0 true .052 8.2 .28 2 error 2.3 270 21 0 error 330   2700 4700 0 unknown 360 3300 4100 0 unknown 890 220 9700 0 true 4.4  490 58   2 out of memory 490    15000 6500   0 out of memory 260     15000 3900    0 timeout 900     700 10000    0 timeout 900   4100 12000 0 true .20 12   2.2 2 timeout 900   1600 12000 0 timeout 900   2700 12000 0 timeout 900   1500 13000 0 true 640   850 6500 2
array-examples/standard_two_index_04_true-unreach-call.i timeout 900   14000 12000 0 timeout 900     610   8600    0 out of memory 130    15000 1700   0 true .050 11   .42 2 error 2.5 280 23 0 timeout 900   2200 13000 0 timeout 900 2200 14000 0 unknown 890 170 9900 0 true 4.4  490 61   2 timeout 900    4200 11000   0 out of memory 260     15000 3600    0 timeout 900     710 9200    0 true 1.4 95 17 2 true .47 35   6.4 2 timeout 900   1500 13000 0 timeout 900   3800 13000 0 timeout 900   1600 11000 0 true 640   850 7200 2
array-examples/standard_two_index_05_true-unreach-call.i timeout 900   14000 9700 0 timeout 900     700   10000    0 out of memory 130    15000 1800   0 true .070 11   .40 2 error 2.5 270 22 0 timeout 900   2500 11000 0 timeout 900 2400 13000 0 unknown 890 180 8800 0 true 4.5  490 54   2 timeout 900    4200 12000   0 out of memory 260     15000 4100    0 timeout 900     610 7900    0 true 1.4 83 16 2 true .36 30   4.6 2 timeout 900   1600 12000 0 timeout 900   3300 14000 0 timeout 900   1500 11000 0 true 650   850 7200 2
array-examples/standard_two_index_06_true-unreach-call.i timeout 900   5600 8800 0 timeout 900     690   11000    0 true 100    8800 1500   2 true .070 8.2 .27 2 error 2.6 280 24 0 error 96   3900 1100 0 unknown 98 4000 1200 0 unknown 900 170 9200 0 true 4.4  490 53   2 out of memory 480    15000 6200   0 true 130     7600 1400    2 timeout 900     690 8700    0 timeout 890   1000 11000 0 true .18 11   1.7 2 timeout 900   1400 12000 0 timeout 900   3800 13000 0 timeout 900   1500 13000 0 true 640   860 6000 2
array-examples/standard_two_index_07_true-unreach-call.i timeout 900   14000 10000 0 exception (gremlins) 200     260   2300    0 out of memory 130    15000 1600   0 true .051 11   .33 2 error 2.6 280 24 0 timeout 900   2000 11000 0 timeout 900 2200 14000 0 unknown 900 190 8700 0 true 4.5  490 52   2 timeout 900    4200 15000   0 out of memory 260     15000 3400    0 timeout 900     610 9600    0 true 1.4 76 17 2 true .30 26   3.6 2 timeout 900   1500 12000 0 timeout 900   4300 13000 0 timeout 900   1500 12000 0 true 640   870 6400 2
array-examples/standard_two_index_08_true-unreach-call.i timeout 900   14000 12000 0 timeout 900     600   9600    0 out of memory 130    15000 1600   0 true .071 8.3 .34 2 error 2.6 270 20 0 timeout 900   2300 12000 0 timeout 900 2200 11000 0 unknown 890 180 9800 0 true 4.5  490 58   2 timeout 900    4200 11000   0 out of memory 260     15000 3500    0 timeout 900     690 13000    0 true 1.4 80 16 2 true .34 24   3.7 2 timeout 900   1500 12000 0 timeout 900   3900 12000 0 timeout 900   1600 12000 0 true 640   840 6400 2
array-examples/standard_two_index_09_true-unreach-call.i timeout 900   14000 12000 0 timeout 900     680   9700    0 out of memory 130    15000 1600   0 true .057 11   .36 2 error 2.5 280 22 0 timeout 900   2100 12000 0 timeout 900 2100 11000 0 unknown 890 170 9900 0 true 4.4  490 53   2 timeout 900    4200 12000   0 out of memory 260     15000 3200    0 timeout 900     640 8500    0 true 1.3 75 18 2 true .30 23   4.1 2 timeout 900   1500 14000 0 timeout 900   3100 14000 0 timeout 900   1500 12000 0 true 640   840 6700 2
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i out of memory 260   15000 2900 0 timeout 900     280   11000    0 error (42) 850    7700 5000   0 true .038 11   .79 2 error 2.4 260 24 0 timeout 900   3000 12000 0 timeout 900 2500 12000 0 unknown 97 100 1400 0 true 14    850 180   2 out of memory 860    15000 12000   0 timeout 900     7700 2600    0 out of memory 350     15000 5100    0 true 880   480 12000 2 timeout (timeout) 900    560   12000   0 timeout 900   2900 13000 0 timeout 900   850 13000 0 timeout 900   2900 14000 0 true 640   850 6300 2
array-examples/standard_vector_difference_true-unreach-call_ground.i out of memory 40   15000 520 0 exception (gremlins) 32     63   430    0 error (1) 140    15000 2100   0 true .065 11   .30 2 error 2.5 280 20 0 timeout 900   2100 12000 0 timeout 900 2200 12000 0 timeout 900 2200 12000 0 true 3.9  420 46   2 timeout 900    4400 11000   0 out of memory 300     15000 3900    0 timeout 900     500 10000    0 true 2.1 76 22 2 true 1.7  200   26   2 timeout 900   4400 12000 0 timeout 900   4400 12000 0 timeout 900   1600 14000 0 true 640   830 7400 2
array-industry-pattern/array_assert_loop_dep_false-unreach-call.i out of memory 41   15000 550 0 exception (gremlins) 29     45   350    0 out of memory 66    15000 970   0 false(unreach-call) .052 8.2 .34 1 error 2.3 260 23 0 timeout 900   1800 12000 0 timeout 900 860 14000 0 unknown 890 320 8900 0 false(unreach-call) 520    830 7200   1 timeout 900    6000 11000   0 out of memory 260     15000 3300    0 timeout 900     700 2100    0 false(unreach-call) 1.8 81 21 1 false(unreach-call) 1.3  280   18   1 timeout 900   1800 11000 0 timeout 900   3300 13000 0 timeout 900   1600 14000 0 out of memory 250   15000 2200 0
array-industry-pattern/array_of_struct_loop_dep_false-unreach-call.i out of memory 41   15000 470 0 exception (gremlins) 35     51   380    0 out of memory 550    15000 8000   0 false(unreach-call) .11  8.2 .29 1 timeout 900   4300 11000 0 timeout 900   3800 7300 0 timeout 900 4200 11000 0 unknown 890 310 8300 0 false(unreach-call) 61    4900 450   1 timeout 900    5300 11000   0 out of memory 240     15000 3500    0 timeout 900     1400 8500    0 false(unreach-call) 1.8 80 22 1 false(unreach-call) 1.4  280   20   1 timeout 900   5200 9000 0 timeout 900   5200 10000 0 timeout 900   5000 8900 0 timeout 900   14000 8500 0
array-industry-pattern/array_ptr_single_elem_init_false-unreach-call.i out of memory 32   15000 380 0 timeout 900     320   10000    0 out of memory 75    15000 1200   0 false(unreach-call) .051 11   .53 1 error 2.5 280 22 0 timeout 900   2600 13000 0 timeout 900 2200 9900 0 unknown 890 230 9600 0 true 14    1100 160   -32 timeout 900    1500 11000   0 out of memory 340     15000 4500    0 timeout 900     550 10000    0 false(unreach-call) 2.5 88 27 1 timeout (timeout) 900    130   11000   0 timeout 900   3100 11000 0 timeout 900   3700 13000 0 timeout 900   3400 14000 0 out of memory 36   15000 440 0
array-industry-pattern/array_range_init_false-unreach-call.i timeout 900   12000 9100 0 timeout 900     400   9900    0 error (42) 850    14000 11000   0 false(unreach-call) .050 11   .44 1 error 2.6 270 24 0 timeout 900   2200 11000 0 timeout 900 750 12000 0 unknown 900 190 8500 0 true 670    790 7000   -32 timeout 900    3700 12000   0 out of memory 390     15000 5100    0 timeout 900     490 9600    0 false(unreach-call) 1.8 87 25 1 false(unreach-call) 1.6  330   20   1 timeout 900   4900 8500 0 timeout 900   4900 9700 0 timeout 900   4900 9600 0 false(unreach-call) 5.6 270 46 1
array-industry-pattern/array_single_elem_init_false-unreach-call.i out of memory 32   15000 460 0 timeout 900     400   11000    0 out of memory 75    15000 1000   0 false(unreach-call) .087 11   .47 1 error 2.6 280 21 0 timeout 900   2400 14000 0 timeout 900 2300 13000 0 unknown 890 250 11000 0 true 14    1100 150   -32 timeout 900    1500 10000   0 out of memory 340     15000 4200    0 timeout 900     540 13000    0 false(unreach-call) 2.5 94 30 1 timeout (timeout) 900    4200   11000   0 timeout 900   3200 12000 0 timeout 900   5200 15000 0 timeout 900   3400 11000 0 out of memory 36   15000 470 0
array-industry-pattern/check_removal_from_set_after_insertion_false-unreach-call.i out of memory 39   15000 510 0 exception (gremlins) 240     150   3000    0 error (134) 23    12000 290   0 false(unreach-call) .061 11   .55 1 timeout 900   5700 9700 0 timeout 960   4200 10000 0 timeout 900 5900 9800 0 timeout 900 6000 8700 0 timeout 900    4200 12000   0 timeout 900    230 12000   0 timeout 900     1100 12000    0 timeout 900     940 7600    0 false(unreach-call) 4.9 110 64 1 timeout (timeout) 900    1300   9000   0 timeout 900   4000 13000 0 timeout 900   5300 13000 0 timeout 900   4800 12000 0 out of memory 50   15000 550 0
array-industry-pattern/array_monotonic_true-unreach-call.i out of memory 39   15000 520 0 timeout 900     540   10000    0 out of memory 110    15000 1700   0 true .052 8.2 .41 2 error 2.4 260 21 0 timeout 900   2400 13000 0 timeout 900 1800 11000 0 unknown 890 340 12000 0 timeout 900    730 9400   0 timeout 900    1000 9300   0 out of memory 330     15000 4000    0 timeout 900     600 9200    0 true 1.6 75 17 2 out of memory 9.6  15000   120   0 timeout 900   1700 12000 0 timeout 900   2700 13000 0 timeout 900   1700 14000 0 true 640   870 6400 2
array-industry-pattern/array_mul_init_true-unreach-call.i out of memory 38   15000 530 0 exception (gremlins) 170     100   2200    0 out of memory 130    15000 1600   0 true .064 11   .50 2 error 2.5 270 23 0 timeout 900   2200 12000 0 timeout 900 810 10000 0 unknown 890 1700 10000 0 timeout 900    1300 10000   0 timeout 900    3900 13000   0 out of memory 270     15000 3400    0 timeout 900     730 8600    0 timeout 880   170 13000 0 out of memory 15    15000   190   0 timeout 900   2400 14000 0 timeout 900   3600 15000 0 timeout 900   3500 9800 0 out of memory 35   15000 460 0
array-industry-pattern/array_of_struct_break_true-unreach-call.i timeout 900   10000 11000 0 exception (gremlins) 41     53   450    0 out of memory 290    15000 3400   0 true .046 8.3 .42 2 timeout 900   4300 9600 0 timeout 900   4300 6300 0 timeout 900 3000 8300 0 unknown 890 210 9400 0 true 70    5200 580   2 out of memory 880    15000 12000   0 out of memory 490     15000 6200    0 timeout 900     740 9600    0 true 1.7 80 19 2 true .81 60   10   2 timeout 900   4900 8400 0 timeout 900   5200 9000 0 timeout 900   5300 8800 0 true 640   880 6400 2
array-industry-pattern/array_of_struct_ptr_cond_init_true-unreach-call.i timeout 900   9200 12000 0 exception (gremlins) 80     80   880    0 error (1) 230    4200 3000   0 true .080 11   .46 2 timeout 900   4300 9200 0 timeout 900   3500 5300 0 timeout 900 3700 8200 0 timeout 900 3800 10000 0 out of memory 320    15000 2600   0 timeout 900    5200 9900   0 timeout 900     14000 8100    0 true .32  23 .64 2 true 4.2 88 49 2 timeout (timeout) 900    210   9300   0 timeout 900   5400 8800 0 timeout 900   5500 8600 0 timeout 900   5400 7600 0 true 650   880 6900 2
array-industry-pattern/array_of_struct_ptr_flag_init_true-unreach-call.i timeout 900   13000 10000 0 timeout 900     300   10000    0 out of memory 180    15000 2700   0 true .062 11   .43 2 timeout 910   11000 4300 0 timeout 900   5400 6400 0 timeout 900 4700 8400 0 unknown 530 670 4900 0 true 130    12000 930   2 timeout 900    3900 8000   0 timeout 900     12000 11000    0 out of memory 810     15000 9400    0 true 1.8 77 22 2 true 1.0  74   14   2 timeout 900   4200 13000 0 timeout 900   3800 13000 0 timeout 900   3100 12000 0 true 650   900 6200 2
array-industry-pattern/array_of_struct_ptr_monotonic_true-unreach-call.i timeout 900   9200 11000 0 timeout 900     630   9300    0 error (1) 230    4200 2900   0 true .073 11   .38 2 timeout 900   4300 9000 0 timeout 900   3900 5200 0 timeout 900 4100 7900 0 timeout 900 4100 8200 0 out of memory 330    15000 2900   0 timeout 900    2100 9700   0 out of memory 350     15000 4400    0 true .32  23 .81 2 true 1.8 78 23 2 timeout (timeout) 900    4100   9600   0 timeout 900   5500 8000 0 timeout 900   5400 7100 0 timeout 900   5400 7600 0 true 650   870 6500 2
array-industry-pattern/array_of_struct_ptr_mul_init_true-unreach-call.i out of memory 42   15000 510 0 exception (gremlins) 230     150   2500    0 error (42) 850    10000 12000   0 true .076 9.9 .31 2 timeout 900   5000 9700 0 timeout 900   4600 7100 0 timeout 900 4000 7800 0 unknown 890 240 9300 0 out of memory 350    15000 2300   0 timeout 900    2400 11000   0 out of memory 350     15000 5000    0 timeout 900     840 8900    0 timeout 880   680 9800 0 timeout (timeout) 900    7200   12000   0 timeout 900   5200 8400 0 timeout 900   5200 8000 0 timeout 900   5200 7300 0 out of memory 44   15000 470 0
array-industry-pattern/array_of_struct_single_elem_init_true-unreach-call.i out of memory 37   15000 520 0 exception (gremlins) 74     70   970    0 out of memory 150    15000 1800   0 true .076 11   .38 2 timeout 900   3900 12000 0 timeout 900   6300 7200 0 timeout 900 4800 8300 0 unknown 890 360 8600 0 true 70    4700 480   2 timeout 900    1400 11000   0 timeout 900     6000 11000    0 timeout 900     900 8500    0 true 7.4 94 91 2 true 3.0  180   41   2 error 8.0 310 60 0 error 8.0 300 66 0 error 8.2 310 60 0 true 650   870 6800 2
array-industry-pattern/array_ptr_partial_init_true-unreach-call.i out of memory 43   15000 510 0 timeout 900     320   12000    0 out of memory 830    15000 12000   0 true .077 11   .38 2 timeout 900   4000 10000 0 timeout 900   4100 6700 0 timeout 900 3700 8900 0 unknown 890 400 7900 0 true 170    14000 1000   2 timeout 900    6300 11000   0 out of memory 240     15000 3400    0 timeout 900     1000 10000    0 true 1.6 85 19 2 true .97 67   12   2 timeout 900   5500 7000 0 timeout 900   5500 8300 0 timeout 900   5500 9500 0 true 640   890 6500 2
array-industry-pattern/array_ptr_single_elem_init_true-unreach-call.i timeout 900   9200 11000 0 exception (gremlins) 100     74   1200    0 error (1) 120    4600 1400   0 true .080 8.4 .49 2 timeout 900   6400 8200 0 timeout 900   5100 5000 0 timeout 900 4400 7800 0 unknown 890 370 8700 0 out of memory 480    15000 4300   0 timeout 900    2400 9000   0 out of memory 320     15000 2400    0 timeout 900     1400 8800    0 true 14   100 200 2 timeout (timeout) 900    4300   8500   0 timeout 900   5400 8600 0 timeout 900   5500 9800 0 timeout 900   5400 7800 0 true 650   910 7100 2
array-industry-pattern/array_shadowinit_true-unreach-call.i timeout 900   14000 5900 0 false(unreach-call) .37  22   2.0  -16 error (42) 850    5500 6200   0 true .070 13   .39 2 timeout 910   11000 6400 0 segmentation fault 340   5000 2700 0 timeout 900 3800 9200 0 timeout 900 3600 8100 0 true 890    1300 12000   2 timeout 900    430 11000   0 timeout 900     610 9700    0 timeout 900     880 9200    0 true 880   390 13000 2 unknown .17 10   1.8 0 timeout 900   1700 14000 0 timeout 900   920 12000 0 timeout 900   1600 13000 0 true 650   890 6800 2
reducercommutativity/rangesum05_false-unreach-call.i false(unreach-call) 13   110 150 1 unknown .048 7.8 .58 0 false(unreach-call) .25 21 3.4 1 false(unreach-call) .052 8.3 .32 1 false(unreach-call) 5.3 390 54 1 false(unreach-call) 47   1200 340 1 false(unreach-call) 35 560 460 1 false(unreach-call) 490 180 5700 1 false(unreach-call) .20 24 2.4 1 false(unreach-call) .24 37 2.9 1 false(unreach-call) .25  38 3.2  1 false(unreach-call) 2.0   120 23    1 false(unreach-call) 1.6 75 22 1 false(unreach-call) .15 11   1.8 1 false(unreach-call) 18   490 200 1 false(unreach-call) 9.4 490 74 1 false(unreach-call) 19   570 190 1 false(unreach-call) 25   430 250 1
reducercommutativity/rangesum10_false-unreach-call.i false(unreach-call) 13   140 150 1 unknown .055 8.2 .42 0 false(unreach-call) .39 20 4.2 1 false(unreach-call) .049 11   .50 1 false(unreach-call) 7.2 410 58 1 false(unreach-call) 120   1800 930 1 false(unreach-call) 110 730 1500 1 false(unreach-call) 500 180 5800 1 false(unreach-call) .24 23 3.3 1 false(unreach-call) .29 38 3.3 1 false(unreach-call) .32  40 4.0  1 false(unreach-call) 12     250 150    1 false(unreach-call) 1.7 73 20 1 false(unreach-call) .18 11   1.6 1 false(unreach-call) 32   550 440 1 false(unreach-call) 13   490 110 1 false(unreach-call) 30   530 290 1 false(unreach-call) 32   490 290 1
reducercommutativity/rangesum20_false-unreach-call.i false(unreach-call) 21   220 210 1 unknown .046 7.8 .62 0 false(unreach-call) 1.1  24 13   1 false(unreach-call) .057 11   .33 1 false(unreach-call) 13   570 130 1 segmentation fault 290   2000 3100 0 timeout 900 5300 8800 0 false(unreach-call) 650 180 9000 1 false(unreach-call) .43 24 4.8 1 false(unreach-call) 1.0  40 13   1 false(unreach-call) 3.9   46 20    1 false(unreach-call) 120     600 1200    1 false(unreach-call) 1.9 75 24 1 false(unreach-call) .23 22   3.1 1 false(unreach-call) 74   840 730 1 false(unreach-call) 26   670 240 1 false(unreach-call) 46   610 530 1 false(unreach-call) 50   950 420 1
reducercommutativity/rangesum40_false-unreach-call.i false(unreach-call) 56   450 510 1 unknown .046 8.1 .47 0 false(unreach-call) 1.1  27 14   1 false(unreach-call) .059 13   .37 1 false(unreach-call) 61   1900 450 1 timeout 950   8100 11000 0 timeout 900 4000 8400 0 unknown 890 180 11000 0 false(unreach-call) 6.1  36 78   1 false(unreach-call) 2.7  45 30   1 false(unreach-call) 2.7   57 36    1 timeout 900     1100 9000    0 false(unreach-call) 2.3 94 29 1 false(unreach-call) .27 25   2.7 1 false(unreach-call) 150   2700 1600 1 timeout 900   1500 9100 0 false(unreach-call) 60   1500 660 1 false(unreach-call) 95   2200 860 1
reducercommutativity/rangesum60_false-unreach-call.i false(unreach-call) 320   1300 2600 1 unknown .046 8.1 .49 0 false(unreach-call) 7.4  50 84   1 false(unreach-call) .056 13   .62 1 false(unreach-call) 110   4200 990 1 timeout 940   8000 10000 0 timeout 900 4000 11000 0 unknown 900 180 9100 0 false(unreach-call) .96 32 13   1 false(unreach-call) 2.6  48 30   1 false(unreach-call) 2.8   67 32    1 timeout 900     820 2200    0 false(unreach-call) 2.8 120 35 1 false(unreach-call) .30 29   3.1 1 false(unreach-call) 270   4400 3100 1 timeout 900   2400 8700 0 unknown 64   2300 640 0 false(unreach-call) 190   3700 2300 1
reducercommutativity/rangesum_false-unreach-call.i false(unreach-call) 39   400 290 1 unknown .076 8.7 .47 0 false(unreach-call) .52 40 6.5 1 false(unreach-call) .075 10   .35 1 false(unreach-call) 13   590 100 1 segmentation fault 260   4600 2200 0 false(unreach-call) 170 2200 1800 1 false(unreach-call) 490 180 6000 1 false(unreach-call) 890    2800 9200   1 false(unreach-call) .65 92 6.9 1 false(unreach-call) 3.4   120 6.8  1 false(unreach-call) 1.5   160 16    1 false(unreach-call) 2.0 79 30 1 timeout (timeout) 900    210   7300   0 false(unreach-call) 14   530 100 1 timeout 900   1200 11000 0 false(unreach-call) 20   680 190 1 false(unreach-call) 150   460 1800 1
reducercommutativity/avg05_true-unreach-call.i timeout 900   1600 9100 0 unknown .051 8.2 .43 0 true 36    40 430   2 true .028 7.9 .13 2 timeout 900   1500 9100 0 timeout 910   3200 5500 0 timeout 900 1700 10000 0 timeout 900 2200 9100 0 true 150    90 1800   2 out of memory 160    15000 2100   0 true .091 23 .85 2 true 1.9   95 21    2 true 1.3 68 17 2 true .15 9.3 1.8 2 true 210   1200 2600 2 timeout 900   5600 6300 0 timeout 900   1100 13000 0 out of memory 670   15000 7300 0
reducercommutativity/avg10_true-unreach-call.i timeout 900   2100 9300 0 unknown .045 8.2 .50 0 true 540    170 7800   2 true .029 7.9 .11 2 timeout 900   1900 8700 0 timeout 910   4000 7300 0 timeout 900 3300 8900 0 timeout 900 3600 8800 0 timeout 900    270 11000   0 out of memory 220    15000 3300   0 true .11  23 1.1  2 true 16     190 180    2 true 1.3 67 18 2 true .17 9.5 1.8 2 true 390   1600 4500 2 timeout 900   1300 11000 0 timeout 900   4400 11000 0 out of memory 420   15000 6100 0
reducercommutativity/avg20_true-unreach-call.i timeout 900   3600 8500 0 unknown .068 8.7 .45 0 error (42) 850    280 10000   0 true .035 8.0 .13 2 timeout 900   3600 9700 0 segmentation fault 270   2300 2700 0 timeout 900 4400 9300 0 unknown 900 700 7800 0 timeout 900    330 11000   0 out of memory 280    15000 3800   0 true .13  23 1.6  2 timeout 900     490 2400    0 true 1.5 84 18 2 true .17 9.5 1.6 2 timeout 900   3700 11000 0 timeout 900   1900 13000 0 timeout 900   4700 13000 0 timeout 900   500 11000 0
reducercommutativity/avg40_true-unreach-call.i timeout 900   2200 10000 0 unknown .077 8.0 .38 0 error (42) 850    290 9600   0 true .032 7.7 .12 2 false(unreach-call) 110   3100 1000 -16 segmentation fault 130   1900 1200 0 timeout 910 5900 9200 0 unknown 890 270 7800 0 timeout 900    390 12000   0 out of memory 340    15000 3800   0 true .21  30 2.5  2 timeout 900     660 8500    0 true 1.9 130 20 2 true .17 9.3 1.7 2 unknown 170   4600 2000 0 timeout 900   4000 11000 0 unknown 230   4600 2400 0 timeout 900   500 11000 0
reducercommutativity/avg60_true-unreach-call.i timeout 900   1500 7000 0 unknown .048 8.9 .49 0 error (42) 850    340 11000   0 true .021 7.7 .15 2 false(unreach-call) 560   4700 7500 -16 timeout 960   3300 8400 0 timeout 900 4700 12000 0 unknown 890 270 7900 0 timeout 900    470 11000   0 out of memory 410    15000 5300   0 true .35  41 4.4  2 timeout 900     660 11000    0 true 2.8 200 35 2 true .19 9.5 1.7 2 unknown 280   4900 3700 0 error 750   4700 10000 0 unknown 440   5300 5700 0 timeout 900   500 12000 0
reducercommutativity/avg_true-unreach-call.i timeout 900   3300 7000 0 unknown .051 8.7 .51 0 error (42) 850    220 11000   0 aborted .11  8.1 1.3  0 timeout 900   5300 11000 0 segmentation fault 95   2500 760 0 timeout 900 4400 7200 0 unknown 890 180 11000 0 timeout 900    410 11000   0 timeout 900    170 13000   0 timeout 900     230 11000    0 timeout 900     300 9500    0 true 880   140 12000 2 unknown .16 9.9 1.7 0 timeout 900   770 13000 0 timeout 900   580 12000 0 timeout 900   780 13000 0 out of memory 470   15000 3300 0
reducercommutativity/max05_true-unreach-call_true-termination.i true 8.3 84 96 2 unknown .046 8.1 .50 0 true 1.9  23 20   2 true .026 7.8 .13 2 error 10   470 80 0 segmentation fault 82   1500 800 0 timeout 910 1500 11000 0 timeout 900 1600 9500 0 true 6.5  26 12   2 timeout 900    1000 12000   0 true 4.8   25 66    2 true 5.4   34 72    2 true 1.3 66 16 2 true 1.6  12   18   2 timeout 900   1200 11000 0 timeout 900   2200 14000 0 timeout 900   1400 12000 0 true 680   1100 7900 2
reducercommutativity/max10_true-unreach-call_true-termination.i true 160   1100 2200 2 unknown .078 8.1 .37 0 true 89    56 1100   2 true .034 7.7 .15 2 error 500   1000 6100 0 segmentation fault 56   1100 460 0 timeout 900 2600 8100 0 timeout 900 2500 9500 0 true 44    58 520   2 timeout 900    120 10000   0 true 330     58 4300    2 true 240     90 3000    2 true 1.6 80 21 2 true 52    34   530   2 timeout 900   2200 11000 0 timeout 900   3300 11000 0 timeout 900   2400 11000 0 true 790   1000 8100 2
reducercommutativity/max20_true-unreach-call.i timeout 900   4200 8600 0 unknown .046 9.0 .44 0 error (42) 850    180 13000   0 true .018 7.9 .14 2 timeout 900   1200 13000 0 timeout 900   3000 7300 0 timeout 900 2800 8300 0 unknown 890 190 12000 0 true 850    130 12000   2 timeout 900    140 12000   0 timeout 900     150 11000    0 timeout 900     330 13000    0 true 3.6 100 44 2 timeout (timeout) 900    140   10000   0 timeout 900   5300 13000 0 timeout 900   4600 7100 0 timeout 900   4600 12000 0 timeout 900   520 10000 0
reducercommutativity/max40_true-unreach-call.i timeout 900   2600 6400 0 unknown .063 8.2 .45 0 error (42) 850    220 8700   0 true .027 8.0 .11 2 false(unreach-call) 220   3300 2300 -16 timeout 910   3700 9600 0 timeout 900 2500 9100 0 unknown 890 230 9400 0 timeout 900    220 11000   0 timeout 900    170 9400   0 timeout 900     170 10000    0 timeout 900     580 8800    0 true 26   180 200 2 timeout (timeout) 900    260   11000   0 timeout 900   4800 12000 0 timeout 900   6000 8700 0 timeout 900   4700 11000 0 timeout 900   520 13000 0
reducercommutativity/max60_true-unreach-call.i timeout 900   1800 6100 0 unknown .072 8.2 .42 0 error (42) 850    260 8500   0 true .022 7.8 .12 2 false(unreach-call) 780   4800 8200 -16 timeout 910   2200 9900 0 timeout 900 4000 9600 0 unknown 890 250 8200 0 timeout 900    280 12000   0 timeout 900    200 10000   0 timeout 900     180 9100    0 timeout 900     630 11000    0 true 180   320 1100 2 timeout (timeout) 900    300   11000   0 timeout 900   5000 12000 0 timeout 900   6100 10000 0 timeout 900   5100 13000 0 timeout 900   530 11000 0
reducercommutativity/max_true-unreach-call.i timeout 900   1700 4400 0 unknown .050 8.9 .47 0 error (42) 850    230 10000   0 aborted .11  7.9 1.1  0 error 530   3900 5400 0 segmentation fault 41   1400 270 0 segmentation fault 120 2200 1300 0 unknown 890 260 11000 0 timeout 900    450 12000   0 timeout 900    120 13000   0 timeout 900     140 13000    0 timeout 900     110 1800    0 true 880   390 9200 2 unknown .18 10   1.8 0 timeout 900   2200 10000 0 timeout 900   1900 13000 0 timeout 900   1800 9900 0 out of memory 270   15000 3300 0
reducercommutativity/sep05_true-unreach-call.i true 5.2 73 61 2 unknown .073 7.9 .47 0 true .40 23 4.7 2 true .029 7.9 .13 2 error 44   1400 380 0 true 57   2100 440 2 true 840 1500 10000 2 true 850 1400 11000 2 true .61 23 7.4 2 timeout 900    8000 13000   0 true .55  24 6.2  2 true .80  36 10    2 true 1.3 67 16 2 true .18 9.4 1.6 2 timeout 900   4800 14000 0 true 290   1900 3900 2 timeout 900   4900 11000 0 true 680   1100 7300 2
reducercommutativity/sep10_true-unreach-call.i true 10   110 110 2 unknown .047 8.2 .48 0 true .77 27 8.1 2 true .021 7.8 .16 2 error 38   960 350 0 timeout 900   4800 7300 0 timeout 900 4800 8300 0 timeout 900 4800 8400 0 true .60 23 8.1 2 timeout 900    1400 13000   0 true 6.6   33 90    2 true 11     100 140    2 true 2.2 74 28 2 true .16 9.4 1.8 2 timeout 910   8700 9200 0 timeout 900   2500 12000 0 timeout 900   7400 9500 0 true 680   1000 7800 2
reducercommutativity/sep20_true-unreach-call.i true 17   230 200 2 unknown .083 7.9 .35 0 true 3.5  36 40   2 true .026 7.9 .13 2 timeout 900   4100 12000 0 timeout 910   5000 7900 0 timeout 900 3700 8800 0 unknown 890 190 12000 0 true .65 23 7.0 2 timeout 900    64 10000   0 timeout 900     67 13000    0 timeout 900     370 13000    0 timeout 880   100 12000 0 true .16 9.4 1.7 2 timeout 910   13000 7000 0 timeout 910   13000 7700 0 timeout 900   4700 9800 0 true 670   1000 7400 2
reducercommutativity/sep40_true-unreach-call.i true 470   1700 5000 2 unknown .045 11   .70 0 true 34    93 430   2 true .021 7.8 .17 2 false(unreach-call) 600   7300 4600 -16 segmentation fault 220   3000 2000 0 timeout 900 3900 8600 0 unknown 900 190 10000 0 true .69 29 9.3 2 timeout 900    92 10000   0 timeout 900     110 10000    0 timeout 900     520 2600    0 timeout 880   160 11000 0 true .18 9.2 2.2 2 timeout 900   9500 11000 0 timeout 900   13000 8000 0 timeout 900   4800 11000 0 true 690   1100 7600 2
reducercommutativity/sep60_true-unreach-call.i timeout 900   2900 7100 0 unknown .051 8.3 .49 0 true 160    160 1900   2 true .032 7.7 .12 2 timeout 900   8900 7300 0 timeout 910   3500 8600 0 timeout 900 4300 9100 0 unknown 900 190 11000 0 true .74 35 8.8 2 timeout 900    130 9400   0 timeout 900     150 11000    0 timeout 900     880 11000    0 timeout 880   250 8800 0 true .19 9.4 1.9 2 timeout 900   6000 13000 0 timeout 900   12000 9600 0 timeout 900   5300 13000 0 true 770   1100 8900 2
reducercommutativity/sep_true-unreach-call.i timeout 900   9400 3600 0 unknown .075 8.1 .44 0 error (134) 640    13000 4600   0 aborted .14  8.0 1.1  0 timeout 900   5800 10000 0 timeout 960   5300 9700 0 timeout 900 2700 9600 0 unknown 890 190 8400 0 timeout 900    450 10000   0 timeout 900    170 10000   0 timeout 900     250 11000    0 timeout 900     390 12000    0 true 880   180 11000 2 unknown .16 10   2.0 0 timeout 900   5100 11000 0 timeout 900   1700 11000 0 timeout 900   7900 8500 0 out of memory 270   15000 3100 0
reducercommutativity/sum05_true-unreach-call_true-termination.i true 20   220 230 2 unknown .049 8.1 .50 0 true 4.2  25 51   2 true .020 7.9 .14 2 timeout 900   1200 9700 0 segmentation fault 16   610 120 0 timeout 900 3800 13000 0 timeout 900 3900 11000 0 true .16 23 2.0 2 out of memory 180    15000 2700   0 true .12  23 .94 2 true 1.4   31 2.7  2 true 1.3 70 18 2 true .17 9.3 1.6 2 true 26   850 230 2 true 24   720 240 2 timeout 900   1100 11000 0 true 710   990 7800 2
reducercommutativity/sum10_true-unreach-call.i timeout 900   2300 9800 0 unknown .049 8.7 .46 0 true 180    110 2300   2 true .017 7.9 .18 2 timeout 900   1700 11000 0 timeout 910   3100 8300 0 timeout 900 2000 10000 0 timeout 900 2400 11000 0 true .20 23 1.9 2 timeout 900    13000 2300   0 true .40  23 .94 2 true 4.0   74 51    2 true 1.3 70 23 2 true .28 19   2.3 2 true 77   1400 750 2 true 88   1200 950 2 timeout 900   5100 13000 0 out of memory 420   15000 4700 0
reducercommutativity/sum20_true-unreach-call.i timeout 900   3600 10000 0 unknown .069 8.0 .43 0 error (42) 850    260 11000   0 true .026 7.8 .15 2 timeout 900   2600 11000 0 timeout 910   2900 9300 0 timeout 910 6600 8600 0 unknown 900 240 7900 0 true .19 23 2.8 2 out of memory 280    15000 3600   0 true .16  23 1.6  2 true 240     310 2200    2 true 1.4 82 16 2 true .18 9.4 1.9 2 timeout 900   4800 6600 0 true 790   2600 9800 2 timeout 900   5000 6800 0 timeout 900   490 9600 0
reducercommutativity/sum40_true-unreach-call.i timeout 900   1600 7300 0 unknown .047 8.1 .53 0 error (42) 850    280 10000   0 true .048 7.8 .13 2 false(unreach-call) 88   2900 870 -16 timeout 960   7600 9600 0 timeout 910 7400 11000 0 unknown 890 270 7500 0 true .23 23 3.0 2 out of memory 340    15000 4300   0 true .22  30 2.6  2 timeout 900     490 8100    0 true 1.8 120 23 2 true .17 9.3 2.0 2 timeout 900   4600 12000 0 timeout 900   4700 11000 0 timeout 900   4700 12000 0 timeout 900   490 11000 0
reducercommutativity/sum60_true-unreach-call.i timeout 900   2000 7600 0 unknown .048 8.1 .59 0 error (42) 850    260 11000   0 true .023 7.9 .14 2 false(unreach-call) 240   4600 2400 -16 timeout 910   2900 8600 0 timeout 910 6500 10000 0 unknown 890 200 8700 0 true .28 24 3.1 2 out of memory 410    15000 4700   0 true .35  41 3.4  2 timeout 900     500 6800    0 true 2.8 200 33 2 true .27 17   1.7 2 timeout 900   6400 8200 0 timeout 900   4900 13000 0 timeout 900   6300 11000 0 timeout 900   490 12000 0
reducercommutativity/sum_true-unreach-call.i timeout 900   2000 4800 0 unknown .083 8.6 .30 0 error (42) 850    250 11000   0 aborted .14  7.9 1.2  0 error 160   3600 2200 0 segmentation fault 47   1500 300 0 timeout 900 4300 9100 0 unknown 890 240 10000 0 timeout 900    530 12000   0 timeout 900    190 11000   0 timeout 900     190 12000    0 timeout 900     200 11000    0 true 880   390 11000 2 unknown .17 10   2.1 0 timeout 900   4700 6300 0 timeout 900   990 11000 0 timeout 900   4700 9700 0 out of memory 420   15000 3900 0
../../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score
total 135 45000 1500000 470000 -10 135 63000    30000 710000   -42 135 36000 1400000 370000 30 135 86 1400 960 214 135 25000   180000 270000 -104 135 110000 370000 1300000 8 135 120000 340000 1400000 9 135 110000 93000 1200000 6 135 46000 350000 540000 48 135 110000   680000 1300000 6 135 48000 1400000 580000 36 135 100000 220000 1000000 30 135 17000 23000 210000 212 135 25000 150000 280000 145 135 110000 470000 1500000 22 135 110000 470000 1500000 17 135 110000 440000 1500000 13 135 63000 530000 670000 162
    correct results 14 1200 12000 12000 22 3 .66 55 3.9 6 18 1200 9700 16000 30 127 85 1300 960 214 7 210   8300 1800 8 5 230 5700 1800 8 6 1400 9600 17000 9 5 3000 2100 38000 6 95 23000 110000 280000 160 6 7.5 300 86 6 21 490 8400 6000 36 17 660 2200 7000 30 126 8800 14000 110000 212 87 260 31000 3100 145 14 1300 16000 14000 22 10 1300 9100 15000 17 9 210 5400 2100 13 94 45000 74000 470000 162
        correct true 8 730 9000 8400 16 3 .66 55 3.9 6 12 1100 9500 16000 24 87 31 840 330 174 1 2.7 280 25 2 3 64 2700 490 6 3 1100 6100 14000 6 1 850 1400 11000 2 65 5400 70000 67000 130 0 15 470 8000 5900 30 13 520 1100 5700 26 86 8500 9900 110000 172 58 110 4500 1400 116 8 730 6600 8300 16 7 1200 7500 15000 14 4 31 1500 230 8 68 45000 61000 470000 136
        correct false 6 460 2700 3900 6 0 6 11 180 130 6 40 54 450 630 40 6 210   8000 1800 6 2 170 3000 1300 2 3 320 3500 3700 3 4 2100 730 27000 4 30 17000 45000 210000 30 6 7.5 300 86 6 6 13 370 100 6 4 140 1100 1400 4 40 240 4500 2900 40 29 150 27000 1800 29 6 550 9600 6200 6 3 49 1600 420 3 5 180 3900 1900 5 26 670 13000 6900 26
    correct-unconfimed results 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
        correct-unconfirmed false 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
    incorrect results 2 89 10000 880 -32 3 36    82 370   -48 0 0 7 2600   31000 27000 -112 0 0 0 4 1100 3600 13000 -112 0 0 0 0 0 0 0 0 0
        incorrect true 0 0 0 0 0 0 0 0 3 700 2900 7300 -96 0 0 0 0 0 0 0 0 0
        incorrect false 2 89 10000 880 -32 3 36    82 370   -48 0 0 7 2600   31000 27000 -112 0 0 0 1 440 680 5700 -16 0 0 0 0 0 0 0 0 0
score (135 tasks, max score: 230) -10 -42 30 214 -104 8 9 6 48 6 36 30 212 145 22 17 13 162
Run set 2ls.sv-comp17.ReachSafety-Arrays blast.sv-comp17.ReachSafety-Arrays cbmc.sv-comp17.ReachSafety-Arrays ceagle.sv-comp17.ReachSafety-Arrays cpa-bam-bnb.sv-comp17.ReachSafety-Arrays cpa-kind.sv-comp17.ReachSafety-Arrays cpa-seq.sv-comp17.ReachSafety-Arrays depthk.sv-comp17.ReachSafety-Arrays esbmc.sv-comp17.ReachSafety-Arrays esbmc-falsi.sv-comp17.ReachSafety-Arrays esbmc-incr.sv-comp17.ReachSafety-Arrays esbmc-kind.sv-comp17.ReachSafety-Arrays smack.sv-comp17.ReachSafety-Arrays symbiotic4.sv-comp17.ReachSafety-Arrays uautomizer.sv-comp17.ReachSafety-Arrays ukojak.sv-comp17.ReachSafety-Arrays utaipan.sv-comp17.ReachSafety-Arrays veriabs.sv-comp17.ReachSafety-Arrays