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 skink SMACK+Corral 1.7.2 symbiotic KLEE:7f3c74aa-dg:96e851cf-symbiotic:69a1d8e6-minisat:3db58943-stp:39fa956f-LLVMInstrumentation:f750b24a SymDIVINE 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:20 CET [[ 2017-01-15 01:36:45 CET ]] [[ 2017-01-15 01:53:26 CET ]] [[ 2017-01-15 01:38:17 CET ]] [[ 2017-01-15 01:54:04 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:13:29 CET [[ 2017-01-15 02:06:46 CET ]] [[ 2017-01-15 03:46:01 CET ]] [[ 2017-01-15 02:24:39 CET ]] [[ 2017-01-15 04:02:29 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-Loops blast.sv-comp17.ReachSafety-Loops cbmc.sv-comp17.ReachSafety-Loops ceagle.sv-comp17.ReachSafety-Loops cpa-bam-bnb.sv-comp17.ReachSafety-Loops cpa-kind.sv-comp17.ReachSafety-Loops cpa-seq.sv-comp17.ReachSafety-Loops depthk.sv-comp17.ReachSafety-Loops esbmc.sv-comp17.ReachSafety-Loops esbmc-falsi.sv-comp17.ReachSafety-Loops esbmc-incr.sv-comp17.ReachSafety-Loops esbmc-kind.sv-comp17.ReachSafety-Loops skink.sv-comp17.ReachSafety-Loops smack.sv-comp17.ReachSafety-Loops symbiotic4.sv-comp17.ReachSafety-Loops symdivine.sv-comp17.ReachSafety-Loops uautomizer.sv-comp17.ReachSafety-Loops ukojak.sv-comp17.ReachSafety-Loops utaipan.sv-comp17.ReachSafety-Loops veriabs.sv-comp17.ReachSafety-Loops
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 ]] [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/skink.2017-01-13_1109.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/skink.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/skink.2017-01-13_1109.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/skink.2017-01-13_1109.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 ]] --fix_volatile --fix_inline --silent -Os [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/symdivine.2017-01-13_1113.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/symdivine.2017-01-13_1113.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/symdivine.2017-01-13_1113.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/symdivine.2017-01-13_1113.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 status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score
loops/array_false-unreach-call_true-termination.i .13  23 1.2  1 .42  21 4.5  1 .11 17 .89 1 .11  7.9 1.1  0 3.2 300 29 1 3.9 290 31 1 2.6 250 24 1 1.1  76 14   1 .19 23 1.9 1 .099 23 1.1  1 .12  23 1.0  1 .10  23 1.1  1 6.1 340 49 1 1.6 77 19 1 .18 10   1.6 1 .074 9.8 .56 1 5.6 320 46 1 7.2 380 58 1 6.2 330 53 1 10   290 84 1
loops/bubble_sort_false-unreach-call.i .40  62 4.0  0 .059 20 .73 0 .30 26 3.1  0 .13  8.2 1.5  0 5.2 310 45 0 440   1900 5000 0 420   2500 5500 0 3.0  240 42   0 230    15000 1900   0 .64  49 6.9  1 .66  49 8.1  1 .65  50 8.5  1 38   1100 300 0 2.4 90 31 1 .25 10   2.4 1 .086 10   .55 0 8.6 320 73 0 8.4 310 67 0 9.2 320 72 0 290   2100 2300 1
loops/count_up_down_false-unreach-call_true-termination.i .13  22 .87 1 .068 20 .77 1 .12 17 .90 1 .16  7.8 1.6  1 2.9 280 26 1 6.1 410 41 1 2.4 250 23 1 .55 75 7.1 1 1.2  130 13   1 .11  23 .68 1 .072 23 .80 1 .093 23 .65 1 4.9 300 40 1 1.6 78 21 1 .16 9.5 1.6 1 .088 9.7 .40 1 5.4 320 43 1 5.5 320 47 1 6.0 340 48 1 9.5 280 76 1
loops/eureka_01_false-unreach-call.i 1.4   43 16    1 1.1   33 11    0 .39 26 3.9  1 .10  7.7 1.1  0 21   800 190 -32 520   4000 5200 0 960   2900 14000 0 2.9  190 34   0 900    7800 6800   0 .15  23 1.9  0 .17  24 1.9  0 .23  24 2.1  0 15   660 130 0 2.7 94 35 1 .44 13   5.2 0 83     580   1000    -32 60   820 730 1 140   970 1700 1 88   1000 950 1 47   1100 380 1
loops/for_bounded_loop1_false-unreach-call_true-termination.i .24  26 2.3  1 .40  24 3.7  1 .12 17 .99 1 .99  7.8 10    1 3.3 290 34 1 12   710 78 1 3.3 280 28 1 1.3  110 15   1 890    4300 9200   1 .076 23 .83 1 .11  23 .71 1 .093 23 .86 1 7.0 360 56 1 1.7 77 22 1 .18 9.2 1.6 0 .084 9.9 .91 1 6.9 340 50 1 7.3 360 54 1 8.4 380 68 1 10   280 79 1
loops/insertion_sort_false-unreach-call_true-termination.i 380     6400 2000    1 3.5   24 40    0 2.4  320 26    1 .10  8.2 1.0  0 4.1 310 34 0 55   2200 390 0 240   1500 2800 0 3.6  130 56   1 900    3000 7800   0 .66  23 7.5  1 2.9   25 5.9  1 .84  30 11    1 900   1700 8200 0 2.6 82 37 1 .18 10   1.7 0 .057 9.7 .43 0 64   1100 650 1 42   650 500 1 900   8800 6100 0 96   15000 1300 0
loops/invert_string_false-unreach-call_true-termination.i .68  36 8.4  1 .86  30 8.5  1 .51 38 4.8  1 .12  7.7 1.0  0 5.2 320 46 1 31   1700 230 1 220   1100 2700 1 1.9  130 26   1 890    1700 13000   1 .16  23 1.9  1 .18  23 2.3  1 .19  23 2.0  1 14   640 130 1 1.9 80 23 1 .19 10   1.8 0 .072 9.5 .45 0 11   480 94 1 12   500 92 1 13   490 120 1 110   15000 1200 0
loops/linear_search_false-unreach-call.i 1.1   58 11    1 .099 20 .75 0 .85 23 9.8  1 .10  44   2.8  0 3.2 290 26 0 15   580 100 1 12   560 110 1 16    76 250   0 1.3  85 17   0 .50  41 6.3  0 .84  66 11    0 2.4   120 34    0 6.1 350 50 0 11   93 150 1 .24 21   2.2 0 .052 9.8 .53 0 900   810 10000 0 900   4600 9200 0 900   2600 12000 0 9.8 280 72 0
loops/ludcmp_false-unreach-call.i 900     3500 9200    0 1.3   30 15    0 5.0  130 76    0 17     15000   210    0 11   1000 110 1 960   1900 12000 0 32   3800 310 1 7.1  350 100   0 9.7  15000 120   0 2.1   31 29    0 2.1   33 30    0 3.5   80 46    0 10   680 94 0 82   560 1100 1 .15 9.4 1.9 1 .064 9.9 .53 0 78   13000 660 0 63   12000 630 0 75   13000 680 0 270   1300 2800 1
loops/matrix_false-unreach-call_true-termination.i 64     1900 370    1 .049 11 .61 0 .15 21 1.3  1 .12  7.9 1.2  0 16   660 180 1 59   2200 450 1 100   2200 1000 1 480    180 5400   1 900    6500 7100   0 .12  23 1.3  1 .11  23 1.6  1 .15  23 1.2  1 5.9 320 47 0 1.9 81 23 1 900    2400   8800   0 .054 9.8 .50 0 7.6 370 59 1 8.2 370 70 1 7.3 360 54 1 66   15000 730 0
loops/n.c24_false-unreach-call.i 900     6800 6800    0 900     320 9800    0 190    15000 2100    0 .10  8.0 1.1  0 900   4300 9200 0 900   5000 8100 0 900   3900 7900 0 900    1400 7200   0 80    15000 760   0 340     15000 3900    0 310     15000 3600    0 900     1000 1900    0 5.1 330 41 0 880   1400 6900 0 900    3800   10000   0 7.8   360   82    0 900   4600 11000 0 900   3700 14000 0 900   4400 12000 0 850   15000 8400 0
loops/nec11_false-unreach-call_false-termination.i .11  22 .83 1 .089 22 .72 1 .13 17 .98 1 .11  7.8 1.2  0 2.9 270 29 1 3.7 290 31 1 2.4 250 22 1 .54 76 6.4 1 1.8  140 20   1 .073 23 .80 1 .10  23 .73 1 .072 23 .90 1 5.3 320 41 1 1.7 75 20 1 .16 9.3 1.7 1 .086 9.8 .47 1 5.9 330 45 1 5.5 340 45 1 6.1 340 45 1 9.5 280 71 1
loops/nec20_false-unreach-call_true-termination.i .91  56 8.2  1 .21  23 2.1  1 .25 39 3.4  1 .12  7.9 1.1  0 3.3 300 32 1 6.7 450 47 1 4.0 460 43 1 1.2  76 14   1 1.0  130 11   1 .077 23 .89 1 .073 23 .85 1 .084 23 .71 1 900   1000 12000 0 1.7 82 25 1 .18 9.4 1.6 1 .060 9.5 .46 1 5.9 330 45 1 5.8 320 48 1 5.9 330 45 1 25   290 230 1
loops/s3_false-unreach-call.i 210     860 1400    0 18     40 130    1 26    1200 320    1 .13  8.7 1.4  0 11   490 79 0 240   15000 2000 0 180   15000 2100 0 890    1600 11000   0 350    15000 3900   0 370     2600 3600    1 900     3600 8800    0 810     4000 8000    1 32   1100 250 0 15   210 160 1 .36 12   4.6 0 .066 11   .60 0 900   2500 11000 0 680   2000 8500 0 810   1600 9400 1 110   2500 1100 1
loops/string_false-unreach-call_true-termination.i 2.0   45 21    1 1.1   23 12    1 .26 19 2.8  1 .12  7.9 .99 0 5.3 320 40 1 7.1 360 56 1 3.2 250 32 1 4.1  190 61   1 890    1000 9100   1 .15  23 1.8  1 .16  23 1.9  1 .41  28 4.7  1 6.6 330 53 0 1.9 86 23 0 .18 9.9 2.0 1 .18  9.8 1.8  1 17   490 150 1 16   470 110 1 16   460 140 1 12   320 90 0
loops/sum01_bug02_false-unreach-call_true-termination.i .60  31 6.5  1 18     34 210    1 .40 17 4.3  1 16     40   190    1 4.0 290 31 1 9.0 500 65 1 4.1 300 35 1 3.9  110 46   1 .92 130 10   1 .092 23 1.1  1 .10  23 1.1  1 .15  26 1.6  1 66   690 800 1 1.7 76 25 1 .15 9.3 1.7 1 .16  12   1.6  1 10   490 73 1 10   490 80 1 12   490 99 1 12   300 90 1
loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i .36  29 4.4  1 8.8   30 120    1 .28 17 2.1  1 8.5   53   75    1 3.6 290 32 1 7.7 470 49 1 3.5 290 31 1 2.7  76 38   1 1.8  140 27   0 .11  23 .83 1 .34  23 .70 1 .13  23 1.1  1 8.7 380 65 1 1.7 87 20 1 .18 9.3 1.6 1 .15  12   1.3  1 8.2 430 62 1 8.3 380 66 1 10   490 79 1 81   310 840 1
loops/sum01_false-unreach-call_true-termination.i .41  28 6.0  1 29     36 310    1 .43 17 3.5  1 62     250   760    1 4.0 300 39 1 9.8 490 67 1 4.9 300 47 1 5.9  76 77   1 .63 81 8.0 1 .14  23 1.3  1 .14  25 1.7  1 .20  33 2.3  1 410   700 4200 1 1.9 82 22 1 .16 9.4 2.0 1 .20  12   2.7  1 10   480 83 1 11   490 91 1 13   550 99 1 13   350 100 1
loops/sum03_false-unreach-call_true-termination.i .25  26 2.7  1 4.3   32 43    0 .38 17 3.9  1 55     38   580    1 4.1 300 34 1 4.9 290 37 1 3.3 260 29 1 5.7  75 72   1 .22 23 2.8 1 .093 23 1.0  1 .11  23 1.1  1 .18  26 1.8  1 24   680 240 1 2.6 87 32 1 .14 9.4 2.0 0 .096 11   .51 1 13   530 95 1 22   530 190 1 15   550 120 1 15   460 110 1
loops/sum04_false-unreach-call_true-termination.i .42  28 4.7  1 .95  23 11    1 .41 17 3.7  1 .063 43   .76 0 3.3 280 29 1 4.0 290 29 1 2.6 250 23 1 4.6  76 57   1 .17 23 1.3 1 .073 23 .80 1 .11  23 .85 1 .13  23 1.7  1 17   570 160 1 1.5 75 21 1 .16 9.2 1.5 1 .086 11   .58 1 6.7 340 53 1 7.7 350 60 1 8.1 400 60 1 11   300 86 1
loops/sum_array_false-unreach-call.i .31  36 3.8  1 .52  25 6.6  1 .11 20 1.0  1 .11  7.7 .90 0 3.9 310 39 1 32   1700 180 1 5.1 320 49 1 1.4  160 18   1 52    2100 720   1 .15  23 2.0  1 .16  23 2.0  1 .15  23 1.7  1 14   660 110 1 1.9 91 22 1 .20 10   1.8 0 .079 9.8 .46 0 6.7 330 53 1 7.6 330 56 1 7.0 340 57 1 15   290 120 1
loops/terminator_01_false-unreach-call_true-termination.i .11  22 .82 1 .082 17 .75 1 .12 17 .75 1 .11  7.7 1.2  0 3.0 280 27 1 3.5 280 29 1 2.4 250 20 1 .54 75 6.0 1 .60 81 6.7 1 .077 23 .73 1 .072 23 .82 1 .11  23 .68 1 5.1 330 41 1 1.6 80 20 1 .17 9.5 1.4 1 .064 9.8 .45 1 6.9 350 52 1 5.7 320 45 1 6.8 330 54 1 9.4 280 63 1
loops/terminator_02_false-unreach-call_true-termination.i .10  22 .95 1 .096 19 .54 1 .14 19 .93 1 .15  7.9 1.6  0 3.0 280 31 1 3.6 280 29 1 2.4 250 20 1 .40 75 4.7 1 16    920 170   1 .10  23 .73 1 .080 23 .84 1 .082 23 .79 1 5.2 340 39 1 1.7 85 22 1 .18 9.4 1.8 1 .092 12   .92 1 5.9 320 43 1 5.5 320 43 1 5.6 340 42 1 9.2 280 73 1
loops/terminator_03_false-unreach-call_true-termination.i .12  22 .76 1 .14  20 1.3  1 .11 17 .98 1 .46  7.6 5.1  1 3.3 280 32 1 4.5 330 34 1 3.0 280 24 1 .56 75 6.4 1 13    160 150   1 .074 23 .86 1 .077 23 .78 1 .10  23 .82 1 6.0 340 50 1 1.7 86 22 1 .17 9.3 1.6 1 .12  9.9 1.7  1 6.1 320 55 1 6.1 330 44 1 5.7 330 45 1 9.6 290 66 1
loops/trex01_false-unreach-call_true-termination.i .13  23 .95 1 .11  19 .50 1 .14 18 .90 1 .19  7.8 1.9  1 3.1 280 25 1 5.0 320 38 1 2.5 250 24 1 .61 160 6.6 1 42    1800 490   1 .076 23 .99 1 .082 23 .79 1 .11  23 .81 1 7.7 450 63 1 1.7 78 20 1 .18 9.4 1.8 1 .084 10   .55 1 5.7 320 47 1 6.0 320 51 1 5.9 320 41 1 10   280 68 1
loops/trex02_false-unreach-call_true-termination.i .11  22 .97 1 .064 21 .61 1 .11 17 1.1  1 .10  7.9 .92 0 2.8 280 28 1 3.5 280 30 1 2.5 250 21 1 .36 75 4.1 1 15    890 200   0 .079 23 .86 1 .074 23 .81 1 .11  23 .70 1 5.2 330 39 1 1.7 82 20 1 .15 10   1.8 1 .077 9.7 .74 1 5.8 320 46 1 5.5 320 43 1 5.9 340 49 1 9.8 290 70 1
loops/trex03_false-unreach-call_true-termination.i .11  23 .93 1 .11  21 .62 1 .15 18 .98 1 .37  7.8 4.1  1 3.1 300 28 1 4.5 330 31 1 2.9 290 26 1 .38 76 4.6 1 9.7  510 110   1 .080 23 2.0  1 .10  23 .75 1 .11  23 .83 1 5.8 320 44 1 1.8 83 26 1 .19 10   1.8 1 .17  9.8 1.9  1 5.7 320 41 1 6.3 320 52 1 5.3 320 45 1 11   280 74 1
loops/verisec_NetBSD-libc__loop_false-unreach-call_true-termination.i .11  23 1.1  1 .43  22 4.1  1 .28 17 2.6  1 .031 7.8 .29 0 3.3 300 29 1 3.9 300 33 1 2.7 250 21 1 1.4  75 21   1 10    1200 110   1 .099 23 .94 1 .084 23 .93 1 .12  23 .97 1 5.4 340 46 0 1.7 86 21 1 .16 9.3 1.6 0 .087 9.8 .49 1 8.2 400 74 1 7.2 330 54 1 9.7 370 77 1 10   290 73 1
loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call_true-termination.i .47  33 5.6  1 30     36 320    1 .35 23 3.7  1 .035 7.8 .34 0 3.9 300 34 1 23   880 150 1 3.0 270 25 1 2.1  130 25   1 900    1800 10000   0 .16  23 1.2  1 .17  24 1.7  1 .13  24 1.1  0 5.7 350 39 0 2.0 86 25 0 .21 10   2.2 1 .11  10   1.2  0 14   560 120 1 9.7 490 75 1 16   510 130 1 18   290 150 1
loops/vogal_false-unreach-call.i 7.2   150 72    1 900     330 11000    0 .54 27 5.4  1 .11  7.7 1.2  0 6.5 360 53 1 98   2300 880 0 18   270 24 1 13    210 160   0 140    15000 1400   0 .57  38 7.1  0 .60  40 6.6  0 6.3   160 69    0 6.2 350 44 0 5.2 110 61 0 .18 10   1.9 1 6.1   63   84    -32 900   1200 12000 0 32   790 270 1 900   1200 12000 0 18   460 130 1
loops/while_infinite_loop_4_false-unreach-call_true-termination.i .11  22 .90 1 .10  21 .51 1 .11 17 .78 1 .046 7.7 .27 0 2.9 270 28 1 3.4 290 27 1 2.4 250 22 1 .37 75 4.2 1 .22 23 2.1 1 .077 23 .68 1 .10  23 .73 1 .086 23 .75 1 4.6 330 35 1 1.6 76 24 1 .13 9.3 1.6 1 .057 9.6 .46 1 6.5 340 48 1 6.1 330 43 1 5.8 320 46 1 9.8 280 72 1
loops/array_true-unreach-call_true-termination.i .13  23 .86 2 .64  23 7.2  2 .19 19 1.7  2 .11  8.1 .97 0 3.0 280 24 2 4.2 310 31 2 3.2 270 27 2 4.2  280 38   2 .19 23 1.8 2 170     15000 2400    0 .12  23 .86 2 .083 23 .93 2 11   440 91 2 1.2 73 15 2 .15 10   1.7 2 .074 9.8 .44 2 7.3 360 57 2 6.0 320 47 2 12   360 95 2 510   870 6100 2
loops/bubble_sort_true-unreach-call.i 1.1   77 8.2  2 .055 18 .60 2 850    14000 5100    0 .11  7.9 1.2  0 2.7 260 23 2 3.1 280 25 2 93   2200 1200 2 900    450 10000   0 900    7000 5500   0 900     1100 8900    0 900     5100 11000    0 .10  23 1.3  2 6.3 380 47 0 1.4 86 15 2 .18 9.4 1.6 2 .058 9.9 .54 0 5.8 320 45 2 6.7 350 57 2 6.0 320 51 2 6.8 280 51 2
loops/count_up_down_true-unreach-call_true-termination.i 900     1500 11000    0 .064 21 .65 -16 850    7200 6000    0 900     7000   13000    0 2.8 270 27 0 900   8900 8200 0 910   11000 8200 0 69    75 900   0 1.3  140 18   -16 900     2200 11000    0 900     5500 12000    0 900     9900 13000    0 7.3 360 65 2 880   1200 11000 2 .14 9.3 1.3 2 .053 9.8 .51 2 75   480 880 1 49   380 560 2 43   480 580 1 15   510 110 2
loops/eureka_01_true-unreach-call.i 16     710 150    1 900     600 10000    0 .95 23 11    1 .11  7.8 1.1  0 9.4 450 82 1 6.6 350 40 1 3.6 260 32 1 890    330 7300   0 20    3000 270   1 400     15000 6000    0 .31  38 5.0  1 900     430 8900    0 8.5 430 70 0 880   1100 8100 0 .17 9.1 1.6 1 .25  32   2.5  1 900   3300 12000 0 230   1600 3300 0 900   9400 8400 0 12   260 99 1
loops/eureka_05_true-unreach-call_true-termination.i 2.3   68 28    2 5.7   34 63    -16 .31 17 2.8  2 .035 7.9 .28 0 5.3 290 45 2 4.0 280 33 2 2.7 250 22 2 6.1  260 64   2 7.9  1100 100   2 130     15000 1900    0 .083 23 1.1  2 .22  26 2.0  2 900   1400 11000 0 1.6 82 18 2 .16 9.2 1.4 2 .063 9.8 .69 2 28   900 220 2 59   1000 660 1 900   3900 8700 0 11   270 82 2
loops/for_infinite_loop_1_true-unreach-call_false-termination.i .088 22 .79 2 .052 15 .56 2 250    15000 3800    0 .13  7.9 1.4  0 2.6 270 23 2 3.0 270 24 2 93   2200 1100 2 37    75 510   0 .23 31 2.5 2 900     13000 12000    0 410     15000 6800    0 .28  23 .55 2 6.0 350 49 2 1.3 78 18 2 890    15000   13000   0 .077 9.4 .63 2 6.1 340 51 2 6.6 330 53 2 6.2 320 49 2 9.4 300 77 2
loops/for_infinite_loop_2_true-unreach-call_false-termination.i .10  22 .72 2 .053 16 .50 2 260    15000 3500    0 .13  7.9 1.4  0 2.6 260 24 2 2.9 270 23 2 93   2300 1100 2 37    75 400   0 .19 23 2.1 -16 900     13000 13000    0 420     15000 5800    0 .077 23 .75 2 6.0 340 47 2 1.3 75 18 2 890    15000   11000   0 .054 9.7 .49 2 6.2 340 53 2 6.2 330 45 2 6.1 330 47 2 9.2 290 64 2
loops/insertion_sort_true-unreach-call_true-termination.i 900     5100 4900    0 3.0   23 40    -16 850    3100 3700    0 .14  8.1 1.3  0 4.1 310 34 0 910   4200 6800 0 900   2000 7300 0 890    160 10000   0 900    6000 8200   0 900     120 11000    0 900     130 11000    0 900     160 11000    0 900   1400 7800 0 880   240 12000 0 .16 9.9 2.0 0 .080 9.9 .47 0 900   1600 12000 0 900   1200 12000 0 900   2500 8200 0 49   15000 630 0
loops/invert_string_true-unreach-call_true-termination.i .85  35 9.9  2 1.5   37 17    -16 .32 17 3.2  2 .11  8.2 1.1  0 5.1 320 44 0 21   720 180 2 14   450 140 2 17    460 180   2 .18 24 2.1 2 110     15000 1300    0 .089 23 .97 2 .18  24 2.0  2 46   700 580 2 1.6 95 19 2 .17 9.3 1.8 2 .083 9.9 .76 2 35   640 310 2 81   680 940 2 61   740 610 2 650   910 7300 2
loops/linear_sea.ch_true-unreach-call.i 900     3900 7700    0 .070 18 .83 -16 810    11000 3600    0 .11  8.0 1.0  0 3.2 300 26 0 900   6900 10000 0 900   6200 9500 0 110    76 1400   0 4.8  110 67   1 900     5800 13000    0 900     11000 13000    0 900     9900 8200    0 6.2 360 55 0 880   160 11000 1 .19 10   1.9 0 .052 9.4 .51 0 900   640 12000 0 900   1100 11000 0 900   2400 11000 0 640   850 6200 1
loops/lu.cmp_true-unreach-call.i 290     3500 3100    1 47     64 580    1 11    210 140    1 17     15000   220    0 4.2 290 37 1 4.9 320 38 1 2.9 260 25 1 9.2  350 120   1 9.8  15000 110   0 900     5200 12000    0 .14  24 1.5  1 1.5   68 19    1 11   710 96 0 290   1100 2900 1 .17 9.4 1.6 1 .064 10   .48 0 78   13000 810 0 63   12000 570 0 76   13000 830 0 270   1200 2600 1
loops/matrix_true-unreach-call_true-termination.i .15  25 1.5  2 .086 11 .41 0 .19 17 1.6  2 .13  7.9 1.0  0 3.1 290 28 2 9.9 480 69 2 13   370 170 2 14    370 170   2 26    1700 330   2 230     15000 2900    0 .10  23 1.1  2 .088 23 .95 2 5.3 330 39 0 1.2 73 14 2 .18 10   1.7 2 .053 9.7 .48 2 8.9 430 75 2 9.1 430 74 2 900   7500 9100 0 28   630 200 2
loops/n.c11_true-unreach-call_false-termination.i 900     1800 9700    0 .60  22 8.2  2 850    3600 4400    0 .13  7.8 1.0  0 3.0 280 30 2 2.9 270 23 2 2.3 240 20 2 57    75 720   0 2.2  220 25   2 900     8800 2900    0 180     15000 2400    0 .10  23 .74 0 39   700 440 2 890   530 9000 2 900    76   13000   0 .096 9.5 .79 2 7.9 390 67 2 7.7 350 64 2 8.8 430 78 2 570   670 6800 2
loops/n.c40_true-unreach-call_true-termination.i .13  27 1.0  2 .23  20 2.4  -16 .19 17 1.5  2 .14  7.7 1.1  0 2.8 270 26 2 4.4 280 33 2 3.7 280 35 2 4.5  280 41   2 .16 23 1.9 2 49     15000 590    0 .11  23 .87 2 .085 23 .75 2 6.2 340 47 2 1.5 73 18 2 .18 9.5 1.3 2 .14  19   1.5  2 170   730 2100 2 170   640 2200 2 160   570 1900 2 650   870 6000 2
loops/nec40_true-unreach-call_true-termination.i .13  25 1.1  2 .27  21 2.4  -16 .15 17 1.6  2 .10  7.9 1.2  0 2.9 270 25 2 4.1 280 30 2 3.5 280 35 2 4.4  280 48   2 .14 23 1.8 2 900     6800 13000    0 .075 23 .81 2 .076 23 .89 2 6.7 340 55 2 1.4 76 17 2 .14 9.1 1.7 2 .14  9.8 1.2  2 170   720 2000 2 170   680 1900 2 170   720 2200 2 650   910 6000 2
loops/string_true-unreach-call_true-termination.i .13  23 .68 2 .75  22 5.7  2 .51 22 5.2  2 .11  8.0 1.1  0 2.9 270 23 2 5.6 320 41 2 3.2 260 25 2 4.8  270 50   2 12    500 140   2 660     15000 6300    0 3.1   39 8.4  2 .083 23 .83 2 470   990 5900 0 1.5 89 17 2 .18 9.3 2.0 2 8.2   30   110    2 8.0 380 67 2 8.3 390 66 2 20   600 160 2 11   270 89 2
loops/sum01_true-unreach-call_true-termination.i 900     1700 11000    0 1.5   22 16    2 19    120 210    2 900     11000   13000    0 3.7 280 28 2 120   3900 1000 2 300   3600 3000 2 300    3300 2900   2 1.4  130 17   -16 290     15000 3500    0 200     15000 2900    0 200     15000 2100    0 8.1 370 60 2 880   960 11000 2 .15 10   1.7 2 .16  12   .87 2 8.6 430 70 1 7.0 340 54 1 9.5 470 81 1 14   470 100 2
loops/sum03_true-unreach-call_false-termination.i .41  26 4.9  2 .18  20 1.4  2 320    15000 4200    0 .48  7.6 6.2  2 5.6 400 47 2 3.9 280 27 2 180   2200 2200 2 180    1400 2100   2 .27 41 3.6 2 900     9700 13000    0 410     15000 5800    0 120     15000 1400    0 6.7 340 52 2 900   190 10000 0 880    15000   12000   0 .057 9.9 .53 2 5.9 330 51 2 6.6 340 47 2 5.9 330 48 2 12   360 99 2
loops/sum04_true-unreach-call_true-termination.i .32  27 3.7  2 .76  23 8.0  2 .40 17 5.4  2 .039 7.9 .20 0 2.9 270 27 2 2.8 270 22 2 2.2 240 18 2 3.3  260 31   2 .13 23 1.8 2 900     8700 12000    0 .087 23 .88 2 .41  23 1.4  2 14   480 130 2 1.1 68 14 2 .19 18   2.2 2 .053 9.9 .47 2 9.2 480 76 2 8.6 480 60 2 9.5 550 71 2 14   490 100 2
loops/sum_array_true-unreach-call.i 900     12000 4900    0 .62  25 6.5  -16 850    1500 3900    0 .17  33   1.3  0 6.4 350 59 0 210   4400 1700 0 910   5800 8100 0 890    240 8500   0 900    1300 11000   0 900     330 2800    0 900     790 9300    0 900     750 8600    0 900   1200 12000 0 880   550 12000 1 .17 9.8 2.2 0 .081 9.9 .47 0 900   1900 11000 0 900   650 10000 0 900   2300 10000 0 660   1100 7400 1
loops/terminator_02_true-unreach-call_true-termination.i .12  22 .75 2 .21  20 1.9  2 .17 19 1.8  2 1.3   7.8 14    2 2.7 260 28 2 3.4 280 31 2 2.9 260 25 2 4.0  280 35   2 35    4700 370   2 510     15000 5400    0 .10  23 .89 2 .29  23 .61 2 10   530 93 2 1.4 75 15 2 .19 10   1.8 2 .15  9.9 2.1  2 5.8 320 44 2 6.6 340 46 2 6.6 340 50 2 9.8 320 71 2
loops/terminator_03_true-unreach-call_true-termination.i .10  22 1.0  2 .40  22 2.0  2 850    500 6200    0 900     990   10000    0 2.7 270 24 2 3.8 300 28 2 3.0 260 26 2 4.0  270 38   2 43    320 490   -16 900     3700 9600    0 900     6700 10000    0 .088 23 .79 2 7.6 350 60 2 1.3 82 18 2 900    64   12000   0 900     1200   11000    0 6.0 320 48 2 6.1 340 46 2 6.8 340 52 2 12   470 89 2
loops/trex01_true-unreach-call_true-termination.i 6.4   120 81    2 .83  22 7.2  2 850    6100 4300    0 900     8400   13000    0 6.0 320 52 2 5.9 320 44 2 160   2400 1900 2 820    160 8800   0 42    1800 490   -16 900     13000 11000    0 900     7000 11000    0 900     8500 11000    0 9.5 540 86 2 1.5 75 17 2 900    2400   12000   0 .40  9.9 5.4  0 6.3 330 49 2 5.8 320 51 2 5.9 330 49 2 19   580 150 2
loops/trex02_true-unreach-call_true-termination.i .12  22 .76 2 .14  20 1.2  2 850    1000 7900    0 .10  7.8 1.2  0 2.6 270 26 2 3.5 280 26 2 2.8 260 24 2 3.6  260 35   2 15    890 180   -16 900     4000 9300    0 900     12000 11000    0 .11  23 .82 2 5.9 340 50 2 1.3 78 19 2 .17 9.4 1.7 2 900     3200   9900    0 5.8 320 45 2 6.2 350 52 2 6.0 330 47 2 15   560 110 2
loops/trex03_true-unreach-call_true-termination.i .12  22 .78 2 .068 18 .66 -16 850    840 7000    0 1.9   7.9 23    2 3.0 280 27 0 4.1 280 28 2 2.9 260 22 2 3.9  260 36   2 560    890 8000   -16 900     3800 9500    0 900     5300 11000    0 .11  23 .89 2 900   1300 7100 0 880   410 10000 2 900    3800   9800   0 .28  9.6 2.9  0 6.4 320 47 2 5.9 320 50 2 6.1 340 49 2 31   690 230 2
loops/trex04_true-unreach-call_false-termination.i .11  22 .74 2 .35  29 3.3  2 850    2700 7200    0 900     6600   13000    0 2.8 270 24 2 3.8 280 27 2 3.0 260 29 2 4.5  280 39   2 22    300 250   -16 900     3900 10000    0 900     7300 12000    0 .092 23 .86 2 900   1000 12000 0 1.4 82 15 2 .18 9.4 2.0 2 .085 9.9 .67 0 5.8 330 46 2 6.2 330 48 2 6.1 320 50 2 12   440 82 2
loops/veris.c_NetBSD-libc__loop_true-unreach-call_true-termination.i .099 23 .95 2 .29  21 1.6  2 .29 17 3.2  2 .083 7.8 .19 0 2.9 280 27 2 910   9600 6900 0 3.2 260 24 2 4.0  280 37   2 11    1200 140   2 360     15000 4200    0 .12  23 .87 2 .086 23 .80 2 5.3 340 43 0 1.3 80 20 2 .16 9.5 1.4 2 .052 9.8 .49 2 8.6 390 61 2 7.3 380 66 2 8.3 370 60 2 13   460 89 2
loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i .11  24 .88 2 1.0   23 8.6  2 1.6  35 20    2 .11  7.9 1.1  0 16   720 120 2 27   1200 230 2 150   2400 2100 2 160    2400 2000   2 900    1800 11000   0 900     6900 12000    0 .35  36 3.4  2 .11  24 .90 0 5.5 360 50 0 5.0 110 63 2 .52 11   6.5 2 .14  9.7 1.3  0 7.8 370 60 2 6.6 330 48 2 7.1 350 60 2 20   270 190 2
loops/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call_true-termination.i .083 22 .88 2 .37  24 3.9  2 .48 18 4.3  2 .14  7.7 .94 0 3.1 280 30 2 4.0 290 31 2 4.0 270 39 2 5.1  290 44   2 2.0  290 21   2 360     15000 4500    0 .097 23 1.1  2 .081 23 .82 2 38   700 370 2 1.7 85 21 2 .14 9.2 1.5 2 .15  9.8 1.2  2 6.0 320 52 2 6.1 320 45 2 6.5 340 54 2 12   420 82 2
loops/vogal_true-unreach-call.i 5.5   89 64    2 900     300 11000    0 .33 18 3.5  2 .11  7.6 1.2  0 53   2800 460 2 61   1800 460 0 330   2200 3800 2 330    2100 3500   2 290    14000 3300   2 900     14000 11000    0 .30  24 3.9  2 2.8   38 6.5  2 6.1 330 57 0 3.6 89 50 2 .17 9.4 1.7 2 .48  9.7 5.5  2 900   5400 12000 0 900   2400 11000 0 900   5300 12000 0 660   1200 7100 2
loops/while_infinite_loop_1_true-unreach-call_false-termination.i .11  22 .65 2 .051 16 .62 2 260    15000 3300    0 .037 7.7 .33 0 2.6 270 24 2 2.9 280 22 2 2.2 250 19 2 3.1  260 29   2 .19 23 1.7 -16 740     15000 9200    0 430     15000 6700    0 .099 23 .77 2 5.4 360 40 2 1.3 79 16 2 900    15000   14000   0 .053 9.9 .44 2 5.7 320 41 2 5.8 330 51 2 5.9 320 46 2 12   470 89 2
loops/while_infinite_loop_2_true-unreach-call_false-termination.i .097 22 .77 2 .057 15 .52 2 260    15000 3200    0 .034 7.8 .30 0 2.5 270 24 2 2.7 260 23 2 2.4 240 21 2 3.2  250 28   2 .19 23 1.9 2 740     15000 9900    0 430     15000 6600    0 .079 23 .84 2 5.4 340 40 2 1.3 72 16 2 .13 9.3 1.3 2 .065 9.9 .46 2 6.1 340 47 2 5.6 330 44 2 6.0 340 47 2 9.0 280 65 2
loops/while_infinite_loop_3_true-unreach-call_false-termination.i .093 22 .83 2 .054 17 .66 2 230    15000 2800    0 .037 7.9 .27 0 2.7 270 27 2 3.0 290 25 2 2.4 250 20 2 3.3  260 30   2 .20 23 2.2 -16 900     15000 13000    0 420     15000 6000    0 .10  23 .76 2 5.5 330 42 2 1.3 79 17 2 890    15000   12000   0 .098 11   .47 2 6.3 350 46 2 5.6 320 46 2 5.9 320 42 2 13   480 95 2
loop-acceleration/array_false-unreach-call1_true-termination.i 900     10000 8900    0 900     260 8400    0 29    1700 370    0 .11  7.8 1.1  0 900   4000 11000 0 680   7200 6300 0 900   15000 11000 0 900    230 9400   0 140    160 1900   0 300     510 3900    0 310     2000 4800    0 900     590 10000    0 900   1000 8400 0 15   280 210 0 .15 10   2.0 0 .074 9.9 .47 0 900   2400 14000 0 900   3800 12000 0 900   2000 12000 0 340   3700 4100 0
loop-acceleration/array_false-unreach-call2_true-termination.i 900     11000 10000    0 900     500 9300    0 61    3500 830    0 .099 7.6 1.2  0 900   4300 9300 0 930   14000 7300 0 870   15000 9400 0 890    610 9000   0 140    180 2000   0 110     1200 1500    0 180     9200 2400    0 900     640 9000    0 900   1100 11000 0 140   3500 1700 0 .16 14   1.6 0 .058 9.9 .50 0 900   3400 12000 0 900   3700 14000 0 900   3200 13000 0 360   4000 4200 0
loop-acceleration/array_false-unreach-call3_true-termination.i 900     10000 7300    0 900     360 10000    0 23    930 310    0 .11  7.8 1.1  0 900   4300 8900 0 920   4000 9600 0 920   10000 9700 0 900    8300 9300   0 150    230 2000   0 300     700 4000    0 320     2300 4300    0 900     530 9500    0 900   1100 10000 0 880   820 8000 0 2.0  12   32   0 130     820   1800    0 900   1900 13000 0 900   2400 13000 0 900   1700 12000 0 350   3700 4100 0
loop-acceleration/const_false-unreach-call1.i 900     1700 10000    0 900     340 8700    0 1.3  20 16    1 .035 7.8 .26 0 900   4200 8800 0 920   9300 8400 0 68   1600 880 1 54    75 670   0 .14 23 1.7 1 10     130 120    1 21     1500 280    1 150     15000 1700    0 900   1000 12000 0 2.3 69 29 1 .17 11   1.4 1 .11  9.7 .97 1 900   1700 12000 0 900   880 12000 0 900   760 11000 0 340   3700 3500 0
loop-acceleration/diamond_false-unreach-call1.i .83  31 9.2  1 54     40 520    0 1.4  50 15    1 900     560   12000    0 47   1700 460 0 43   2000 360 1 12   1200 110 1 32    75 410   1 1.3  130 17   0 1.3   150 17    1 2.2   260 29    1 4.0   410 53    1 900   1000 11000 0 260   120 3700 1 .16 9.9 1.9 1 27     150   380    1 150   1000 1800 1 850   820 12000 1 520   670 6800 1 83   1900 820 1
loop-acceleration/functions_false-unreach-call1_true-termination.i 900     1400 12000    0 900     250 12000    0 260    15000 3400    0 .035 7.7 .22 0 900   4400 8600 0 910   7900 8000 0 910   7200 8900 0 36    75 390   0 .16 23 1.8 0 640     15000 9400    0 260     15000 3800    0 210     15000 2600    0 900   1000 12000 0 880   1400 10000 0 .13 9.3 1.5 0 120     15000   1400    0 900   2300 14000 0 900   1900 11000 0 900   1100 11000 0 24   220 210 0
loop-acceleration/multivar_false-unreach-call1_true-termination.i .098 22 .90 1 .10  20 .58 1 .13 17 .94 1 .19  7.9 1.7  1 3.0 280 27 1 3.9 310 29 1 2.4 250 22 1 .53 75 6.5 1 2.9  170 34   1 .11  23 .81 1 .088 23 .77 1 .11  23 .66 1 5.0 330 37 1 1.6 80 22 1 .17 9.4 1.4 1 .078 9.6 .53 1 5.8 330 45 1 6.6 340 47 1 5.9 320 46 1 22   280 260 1
loop-acceleration/nested_false-unreach-call1.i 900     9600 10000    0 900     410 8800    0 310    15000 4000    0 .031 7.7 .32 0 900   3900 11000 0 19   840 120 0 900   4000 8900 0 900    1400 8100   0 3.3  450 33   0 900     8200 11000    0 330     15000 4100    0 900     12000 10000    0 900   1100 11000 0 880   880 12000 0 .16 9.4 1.5 0 .050 9.8 .56 0 900   3600 13000 0 900   1500 12000 0 900   2200 11000 0 150   7100 1900 0
loop-acceleration/phases_false-unreach-call1.i 900     1200 12000    0 .11  22 1.2  0 310    15000 3700    0 .035 7.9 .30 0 900   4100 9300 0 900   5100 8600 0 900   3600 8900 0 150    75 1800   0 .15 23 1.8 0 900     5700 11000    0 510     15000 6700    0 900     4200 11000    0 900   1000 10000 0 880   380 11000 0 230    15000   3500   0 160     15000   1700    0 900   1600 13000 0 900   2300 12000 0 900   1000 13000 0 140   6000 1600 0
loop-acceleration/phases_false-unreach-call2.i .17  25 1.1  1 .075 16 .59 1 .13 17 .97 1 .23  7.9 2.2  1 3.1 280 28 1 4.7 300 35 1 2.4 250 21 1 .55 76 7.0 1 56    3200 640   1 .096 23 .78 1 .074 23 .83 1 .28  23 .55 1 5.0 330 40 1 880   170 10000 0 .15 9.4 1.5 1 .086 9.9 .93 1 5.5 320 47 1 5.5 320 48 1 5.6 320 48 1 37   580 310 1
loop-acceleration/simple_false-unreach-call1.i 900     1400 13000    0 770     160 9300    0 270    15000 3600    0 .035 7.7 .19 0 900   4200 8200 0 90   2900 650 0 910   8400 11000 0 54    75 660   0 .14 23 1.8 0 900     9100 11000    0 310     15000 3800    0 260     15000 2800    0 900   1000 9900 0 880   880 11000 0 .14 9.3 1.6 0 .079 9.8 .46 0 900   1500 13000 0 900   980 13000 0 900   830 12000 0 140   8700 2000 0
loop-acceleration/simple_false-unreach-call2_true-termination.i .12  22 .78 1 .085 16 .56 1 .13 17 1.1  1 .16  7.6 2.0  1 2.9 280 29 1 3.3 300 27 1 2.4 250 20 1 .38 75 4.5 1 2.6  120 27   1 .11  23 .66 1 .074 23 1.1  1 .072 23 .96 1 5.0 340 46 1 1.6 72 19 1 .16 9.4 1.7 1 .081 9.9 .40 1 5.6 310 40 1 5.5 320 47 1 5.5 320 44 1 8.9 280 63 1
loop-acceleration/simple_false-unreach-call3_true-termination.i .099 22 .87 1 .067 17 .71 1 .11 17 .86 1 .17  7.8 1.7  1 2.9 270 29 1 5.6 370 38 1 2.5 250 21 1 .52 75 7.2 1 1.3  83 14   1 .086 23 .79 1 .10  23 .83 1 .072 23 .92 1 4.9 350 38 1 1.6 79 22 1 .17 9.3 1.3 1 .062 16   .72 1 5.5 320 45 1 5.6 310 45 1 5.6 320 52 1 130   860 690 1
loop-acceleration/simple_false-unreach-call4.i 900     1400 12000    0 1.1   35 8.9  0 290    15000 3000    0 .036 7.8 .32 0 900   4300 7900 0 200   3100 1900 0 910   7700 9300 0 53    75 670   0 .14 23 1.7 0 900     9000 13000    0 310     15000 4100    0 210     15000 2500    0 900   1000 11000 0 880   910 9900 0 .13 9.4 1.6 0 .078 9.5 .52 0 900   1400 14000 0 900   960 11000 0 900   880 13000 0 150   8400 1600 0
loop-acceleration/underapprox_false-unreach-call1_true-termination.i .23  25 2.1  1 .99  23 12    1 .40 17 3.3  1 .034 7.9 .28 0 3.3 290 30 1 3.7 280 28 1 2.6 250 22 1 3.5  75 46   1 .14 23 1.5 1 .073 23 .89 1 .11  23 .66 1 .093 23 1.0  1 9.1 380 69 0 1.5 73 20 1 .16 9.3 1.5 1 .085 10   .54 1 7.4 380 56 1 7.0 360 49 1 9.3 430 64 1 10   290 80 1
loop-acceleration/underapprox_false-unreach-call2_true-termination.i .24  26 2.2  1 .72  23 7.2  1 .36 17 3.6  1 .078 7.8 .23 0 3.2 270 26 1 3.6 280 27 1 2.8 260 24 1 3.5  75 44   1 .14 23 1.5 1 .075 23 .80 1 .29  23 1.1  1 .089 23 1.1  1 9.0 360 72 0 1.5 75 16 1 .13 9.2 1.5 1 .052 9.9 .44 1 7.3 370 57 1 7.4 350 50 1 9.0 430 71 1 10   290 76 1
loop-acceleration/array_true-unreach-call1_true-termination.i 38     540 390    2 900     340 8700    0 10    1100 120    2 .098 7.7 1.0  0 900   4000 11000 0 4.0 300 28 2 98   430 1000 2 99    550 1300   2 140    160 1800   -16 180     15000 2200    0 110     1600 200    2 .089 23 .82 2 900   1000 9200 0 2.9 210 36 2 .13 9.3 1.6 2 .059 9.9 .56 0 900   3100 13000 0 900   2900 13000 0 900   2000 12000 0 640   840 6500 2
loop-acceleration/array_true-unreach-call2_true-termination.i 900     12000 9300    0 900     500 9700    0 23    2200 260    1 .14  7.8 1.0  0 900   4200 9000 0 940   14000 7100 0 880   15000 8900 0 890    280 12000   0 140    180 1900   -16 270     15000 3400    0 140     8500 1800    1 900     570 8800    0 900   1000 11000 0 35   3100 410 1 .15 10   1.6 1 .057 9.9 .44 1 900   3100 13000 0 900   3100 12000 0 900   1900 14000 0 640   830 7500 1
loop-acceleration/array_true-unreach-call3_true-termination.i 3.8   130 38    2 .39  22 2.9  1 7.9  630 98    1 .099 7.8 1.3  0 900   4300 11000 0 4.0 310 27 2 14   1200 130 1 14    1200 120   1 .83 130 9.4 1 900     4600 11000    0 64     2100 810    1 900     720 9600    0 900   1000 9200 0 880   850 7400 0 6.6  13   79   1 370     1700   4800    1 900   1800 13000 0 900   4400 15000 0 7.8 360 61 1 640   860 6200 1
loop-acceleration/array_true-unreach-call4_true-termination.i 900     10000 8700    0 900     350 8600    0 7.7  630 110    1 .13  7.7 .91 0 900   4200 9500 0 900   5200 8000 0 13   1200 110 1 890    220 11000   0 .82 130 10   1 900     4800 11000    0 65     2000 850    1 900     610 10000    0 900   1000 11000 0 880   830 6800 0 6.6  13   87   1 360     1700   4700    1 900   1800 12000 0 900   3400 12000 0 900   1700 11000 0 640   860 6300 1
loop-acceleration/const_true-unreach-call1.i .19  24 1.8  2 .24  21 1.9  1 1.6  19 15    2 .078 7.7 .21 0 3.0 270 25 2 3.2 270 28 2 5.9 600 60 2 7.4  430 65   2 .19 30 2.2 2 900     1700 2200    0 21     1500 270    2 .090 23 .94 2 5.4 340 49 2 1.9 66 23 2 .14 9.4 1.7 2 .088 9.9 .81 2 900   1600 14000 0 900   870 12000 0 900   620 11000 0 11   420 89 2
loop-acceleration/diamond_true-unreach-call1_true-termination.i .84  31 11    2 47     41 600    -16 1.9  50 21    2 900     520   11000    0 57   2100 590 0 34   1800 280 2 150   2800 2200 2 270    2900 3500   2 1.4  180 17   2 160     15000 2100    0 11     1100 140    2 56     1600 820    2 900   1000 9900 0 880   170 9500 2 .16 9.8 1.9 2 180     1600   2400    2 500   980 6300 1 900   680 12000 0 900   810 13000 0 20   480 150 2
loop-acceleration/diamond_true-unreach-call2.i .17  26 2.1  2 77     41 820    -16 .42 24 4.6  2 740     5800   8200    2 9.8 470 79 2 9.1 720 62 2 4.8 290 39 2 8.9  290 99   2 96    2600 1000   2 550     15000 1400    0 .25  37 3.3  2 .45  45 5.8  2 900   1100 9000 0 2.0 100 25 2 .20 17   2.4 2 .21  10   2.6  2 30   600 310 1 13   470 120 1 220   630 3100 1 140   670 1700 2
loop-acceleration/functions_true-unreach-call1_true-termination.i 900     1600 12000    0 900     290 12000    0 260    15000 3100    0 .038 7.8 .26 0 900   4400 9600 0 44   1900 320 0 910   7600 9000 0 36    75 440   0 .26 39 2.3 1 640     15000 8900    0 260     15000 3000    0 200     15000 2300    0 900   1000 10000 0 880   1300 11000 1 .13 9.5 2.0 1 110     15000   1400    0 900   2600 14000 0 900   1800 12000 0 9.0 410 75 2 16   540 110 1
loop-acceleration/multivar_true-unreach-call1_true-termination.i 900     1700 12000    0 .13  19 .74 2 100    270 850    2 .51  7.8 5.2  2 2.8 270 21 2 3.6 310 26 2 2.7 260 24 2 63    75 750   0 1.1  160 15   2 210     15000 2700    0 160     15000 1700    0 180     15000 2100    0 5.8 340 43 2 880   1100 13000 2 .14 9.1 1.5 2 .061 9.7 .44 2 6.5 350 45 2 5.8 320 46 2 6.4 330 49 2 12   440 88 2
loop-acceleration/nested_true-unreach-call1.i .17  24 1.3  2 900     280 9200    0 310    15000 4300    0 .078 7.8 .25 0 900   3900 11000 0 3.4 270 26 2 350   4500 4000 2 360    4200 4100   2 3.6  550 35   2 900     8200 11000    0 330     15000 3800    0 .11  23 .84 2 900   1000 9500 0 880   940 12000 0 .16 9.4 1.4 2 .050 9.9 .52 2 900   3700 14000 0 900   1500 13000 0 900   2500 12000 0 16   620 110 2
loop-acceleration/overflow_true-unreach-call1.i 900     1400 13000    0 .17  22 1.4  1 280    15000 3400    0 .036 7.8 .32 0 3.2 270 23 1 900   8700 7900 0 910   7800 8700 0 53    75 590   0 .16 23 2.1 1 900     9200 11000    0 320     15000 3600    0 220     15000 2300    0 5.9 340 46 1 880   930 12000 0 .15 9.5 1.4 1 .053 9.9 .56 1 900   1800 13000 0 900   1100 14000 0 6.6 360 48 1 12   450 97 1
loop-acceleration/phases_true-unreach-call1.i 900     1500 12000    0 .14  20 1.2  0 310    15000 4900    0 .045 7.6 .25 0 900   4100 10000 0 900   5000 7800 0 900   4300 8600 0 130    75 1900   0 .15 23 1.9 -16 900     5700 12000    0 510     15000 6600    0 900     4400 9900    0 900   1000 10000 0 880   350 12000 0 210    15000   2900   1 160     15000   2200    0 900   1500 13000 0 900   2400 12000 0 900   900 13000 0 140   6100 1900 0
loop-acceleration/phases_true-unreach-call2_false-termination.i .12  24 1.1  2 .48  21 4.4  0 850    5900 7900    0 1.4   11   16    2 3.1 290 31 0 4.7 310 36 2 2.8 260 25 2 5.3  280 53   2 57    3200 540   -16 900     13000 7300    0 740     15000 5200    0 110     83 1500    2 43   690 500 0 880   170 11000 0 900    11000   8800   0 .12  9.5 1.1  2 7.6 340 69 2 6.8 320 58 2 120   400 1400 2 11   440 90 2
loop-acceleration/simple_true-unreach-call1.i 900     1600 10000    0 770     160 9200    0 280    15000 3500    0 .065 7.8 .21 0 900   4200 7900 0 910   8600 7900 0 910   7900 8900 0 53    75 640   0 .18 23 1.9 1 900     9200 11000    0 310     15000 4200    0 240     15000 2700    0 900   1000 12000 0 880   970 11000 0 .13 9.5 1.5 1 .049 9.9 .65 1 900   3800 15000 0 900   1000 13000 0 6.7 350 54 2 12   450 77 1
loop-acceleration/simple_true-unreach-call2_true-termination.i .083 22 .77 2 .15  21 .62 0 850    4600 7300    0 .27  7.9 3.7  2 2.7 270 23 2 3.3 280 26 2 2.7 260 24 2 3.6  280 35   2 2.6  120 33   -16 900     4300 11000    0 900     8200 10000    0 .11  23 .81 2 5.5 340 44 2 1.3 80 15 2 .13 9.3 1.7 2 .073 9.7 .47 2 5.7 320 50 2 5.4 330 46 2 5.9 330 50 2 13   480 87 2
loop-acceleration/simple_true-unreach-call3_true-termination.i 900     1200 9600    0 .065 20 .67 -16 850    11000 3300    0 .13  7.8 1.8  0 900   8800 8200 0 900   7300 8700 0 900   5800 9400 0 56    110 750   0 .67 94 7.4 1 130     15000 1800    0 130     15000 1500    0 140     15000 1900    0 6.7 350 54 1 880   400 11000 1 .17 9.3 1.8 1 .058 9.9 .48 1 900   770 10000 0 900   1200 12000 0 7.5 360 52 2 11   440 85 1
loop-acceleration/simple_true-unreach-call4.i .12  22 .64 2 1.4   35 18    0 290    15000 3700    0 .037 7.5 .29 0 900   4300 9100 0 3.0 270 24 2 150   2200 1700 2 150    1300 1600   2 .19 23 2.1 2 900     9100 11000    0 310     15000 4000    0 .10  23 .82 2 900   1000 9600 0 880   960 11000 0 .14 9.6 1.5 2 .050 9.9 .56 2 5.9 330 48 2 900   1100 13000 0 6.9 360 52 2 12   450 85 2
loop-acceleration/underapprox_true-unreach-call1_true-termination.i .22  25 2.6  2 .58  22 4.0  2 .41 17 3.8  2 .079 7.7 .26 0 3.8 270 35 2 2.8 270 21 2 2.3 240 20 2 5.8  260 63   2 .16 23 1.4 2 900     9100 11000    0 .080 23 .98 2 .11  23 1.4  2 11   450 92 2 1.2 69 14 2 .16 9.2 1.4 2 .080 9.7 .45 2 63   510 810 2 900   500 12000 0 190   570 2400 2 20   520 150 2
loop-acceleration/underapprox_true-unreach-call2_true-termination.i .10  25 1.7  2 .21  20 1.8  2 .42 17 4.8  2 .040 7.8 .24 0 2.7 270 23 2 2.8 270 24 2 2.3 240 21 2 3.2  260 30   2 .14 24 1.6 2 900     9400 11000    0 .081 23 .83 2 .11  23 .79 2 9.7 370 83 2 1.1 66 14 2 .14 9.5 1.4 2 .055 9.9 .47 2 7.8 390 57 2 8.1 390 56 2 10   470 72 2 13   470 93 2
loop-invgen/id_trans_false-unreach-call_true-termination.i .10  23 .98 1 .21  23 2.0  0 .12 18 1.1  1 8.6   110   100    1 3.4 280 28 1 9.5 530 74 1 3.3 290 29 1 .59 76 6.9 1 24    2300 300   0 .30  23 .99 1 .095 23 .90 1 .093 23 .84 1 7.0 360 59 1 1.8 79 22 1 .20 10   1.8 0 .10  11   1.2  1 6.5 320 49 1 7.2 340 56 1 7.9 370 63 1 10   280 70 1
loop-invgen/MADWiFi-encode_ie_ok_true-unreach-call_true-termination.i 900     540 12000    0 1.6   31 21    2 850    200 12000    0 900     4500   14000    0 3.2 270 30 2 900   5000 8200 0 900   1800 8700 0 900    76 12000   0 900    2400 10000   2 900     770 11000    0 900     1600 11000    0 900     2600 11000    0 12   530 110 2 56   170 630 2 900    2200   11000   0 900     3500   10000    0 7.7 380 63 2 9.3 460 75 2 10   450 79 2 15   480 100 2
loop-invgen/NetBSD_loop_true-unreach-call_true-termination.i .12  23 1.1  2 .59  25 5.1  2 850    11000 5700    0 900     12000   11000    0 5.4 330 45 2 330   5600 2900 2 910   8000 8600 0 54    76 670   0 9.3  870 120   2 410     15000 4600    0 220     15000 2700    0 150     15000 2000    0 11   430 79 2 880   560 9700 2 900    1200   11000   0 900     1300   12000    0 7.8 410 57 2 7.7 430 56 2 9.4 500 76 2 13   470 90 2
loop-invgen/SpamAssassin-loop_true-unreach-call_false-termination.i 3.7   48 42    2 210     95 2300    2 850    470 9400    0 900     5000   13000    0 130   3800 1500 1 83   3000 690 0 9.0 360 87 2 890    120 13000   0 34    15000 380   0 900     140 10000    0 900     170 9300    0 900     130 2300    0 900   1200 9300 0 880   370 7800 0 900    1700   6700   0 900     2400   11000    0 12   490 100 2 21   710 180 2 280   1000 3800 1 55   800 400 2
loop-invgen/apache-escape-absolute_true-unreach-call_true-termination.i 900     2000 9000    0 9.7   32 110    2 850    470 9000    0 900     2800   11000    0 19   620 140 2 66   3700 440 2 4.1 280 37 2 890    100 13000   0 900    650 13000   0 900     110 1800    0 900     310 12000    0 900     420 11000    0 780   990 11000 2 880   340 9000 2 900    3500   10000   0 900     990   14000    0 11   500 84 2 18   550 130 2 19   520 150 2 670   1200 5400 0
loop-invgen/apache-get-tag_true-unreach-call_true-termination.i 3.4   43 43    2 5.5   33 52    2 850    680 8900    0 900     12000   11000    0 19   850 160 2 910   5600 6900 0 910   6300 8100 0 900    100 12000   0 140    15000 1500   0 900     220 13000    0 900     400 13000    0 900     640 11000    0 900   1200 11000 0 880   370 9200 2 900    4400   8200   0 900     1500   13000    0 10   480 98 1 11   490 97 2 12   500 100 1 650   1400 5300 0
loop-invgen/down_true-unreach-call_true-termination.i 900     1900 8900    0 900     280 9500    0 850    3600 4800    0 900     9100   11000    0 900   4100 9000 0 910   4200 9100 0 910   12000 8300 0 89    100 1100   0 18    1000 250   1 900     6900 8800    0 900     14000 9900    0 600     15000 6500    0 900   1000 12000 0 880   460 14000 1 900    730   11000   0 900     6700   11000    0 900   4000 12000 0 900   3600 13000 0 9.0 360 71 1 19   640 150 1
loop-invgen/fragtest_simple_true-unreach-call_true-termination.i 900     3200 9900    0 900     260 12000    0 850    1600 6200    0 900     640   11000    0 900   4400 12000 0 930   3900 9300 0 910   15000 9600 0 91    130 1100   0 13    1400 130   1 900     15000 12000    0 450     15000 5800    0 .098 23 .85 0 900   1100 11000 0 880   580 9600 1 900    3400   9400   0 250     15000   2900    0 900   4200 13000 0 900   4200 12000 0 900   5100 13000 0 530   510 3500 0
loop-invgen/half_2_true-unreach-call_true-termination.i 900     2100 12000    0 .11  20 .86 0 850    1400 6700    0 900     3500   13000    0 900   4100 8800 0 900   5500 7400 0 910   7700 7500 0 170    110 2100   0 31    1000 410   1 900     4400 9400    0 900     9100 9700    0 900     5400 2500    0 900   1000 12000 0 600   270 8200 1 900    2000   10000   0 900     5700   11000    0 900   1500 12000 0 900   760 15000 0 900   1400 15000 0 21   620 150 1
loop-invgen/heapsort_true-unreach-call_true-termination.i 900     1400 7200    0 .22  24 2.1  0 850    12000 7100    0 .11  7.9 1.2  0 63   2700 600 2 490   4300 3600 0 900   4900 7900 0 900    710 12000   0 39    15000 370   0 900     1200 7600    0 900     2300 8700    0 900     3200 8000    0 900   1300 9900 0 880   380 7300 2 900    1600   8300   0 900     730   10000    0 200   1100 2500 2 67   1000 840 2 850   12000 9500 0 900   1500 4600 0
loop-invgen/id_build_true-unreach-call_true-termination.i .18  25 1.5  2 .38  23 3.8  2 200    12000 1700    0 900     6200   11000    0 3.1 270 27 2 9.4 550 68 2 200   1100 2400 2 210    1000 2400   2 70    15000 970   0 420     15000 5300    0 240     15000 2700    0 900     5700 2800    0 900   1600 7100 0 880   550 10000 2 900    1900   9200   0 900     4100   13000    0 6.3 330 49 2 7.4 380 63 2 11   540 87 2 19   630 140 2
loop-invgen/large_const_true-unreach-call_true-termination.i .23  26 2.3  2 41     38 490    2 .20 17 1.8  2 .11  7.8 1.2  0 4.2 300 40 2 5.5 310 38 2 3.4 270 29 2 4.5  310 41   2 31    2000 410   2 900     14000 8400    0 .091 23 .97 2 .13  23 .87 2 900   1500 7900 0 1.4 82 16 2 .16 10   1.9 2 .24  18   2.3  2 8.1 430 64 2 8.4 440 62 2 30   890 310 2 27   720 180 2
loop-invgen/nest-if3_true-unreach-call_true-termination.i .70  32 8.1  2 .23  21 2.2  2 710    13000 4300    0 900     9700   11000    0 4.4 290 37 2 23   870 160 0 900   2600 9100 0 900    320 7700   0 900    11000 8700   0 900     1200 7700    0 900     2400 8700    0 900     3400 7500    0 900   1600 6300 0 880   370 11000 2 900    77   12000   0 900     23   11000    0 6.1 330 48 2 9.5 480 80 2 7.2 340 59 2 28   680 180 2
loop-invgen/nested6_true-unreach-call_true-termination.i 900     3200 5300    0 89     41 1000    0 850    470 2900    0 900     5500   13000    0 130   4000 1400 2 960   4000 8800 0 910   6100 8100 0 900    4100 8400   0 52    15000 540   0 900     1600 10000    0 900     2500 11000    0 900     4600 12000    0 910   1500 6100 0 880   320 9500 2 900    4700   9000   0 900     2200   11000    0 9.0 490 72 2 9.5 470 80 2 17   520 140 2 900   2800 6000 0
loop-invgen/nested9_true-unreach-call_true-termination.i 900     280 8400    0 .27  21 3.2  2 170    12000 1400    0 900     10000   12000    0 12   480 92 2 72   3400 510 0 900   6100 7800 0 900    6100 10000   0 32    15000 310   0 330     15000 3900    0 210     15000 2800    0 900     2500 2200    0 900   1600 7800 0 880   470 9900 2 900    1100   12000   0 900     5000   10000    0 8.9 440 66 2 16   510 150 2 9.5 410 72 2 82   950 810 2
loop-invgen/sendmail-close-angle_true-unreach-call_true-termination.i 900     2200 11000    0 8.9   35 98    0 850    4500 10000    0 900     9400   12000    0 16   610 120 2 880   6500 6900 0 900   9700 8800 0 230    82 3000   0 38    3500 460   2 900     4100 12000    0 900     11000 12000    0 .095 23 1.1  0 48   710 500 2 880   490 11000 2 900    1000   11000   0 900     1900   11000    0 16   640 140 1 20   550 180 2 25   630 240 1 820   2000 7200 2
loop-invgen/seq_true-unreach-call_true-termination.i 900     1500 10000    0 900     270 11000    0 850    600 6100    0 900     9100   11000    0 900   4000 10000 0 960   3900 9300 0 900   10000 10000 0 900    10000 8800   0 92    1200 1000   1 900     690 11000    0 900     1400 11000    0 900     2500 13000    0 900   1000 9900 0 880   320 14000 1 900    1900   10000   0 900     3300   11000    0 900   1600 12000 0 900   2500 11000 0 900   1600 12000 0 46   650 430 1
loop-invgen/string_concat-noarr_true-unreach-call_true-termination.i .12  23 .75 1 900     250 11000    0 850    9400 4600    0 900     660   9700    0 900   4300 8900 0 530   3100 4600 0 910   7300 8800 0 900    15000 10000   0 900    2800 10000   0 74     15000 810    0 74     15000 780    0 74     15000 780    0 900   1100 10000 0 880   670 9600 1 900    120   11000   0 900     4900   12000    0 900   1800 13000 0 900   3300 14000 0 9.2 380 68 1 520   530 4300 0
loop-invgen/up_true-unreach-call_true-termination.i 900     2100 9400    0 900     260 12000    0 850    1400 9000    0 900     11000   9700    0 900   4100 11000 0 23   1100 160 0 900   15000 8500 0 71    100 860   0 17    1000 210   1 900     10000 13000    0 570     15000 6900    0 380     15000 5200    0 900   1000 12000 0 880   530 13000 1 900    2000   9200   0 900     4400   11000    0 900   3100 12000 0 900   2700 13000 0 900   5400 13000 0 19   620 140 1
loop-lit/afnp2014_true-unreach-call_true-termination.c.i 900     2200 11000    0 1.1   21 14    2 14    150 160    2 900     610   11000    0 9.3 450 73 2 77   3300 660 2 12   730 110 2 86    76 1100   0 2.5  230 29   2 900     3500 12000    0 900     7700 13000    0 760     15000 8300    0 900   1000 10000 0 880   730 11000 2 6.2  13   83   2 47     200   580    2 6.6 330 49 2 900   1100 12000 0 7.4 350 54 2 15   520 110 2
loop-lit/bhmr2007_true-unreach-call_true-termination.c.i 900     300 12000    0 27     36 290    2 850    350 9200    0 900     11000   13000    0 2.8 270 25 1 960   3200 8500 0 900   2700 8300 0 900    2200 10000   0 130    880 1600   -16 900     84 12000    0 900     130 13000    0 900     190 14000    0 29   670 250 2 880   120 11000 2 900    50   11000   0 900     2300   11000    0 8.7 460 74 2 6.8 330 58 2 11   480 88 2 26   600 240 2
loop-lit/cggmp2005_true-unreach-call_true-termination.c.i .34  27 3.5  2 .36  22 3.6  2 .28 17 2.9  2 6.3   10   69    2 2.8 270 26 2 2.8 270 22 2 2.3 240 20 2 3.2  270 29   2 .14 23 1.6 2 900     9600 11000    0 .28  23 .79 2 .12  23 .75 2 9.2 380 77 2 1.3 82 15 2 .13 9.4 1.6 2 .079 9.8 .46 2 7.5 390 55 2 7.3 380 64 2 8.8 400 67 2 14   490 88 2
loop-lit/cggmp2005_variant_true-unreach-call_true-termination.c.i 900     1700 9200    0 .88  24 10    2 850    4000 5200    0 900     6200   11000    0 2.9 270 28 2 900   9000 7500 0 910   8900 10000 0 900    8500 9100   0 3.0  220 38   -16 900     3300 9200    0 900     7500 12000    0 900     11000 9700    0 8.2 350 71 2 330   630 4400 2 .17 9.3 1.5 2 .058 9.9 .49 2 8.2 390 65 2 6.9 330 57 2 8.8 410 77 2 17   600 110 2
loop-lit/cggmp2005b_true-unreach-call_true-termination.c.i .95  35 13    2 .57  20 5.2  2 .96 17 11    2 900     330   14000    0 4.6 290 37 2 4.3 270 31 2 3.5 260 27 2 4.5  260 42   2 6.8  990 63   2 900     5800 11000    0 .39  52 4.9  2 .10  23 .88 2 910   1700 6000 0 54   1000 650 2 .15 9.4 1.6 2 .064 9.8 .72 2 6.9 350 57 2 8.1 370 65 2 7.7 350 58 2 13   450 93 2
loop-lit/css2003_true-unreach-call_true-termination.c.i 900     260 10000    0 1.0   31 13    2 850    820 5100    0 900     9800   12000    0 3.0 270 27 2 3.9 280 29 2 3.0 270 25 2 51    77 660   0 5.0  510 62   2 450     15000 5400    0 220     15000 2600    0 150     15000 1800    0 900   1400 7100 0 410   470 6200 2 7.1  360   98   2 510     15000   6300    0 6.4 340 49 2 6.3 330 46 2 5.9 330 49 2 16   560 110 2
loop-lit/ddlm2013_true-unreach-call.i 900     2100 11000    0 16     30 180    -16 850    1300 9000    0 900     15000   13000    0 160   3700 1700 1 930   6200 9300 0 910   8400 9600 0 210    310 2200   0 4.7  440 62   1 170     15000 1400    0 330     15000 2600    0 .30  23 .72 0 900   1100 11000 0 880   310 11000 1 900    74   10000   0 900     3200   14000    0 900   2500 12000 0 900   1200 11000 0 11   520 90 1 310   1200 3600 0
loop-lit/gj2007_true-unreach-call_true-termination.c.i 5.2   82 65    2 900     290 9800    0 1.0  17 11    2 900     590   11000    0 60   3000 670 2 4.1 280 30 2 3.1 270 25 2 36    76 420   0 .15 23 2.0 2 900     5600 11000    0 .45  43 5.5  2 58     680 130    2 900   1000 11000 0 880   580 10000 0 .16 9.4 1.5 2 .075 9.9 .46 2 69   1700 650 2 140   1300 1800 2 86   1400 780 2 21   520 150 2
loop-lit/gj2007b_true-unreach-call_true-termination.c.i 900     1400 13000    0 2.6   32 21    2 850    2800 9000    0 900     12000   11000    0 20   640 160 2 900   4300 6100 0 900   3400 9500 0 210    130 2800   0 8.1  380 94   2 900     5100 13000    0 900     11000 11000    0 850     15000 11000    0 28   680 280 2 880   370 14000 2 900    1700   9000   0 900     920   12000    0 7.7 390 56 2 7.2 370 63 2 11   520 81 1 15   500 110 2
loop-lit/gr2006_true-unreach-call_true-termination.c.i 9.0   120 110    2 900     290 11000    0 .97 19 11    2 900     650   11000    0 67   2400 640 2 4.9 290 38 2 3.2 260 28 2 140    120 1800   0 .18 23 1.5 2 900     5000 11000    0 .49  48 6.8  2 14     740 160    2 900   1300 9300 0 550   440 7100 2 .15 9.3 1.7 2 .058 9.7 .66 2 59   1600 560 2 750   1400 13000 2 71   1700 680 2 21   600 170 2
loop-lit/gsv2008_true-unreach-call_true-termination.c.i 900     810 7200    0 .27  20 1.6  2 220    620 2000    2 900     8400   13000    0 3.4 270 32 1 860   5200 7900 2 880   4900 9900 2 900    620 7100   0 7.3  220 79   -16 900     1500 2300    0 900     6200 9400    0 900     8900 9200    0 17   520 170 2 880   330 12000 2 900    60   11000   0 610     15000   8900    0 7.0 340 54 2 7.3 360 58 2 7.1 370 50 2 130   540 1300 2
loop-lit/hhk2008_true-unreach-call_true-termination.c.i 900     390 14000    0 .80  23 9.9  2 850    260 11000    0 900     5200   13000    0 3.2 270 27 2 53   2000 430 0 910   8000 9100 0 900    8000 8800   0 2.7  150 33   -16 900     420 11000    0 900     740 13000    0 900     1000 14000    0 7.0 350 61 2 140   390 1900 2 .17 9.3 1.5 2 .13  18   1.2  2 8.9 410 66 2 6.6 330 46 2 8.1 370 67 2 15   510 100 2
loop-lit/jm2006_true-unreach-call_true-termination.c.i 900     1500 10000    0 2.4   35 21    0 850    6900 4400    0 900     5000   11000    0 2.8 280 25 2 4.8 300 32 2 2.8 260 24 2 3.8  270 38   2 1.4  140 16   -16 900     2300 12000    0 900     4900 11000    0 900     7600 11000    0 6.8 330 57 2 880   1000 11000 2 .16 9.8 1.7 2 .097 9.9 .77 2 8.7 450 62 2 6.7 330 48 2 9.9 500 74 2 18   640 130 2
loop-lit/jm2006_variant_true-unreach-call_true-termination.c.i 900     1700 11000    0 6.0   35 62    2 850    5300 3900    0 900     5100   13000    0 4.0 280 32 2 900   8300 6800 0 910   10000 8400 0 900    10000 8300   0 2.0  210 27   -16 900     2000 11000    0 900     4800 12000    0 900     8000 12000    0 9.2 380 75 2 290   620 3400 2 .15 9.9 1.7 2 .10  9.9 .96 2 8.8 450 63 2 6.5 320 50 2 11   470 88 2 16   610 110 2
loop-lit/mcmillan2006_true-unreach-call_true-termination.c.i 890     15000 6700    0 .33  21 2.9  -16 850    6000 8000    0 .10  7.8 1.1  0 3.5 280 33 -16 900   3900 11000 0 960   1000 12000 0 890    100 11000   0 900    880 11000   0 900     150 9200    0 900     180 10000    0 900     210 10000    0 5.7 350 41 0 880   360 10000 1 140    330   1800   0 .052 9.9 .64 0 900   960 13000 0 900  <