Tool 2LS 0.5.0 CBMC 5.6 Ceagle Ceagle 1.3 @ 53cfa89 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
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: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 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 11:10:58 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 ]]
Run set 2ls.[sv-comp17.ReachSafety-Arrays; sv-comp17.ReachSafety-BitVectors; sv-comp17.ReachSafety-ControlFlow; sv-comp17.ReachSafety-ECA; sv-comp17.ReachSafety-Floats; sv-comp17.ReachSafety-Heap; sv-comp17.ReachSafety-Loops; sv-comp17.ReachSafety-ProductLines; sv-comp17.ReachSafety-Recursive; sv-comp17.ReachSafety-Sequentialized] cbmc.[sv-comp17.ReachSafety-Arrays; sv-comp17.ReachSafety-BitVectors; sv-comp17.ReachSafety-ControlFlow; sv-comp17.ReachSafety-ECA; sv-comp17.ReachSafety-Floats; sv-comp17.ReachSafety-Heap; sv-comp17.ReachSafety-Loops; sv-comp17.ReachSafety-ProductLines; sv-comp17.ReachSafety-Recursive; sv-comp17.ReachSafety-Sequentialized] ceagle.[sv-comp17.ReachSafety-Arrays; sv-comp17.ReachSafety-BitVectors; sv-comp17.ReachSafety-ControlFlow; sv-comp17.ReachSafety-ECA; sv-comp17.ReachSafety-Floats; sv-comp17.ReachSafety-Heap; sv-comp17.ReachSafety-Loops; sv-comp17.ReachSafety-ProductLines; sv-comp17.ReachSafety-Recursive; sv-comp17.ReachSafety-Sequentialized] cpa-kind.[sv-comp17.ReachSafety-Arrays; sv-comp17.ReachSafety-BitVectors; sv-comp17.ReachSafety-ControlFlow; sv-comp17.ReachSafety-ECA; sv-comp17.ReachSafety-Floats; sv-comp17.ReachSafety-Heap; sv-comp17.ReachSafety-Loops; sv-comp17.ReachSafety-ProductLines; sv-comp17.ReachSafety-Recursive; sv-comp17.ReachSafety-Sequentialized] cpa-seq.[sv-comp17.ReachSafety-Arrays; sv-comp17.ReachSafety-BitVectors; sv-comp17.ReachSafety-ControlFlow; sv-comp17.ReachSafety-ECA; sv-comp17.ReachSafety-Floats; sv-comp17.ReachSafety-Heap; sv-comp17.ReachSafety-Loops; sv-comp17.ReachSafety-ProductLines; sv-comp17.ReachSafety-Recursive; sv-comp17.ReachSafety-Sequentialized] depthk.[sv-comp17.ReachSafety-Arrays; sv-comp17.ReachSafety-BitVectors; sv-comp17.ReachSafety-ControlFlow; sv-comp17.ReachSafety-ECA; sv-comp17.ReachSafety-Floats; sv-comp17.ReachSafety-Heap; sv-comp17.ReachSafety-Loops; sv-comp17.ReachSafety-ProductLines; sv-comp17.ReachSafety-Recursive; sv-comp17.ReachSafety-Sequentialized] esbmc.[sv-comp17.ReachSafety-Arrays; sv-comp17.ReachSafety-BitVectors; sv-comp17.ReachSafety-ControlFlow; sv-comp17.ReachSafety-ECA; sv-comp17.ReachSafety-Floats; sv-comp17.ReachSafety-Heap; sv-comp17.ReachSafety-Loops; sv-comp17.ReachSafety-ProductLines; sv-comp17.ReachSafety-Recursive; sv-comp17.ReachSafety-Sequentialized] esbmc-falsi.[sv-comp17.ReachSafety-Arrays; sv-comp17.ReachSafety-BitVectors; sv-comp17.ReachSafety-ControlFlow; sv-comp17.ReachSafety-ECA; sv-comp17.ReachSafety-Floats; sv-comp17.ReachSafety-Heap; sv-comp17.ReachSafety-Loops; sv-comp17.ReachSafety-ProductLines; sv-comp17.ReachSafety-Recursive; sv-comp17.ReachSafety-Sequentialized] esbmc-incr.[sv-comp17.ReachSafety-Arrays; sv-comp17.ReachSafety-BitVectors; sv-comp17.ReachSafety-ControlFlow; sv-comp17.ReachSafety-ECA; sv-comp17.ReachSafety-Floats; sv-comp17.ReachSafety-Heap; sv-comp17.ReachSafety-Loops; sv-comp17.ReachSafety-ProductLines; sv-comp17.ReachSafety-Recursive; sv-comp17.ReachSafety-Sequentialized] esbmc-kind.[sv-comp17.ReachSafety-Arrays; sv-comp17.ReachSafety-BitVectors; sv-comp17.ReachSafety-ControlFlow; sv-comp17.ReachSafety-ECA; sv-comp17.ReachSafety-Floats; sv-comp17.ReachSafety-Heap; sv-comp17.ReachSafety-Loops; sv-comp17.ReachSafety-ProductLines; sv-comp17.ReachSafety-Recursive; sv-comp17.ReachSafety-Sequentialized] smack.[sv-comp17.ReachSafety-Arrays; sv-comp17.ReachSafety-BitVectors; sv-comp17.ReachSafety-ControlFlow; sv-comp17.ReachSafety-ECA; sv-comp17.ReachSafety-Floats; sv-comp17.ReachSafety-Heap; sv-comp17.ReachSafety-Loops; sv-comp17.ReachSafety-ProductLines; sv-comp17.ReachSafety-Recursive; sv-comp17.ReachSafety-Sequentialized] symbiotic4.[sv-comp17.ReachSafety-Arrays; sv-comp17.ReachSafety-BitVectors; sv-comp17.ReachSafety-ControlFlow; sv-comp17.ReachSafety-ECA; sv-comp17.ReachSafety-Floats; sv-comp17.ReachSafety-Heap; sv-comp17.ReachSafety-Loops; sv-comp17.ReachSafety-ProductLines; sv-comp17.ReachSafety-Recursive; sv-comp17.ReachSafety-Sequentialized] uautomizer.[sv-comp17.ReachSafety-Arrays; sv-comp17.ReachSafety-BitVectors; sv-comp17.ReachSafety-ControlFlow; sv-comp17.ReachSafety-ECA; sv-comp17.ReachSafety-Floats; sv-comp17.ReachSafety-Heap; sv-comp17.ReachSafety-Loops; sv-comp17.ReachSafety-ProductLines; sv-comp17.ReachSafety-Recursive; sv-comp17.ReachSafety-Sequentialized] ukojak.[sv-comp17.ReachSafety-Arrays; sv-comp17.ReachSafety-BitVectors; sv-comp17.ReachSafety-ControlFlow; sv-comp17.ReachSafety-ECA; sv-comp17.ReachSafety-Floats; sv-comp17.ReachSafety-Heap; sv-comp17.ReachSafety-Loops; sv-comp17.ReachSafety-ProductLines; sv-comp17.ReachSafety-Recursive; sv-comp17.ReachSafety-Sequentialized] utaipan.[sv-comp17.ReachSafety-Arrays; sv-comp17.ReachSafety-BitVectors; sv-comp17.ReachSafety-ControlFlow; sv-comp17.ReachSafety-ECA; sv-comp17.ReachSafety-Floats; sv-comp17.ReachSafety-Heap; sv-comp17.ReachSafety-Loops; sv-comp17.ReachSafety-ProductLines; sv-comp17.ReachSafety-Recursive; sv-comp17.ReachSafety-Sequentialized]
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 ]] --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-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 ]]; --witness 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 ]]
../../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J)
array-examples/data_structures_set_multi_proc_false-unreach-call_ground.i 41     15000 470    130    14000 1700    .058 11   .41 900   4400 11000 900   4300 12000 900    750 13000   64    15000 860    900     230 12000    900     590 2500    900     1100 11000    2.7   85   29    2.5   300   28    900   5600 12000 900   5200 12000 900   5300 14000
array-examples/sorting_bubblesort_false-unreach-call2_ground.i 38     15000 530    22    15000 250    24     8.3 250    900   2400 11000 900   1400 13000 46    160 640   150    15000 1100    900     970 11000    360     15000 4400    900     500 9000    2.2   94   25    900     4200   9700    900   2500 13000 900   4400 12000 900   2200 12000
array-examples/sorting_bubblesort_false-unreach-call_ground.i 38     15000 540    22    15000 290    18     11   230    900   2100 11000 900   1400 14000 46    160 610   140    15000 1100    900     970 10000    360     15000 5100    900     450 7700    2.2   90   27    900     4200   9300    900   2300 14000 900   3900 13000 900   2100 14000
array-examples/sorting_selectionsort_false-unreach-call2_ground.i 39     15000 540    58    13000 760    .067 11   .36 900   2300 12000 900   2200 13000 890    330 10000   34    15000 320    900     530 11000    280     15000 3200    900     400 8600    18     560   230    340     71   3500    900   2400 13000 900   3400 14000 900   2400 13000
array-examples/sorting_selectionsort_false-unreach-call_ground.i 40     15000 520    70    13000 910    .056 13   .56 900   2100 13000 900   2200 10000 890    330 8200   34    15000 310    900     530 11000    280     15000 3200    900     430 7600    120     650   1400    340     70   3300    900   3000 13000 900   2600 12000 900   2600 12000
array-examples/standard_allDiff2_false-unreach-call_ground.i 220     15000 1900    410    10000 2400    9.2   11   130    900   2100 12000 900   2200 11000 900    1500 9300   40    15000 440    900     4500 11000    900     7500 11000    900     5900 10000    20     130   240    1.0   150   13    900   5700 15000 900   2300 13000 900   5400 13000
array-examples/standard_copy1_false-unreach-call_ground.i 900     13000 12000    130    15000 1700    .053 9.3 .31 900   2200 14000 900   2200 12000 79    100 1000   310    670 4000    900     1300 1600    280     15000 3600    280     15000 3300    1.8   83   25    1.8   230   21    900   2300 14000 900   3500 14000 900   1800 13000
array-examples/standard_copy2_false-unreach-call_ground.i 38     15000 510    83    15000 1000    .082 11   .33 900   2200 12000 900   2200 12000 890    190 9700   490    820 5800    900     5300 12000    290     15000 3400    900     330 2100    1.8   77   26    4.6   560   50    900   3300 13000 900   3400 13000 900   2400 12000
array-examples/standard_copy3_false-unreach-call_ground.i 39     15000 560    94    15000 1500    .052 11   .43 900   2100 13000 900   2400 12000 890    200 10000   660    970 8500    900     5200 11000    290     15000 3800    900     680 10000    1.9   80   23    5.9   840   64    900   4200 12000 900   3600 12000 900   3500 14000
array-examples/standard_copy4_false-unreach-call_ground.i 38     15000 610    100    15000 1400    .044 8.2 .41 900   2300 12000 900   2400 11000 890    190 11000   810    1100 11000    900     5300 12000    290     15000 3500    900     660 10000    2.0   85   25    7.4   1100   84    900   4900 15000 900   4300 12000 900   5000 13000
array-examples/standard_copy5_false-unreach-call_ground.i 39     15000 550    120    15000 1500    .076 8.3 .33 900   2300 12000 900   2400 11000 900    210 11000   890    1200 10000    900     5300 11000    280     15000 3700    900     830 8300    2.0   83   28    8.7   1400   110    900   5000 13000 900   3800 13000 900   5100 13000
array-examples/standard_copy6_false-unreach-call_ground.i 39     15000 570    93    15000 1200    .053 8.4 .38 900   2100 12000 900   2200 13000 890    240 9300   890    1200 12000    900     5300 12000    290     15000 3900    900     730 9700    2.1   88   26    10     1700   130    900   5100 14000 900   4800 13000 900   5300 13000
array-examples/standard_copy7_false-unreach-call_ground.i 39     15000 470    100    15000 1600    .050 11   .41 900   2000 12000 900   3500 12000 900    270 9700   900    1300 10000    900     5300 14000    290     15000 3500    900     750 10000    2.2   91   27    11     1900   170    900   5200 13000 900   2900 15000 900   5200 14000
array-examples/standard_copy8_false-unreach-call_ground.i 39     15000 460    82    14000 1200    .062 12   .45 900   2300 11000 900   2200 13000 900    300 9900   890    1400 10000    900     5300 13000    280     15000 3700    900     840 12000    2.3   93   25    13     2200   160    900   5100 12000 900   2400 12000 900   5300 14000
array-examples/standard_copy9_false-unreach-call_ground.i 38     15000 530    89    14000 1400    .055 11   .46 900   2100 15000 900   3500 11000 900    330 9200   890    1400 9800    900     5300 12000    290     15000 4700    900     820 8700    2.3   93   28    14     2500   160    900   5100 12000 900   3600 13000 900   5300 12000
array-examples/standard_copyInitSum2_false-unreach-call_ground.i 41     15000 520    78    15000 1200    .049 8.6 .37 900   1900 12000 900   730 11000 890    240 9900   340    680 4200    900     5900 12000    270     15000 3500    900     670 8600    1.9   84   29    2.6   560   35    900   4100 13000 900   2500 12000 900   3300 13000
array-examples/standard_init1_false-unreach-call_ground.i 900     9800 11000    130    15000 1800    .061 11   .45 900   2100 12000 900   740 12000 900    770 13000   160    530 1800    900     5800 11000    260     15000 3400    900     560 10000    1.7   77   23    1.4   280   18    900   2400 15000 900   2500 13000 900   1700 12000
array-examples/standard_init2_false-unreach-call_ground.i 43     15000 550    67    15000 880    .056 13   .47 900   2100 11000 900   720 12000 900    800 12000   490    790 6000    900     5900 11000    270     15000 3200    900     660 10000    1.7   85   23    2.7   560   33    900   2500 13000 900   3900 15000 900   2300 11000
array-examples/standard_init3_false-unreach-call_ground.i 42     15000 570    70    15000 910    .051 11   .42 900   2000 13000 900   760 12000 900    710 14000   790    1100 11000    900     5900 12000    270     15000 3900    900     540 9900    1.8   86   23    3.9   840   49    900   2700 13000 900   4100 12000 900   2500 13000
array-examples/standard_init4_false-unreach-call_ground.i 42     15000 540    73    15000 890    .090 49   .97 900   2100 13000 900   780 13000 900    750 11000   900    1200 12000    900     5800 11000    260     15000 3700    900     690 9300    1.8   82   23    5.1   1100   52    900   3500 13000 900   3700 12000 900   3200 14000
array-examples/standard_init5_false-unreach-call_ground.i 42     15000 540    76    15000 990    .077 11   .28 900   2300 12000 900   730 12000 900    230 9400   890    1300 12000    900     5900 12000    260     15000 4100    900     650 9000    1.8   79   21    6.5   1400   82    900   3800 14000 900   3100 12000 900   3800 13000
array-examples/standard_init6_false-unreach-call_ground.i 42     15000 500    79    15000 1000    .051 8.3 .38 900   1900 12000 900   850 11000 890    240 11000   900    1400 10000    900     5800 11000    260     15000 3900    900     770 8200    1.8   86   22    7.7   1700   93    900   5100 14000 900   3100 14000 900   5000 13000
array-examples/standard_init7_false-unreach-call_ground.i 42     15000 620    55    15000 720    .063 11   .46 900   1800 12000 900   800 14000 890    270 11000   890    1500 10000    900     5900 12000    260     15000 3700    900     450 1900    1.9   80   25    8.5   1900   97    900   5100 12000 900   4200 12000 900   5000 14000
array-examples/standard_init8_false-unreach-call_ground.i 42     15000 600    57    15000 800    .075 11   .39 900   2100 13000 900   760 11000 900    290 8200   890    1600 10000    900     6000 14000    260     15000 3400    900     890 11000    1.9   78   26    9.9   2200   120    900   5100 14000 900   4500 13000 900   5300 13000
array-examples/standard_init9_false-unreach-call_ground.i 42     15000 570    59    15000 920    .052 8.4 .35 900   2000 14000 900   760 11000 900    320 8400   890    1800 12000    900     5900 11000    260     15000 3800    900     740 8900    1.9   81   26    11     2500   130    900   5300 11000 900   4000 15000 900   5200 15000
array-examples/standard_minInArray_false-unreach-call_ground.i 320     15000 3300    850    1300 3500    .049 11   .44 900   2300 11000 900   2200 13000 97    120 1400   33    1300 380    900     530 9500    290     15000 3900    660     15000 8100    1.9   90   23    .50  100   5.8  900   2300 12000 900   2800 14000 900   1900 14000
array-examples/standard_partition_false-unreach-call_ground.i 40     15000 510    68    14000 810    .046 8.2 .38 900   2300 12000 900   2200 12000 900    2200 11000   890    12000 10000    900     1100 11000    330     15000 3700    900     630 8800    2.0   91   29    900     12000   8900    900   3000 12000 900   3800 12000 900   3100 12000
array-examples/standard_running_false-unreach-call.i 42     15000 580    94    15000 1300    .052 13   .60 900   2500 12000 900   2200 12000 890    310 11000   900    1400 13000    470     15000 6200    840     15000 2300    900     730 9500    2.3   100   23    1.2   160   14    900   3300 15000 900   3100 14000 900   2900 13000
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i 41     15000 600    850    1500 4300    .055 11   .47 3.9 280 26 160   2200 1900 900    1200 12000   61    15000 610    900     11000 13000    540     15000 6500    900     1200 8800    2.3   100   27    .16  9.6 1.7  7.1 340 57 900   2200 12000 7.0 350 54
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i 41     15000 560    26    13000 340    .068 11   .42 900   4000 12000 900   3700 12000 900    260 8300   63    15000 760    900     230 12000    900     1100 8900    900     1300 9800    880     220   9900    900     1300   10000    900   5300 14000 900   5200 13000 900   5400 12000
array-examples/relax_true-unreach-call.i 5.7   170 48    850    4800 3300    .031 8.2 .14 950   3800 9200 900   4900 8000 890    190 11000   890    3200 10000    900     540 7200    900     240 2400    900     490 7700    880     370   11000    150     54   1600    900   1100 13000 900   540 11000 900   730 11000
array-examples/sanfoundry_02_true-unreach-call_ground.i 320     15000 3100    850    2300 3500    .047 8.5 .49 900   2200 12000 900   2200 12000 310    180 3700   900    440 10000    900     740 11000    450     15000 5900    900     6400 11000    1.5   77   21    320     120   2300    900   2200 15000 900   3900 14000 900   2000 12000
array-examples/sanfoundry_10_true-unreach-call_ground.i 900     15000 11000    28    13000 370    .067 13   .37 31   1200 200 900   5700 11000 900    180 9800   900    2600 13000    900     10000 8600    900     920 9100    900     1000 10000    4.2   91   60    900     940   10000    900   1400 12000 900   1300 11000 900   1500 12000
array-examples/sanfoundry_24_true-unreach-call.i 41     5500 520    850    4200 9300    .027 7.8 .11 900   3900 11000 900   3900 13000 900    3900 12000   40    1700 560    900     15000 12000    470     15000 6400    .081 23 .99 880     310   12000    900     6400   7900    8.0 370 67 6.7 320 55 6.7 350 52
array-examples/sanfoundry_27_true-unreach-call_ground.i 330     15000 3500    850    1200 3500    .11  8.3 .30 900   2200 12000 900   2200 12000 120    120 1500   900    360 10000    900     530 10000    290     15000 3500    900     14000 12000    1.8   77   20    .47  97   5.8  900   2300 13000 900   3200 14000 900   2000 15000
array-examples/sanfoundry_43_true-unreach-call_ground.i 39     15000 470    110    15000 1600    .12  11   .35 2.9 270 24 93   2300 1200 52    100 760   .80 65 8.4  900     4300 11000    900     10000 13000    .090 23 1.0  1.2   69   14    .16  9.3 1.5  5.6 320 43 5.9 320 47 7.3 350 54
array-examples/sorting_bubblesort_true-unreach-call_ground.i 38     15000 470    19    15000 240    26     12   300    900   2400 12000 900   2200 13000 46    160 630   150    15000 1000    900     970 10000    360     15000 4700    900     490 9700    23     140   260    900     4200   9200    900   2400 12000 900   3000 13000 900   2300 12000
array-examples/sorting_selectionsort_true-unreach-call_ground.i 39     15000 520    70    13000 890    .45  11   5.2  900   2100 14000 900   2200 11000 890    380 8900   34    15000 330    900     530 11000    280     15000 3600    900     410 8300    880     770   9900    330     69   3200    900   3200 13000 900   3800 14000 900   2700 13000
array-examples/standard_compareModified_true-unreach-call_ground.i 42     15000 670    140    15000 2100    .048 8.2 .42 900   2300 14000 900   2200 13000 890    220 11000   29    2300 440    900     490 11000    290     15000 3900    900     780 10000    1.4   75   20    100     170   680    900   2600 13000 900   4900 12000 900   2100 12000
array-examples/standard_compare_true-unreach-call_ground.i 190     15000 2000    850    1400 3700    .070 11   .39 900   3700 12000 900   2400 11000 110    170 1300   13    1200 160    900     530 9900    290     15000 4200    350     15000 4600    1.7   74   21    100     170   780    900   2700 12000 900   2500 13000 900   2000 13000
array-examples/standard_copy1_true-unreach-call_ground.i 900     14000 9100    130    15000 1500    .056 8.4 .40 900   2200 11000 900   2400 14000 900    200 9200   3.9  420 52    900     5200 12000    290     15000 3900    900     650 9500    1.6   82   29    1.1   100   16    900   3700 14000 900   3500 14000 900   1900 13000
array-examples/standard_copy2_true-unreach-call_ground.i 38     15000 630    83    15000 1100    .051 8.2 .34 900   3700 14000 900   2200 11000 900    260 8400   4.1  450 46    900     5200 11000    290     15000 3800    900     630 10000    1.8   78   20    1.5   120   22    900   3400 12000 900   3700 15000 900   2800 13000
array-examples/standard_copy3_true-unreach-call_ground.i 39     15000 480    94    15000 1400    .059 8.5 .39 900   2200 11000 900   2200 13000 890    300 9300   4.2  470 48    900     5200 12000    290     15000 3500    900     640 10000    1.8   83   20    1.8   140   21    900   3800 14000 900   4000 11000 900   3500 13000
array-examples/standard_copy4_true-unreach-call_ground.i 39     15000 510    110    15000 1500    .053 8.4 .36 900   2300 13000 900   3500 11000 890    330 10000   4.3  500 54    900     5300 11000    290     15000 3700    900     370 1600    1.9   87   25    2.2   160   29    900   4400 14000 900   4500 12000 900   4900 12000
array-examples/standard_copy5_true-unreach-call_ground.i 39     15000 520    120    15000 1800    .075 13   .45 900   2200 11000 900   2200 12000 890    270 9700   4.5  520 52    900     5300 12000    280     15000 3700    900     660 9000    2.0   87   26    2.5   180   34    900   4900 14000 900   3000 13000 900   5100 15000
array-examples/standard_copy6_true-unreach-call_ground.i 39     15000 470    92    15000 1300    .063 11   .34 900   2400 13000 900   2400 11000 890    270 8400   4.7  550 55    900     5300 13000    280     15000 3800    900     640 9000    2.1   90   28    2.8   200   35    900   5100 13000 900   3600 13000 900   5300 13000
array-examples/standard_copy7_true-unreach-call_ground.i 44     15000 510    100    15000 1400    .047 8.3 .34 900   3700 11000 900   2200 12000 890    310 8900   4.8  570 63    900     5300 11000    280     15000 4200    900     680 9100    2.2   94   28    3.2   230   49    900   5200 14000 900   3900 12000 900   5200 14000
array-examples/standard_copy8_true-unreach-call_ground.i 38     15000 520    82    14000 1100    .078 11   .34 900   2500 13000 900   2200 14000 890    400 12000   5.0  600 58    900     5200 13000    290     15000 3800    900     730 9800    2.5   92   28    3.5   250   47    900   5000 12000 900   3800 14000 900   5200 13000
array-examples/standard_copy9_true-unreach-call_ground.i 39     15000 560    89    14000 1200    .082 11   .45 900   1900 14000 900   2200 10000 890    340 7600   5.2  620 70    900     5300 12000    290     15000 4200    900     680 8200    2.5   100   30    3.9   270   50    900   5100 13000 900   3400 12000 900   5300 14000
array-examples/standard_copyInitSum2_true-unreach-call_ground.i 41     15000 580    78    15000 1000    .051 11   .42 900   2000 12000 900   690 14000 900    160 10000   4.3  470 50    900     5900 11000    270     15000 3200    900     310 2400    2.1   83   28    1.4   98   17    900   3500 12000 900   3300 12000 900   3400 13000
array-examples/standard_copyInitSum3_true-unreach-call_ground.i 41     15000 540    81    15000 1000    .061 11   .33 900   2000 13000 900   780 12000 890    220 12000   4.4  490 48    900     4800 9400    270     15000 3700    900     580 9800    2.5   88   35    1.8   120   29    900   4400 12000 900   3800 14000 900   4100 13000
array-examples/standard_copyInitSum_true-unreach-call_ground.i 40     15000 520    78    15000 1000    .058 8.5 .32 900   3700 12000 900   780 13000 890    180 8100   4.3  470 55    900     5800 11000    270     15000 4100    900     500 8300    2.0   81   24    1.5   130   19    900   3300 11000 900   2600 13000 900   3100 12000
array-examples/standard_copyInit_true-unreach-call_ground.i 41     15000 510    74    15000 970    .052 8.4 .39 900   1800 12000 900   750 11000 890    220 11000   4.1  450 56    900     5900 11000    260     15000 3200    900     550 9800    1.7   78   22    1.1   79   14    900   2900 13000 900   2700 14000 900   2300 12000
array-examples/standard_find_true-unreach-call_ground.i 900     12000 9400    130    15000 1600    .046 11   .54 900   1900 12000 900   2400 12000 900    2200 11000   15    900 220    900     9400 10000    260     15000 3700    900     600 10000    2.4   81   27    900     88   10000    900   2900 13000 900   3800 11000 900   2100 11000
array-examples/standard_init1_true-unreach-call_ground.i 900     9800 9600    130    15000 1600    .053 11   .42 900   2100 13000 900   820 11000 900    730 11000   3.9  420 47    900     5800 13000    270     15000 3400    900     520 9700    1.5   74   19    .84  67   13    900   3400 12000 900   3400 13000 900   1700 13000
array-examples/standard_init2_true-unreach-call_ground.i 43     15000 570    67    15000 760    .058 8.2 .32 900   2200 12000 900   690 10000 900    730 11000   4.1  440 51    900     5800 11000    270     15000 3800    900     560 9700    1.6   86   22    1.0   77   12    900   2400 13000 900   4000 13000 900   2000 12000
array-examples/standard_init3_true-unreach-call_ground.i 42     15000 630    70    15000 970    .10  11   .34 900   1900 13000 900   710 11000 900    790 11000   4.1  470 50    900     5800 12000    260     15000 3900    900     620 8900    1.7   78   22    1.2   93   17    900   2800 11000 900   3100 13000 900   2700 13000
array-examples/standard_init4_true-unreach-call_ground.i 42     15000 550    73    15000 950    .067 8.4 .36 900   2000 12000 900   900 12000 900    740 12000   4.3  490 50    900     5800 11000    260     15000 3300    900     410 1900    1.8   75   21    1.4   110   17    900   3700 13000 900   4900 15000 900   3600 14000
array-examples/standard_init5_true-unreach-call_ground.i 42     15000 540    76    15000 1100    .073 13   .43 900   2100 13000 900   720 13000 890    210 9600   4.4  510 51    900     5700 12000    260     15000 3400    900     790 11000    1.9   78   23    1.6   130   20    900   4100 14000 900   3400 14000 900   3800 11000
array-examples/standard_init6_true-unreach-call_ground.i 42     15000 580    79    15000 990    .049 8.2 .39 900   2100 12000 900   770 13000 890    240 12000   4.5  540 52    900     5800 11000    260     15000 3300    900     790 8400    1.9   83   23    1.8   140   34    900   5000 13000 900   3200 12000 900   5100 12000
array-examples/standard_init7_true-unreach-call_ground.i 42     15000 480    55    15000 720    .054 11   .42 900   2000 13000 900   730 13000 890    270 9200   4.7  560 57    900     5700 11000    260     15000 3900    900     750 12000    2.0   84   24    2.1   160   28    900   5000 13000 900   3700 14000 900   5200 13000
array-examples/standard_init8_true-unreach-call_ground.i 42     15000 620    57    15000 710    .058 13   .52 900   2300 13000 900   740 12000 890    290 12000   4.7  580 70    900     5800 13000    270     15000 3400    900     770 10000    2.0   86   24    2.2   180   33    900   5300 13000 900   3300 13000 900   5300 14000
array-examples/standard_init9_true-unreach-call_ground.i 43     15000 510    59    15000 750    .087 11   .41 900   3600 11000 900   740 11000 900    320 9700   4.9  610 54    900     5800 12000    270     15000 3400    900     480 2300    2.1   81   27    2.5   200   37    900   5100 14000 900   3700 13000 900   5300 14000
array-examples/standard_maxInArray_true-unreach-call_ground.i 400     15000 4600    850    1300 4500    .078 13   .39 900   2700 13000 900   2200 11000 120    150 1600   900    310 10000    900     530 10000    290     15000 3400    900     5000 1800    1.9   73   24    .47  98   5.8  900   2400 13000 900   3200 14000 900   2000 14000
array-examples/standard_minInArray_true-unreach-call_ground.i 330     15000 3200    850    1200 3900    .067 11   .36 900   2500 12000 900   2200 14000 100    120 1500   900    350 11000    900     540 11000    290     15000 3500    720     15000 10000    1.9   73   24    .52  100   6.9  900   2200 12000 900   3800 13000 900   1900 13000
array-examples/standard_palindrome_true-unreach-call_ground.i 900     13000 10000    130    15000 1800    .059 13   .36 900   2100 13000 900   2200 11000 890    160 9200   4.0  420 49    900     4400 11000    330     15000 3900    900     510 8600    1.4   81   18    .67  57   9.9  900   2600 13000 900   3000 12000 900   2000 12000
array-examples/standard_partial_init_true-unreach-call_ground.i 40     15000 520    91    13000 1100    .074 11   .40 900   2500 15000 900   1400 13000 900    1400 11000   900    2300 6600    900     1100 9600    330     15000 3800    900     330 2600    120     100   1700    900     3900   8400    900   2700 14000 900   4400 14000 900   2200 12000
array-examples/standard_partition_original_true-unreach-call_ground.i 37     15000 480    77    14000 940    .092 8.2 .31 900   2600 12000 900   2200 11000 900    2300 12000   900    2200 9600    500     15000 6500    200     15000 2600    900     600 12000    64     95   820    16     15000   170    900   2300 12000 900   4100 13000 900   2200 11000
array-examples/standard_partition_true-unreach-call_ground.i 40     15000 520    68    14000 860    .098 11   .31 900   2500 14000 900   2200 11000 890    250 9200   900    1700 9200    900     1100 9900    330     15000 4000    900     760 8500    21     86   330    900     12000   10000    900   3100 14000 900   2500 13000 900   2800 14000
array-examples/standard_password_true-unreach-call_ground.i 190     15000 2300    850    1400 4100    .071 11   .39 900   2400 14000 900   2200 9900 110    170 1400   13    1200 160    900     540 9300    290     15000 3400    900     10000 1700    1.7   82   20    94     170   610    900   2700 13000 900   2100 13000 900   2300 12000
array-examples/standard_reverse_true-unreach-call_ground.i 900     14000 12000    130    15000 1800    .053 13   .44 900   2200 11000 900   2200 11000 890    180 9300   440    680 5700    900     4600 13000    320     15000 4100    900     700 10000    1.7   80   25    1.2   100   15    900   2600 14000 900   3600 13000 900   2000 12000
array-examples/standard_running_true-unreach-call.i 42     15000 500    94    15000 1300    .077 11   .39 900   2600 12000 900   2200 12000 890    260 9400   900    1200 9700    460     15000 6200    190     15000 2600    900     730 10000    1.7   71   25    1.3   220   17    900   3100 13000 900   2800 13000 900   3100 12000
array-examples/standard_sentinel_true-unreach-call_true-termination.i 320     15000 3600    850    3900 11000    .066 11   .41 900   3800 12000 900   2400 13000 100    75 1300   14    140 190    900     2400 12000    900     4100 10000    900     6200 10000    1.6   86   20    900     460   9200    8.3 420 64 6.6 320 56 9.6 480 71
array-examples/standard_seq_init_true-unreach-call_ground.i 900     13000 11000    130    15000 1700    .091 8.1 .23 900   3700 14000 900   800 12000 900    740 12000   3.9  420 46    900     4300 15000    310     15000 3900    900     560 9700    1.7   79   22    .93  61   13    900   2100 14000 900   2400 11000 900   1800 14000
array-examples/standard_strcmp_true-unreach-call_ground.i 84     10000 830    850    3300 4200    .058 11   .47 900   3700 12000 900   3500 11000 120    130 1400   5.6  550 70    710     15000 11000    400     15000 6000    900     7400 13000    1.7   74   20    900     670   8700    900   5300 11000 900   5200 12000 900   4300 12000
array-examples/standard_strcpy_original_true-unreach-call.i 40     15000 480    79    15000 1200    .027 7.9 .12 900   2000 12000 900   2400 9900 900    2200 12000   890    1200 12000    900     9700 10000    260     15000 3400    900     450 8600    6.1   97   77    900     89   11000    900   2800 12000 900   4700 13000 900   1900 12000
array-examples/standard_strcpy_true-unreach-call_ground.i 40     15000 530    79    15000 960    .043 7.7 .11 900   2000 12000 900   2200 12000 890    300 9900   900    1200 13000    900     9600 9600    260     15000 3800    900     490 13000    4.2   90   64    900     88   12000    900   2700 13000 900   3200 15000 900   2000 14000
array-examples/standard_two_index_01_true-unreach-call.i 900     5600 11000    160    15000 2100    .046 11   .51 900   2100 13000 900   2200 11000 890    230 12000   4.4  480 51    900     4200 11000    260     15000 3900    900     670 9600    880     900   13000    .24  18   3.2  900   1500 12000 900   2800 12000 900   1500 11000
array-examples/standard_two_index_02_true-unreach-call.i 900     14000 11000    130    15000 1600    .050 8.2 .38 900   2300 12000 900   2200 12000 890    210 8800   4.4  490 61    900     1000 2300    260     15000 3400    900     830 11000    1.5   79   19    .74  58   8.6  900   1500 11000 900   4200 12000 900   1500 13000
array-examples/standard_two_index_03_true-unreach-call.i 900     5700 9800    160    15000 2000    .052 8.2 .28 330   2700 4700 360   3300 4100 890    220 9700   4.4  490 58    490     15000 6500    260     15000 3900    900     700 10000    900     4100   12000    .20  12   2.2  900   1600 12000 900   2700 12000 900   1500 13000
array-examples/standard_two_index_04_true-unreach-call.i 900     14000 12000    130    15000 1700    .050 11   .42 900   2200 13000 900   2200 14000 890    170 9900   4.4  490 61    900     4200 11000    260     15000 3600    900     710 9200    1.4   95   17    .47  35   6.4  900   1500 13000 900   3800 13000 900   1600 11000
array-examples/standard_two_index_05_true-unreach-call.i 900     14000 9700    130    15000 1800    .070 11   .40 900   2500 11000 900   2400 13000 890    180 8800   4.5  490 54    900     4200 12000    260     15000 4100    900     610 7900    1.4   83   16    .36  30   4.6  900   1600 12000 900   3300 14000 900   1500 11000
array-examples/standard_two_index_06_true-unreach-call.i 900     5600 8800    100    8800 1500    .070 8.2 .27 96   3900 1100 98   4000 1200 900    170 9200   4.4  490 53    480     15000 6200    130     7600 1400    900     690 8700    890     1000   11000    .18  11   1.7  900   1400 12000 900   3800 13000 900   1500 13000
array-examples/standard_two_index_07_true-unreach-call.i 900     14000 10000    130    15000 1600    .051 11   .33 900   2000 11000 900   2200 14000 900    190 8700   4.5  490 52    900     4200 15000    260     15000 3400    900     610 9600    1.4   76   17    .30  26   3.6  900   1500 12000 900   4300 13000 900   1500 12000
array-examples/standard_two_index_08_true-unreach-call.i 900     14000 12000    130    15000 1600    .071 8.3 .34 900   2300 12000 900   2200 11000 890    180 9800   4.5  490 58    900     4200 11000    260     15000 3500    900     690 13000    1.4   80   16    .34  24   3.7  900   1500 12000 900   3900 12000 900   1600 12000
array-examples/standard_two_index_09_true-unreach-call.i 900     14000 12000    130    15000 1600    .057 11   .36 900   2100 12000 900   2100 11000 890    170 9900   4.4  490 53    900     4200 12000    260     15000 3200    900     640 8500    1.3   75   18    .30  23   4.1  900   1500 14000 900   3100 14000 900   1500 12000
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i 260     15000 2900    850    7700 5000    .038 11   .79 900   3000 12000 900   2500 12000 97    100 1400   14    850 180    860     15000 12000    900     7700 2600    350     15000 5100    880     480   12000    900     560   12000    900   2900 13000 900   850 13000 900   2900 14000
array-examples/standard_vector_difference_true-unreach-call_ground.i 40     15000 520    140    15000 2100    .065 11   .30 900   2100 12000 900   2200 12000 900    2200 12000   3.9  420 46    900     4400 11000    300     15000 3900    900     500 10000    2.1   76   22    1.7   200   26    900   4400 12000 900   4400 12000 900   1600 14000
array-industry-pattern/array_assert_loop_dep_false-unreach-call.i 41     15000 550    66    15000 970    .052 8.2 .34 900   1800 12000 900   860 14000 890    320 8900   520    830 7200    900     6000 11000    260     15000 3300    900     700 2100    1.8   81   21    1.3   280   18    900   1800 11000 900   3300 13000 900   1600 14000
array-industry-pattern/array_of_struct_loop_dep_false-unreach-call.i 41     15000 470    550    15000 8000    .11  8.2 .29 900   3800 7300 900   4200 11000 890    310 8300   61    4900 450    900     5300 11000    240     15000 3500    900     1400 8500    1.8   80   22    1.4   280   20    900   5200 9000 900   5200 10000 900   5000 8900
array-industry-pattern/array_ptr_single_elem_init_false-unreach-call.i 32     15000 380    75    15000 1200    .051 11   .53 900   2600 13000 900   2200 9900 890    230 9600   14    1100 160    900     1500 11000    340     15000 4500    900     550 10000    2.5   88   27    900     130   11000    900   3100 11000 900   3700 13000 900   3400 14000
array-industry-pattern/array_range_init_false-unreach-call.i 900     12000 9100    850    14000 11000    .050 11   .44 900   2200 11000 900   750 12000 900    190 8500   670    790 7000    900     3700 12000    390     15000 5100    900     490 9600    1.8   87   25    1.6   330   20    900   4900 8500 900   4900 9700 900   4900 9600
array-industry-pattern/array_single_elem_init_false-unreach-call.i 32     15000 460    75    15000 1000    .087 11   .47 900   2400 14000 900   2300 13000 890    250 11000   14    1100 150    900     1500 10000    340     15000 4200    900     540 13000    2.5   94   30    900     4200   11000    900   3200 12000 900   5200 15000 900   3400 11000
array-industry-pattern/check_removal_from_set_after_insertion_false-unreach-call.i 39     15000 510    23    12000 290    .061 11   .55 960   4200 10000 900   5900 9800 900    6000 8700   900    4200 12000    900     230 12000    900     1100 12000    900     940 7600    4.9   110   64    900     1300   9000    900   4000 13000 900   5300 13000 900   4800 12000
array-industry-pattern/array_monotonic_true-unreach-call.i 39     15000 520    110    15000 1700    .052 8.2 .41 900   2400 13000 900   1800 11000 890    340 12000   900    730 9400    900     1000 9300    330     15000 4000    900     600 9200    1.6   75   17    9.6   15000   120    900   1700 12000 900   2700 13000 900   1700 14000
array-industry-pattern/array_mul_init_true-unreach-call.i 38     15000 530    130    15000 1600    .064 11   .50 900   2200 12000 900   810 10000 890    1700 10000   900    1300 10000    900     3900 13000    270     15000 3400    900     730 8600    880     170   13000    15     15000   190    900   2400 14000 900   3600 15000 900   3500 9800
array-industry-pattern/array_of_struct_break_true-unreach-call.i 900     10000 11000    290    15000 3400    .046 8.3 .42 900   4300 6300 900   3000 8300 890    210 9400   70    5200 580    880     15000 12000    490     15000 6200    900     740 9600    1.7   80   19    .81  60   10    900   4900 8400 900   5200 9000 900   5300 8800
array-industry-pattern/array_of_struct_ptr_cond_init_true-unreach-call.i 900     9200 12000    230    4200 3000    .080 11   .46 900   3500 5300 900   3700 8200 900    3800 10000   320    15000 2600    900     5200 9900    900     14000 8100    .32  23 .64 4.2   88   49    900     210   9300    900   5400 8800 900   5500 8600 900   5400 7600
array-industry-pattern/array_of_struct_ptr_flag_init_true-unreach-call.i 900     13000 10000    180    15000 2700    .062 11   .43 900   5400 6400 900   4700 8400 530    670 4900   130    12000 930    900     3900 8000    900     12000 11000    810     15000 9400    1.8   77   22    1.0   74   14    900   4200 13000 900   3800 13000 900   3100 12000
array-industry-pattern/array_of_struct_ptr_monotonic_true-unreach-call.i 900     9200 11000    230    4200 2900    .073 11   .38 900   3900 5200 900   4100 7900 900    4100 8200   330    15000 2900    900     2100 9700    350     15000 4400    .32  23 .81 1.8   78   23    900     4100   9600    900   5500 8000 900   5400 7100 900   5400 7600
array-industry-pattern/array_of_struct_ptr_mul_init_true-unreach-call.i 42     15000 510    850    10000 12000    .076 9.9 .31 900   4600 7100 900   4000 7800 890    240 9300   350    15000 2300    900     2400 11000    350     15000 5000    900     840 8900    880     680   9800    900     7200   12000    900   5200 8400 900   5200 8000 900   5200 7300
array-industry-pattern/array_of_struct_single_elem_init_true-unreach-call.i 37     15000 520    150    15000 1800    .076 11   .38 900   6300 7200 900   4800 8300 890    360 8600   70    4700 480    900     1400 11000    900     6000 11000    900     900 8500    7.4   94   91    3.0   180   41    8.0 310 60 8.0 300 66 8.2 310 60
array-industry-pattern/array_ptr_partial_init_true-unreach-call.i 43     15000 510    830    15000 12000    .077 11   .38 900   4100 6700 900   3700 8900 890    400 7900   170    14000 1000    900     6300 11000    240     15000 3400    900     1000 10000    1.6   85   19    .97  67   12    900   5500 7000 900   5500 8300 900   5500 9500
array-industry-pattern/array_ptr_single_elem_init_true-unreach-call.i 900     9200 11000    120    4600 1400    .080 8.4 .49 900   5100 5000 900   4400 7800 890    370 8700   480    15000 4300    900     2400 9000    320     15000 2400    900     1400 8800    14     100   200    900     4300   8500    900   5400 8600 900   5500 9800 900   5400 7800
array-industry-pattern/array_shadowinit_true-unreach-call.i 900     14000 5900    850    5500 6200    .070 13   .39 340   5000 2700 900   3800 9200 900    3600 8100   890    1300 12000    900     430 11000    900     610 9700    900     880 9200    880     390   13000    .17  10   1.8  900   1700 14000 900   920 12000 900   1600 13000
reducercommutativity/rangesum05_false-unreach-call.i 13     110 150    .25 21 3.4  .052 8.3 .32 47   1200 340 35   560 460 490    180 5700   .20 24 2.4  .24  37 2.9  .25  38 3.2  2.0   120 23    1.6   75   22    .15  11   1.8  18   490 200 9.4 490 74 19   570 190
reducercommutativity/rangesum10_false-unreach-call.i 13     140 150    .39 20 4.2  .049 11   .50 120   1800 930 110   730 1500 500    180 5800   .24 23 3.3  .29  38 3.3  .32  40 4.0  12     250 150    1.7   73   20    .18  11   1.6  32   550 440 13   490 110 30   530 290
reducercommutativity/rangesum20_false-unreach-call.i 21     220 210    1.1  24 13    .057 11   .33 290   2000 3100 900   5300 8800 650    180 9000   .43 24 4.8  1.0   40 13    3.9   46 20    120     600 1200    1.9   75   24    .23  22   3.1  74   840 730 26   670 240 46   610 530
reducercommutativity/rangesum40_false-unreach-call.i 56     450 510    1.1  27 14    .059 13   .37 950   8100 11000 900   4000 8400 890    180 11000   6.1  36 78    2.7   45 30    2.7   57 36    900     1100 9000    2.3   94   29    .27  25   2.7  150   2700 1600 900   1500 9100 60   1500 660
reducercommutativity/rangesum60_false-unreach-call.i 320     1300 2600    7.4  50 84    .056 13   .62 940   8000 10000 900   4000 11000 900    180 9100   .96 32 13    2.6   48 30    2.8   67 32    900     820 2200    2.8   120   35    .30  29   3.1  270   4400 3100 900   2400 8700 64   2300 640
reducercommutativity/rangesum_false-unreach-call.i 39     400 290    .52 40 6.5  .075 10   .35 260   4600 2200 170   2200 1800 490    180 6000   890    2800 9200    .65  92 6.9  3.4   120 6.8  1.5   160 16    2.0   79   30    900     210   7300    14   530 100 900   1200 11000 20   680 190
reducercommutativity/avg05_true-unreach-call.i 900     1600 9100    36    40 430    .028 7.9 .13 910   3200 5500 900   1700 10000 900    2200 9100   150    90 1800    160     15000 2100    .091 23 .85 1.9   95 21    1.3   68   17    .15  9.3 1.8  210   1200 2600 900   5600 6300 900   1100 13000
reducercommutativity/avg10_true-unreach-call.i 900     2100 9300    540    170 7800    .029 7.9 .11 910   4000 7300 900   3300 8900 900    3600 8800   900    270 11000    220     15000 3300    .11  23 1.1  16     190 180    1.3   67   18    .17  9.5 1.8  390   1600 4500 900   1300 11000 900   4400 11000
reducercommutativity/avg20_true-unreach-call.i 900     3600 8500    850    280 10000    .035 8.0 .13 270   2300 2700 900   4400 9300 900    700 7800   900    330 11000    280     15000 3800    .13  23 1.6  900     490 2400    1.5   84   18    .17  9.5 1.6  900   3700 11000 900   1900 13000 900   4700 13000
reducercommutativity/avg40_true-unreach-call.i 900     2200 10000    850    290 9600    .032 7.7 .12 130   1900 1200 910   5900 9200 890    270 7800   900    390 12000    340     15000 3800    .21  30 2.5  900     660 8500    1.9   130   20    .17  9.3 1.7  170   4600 2000 900   4000 11000 230   4600 2400
reducercommutativity/avg60_true-unreach-call.i 900     1500 7000    850    340 11000    .021 7.7 .15 960   3300 8400 900   4700 12000 890    270 7900   900    470 11000    410     15000 5300    .35  41 4.4  900     660 11000    2.8   200   35    .19  9.5 1.7  280   4900 3700 750   4700 10000 440   5300 5700
reducercommutativity/avg_true-unreach-call.i 900     3300 7000    850    220 11000    .11  8.1 1.3  95   2500 760 900   4400 7200 890    180 11000   900    410 11000    900     170 13000    900     230 11000    900     300 9500    880     140   12000    .16  9.9 1.7  900   770 13000 900   580 12000 900   780 13000
reducercommutativity/max05_true-unreach-call_true-termination.i 8.3   84 96    1.9  23 20    .026 7.8 .13 82   1500 800 910   1500 11000 900    1600 9500   6.5  26 12    900     1000 12000    4.8   25 66    5.4   34 72    1.3   66   16    1.6   12   18    900   1200 11000 900   2200 14000 900   1400 12000
reducercommutativity/max10_true-unreach-call_true-termination.i 160     1100 2200    89    56 1100    .034 7.7 .15 56   1100 460 900   2600 8100 900    2500 9500   44    58 520    900     120 10000    330     58 4300    240     90 3000    1.6   80   21    52     34   530    900   2200 11000 900   3300 11000 900   2400 11000
reducercommutativity/max20_true-unreach-call.i 900     4200 8600    850    180 13000    .018 7.9 .14 900   3000 7300 900   2800 8300 890    190 12000   850    130 12000    900     140 12000    900     150 11000    900     330 13000    3.6   100   44    900     140   10000    900   5300 13000 900   4600 7100 900   4600 12000
reducercommutativity/max40_true-unreach-call.i 900     2600 6400    850    220 8700    .027 8.0 .11 910   3700 9600 900   2500 9100 890    230 9400   900    220 11000    900     170 9400    900     170 10000    900     580 8800    26     180   200    900     260   11000    900   4800 12000 900   6000 8700 900   4700 11000
reducercommutativity/max60_true-unreach-call.i 900     1800 6100    850    260 8500    .022 7.8 .12 910   2200 9900 900   4000 9600 890    250 8200   900    280 12000    900     200 10000    900     180 9100    900     630 11000    180     320   1100    900     300   11000    900   5000 12000 900   6100 10000 900   5100 13000
reducercommutativity/max_true-unreach-call.i 900     1700 4400    850    230 10000    .11  7.9 1.1  41   1400 270 120   2200 1300 890    260 11000   900    450 12000    900     120 13000    900     140 13000    900     110 1800    880     390   9200    .18  10   1.8  900   2200 10000 900   1900 13000 900   1800 9900
reducercommutativity/sep05_true-unreach-call.i 5.2   73 61    .40 23 4.7  .029 7.9 .13 57   2100 440 840   1500 10000 850    1400 11000   .61 23 7.4  900     8000 13000    .55  24 6.2  .80  36 10    1.3   67   16    .18  9.4 1.6  900   4800 14000 290   1900 3900 900   4900 11000
reducercommutativity/sep10_true-unreach-call.i 10     110 110    .77 27 8.1  .021 7.8 .16 900   4800 7300 900   4800 8300 900    4800 8400   .60 23 8.1  900     1400 13000    6.6   33 90    11     100 140    2.2   74   28    .16  9.4 1.8  910   8700 9200 900   2500 12000 900   7400 9500
reducercommutativity/sep20_true-unreach-call.i 17     230 200    3.5  36 40    .026 7.9 .13 910   5000 7900 900   3700 8800 890    190 12000   .65 23 7.0  900     64 10000    900     67 13000    900     370 13000    880     100   12000    .16  9.4 1.7  910   13000 7000 910   13000 7700 900   4700 9800
reducercommutativity/sep40_true-unreach-call.i 470     1700 5000    34    93 430    .021 7.8 .17 220   3000 2000 900   3900 8600 900    190 10000   .69 29 9.3  900     92 10000    900     110 10000    900     520 2600    880     160   11000    .18  9.2 2.2  900   9500 11000 900   13000 8000 900   4800 11000
reducercommutativity/sep60_true-unreach-call.i 900     2900 7100    160    160 1900    .032 7.7 .12 910   3500 8600 900   4300 9100 900    190 11000   .74 35 8.8  900     130 9400    900     150 11000    900     880 11000    880     250   8800    .19  9.4 1.9  900   6000 13000 900   12000 9600 900   5300 13000
reducercommutativity/sep_true-unreach-call.i 900     9400 3600    640    13000 4600    .14  8.0 1.1  960   5300 9700 900   2700 9600 890    190 8400   900    450 10000    900     170 10000    900     250 11000    900     390 12000    880     180   11000    .16  10   2.0  900   5100 11000 900   1700 11000 900   7900 8500
reducercommutativity/sum05_true-unreach-call_true-termination.i 20     220 230    4.2  25 51    .020 7.9 .14 16   610 120 900   3800 13000 900    3900 11000   .16 23 2.0  180     15000 2700    .12  23 .94 1.4   31 2.7  1.3   70   18    .17  9.3 1.6  26   850 230 24   720 240 900   1100 11000
reducercommutativity/sum10_true-unreach-call.i 900     2300 9800    180    110 2300    .017 7.9 .18 910   3100 8300 900   2000 10000 900    2400 11000   .20 23 1.9  900     13000 2300    .40  23 .94 4.0   74 51    1.3   70   23    .28  19   2.3  77   1400 750 88   1200 950 900   5100 13000
reducercommutativity/sum20_true-unreach-call.i 900     3600 10000    850    260 11000    .026 7.8 .15 910   2900 9300 910   6600 8600 900    240 7900   .19 23 2.8  280     15000 3600    .16  23 1.6  240     310 2200    1.4   82   16    .18  9.4 1.9  900   4800 6600 790   2600 9800 900   5000 6800
reducercommutativity/sum40_true-unreach-call.i 900     1600 7300    850    280 10000    .048 7.8 .13 960   7600 9600 910   7400 11000 890    270 7500   .23 23 3.0  340     15000 4300    .22  30 2.6  900     490 8100    1.8   120   23    .17  9.3 2.0  900   4600 12000 900   4700 11000 900   4700 12000
reducercommutativity/sum60_true-unreach-call.i 900     2000 7600    850    260 11000    .023 7.9 .14 910   2900 8600 910   6500 10000 890    200 8700   .28 24 3.1  410     15000 4700    .35  41 3.4  900     500 6800    2.8   200   33    .27  17   1.7  900   6400 8200 900   4900 13000 900   6300 11000
reducercommutativity/sum_true-unreach-call.i 900     2000 4800    850    250 11000    .14  7.9 1.2  47   1500 300 900   4300 9100 890    240 10000   900    530 12000    900     190 11000    900     190 12000    900     200 11000    880     390   11000    .17  10   2.1  900   4700 6300 900   990 11000 900   4700 9700
bitvector/byte_add_false-unreach-call_true-no-overflow.i .33  27 4.2  .28 18 3.0  1.1   41   9.2  8.6 480 53 76   1700 1000 2.2  110 28   51    2200 620    .14  24 1.5  .14  24 1.9  .15  24 1.7  4.7   130   59    .20  11   2.3  55   750 540 29   480 270 92   940 1000
bitvector/sum02_false-unreach-call_true-no-overflow.i 900     1500 10000    850    7900 4000    900     13000   11000    71   2800 570 900   4000 7600 69    76 840   2.2  150 24    900     6700 1700    300     15000 3900    250     15000 3400    880     450   11000    900     800   10000    900   340 11000 900   660 13000 180   370 2200
bitvector/byte_add_1_true-unreach-call_true-no-overflow.i .40  28 5.8  .35 18 3.9  1.7   9.0 21    14   590 87 70   1700 770 74    1800 870   41    2200 540    750     15000 8200    .32  24 4.1  .43  28 5.2  12     150   130    .22  10   2.2  900   4100 11000 900   3500 12000 900   1200 11000
bitvector/byte_add_2_true-unreach-call_true-no-overflow.i .42  28 4.5  .36 18 3.9  2.0   9.7 28    15   640 110 25   920 260 28    840 300   42    2200 530    750     15000 9400    .33  24 4.4  .47  28 6.0  15     150   180    .31  18   2.5  580   1400 6800 900   4500 11000 900   1200 13000
bitvector/gcd_1_true-unreach-call_true-no-overflow.i .29  25 3.4  .32 21 3.7  29     490   380    9.5 330 80 6.5 280 87 490    280 6000   120    1200 1200    900     6900 2100    .47  26 5.7  .46  26 5.7  1.7   77   20    .21  11   2.1  900   530 11000 110   480 950 900   460 12000
bitvector/gcd_2_true-unreach-call_true-no-overflow.i .69  32 9.9  1.2  31 17    .59  47   12    240   660 1500 7.1 280 77 240    290 2400   360    1300 3800    900     310 10000    180     150 2000    190     200 2100    860     300   13000    2.0   14   25    900   730 11000 900   720 11000 900   560 11000
bitvector/gcd_3_true-unreach-call_true-no-overflow.i .64  32 8.9  1.2  31 13    .68  11   7.5  220   630 1500 150   310 2000 460    320 5000   230    1400 2500    900     250 11000    900     150 2300    250     200 3100    880     190   11000    2.1   14   27    900   560 11000 900   640 11000 900   610 11000
bitvector/gcd_4_true-unreach-call_true-no-overflow.i .81  33 10    .30 17 3.1  1.7   22   23    2.9 270 25 2.3 240 20 490    260 6400   .16 23 1.4  900     9900 13000    .079 23 .99 .16  30 1.6  1.5   70   18    .13  9.4 1.9  900   670 11000 13   480 110 900   1100 11000
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i .58  44 7.3  .56 17 6.9  .26  8.3 2.9  9.4 450 79 6.9 400 58 17    410 210   .16 23 2.0  92     15000 1400    .15  23 1.3  .69  74 8.7  1.3   68   18    .18  10   2.0  120   1700 1200 91   1800 1100 340   1600 3400
bitvector/jain_1_true-unreach-call_true-no-overflow.i 900     1400 11000    94    14000 1200    .23  7.8 2.2  4.3 310 29 2.8 270 28 300    290 3400   5.3  510 70    230     15000 2300    180     15000 1500    280     15000 3300    890     240   11000    900     75   9100    6.7 340 55 900   890 9500 6.2 340 48
bitvector/jain_2_true-unreach-call_true-no-overflow.i 900     1500 9900    58    14000 790    .23  7.7 2.4  4.3 300 31 2.7 260 26 900    290 7700   6.8  730 91    170     15000 1300    150     15000 1700    900     4600 7100    890     250   8500    900     93   8300    7.2 340 56 900   850 11000 6.7 350 51
bitvector/jain_4_true-unreach-call_true-no-overflow.i 900     2000 10000    69    14000 730    .24  43   3.1  5.0 320 32 2.8 270 25 890    240 7000   8.6  890 110    270     15000 2100    260     15000 2000    900     3100 7600    880     260   9300    900     15000   12000    5.7 330 49 6.4 320 46 6.2 320 43
bitvector/jain_5_true-unreach-call_true-no-overflow.i 900     1500 9900    250    15000 3600    .21  7.7 2.4  910   7500 8500 900   7200 8900 59    75 680   .25 40 3.3  900     12000 13000    340     15000 4900    140     15000 1400    880     200   8900    890     15000   13000    900   2200 13000 900   800 14000 7.2 360 59
bitvector/jain_6_true-unreach-call_true-no-overflow.i 900     1900 12000    150    14000 1600    .24  7.7 2.6  4.6 300 36 2.9 270 24 890    270 8400   8.8  890 96    200     15000 1600    170     15000 1400    900     5700 7600    880     270   7900    890     15000   12000    5.9 330 48 9.7 330 96 6.3 330 51
bitvector/jain_7_true-unreach-call_true-no-overflow.i 900     1700 9600    110    14000 1300    .24  7.5 3.1  8.8 400 73 4.4 270 48 900    290 6700   8.2  760 88    230     15000 2500    580     15000 1400    900     7500 8300    890     290   8700    890     15000   12000    5.9 320 50 900   770 10000 6.6 340 56
bitvector/modulus_true-unreach-call_true-no-overflow.i .77  36 11    380    1100 2100    1.8   49   20    21   1500 160 230   1700 3100 890    380 7500   900    5600 8700    900     1000 7900    900     1400 6300    .43  25 5.4  340     260   2200    270     56   3400    29   330 420 900   830 8600 9.7 330 99
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i .17  24 1.3  .40 17 5.9  .26  7.7 2.7  2.9 270 25 2.3 240 20 7.0  260 77   .16 23 1.8  900     1700 14000    .10  23 1.1  .14  23 1.7  1.2   68   16    .15  9.4 1.4  270   2300 3800 300   2600 3800 110   2400 1300
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i .15  24 1.4  .47 17 3.9  .28  7.5 3.6  5.7 340 39 17   540 160 22    600 230   .18 23 2.0  530     15000 6700    .17  23 1.4  .21  23 2.1  1.3   65   16    .15  9.8 1.7  900   880 11000 900   840 12000 900   740 12000
bitvector/parity_true-unreach-call_true-no-overflow.i 2.5   33 30    2.5  22 32    .68  7.8 6.9  25   650 210 120   730 1600 890    150 10000   2.3  160 25    900     280 11000    900     340 12000    900     200 2600    880     280   12000    1.4   11   20    900   1000 11000 900   1400 12000 900   940 13000
bitvector/sum02_true-unreach-call_true-no-overflow.i 900     1500 11000    850    7300 3500    900     5200   11000    140   3800 1200 900   6300 9800 170    490 1800   2.6  150 34    690     15000 7600    390     15000 5300    290     15000 2600    880     330   11000    900     800   12000    900   510 12000 900   800 8900 37   370 450
bitvector/s3_clnt_1_false-unreach-call_true-no-overflow.BV.c.cil.c 26     240 220    4.3  220 58    .028 8.1 .26 47   1700 290 8.3 440 62 33    100 470   310    15000 3900    3.0   110 35    5.0   240 80    8.5   410 120    16     220   170    .37  11   4.6  24   570 200 900   4900 15000 24   580 170
bitvector/s3_clnt_2_false-unreach-call_true-no-overflow.BV.c.cil.c 16     240 150    3.7  180 47    .064 8.1 .17 70   3000 490 11   510 100 56    110 830   890    15000 12000    5.8   150 68    9.8   390 110    16     680 240    38     240   420    .48  12   5.7  28   720 220 900   4200 13000 28   630 210
bitvector/s3_clnt_3_false-unreach-call_true-no-overflow.BV.c.cil.c 21     170 190    .91 75 12    .040 8.1 .22 25   920 160 6.7 330 53 18    85 210   890    15000 8200    5.7   66 14    2.2   120 33    3.5   190 47    9.1   190   100    .29  11   2.8  22   560 170 87   860 960 22   560 160
bitvector/s3_clnt_1_true-unreach-call_true-no-overflow.BV.c.cil.c 900     760 9000    16    360 170    4.0   8.7 37    57   1800 350 21   1600 220 170    1300 2100   330    15000 3600    900     5500 8500    34     1200 470    59     1900 780    150     380   1400    .62  20   7.2  35   840 280 900   4700 14000 36   850 280
bitvector/s3_clnt_2_true-unreach-call_true-no-overflow.BV.c.cil.c 17     280 160    14    290 160    3.7   8.2 43    36   1300 240 19   1500 210 140    1600 1800   900    15000 7100    900     5300 13000    28     1000 300    43     1600 590    120     340   1000    .52  11   6.3  42   1100 360 900   4400 12000 42   1000 320
bitvector/s3_clnt_3_true-unreach-call_true-no-overflow.BV.c.cil.c 21     250 170    14    270 150    3.7   8.2 41    28   970 180 22   2100 210 140    2200 1800   900    15000 7500    900     4800 9800    29     1000 360    45     1600 490    130     360   1200    .52  12   6.7  25   1100 190 900   1700 12000 130   4800 1500
bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c 900     1400 7600    850    430 11000    3.3   8.3 37    900   3600 4600 910   4200 11000 890    390 9900   900    2800 8500    900     400 11000    900     1000 11000    900     1800 10000    880     580   6900    900     370   9700    900   2400 13000 900   4500 14000 900   2700 12000
bitvector/s3_srvr_1_true-unreach-call_true-no-overflow.BV.c.cil.c 900     8700 9900    850    910 3600    3.3   8.3 35    130   3800 1100 27   2300 270 46    2300 520   410    15000 4400    900     4000 9800    900     11000 11000    900     15000 10000    880     630   6100    900     580   10000    47   1900 460 900   1300 13000 900   4500 12000
bitvector/s3_srvr_2_alt_true-unreach-call_true-no-overflow.BV.c.cil.c 900     7400 11000    850    790 4600    3.3   8.3 37    39   1300 250 94   2300 1200 890    370 11000   420    15000 4500    900     2400 11000    900     6500 11000    900     9700 11000    880     540   6400    900     190   12000    39   1500 340 900   1300 12000 900   4700 12000
bitvector/s3_srvr_2_true-unreach-call_true-no-overflow.BV.c.cil.c 900     7600 9200    850    820 3600    3.2   8.3 40    160   4400 1400 93   2300 1100 890    380 11000   450    15000 4800    900     2600 9700    900     6700 10000    900     10000 12000    880     640   6800    900     160   9300    38   1600 290 900   1100 14000 900   4700 12000
bitvector/s3_srvr_3_alt_true-unreach-call_true-no-overflow.BV.c.cil.c 900     8000 9700    850    850 3400    3.4   8.2 37    190   4900 1600 25   2300 250 890    310 13000   430    15000 5100    900     3700 8800    900     9200 9600    900     12000 9900    880     710   6200    900     270   9800    36   1400 300 900   4800 13000 900   3600 12000
bitvector/s3_srvr_3_true-unreach-call_true-no-overflow.BV.c.cil.c 900     8300 11000    850    830 4000    3.1   8.3 34    910   5700 7100 26   2300 270 890    300 12000   410    15000 4300    900     3700 11000    900     3600 2000    900     12000 10000    880     720   6400    900     270   10000    36   1500 310 900   4700 13000 900   4100 12000
bitvector/soft_float_1_true-unreach-call_true-no-overflow.c.cil.c .22  38 1.7  4.2  41 47    79     120   890    87   2300 750 11   390 110 15    400 140   900    2900 12000    900     3800 11000    19     280 260    1.0   26 15    1.7   83   20    500     190   6200    160   890 1900 900   1900 11000 130   830 1700
bitvector/soft_float_2_true-unreach-call_true-no-overflow.c.cil.c .15  26 1.6  2.8  43 30    3.3   9.1 34    13   610 100 110   1300 1500 120    1200 1300   890    2900 12000    900     4200 12000    .66  51 8.8  .11  24 1.2  1.5   87   20    2.6   15   32    220   1000 2500 900   1300 12000 110   1500 1100
bitvector/soft_float_3_true-unreach-call_true-no-overflow.c.cil.c 6.7   150 80    2.8  42 41    3.0   8.6 35    36   1100 270 100   1300 1500 120    1400 1500   890    2900 11000    900     4100 11000    2.0   53 23    7.0   210 88    11     120   140    4.4   17   66    900   1600 10000 900   1300 13000 900   840 12000
bitvector/soft_float_4_true-unreach-call_true-no-overflow.c.cil.c .79  32 9.2  9.9  44 130    42     51   400    380   2500 3800 200   370 2500 230    360 2600   890    2900 13000    900     1400 12000    220     360 3200    19     38 240    16     95   200    900     150   13000    510   1000 5400 900   2200 9900 610   1900 7500
bitvector/soft_float_5_true-unreach-call_true-no-overflow.c.cil.c .13  26 1.6  2.8  52 36    2.9   8.7 29    8.4 430 59 110   1300 1200 110    1200 1500   900    2900 12000    900     3100 8700    .65  47 7.9  .13  24 .97 1.5   86   22    2.6   23   28    15   610 110 900   1400 13000 46   910 470
bitvector-regression/implicitfloatconversion_false-unreach-call.c .14  22 .78 .14 17 .86 .053 7.6 .33 3.4 290 31 2.3 250 21 .38 48 3.8 .13 23 1.3  .086 23 .76 .071 23 .79 .079 23 .65 1.5   71   16    .13  9.2 1.5  9.1 320 69 4.8 310 38 8.7 310 63
bitvector-regression/implicitunsignedconversion_false-unreach-call.c .12  24 .99 .14 17 .95 .047 7.6 .40 3.1 280 26 2.5 270 20 .37 48 3.9 .14 23 1.4  .27  23 .72 .071 23 .90 .11  23 .74 1.4   73   22    .16  9.1 1.4  5.4 320 45 5.9 330 48 6.4 350 52
bitvector-regression/integerpromotion_false-unreach-call.c .12  22 .82 .12 17 .85 .050 7.8 .40 3.1 270 27 2.5 260 21 .35 48 4.1 .13 24 1.4  .071 23 .86 .10  23 .75 .11  23 .66 1.5   69   18    .13  9.2 1.7  8.9 320 74 9.8 340 70 9.0 330 75
bitvector-regression/recHanoi03_false-unreach-call.c .12  22 .69 .97 23 11    .19  7.8 2.5  3.1 290 22 3.2 300 25 4.6  300 49   4.1  300 51    1.6   46 22    2.0   83 28    2.4   120 30    8.6   78   130    900     2800   12000    87   880 1200 110   840 1500 220   810 2600
bitvector-regression/signextension2_false-unreach-call.c .12  22 .97 .12 17 .84 .087 7.9 .87 3.3 280 28 2.5 240 25 480    70 6200   .13 23 1.5  .11  23 .62 .073 23 .66 .10  23 .71 1.5   72   19    .16  9.4 1.6  5.8 320 43 5.6 320 43 5.4 320 41
bitvector-regression/signextension_false-unreach-call.c .11  22 .75 .13 17 .97 .11  7.7 .87 3.3 270 26 2.4 250 20 .37 48 4.1 .15 23 1.4  .086 23 .91 .088 23 .83 .098 23 .83 1.5   70   18    .16  9.3 1.4  6.7 330 51 5.6 320 43 5.3 310 43
bitvector-regression/implicitunsignedconversion_true-unreach-call.c .097 22 .77 .19 17 1.6  .038 7.7 .35 2.7 270 21 2.1 220 19 3.2  260 29   .17 23 1.3  900     10000 10000    .27  23 .83 .10  23 .63 1.2   75   17    .16  9.4 1.3  5.6 330 44 6.4 330 53 5.8 330 46
bitvector-regression/integerpromotion_true-unreach-call.c .11  22 .76 .19 17 1.6  .040 7.7 .29 2.7 270 26 2.3 250 20 3.2  260 28   .15 23 1.4  50     15000 690    .075 23 .74 .11  23 .58 1.1   68   15    .13  9.3 1.3  9.0 310 75 8.9 320 70 9.7 320 83
bitvector-regression/signextension2_true-unreach-call.c .095 22 .74 .18 17 1.9  .083 7.9 .88 2.7 260 23 2.2 240 19 480    270 5800   .15 23 1.4  900     6800 14000    .10  23 .87 .072 23 .74 1.2   72   15    .16  9.2 1.4  5.7 320 49 5.6 320 44 6.0 330 46
bitvector-regression/signextension_true-unreach-call.c .11  22 .68 .19 17 2.0  .12  7.9 .77 2.8 270 23 2.2 240 19 3.1  260 29   .16 23 1.5  900     4900 12000    .072 23 .82 .11  23 .77 1.2   81   13    .13  9.3 1.6  6.1 330 43 6.6 340 49 5.6 330 44
bitvector-loops/diamond_false-unreach-call2.i .13  24 1.1  .14 18 .93 .54  7.7 5.5  6.3 370 42 3.0 260 26 1.2  78 17   16    1000 190    .085 23 .90 .11  23 .81 .086 23 .97 1.9   93   29    .16  9.3 1.6  8.1 370 61 6.4 330 50 12   450 98
bitvector-loops/overflow_false-unreach-call1.i 900     1400 11000    280    15000 3300    .067 7.8 .23 910   7100 7500 910   7800 9700 54    75 780   .15 23 1.5  900     9100 11000    310     15000 3600    200     15000 2200    880     930   12000    .13  9.3 1.7  900   1500 15000 900   980 13000 900   870 14000
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call.i .94  37 12    .40 21 3.7  .13  7.7 .97 13   500 91 210   890 2500 7.9  100 97   2.1  220 24    .16  24 1.4  .18  25 1.9  1.1   59 13    4.7   110   62    .23  12   2.8  160   740 2000 670   650 7500 190   740 2300
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c 1.3   370 13    1.0  150 13    .20  8.9 2.8  16   730 120 8.0 340 63 3.3  88 40   1.0  56 11    .52  49 6.2  .48  49 6.0  .49  50 6.1  4.3   120   66    .39  23   4.5  55   1100 440 900   2000 14000 58   1200 430
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c .35  60 3.3  .27 31 2.6  .14  8.4 1.7  36   1300 230 8.4 360 67 1.6  95 19   .44 38 5.3  .20  28 2.5  .23  28 2.5  .80  28 1.9  4.0   110   47    .28  14   3.6  31   920 260 390   2100 5500 32   910 230
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c .55  120 4.9  .49 53 4.9  .24  45   2.1  960   4600 9100 9.3 370 76 2.3  100 26   .69 48 8.5  .35  32 3.5  .31  32 3.7  .34  32 4.0  8.7   120   110    .39  20   4.8  46   1000 330 470   1700 6400 44   1000 350
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c .29  39 2.4  .20 25 2.0  .14  8.2 1.5  10   490 76 5.4 300 40 1.2  64 14   .32 27 4.2  .18  27 2.3  .20  27 1.7  .19  27 1.7  3.3   96   44    .25  13   2.6  17   530 130 36   810 330 17   530 120
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c