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 false(unreach-call) .13  23 1.2  1 false(unreach-call) .42  21 4.5  1 false(unreach-call) .11 17 .89 1 aborted .11  7.9 1.1  0 false(unreach-call) 3.2 300 29 1 false(unreach-call) 3.9 290 31 1 false(unreach-call) 2.6 250 24 1 false(unreach-call) 1.1  76 14   1 false(unreach-call) .19 23 1.9 1 false(unreach-call) .099 23 1.1  1 false(unreach-call) .12  23 1.0  1 false(unreach-call) .10  23 1.1  1 false(unreach-call) 6.1 340 49 1 false(unreach-call) 1.6 77 19 1 false(unreach-call) .18 10   1.6 1 false(unreach-call) .074 9.8 .56 1 false(unreach-call) 5.6 320 46 1 false(unreach-call) 7.2 380 58 1 false(unreach-call) 6.2 330 53 1 false(unreach-call) 10   290 84 1
loops/bubble_sort_false-unreach-call.i error (134) .40  62 4.0  0 exception (gremlins) .059 20 .73 0 error (1) .30 26 3.1  0 aborted .13  8.2 1.5  0 false(unreach-call) 5.2 310 45 0 unknown 440   1900 5000 0 unknown 420   2500 5500 0 false(unreach-call) 3.0  240 42   0 out of memory 230    15000 1900   0 false(unreach-call) .64  49 6.9  1 false(unreach-call) .66  49 8.1  1 false(unreach-call) .65  50 8.5  1 unknown 38   1100 300 0 false(unreach-call) 2.4 90 31 1 false(unreach-call) .25 10   2.4 1 unknown .086 10   .55 0 error 8.6 320 73 0 error 8.4 310 67 0 error 9.2 320 72 0 false(unreach-call) 290   2100 2300 1
loops/count_up_down_false-unreach-call_true-termination.i false(unreach-call) .13  22 .87 1 false(unreach-call) .068 20 .77 1 false(unreach-call) .12 17 .90 1 false(unreach-call) .16  7.8 1.6  1 false(unreach-call) 2.9 280 26 1 false(unreach-call) 6.1 410 41 1 false(unreach-call) 2.4 250 23 1 false(unreach-call) .55 75 7.1 1 false(unreach-call) 1.2  130 13   1 false(unreach-call) .11  23 .68 1 false(unreach-call) .072 23 .80 1 false(unreach-call) .093 23 .65 1 false(unreach-call) 4.9 300 40 1 false(unreach-call) 1.6 78 21 1 false(unreach-call) .16 9.5 1.6 1 false(unreach-call) .088 9.7 .40 1 false(unreach-call) 5.4 320 43 1 false(unreach-call) 5.5 320 47 1 false(unreach-call) 6.0 340 48 1 false(unreach-call) 9.5 280 76 1
loops/eureka_01_false-unreach-call.i false(unreach-call) 1.4   43 16    1 false(unreach-call) 1.1   33 11    0 false(unreach-call) .39 26 3.9  1 aborted .10  7.7 1.1  0 true 21   800 190 -32 false(unreach-call) 520   4000 5200 0 timeout 960   2900 14000 0 false(unreach-call) 2.9  190 34   0 timeout 900    7800 6800   0 false(unreach-call) .15  23 1.9  0 false(unreach-call) .17  24 1.9  0 false(unreach-call) .23  24 2.1  0 unknown 15   660 130 0 false(unreach-call) 2.7 94 35 1 false(unreach-call) .44 13   5.2 0 true 83     580   1000    -32 false(unreach-call) 60   820 730 1 false(unreach-call) 140   970 1700 1 false(unreach-call) 88   1000 950 1 false(unreach-call) 47   1100 380 1
loops/for_bounded_loop1_false-unreach-call_true-termination.i false(unreach-call) .24  26 2.3  1 false(unreach-call) .40  24 3.7  1 false(unreach-call) .12 17 .99 1 false(unreach-call) .99  7.8 10    1 false(unreach-call) 3.3 290 34 1 false(unreach-call) 12   710 78 1 false(unreach-call) 3.3 280 28 1 false(unreach-call) 1.3  110 15   1 false(unreach-call) 890    4300 9200   1 false(unreach-call) .076 23 .83 1 false(unreach-call) .11  23 .71 1 false(unreach-call) .093 23 .86 1 false(unreach-call) 7.0 360 56 1 false(unreach-call) 1.7 77 22 1 false(unreach-call) .18 9.2 1.6 0 false(unreach-call) .084 9.9 .91 1 false(unreach-call) 6.9 340 50 1 false(unreach-call) 7.3 360 54 1 false(unreach-call) 8.4 380 68 1 false(unreach-call) 10   280 79 1
loops/insertion_sort_false-unreach-call_true-termination.i false(unreach-call) 380     6400 2000    1 false(unreach-call) 3.5   24 40    0 false(unreach-call) 2.4  320 26    1 aborted .10  8.2 1.0  0 error 4.1 310 34 0 segmentation fault 55   2200 390 0 unknown 240   1500 2800 0 false(unreach-call) 3.6  130 56   1 timeout 900    3000 7800   0 false(unreach-call) .66  23 7.5  1 false(unreach-call) 2.9   25 5.9  1 false(unreach-call) .84  30 11    1 timeout 900   1700 8200 0 false(unreach-call) 2.6 82 37 1 unknown .18 10   1.7 0 unknown .057 9.7 .43 0 false(unreach-call) 64   1100 650 1 false(unreach-call) 42   650 500 1 timeout 900   8800 6100 0 out of memory 96   15000 1300 0
loops/invert_string_false-unreach-call_true-termination.i false(unreach-call) .68  36 8.4  1 false(unreach-call) .86  30 8.5  1 false(unreach-call) .51 38 4.8  1 aborted .12  7.7 1.0  0 false(unreach-call) 5.2 320 46 1 false(unreach-call) 31   1700 230 1 false(unreach-call) 220   1100 2700 1 false(unreach-call) 1.9  130 26   1 false(unreach-call) 890    1700 13000   1 false(unreach-call) .16  23 1.9  1 false(unreach-call) .18  23 2.3  1 false(unreach-call) .19  23 2.0  1 false(unreach-call) 14   640 130 1 false(unreach-call) 1.9 80 23 1 error .19 10   1.8 0 unknown .072 9.5 .45 0 false(unreach-call) 11   480 94 1 false(unreach-call) 12   500 92 1 false(unreach-call) 13   490 120 1 out of memory 110   15000 1200 0
loops/linear_search_false-unreach-call.i false(unreach-call) 1.1   58 11    1 false(unreach-call) .099 20 .75 0 false(unreach-call) .85 23 9.8  1 aborted .10  44   2.8  0 error 3.2 290 26 0 false(unreach-call) 15   580 100 1 false(unreach-call) 12   560 110 1 false(unreach-call) 16    76 250   0 false(unreach-call) 1.3  85 17   0 false(unreach-call) .50  41 6.3  0 false(unreach-call) .84  66 11    0 false(unreach-call) 2.4   120 34    0 unknown 6.1 350 50 0 false(unreach-call) 11   93 150 1 error .24 21   2.2 0 unknown .052 9.8 .53 0 timeout 900   810 10000 0 timeout 900   4600 9200 0 timeout 900   2600 12000 0 false(unreach-call) 9.8 280 72 0
loops/ludcmp_false-unreach-call.i timeout 900     3500 9200    0 false(unreach-call) 1.3   30 15    0 false(unreach-call) 5.0  130 76    0 out of memory 17     15000   210    0 false(unreach-call) 11   1000 110 1 timeout 960   1900 12000 0 false(unreach-call) 32   3800 310 1 false(unreach-call) 7.1  350 100   0 out of memory 9.7  15000 120   0 false(unreach-call) 2.1   31 29    0 false(unreach-call) 2.1   33 30    0 false(unreach-call) 3.5   80 46    0 unknown 10   680 94 0 false(unreach-call) 82   560 1100 1 false(unreach-call) .15 9.4 1.9 1 unknown .064 9.9 .53 0 error 78   13000 660 0 error 63   12000 630 0 error 75   13000 680 0 false(unreach-call) 270   1300 2800 1
loops/matrix_false-unreach-call_true-termination.i false(unreach-call) 64     1900 370    1 exception (gremlins) .049 11 .61 0 false(unreach-call) .15 21 1.3  1 aborted .12  7.9 1.2  0 false(unreach-call) 16   660 180 1 false(unreach-call) 59   2200 450 1 false(unreach-call) 100   2200 1000 1 false(unreach-call) 480    180 5400   1 timeout 900    6500 7100   0 false(unreach-call) .12  23 1.3  1 false(unreach-call) .11  23 1.6  1 false(unreach-call) .15  23 1.2  1 unknown 5.9 320 47 0 false(unreach-call) 1.9 81 23 1 timeout (timeout) 900    2400   8800   0 unknown .054 9.8 .50 0 false(unreach-call) 7.6 370 59 1 false(unreach-call) 8.2 370 70 1 false(unreach-call) 7.3 360 54 1 out of memory 66   15000 730 0
loops/n.c24_false-unreach-call.i timeout 900     6800 6800    0 timeout 900     320 9800    0 out of memory 190    15000 2100    0 aborted .10  8.0 1.1  0 timeout 900   4300 9200 0 timeout 900   5000 8100 0 timeout 900   3900 7900 0 unknown 900    1400 7200   0 out of memory 80    15000 760   0 out of memory 340     15000 3900    0 out of memory 310     15000 3600    0 timeout 900     1000 1900    0 unknown 5.1 330 41 0 timeout 880   1400 6900 0 timeout (timeout) 900    3800   10000   0 unknown 7.8   360   82    0 timeout 900   4600 11000 0 timeout 900   3700 14000 0 timeout 900   4400 12000 0 out of memory 850   15000 8400 0
loops/nec11_false-unreach-call_false-termination.i false(unreach-call) .11  22 .83 1 false(unreach-call) .089 22 .72 1 false(unreach-call) .13 17 .98 1 aborted .11  7.8 1.2  0 false(unreach-call) 2.9 270 29 1 false(unreach-call) 3.7 290 31 1 false(unreach-call) 2.4 250 22 1 false(unreach-call) .54 76 6.4 1 false(unreach-call) 1.8  140 20   1 false(unreach-call) .073 23 .80 1 false(unreach-call) .10  23 .73 1 false(unreach-call) .072 23 .90 1 false(unreach-call) 5.3 320 41 1 false(unreach-call) 1.7 75 20 1 false(unreach-call) .16 9.3 1.7 1 false(unreach-call) .086 9.8 .47 1 false(unreach-call) 5.9 330 45 1 false(unreach-call) 5.5 340 45 1 false(unreach-call) 6.1 340 45 1 false(unreach-call) 9.5 280 71 1
loops/nec20_false-unreach-call_true-termination.i false(unreach-call) .91  56 8.2  1 false(unreach-call) .21  23 2.1  1 false(unreach-call) .25 39 3.4  1 aborted .12  7.9 1.1  0 false(unreach-call) 3.3 300 32 1 false(unreach-call) 6.7 450 47 1 false(unreach-call) 4.0 460 43 1 false(unreach-call) 1.2  76 14   1 false(unreach-call) 1.0  130 11   1 false(unreach-call) .077 23 .89 1 false(unreach-call) .073 23 .85 1 false(unreach-call) .084 23 .71 1 timeout 900   1000 12000 0 false(unreach-call) 1.7 82 25 1 false(unreach-call) .18 9.4 1.6 1 false(unreach-call) .060 9.5 .46 1 false(unreach-call) 5.9 330 45 1 false(unreach-call) 5.8 320 48 1 false(unreach-call) 5.9 330 45 1 false(unreach-call) 25   290 230 1
loops/s3_false-unreach-call.i error (134) 210     860 1400    0 false(unreach-call) 18     40 130    1 false(unreach-call) 26    1200 320    1 aborted .13  8.7 1.4  0 false(unreach-call) 11   490 79 0 out of memory 240   15000 2000 0 out of memory 180   15000 2100 0 unknown 890    1600 11000   0 out of memory 350    15000 3900   0 false(unreach-call) 370     2600 3600    1 timeout 900     3600 8800    0 false(unreach-call) 810     4000 8000    1 unknown 32   1100 250 0 false(unreach-call) 15   210 160 1 error .36 12   4.6 0 unknown .066 11   .60 0 timeout 900   2500 11000 0 error 680   2000 8500 0 false(unreach-call) 810   1600 9400 1 false(unreach-call) 110   2500 1100 1
loops/string_false-unreach-call_true-termination.i false(unreach-call) 2.0   45 21    1 false(unreach-call) 1.1   23 12    1 false(unreach-call) .26 19 2.8  1 aborted .12  7.9 .99 0 false(unreach-call) 5.3 320 40 1 false(unreach-call) 7.1 360 56 1 false(unreach-call) 3.2 250 32 1 false(unreach-call) 4.1  190 61   1 false(unreach-call) 890    1000 9100   1 false(unreach-call) .15  23 1.8  1 false(unreach-call) .16  23 1.9  1 false(unreach-call) .41  28 4.7  1 unknown 6.6 330 53 0 false(unreach-call) 1.9 86 23 0 false(unreach-call) .18 9.9 2.0 1 false(unreach-call) .18  9.8 1.8  1 false(unreach-call) 17   490 150 1 false(unreach-call) 16   470 110 1 false(unreach-call) 16   460 140 1 witness invalid (false(unreach-call)) 12   320 90 0
loops/sum01_bug02_false-unreach-call_true-termination.i false(unreach-call) .60  31 6.5  1 false(unreach-call) 18     34 210    1 false(unreach-call) .40 17 4.3  1 false(unreach-call) 16     40   190    1 false(unreach-call) 4.0 290 31 1 false(unreach-call) 9.0 500 65 1 false(unreach-call) 4.1 300 35 1 false(unreach-call) 3.9  110 46   1 false(unreach-call) .92 130 10   1 false(unreach-call) .092 23 1.1  1 false(unreach-call) .10  23 1.1  1 false(unreach-call) .15  26 1.6  1 false(unreach-call) 66   690 800 1 false(unreach-call) 1.7 76 25 1 false(unreach-call) .15 9.3 1.7 1 false(unreach-call) .16  12   1.6  1 false(unreach-call) 10   490 73 1 false(unreach-call) 10   490 80 1 false(unreach-call) 12   490 99 1 false(unreach-call) 12   300 90 1
loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i false(unreach-call) .36  29 4.4  1 false(unreach-call) 8.8   30 120    1 false(unreach-call) .28 17 2.1  1 false(unreach-call) 8.5   53   75    1 false(unreach-call) 3.6 290 32 1 false(unreach-call) 7.7 470 49 1 false(unreach-call) 3.5 290 31 1 false(unreach-call) 2.7  76 38   1 false(unreach-call) 1.8  140 27   0 false(unreach-call) .11  23 .83 1 false(unreach-call) .34  23 .70 1 false(unreach-call) .13  23 1.1  1 false(unreach-call) 8.7 380 65 1 false(unreach-call) 1.7 87 20 1 false(unreach-call) .18 9.3 1.6 1 false(unreach-call) .15  12   1.3  1 false(unreach-call) 8.2 430 62 1 false(unreach-call) 8.3 380 66 1 false(unreach-call) 10   490 79 1 false(unreach-call) 81   310 840 1
loops/sum01_false-unreach-call_true-termination.i false(unreach-call) .41  28 6.0  1 false(unreach-call) 29     36 310    1 false(unreach-call) .43 17 3.5  1 false(unreach-call) 62     250   760    1 false(unreach-call) 4.0 300 39 1 false(unreach-call) 9.8 490 67 1 false(unreach-call) 4.9 300 47 1 false(unreach-call) 5.9  76 77   1 false(unreach-call) .63 81 8.0 1 false(unreach-call) .14  23 1.3  1 false(unreach-call) .14  25 1.7  1 false(unreach-call) .20  33 2.3  1 false(unreach-call) 410   700 4200 1 false(unreach-call) 1.9 82 22 1 false(unreach-call) .16 9.4 2.0 1 false(unreach-call) .20  12   2.7  1 false(unreach-call) 10   480 83 1 false(unreach-call) 11   490 91 1 false(unreach-call) 13   550 99 1 false(unreach-call) 13   350 100 1
loops/sum03_false-unreach-call_true-termination.i false(unreach-call) .25  26 2.7  1 false(unreach-call) 4.3   32 43    0 false(unreach-call) .38 17 3.9  1 false(unreach-call) 55     38   580    1 false(unreach-call) 4.1 300 34 1 false(unreach-call) 4.9 290 37 1 false(unreach-call) 3.3 260 29 1 false(unreach-call) 5.7  75 72   1 false(unreach-call) .22 23 2.8 1 false(unreach-call) .093 23 1.0  1 false(unreach-call) .11  23 1.1  1 false(unreach-call) .18  26 1.8  1 false(unreach-call) 24   680 240 1 false(unreach-call) 2.6 87 32 1 false(unreach-call) .14 9.4 2.0 0 false(unreach-call) .096 11   .51 1 false(unreach-call) 13   530 95 1 false(unreach-call) 22   530 190 1 false(unreach-call) 15   550 120 1 false(unreach-call) 15   460 110 1
loops/sum04_false-unreach-call_true-termination.i false(unreach-call) .42  28 4.7  1 false(unreach-call) .95  23 11    1 false(unreach-call) .41 17 3.7  1 unknown .063 43   .76 0 false(unreach-call) 3.3 280 29 1 false(unreach-call) 4.0 290 29 1 false(unreach-call) 2.6 250 23 1 false(unreach-call) 4.6  76 57   1 false(unreach-call) .17 23 1.3 1 false(unreach-call) .073 23 .80 1 false(unreach-call) .11  23 .85 1 false(unreach-call) .13  23 1.7  1 false(unreach-call) 17   570 160 1 false(unreach-call) 1.5 75 21 1 false(unreach-call) .16 9.2 1.5 1 false(unreach-call) .086 11   .58 1 false(unreach-call) 6.7 340 53 1 false(unreach-call) 7.7 350 60 1 false(unreach-call) 8.1 400 60 1 false(unreach-call) 11   300 86 1
loops/sum_array_false-unreach-call.i false(unreach-call) .31  36 3.8  1 false(unreach-call) .52  25 6.6  1 false(unreach-call) .11 20 1.0  1 aborted .11  7.7 .90 0 false(unreach-call) 3.9 310 39 1 false(unreach-call) 32   1700 180 1 false(unreach-call) 5.1 320 49 1 false(unreach-call) 1.4  160 18   1 false(unreach-call) 52    2100 720   1 false(unreach-call) .15  23 2.0  1 false(unreach-call) .16  23 2.0  1 false(unreach-call) .15  23 1.7  1 false(unreach-call) 14   660 110 1 false(unreach-call) 1.9 91 22 1 unknown .20 10   1.8 0 unknown .079 9.8 .46 0 false(unreach-call) 6.7 330 53 1 false(unreach-call) 7.6 330 56 1 false(unreach-call) 7.0 340 57 1 false(unreach-call) 15   290 120 1
loops/terminator_01_false-unreach-call_true-termination.i false(unreach-call) .11  22 .82 1 false(unreach-call) .082 17 .75 1 false(unreach-call) .12 17 .75 1 aborted .11  7.7 1.2  0 false(unreach-call) 3.0 280 27 1 false(unreach-call) 3.5 280 29 1 false(unreach-call) 2.4 250 20 1 false(unreach-call) .54 75 6.0 1 false(unreach-call) .60 81 6.7 1 false(unreach-call) .077 23 .73 1 false(unreach-call) .072 23 .82 1 false(unreach-call) .11  23 .68 1 false(unreach-call) 5.1 330 41 1 false(unreach-call) 1.6 80 20 1 false(unreach-call) .17 9.5 1.4 1 false(unreach-call) .064 9.8 .45 1 false(unreach-call) 6.9 350 52 1 false(unreach-call) 5.7 320 45 1 false(unreach-call) 6.8 330 54 1 false(unreach-call) 9.4 280 63 1
loops/terminator_02_false-unreach-call_true-termination.i false(unreach-call) .10  22 .95 1 false(unreach-call) .096 19 .54 1 false(unreach-call) .14 19 .93 1 aborted .15  7.9 1.6  0 false(unreach-call) 3.0 280 31 1 false(unreach-call) 3.6 280 29 1 false(unreach-call) 2.4 250 20 1 false(unreach-call) .40 75 4.7 1 false(unreach-call) 16    920 170   1 false(unreach-call) .10  23 .73 1 false(unreach-call) .080 23 .84 1 false(unreach-call) .082 23 .79 1 false(unreach-call) 5.2 340 39 1 false(unreach-call) 1.7 85 22 1 false(unreach-call) .18 9.4 1.8 1 false(unreach-call) .092 12   .92 1 false(unreach-call) 5.9 320 43 1 false(unreach-call) 5.5 320 43 1 false(unreach-call) 5.6 340 42 1 false(unreach-call) 9.2 280 73 1
loops/terminator_03_false-unreach-call_true-termination.i false(unreach-call) .12  22 .76 1 false(unreach-call) .14  20 1.3  1 false(unreach-call) .11 17 .98 1 false(unreach-call) .46  7.6 5.1  1 false(unreach-call) 3.3 280 32 1 false(unreach-call) 4.5 330 34 1 false(unreach-call) 3.0 280 24 1 false(unreach-call) .56 75 6.4 1 false(unreach-call) 13    160 150   1 false(unreach-call) .074 23 .86 1 false(unreach-call) .077 23 .78 1 false(unreach-call) .10  23 .82 1 false(unreach-call) 6.0 340 50 1 false(unreach-call) 1.7 86 22 1 false(unreach-call) .17 9.3 1.6 1 false(unreach-call) .12  9.9 1.7  1 false(unreach-call) 6.1 320 55 1 false(unreach-call) 6.1 330 44 1 false(unreach-call) 5.7 330 45 1 false(unreach-call) 9.6 290 66 1
loops/trex01_false-unreach-call_true-termination.i false(unreach-call) .13  23 .95 1 false(unreach-call) .11  19 .50 1 false(unreach-call) .14 18 .90 1 false(unreach-call) .19  7.8 1.9  1 false(unreach-call) 3.1 280 25 1 false(unreach-call) 5.0 320 38 1 false(unreach-call) 2.5 250 24 1 false(unreach-call) .61 160 6.6 1 false(unreach-call) 42    1800 490   1 false(unreach-call) .076 23 .99 1 false(unreach-call) .082 23 .79 1 false(unreach-call) .11  23 .81 1 false(unreach-call) 7.7 450 63 1 false(unreach-call) 1.7 78 20 1 false(unreach-call) .18 9.4 1.8 1 false(unreach-call) .084 10   .55 1 false(unreach-call) 5.7 320 47 1 false(unreach-call) 6.0 320 51 1 false(unreach-call) 5.9 320 41 1 false(unreach-call) 10   280 68 1
loops/trex02_false-unreach-call_true-termination.i false(unreach-call) .11  22 .97 1 false(unreach-call) .064 21 .61 1 false(unreach-call) .11 17 1.1  1 aborted .10  7.9 .92 0 false(unreach-call) 2.8 280 28 1 false(unreach-call) 3.5 280 30 1 false(unreach-call) 2.5 250 21 1 false(unreach-call) .36 75 4.1 1 false(unreach-call) 15    890 200   0 false(unreach-call) .079 23 .86 1 false(unreach-call) .074 23 .81 1 false(unreach-call) .11  23 .70 1 false(unreach-call) 5.2 330 39 1 false(unreach-call) 1.7 82 20 1 false(unreach-call) .15 10   1.8 1 false(unreach-call) .077 9.7 .74 1 false(unreach-call) 5.8 320 46 1 false(unreach-call) 5.5 320 43 1 false(unreach-call) 5.9 340 49 1 false(unreach-call) 9.8 290 70 1
loops/trex03_false-unreach-call_true-termination.i false(unreach-call) .11  23 .93 1 false(unreach-call) .11  21 .62 1 false(unreach-call) .15 18 .98 1 false(unreach-call) .37  7.8 4.1  1 false(unreach-call) 3.1 300 28 1 false(unreach-call) 4.5 330 31 1 false(unreach-call) 2.9 290 26 1 false(unreach-call) .38 76 4.6 1 false(unreach-call) 9.7  510 110   1 false(unreach-call) .080 23 2.0  1 false(unreach-call) .10  23 .75 1 false(unreach-call) .11  23 .83 1 false(unreach-call) 5.8 320 44 1 false(unreach-call) 1.8 83 26 1 false(unreach-call) .19 10   1.8 1 false(unreach-call) .17  9.8 1.9  1 false(unreach-call) 5.7 320 41 1 false(unreach-call) 6.3 320 52 1 false(unreach-call) 5.3 320 45 1 false(unreach-call) 11   280 74 1
loops/verisec_NetBSD-libc__loop_false-unreach-call_true-termination.i false(unreach-call) .11  23 1.1  1 false(unreach-call) .43  22 4.1  1 false(unreach-call) .28 17 2.6  1 unknown .031 7.8 .29 0 false(unreach-call) 3.3 300 29 1 false(unreach-call) 3.9 300 33 1 false(unreach-call) 2.7 250 21 1 false(unreach-call) 1.4  75 21   1 false(unreach-call) 10    1200 110   1 false(unreach-call) .099 23 .94 1 false(unreach-call) .084 23 .93 1 false(unreach-call) .12  23 .97 1 unknown 5.4 340 46 0 false(unreach-call) 1.7 86 21 1 false(unreach-call) .16 9.3 1.6 0 false(unreach-call) .087 9.8 .49 1 false(unreach-call) 8.2 400 74 1 false(unreach-call) 7.2 330 54 1 false(unreach-call) 9.7 370 77 1 false(unreach-call) 10   290 73 1
loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call_true-termination.i false(unreach-call) .47  33 5.6  1 false(unreach-call) 30     36 320    1 false(unreach-call) .35 23 3.7  1 unknown .035 7.8 .34 0 false(unreach-call) 3.9 300 34 1 false(unreach-call) 23   880 150 1 false(unreach-call) 3.0 270 25 1 false(unreach-call) 2.1  130 25   1 timeout 900    1800 10000   0 false(unreach-call) .16  23 1.2  1 false(unreach-call) .17  24 1.7  1 unknown .13  24 1.1  0 unknown 5.7 350 39 0 false(unreach-call) 2.0 86 25 0 false(unreach-call) .21 10   2.2 1 unknown .11  10   1.2  0 false(unreach-call) 14   560 120 1 false(unreach-call) 9.7 490 75 1 false(unreach-call) 16   510 130 1 false(unreach-call) 18   290 150 1
loops/vogal_false-unreach-call.i false(unreach-call) 7.2   150 72    1 timeout 900     330 11000    0 false(unreach-call) .54 27 5.4  1 aborted .11  7.7 1.2  0 false(unreach-call) 6.5 360 53 1 false(unreach-call) 98   2300 880 0 false(unreach-call) 18   270 24 1 false(unreach-call) 13    210 160   0 out of memory 140    15000 1400   0 false(unreach-call) .57  38 7.1  0 false(unreach-call) .60  40 6.6  0 false(unreach-call) 6.3   160 69    0 unknown 6.2 350 44 0 false(unreach-call) 5.2 110 61 0 false(unreach-call) .18 10   1.9 1 true 6.1   63   84    -32 timeout 900   1200 12000 0 false(unreach-call) 32   790 270 1 timeout 900   1200 12000 0 false(unreach-call) 18   460 130 1
loops/while_infinite_loop_4_false-unreach-call_true-termination.i false(unreach-call) .11  22 .90 1 false(unreach-call) .10  21 .51 1 false(unreach-call) .11 17 .78 1 unknown .046 7.7 .27 0 false(unreach-call) 2.9 270 28 1 false(unreach-call) 3.4 290 27 1 false(unreach-call) 2.4 250 22 1 false(unreach-call) .37 75 4.2 1 false(unreach-call) .22 23 2.1 1 false(unreach-call) .077 23 .68 1 false(unreach-call) .10  23 .73 1 false(unreach-call) .086 23 .75 1 false(unreach-call) 4.6 330 35 1 false(unreach-call) 1.6 76 24 1 false(unreach-call) .13 9.3 1.6 1 false(unreach-call) .057 9.6 .46 1 false(unreach-call) 6.5 340 48 1 false(unreach-call) 6.1 330 43 1 false(unreach-call) 5.8 320 46 1 false(unreach-call) 9.8 280 72 1
loops/array_true-unreach-call_true-termination.i true .13  23 .86 2 true .64  23 7.2  2 true .19 19 1.7  2 aborted .11  8.1 .97 0 true 3.0 280 24 2 true 4.2 310 31 2 true 3.2 270 27 2 true 4.2  280 38   2 true .19 23 1.8 2 out of memory 170     15000 2400    0 true .12  23 .86 2 true .083 23 .93 2 true 11   440 91 2 true 1.2 73 15 2 true .15 10   1.7 2 true .074 9.8 .44 2 true 7.3 360 57 2 true 6.0 320 47 2 true 12   360 95 2 true 510   870 6100 2
loops/bubble_sort_true-unreach-call.i true 1.1   77 8.2  2 true .055 18 .60 2 error (42) 850    14000 5100    0 aborted .11  7.9 1.2  0 true 2.7 260 23 2 true 3.1 280 25 2 true 93   2200 1200 2 unknown 900    450 10000   0 timeout 900    7000 5500   0 timeout 900     1100 8900    0 timeout 900     5100 11000    0 true .10  23 1.3  2 unknown 6.3 380 47 0 true 1.4 86 15 2 true .18 9.4 1.6 2 unknown .058 9.9 .54 0 true 5.8 320 45 2 true 6.7 350 57 2 true 6.0 320 51 2 true 6.8 280 51 2
loops/count_up_down_true-unreach-call_true-termination.i timeout 900     1500 11000    0 false(unreach-call) .064 21 .65 -16 error (42) 850    7200 6000    0 timeout 900     7000   13000    0 error 2.8 270 27 0 timeout 900   8900 8200 0 timeout 910   11000 8200 0 unknown 69    75 900   0 false(unreach-call) 1.3  140 18   -16 timeout 900     2200 11000    0 timeout 900     5500 12000    0 timeout 900     9900 13000    0 true 7.3 360 65 2 true 880   1200 11000 2 true .14 9.3 1.3 2 true .053 9.8 .51 2 true 75   480 880 1 true 49   380 560 2 true 43   480 580 1 true 15   510 110 2
loops/eureka_01_true-unreach-call.i true 16     710 150    1 timeout 900     600 10000    0 true .95 23 11    1 aborted .11  7.8 1.1  0 true 9.4 450 82 1 true 6.6 350 40 1 true 3.6 260 32 1 unknown 890    330 7300   0 true 20    3000 270   1 out of memory 400     15000 6000    0 true .31  38 5.0  1 timeout 900     430 8900    0 unknown 8.5 430 70 0 timeout 880   1100 8100 0 true .17 9.1 1.6 1 true .25  32   2.5  1 timeout 900   3300 12000 0 error 230   1600 3300 0 timeout 900   9400 8400 0 true 12   260 99 1
loops/eureka_05_true-unreach-call_true-termination.i true 2.3   68 28    2 false(unreach-call) 5.7   34 63    -16 true .31 17 2.8  2 unknown .035 7.9 .28 0 true 5.3 290 45 2 true 4.0 280 33 2 true 2.7 250 22 2 true 6.1  260 64   2 true 7.9  1100 100   2 out of memory 130     15000 1900    0 true .083 23 1.1  2 true .22  26 2.0  2 timeout 900   1400 11000 0 true 1.6 82 18 2 true .16 9.2 1.4 2 true .063 9.8 .69 2 true 28   900 220 2 true 59   1000 660 1 timeout 900   3900 8700 0 true 11   270 82 2
loops/for_infinite_loop_1_true-unreach-call_false-termination.i true .088 22 .79 2 true .052 15 .56 2 out of memory 250    15000 3800    0 aborted .13  7.9 1.4  0 true 2.6 270 23 2 true 3.0 270 24 2 true 93   2200 1100 2 unknown 37    75 510   0 true .23 31 2.5 2 timeout 900     13000 12000    0 out of memory 410     15000 6800    0 true .28  23 .55 2 true 6.0 350 49 2 true 1.3 78 18 2 timeout (timeout) 890    15000   13000   0 true .077 9.4 .63 2 true 6.1 340 51 2 true 6.6 330 53 2 true 6.2 320 49 2 true 9.4 300 77 2
loops/for_infinite_loop_2_true-unreach-call_false-termination.i true .10  22 .72 2 true .053 16 .50 2 out of memory 260    15000 3500    0 aborted .13  7.9 1.4  0 true 2.6 260 24 2 true 2.9 270 23 2 true 93   2300 1100 2 unknown 37    75 400   0 false(unreach-call) .19 23 2.1 -16 timeout 900     13000 13000    0 out of memory 420     15000 5800    0 true .077 23 .75 2 true 6.0 340 47 2 true 1.3 75 18 2 timeout (timeout) 890    15000   11000   0 true .054 9.7 .49 2 true 6.2 340 53 2 true 6.2 330 45 2 true 6.1 330 47 2 true 9.2 290 64 2
loops/insertion_sort_true-unreach-call_true-termination.i timeout 900     5100 4900    0 false(unreach-call) 3.0   23 40    -16 error (42) 850    3100 3700    0 aborted .14  8.1 1.3  0 error 4.1 310 34 0 timeout 910   4200 6800 0 timeout 900   2000 7300 0 unknown 890    160 10000   0 timeout 900    6000 8200   0 timeout 900     120 11000    0 timeout 900     130 11000    0 timeout 900     160 11000    0 timeout 900   1400 7800 0 timeout 880   240 12000 0 unknown .16 9.9 2.0 0 unknown .080 9.9 .47 0 timeout 900   1600 12000 0 timeout 900   1200 12000 0 timeout 900   2500 8200 0 out of memory 49   15000 630 0
loops/invert_string_true-unreach-call_true-termination.i true .85  35 9.9  2 false(unreach-call) 1.5   37 17    -16 true .32 17 3.2  2 aborted .11  8.2 1.1  0 error 5.1 320 44 0 true 21   720 180 2 true 14   450 140 2 true 17    460 180   2 true .18 24 2.1 2 out of memory 110     15000 1300    0 true .089 23 .97 2 true .18  24 2.0  2 true 46   700 580 2 true 1.6 95 19 2 true .17 9.3 1.8 2 true .083 9.9 .76 2 true 35   640 310 2 true 81   680 940 2 true 61   740 610 2 true 650   910 7300 2
loops/linear_sea.ch_true-unreach-call.i timeout 900     3900 7700    0 false(unreach-call) .070 18 .83 -16 error (1) 810    11000 3600    0 aborted .11  8.0 1.0  0 error 3.2 300 26 0 timeout 900   6900 10000 0 timeout 900   6200 9500 0 unknown 110    76 1400   0 true 4.8  110 67   1 timeout 900     5800 13000    0 timeout 900     11000 13000    0 timeout 900     9900 8200    0 unknown 6.2 360 55 0 true 880   160 11000 1 unknown .19 10   1.9 0 unknown .052 9.4 .51 0 timeout 900   640 12000 0 timeout 900   1100 11000 0 timeout 900   2400 11000 0 true 640   850 6200 1
loops/lu.cmp_true-unreach-call.i true 290     3500 3100    1 true 47     64 580    1 true 11    210 140    1 out of memory 17     15000   220    0 true 4.2 290 37 1 true 4.9 320 38 1 true 2.9 260 25 1 true 9.2  350 120   1 out of memory 9.8  15000 110   0 timeout 900     5200 12000    0 true .14  24 1.5  1 true 1.5   68 19    1 unknown 11   710 96 0 true 290   1100 2900 1 true .17 9.4 1.6 1 unknown .064 10   .48 0 error 78   13000 810 0 error 63   12000 570 0 error 76   13000 830 0 true 270   1200 2600 1
loops/matrix_true-unreach-call_true-termination.i true .15  25 1.5  2 exception (gremlins) .086 11 .41 0 true .19 17 1.6  2 aborted .13  7.9 1.0  0 true 3.1 290 28 2 true 9.9 480 69 2 true 13   370 170 2 true 14    370 170   2 true 26    1700 330   2 out of memory 230     15000 2900    0 true .10  23 1.1  2 true .088 23 .95 2 unknown 5.3 330 39 0 true 1.2 73 14 2 true .18 10   1.7 2 true .053 9.7 .48 2 true 8.9 430 75 2 true 9.1 430 74 2 timeout 900   7500 9100 0 true 28   630 200 2
loops/n.c11_true-unreach-call_false-termination.i timeout 900     1800 9700    0 true .60  22 8.2  2 error (42) 850    3600 4400    0 aborted .13  7.8 1.0  0 true 3.0 280 30 2 true 2.9 270 23 2 true 2.3 240 20 2 unknown 57    75 720   0 true 2.2  220 25   2 timeout 900     8800 2900    0 out of memory 180     15000 2400    0 unknown .10  23 .74 0 true 39   700 440 2 true 890   530 9000 2 timeout (timeout) 900    76   13000   0 true .096 9.5 .79 2 true 7.9 390 67 2 true 7.7 350 64 2 true 8.8 430 78 2 true 570   670 6800 2
loops/n.c40_true-unreach-call_true-termination.i true .13  27 1.0  2 false(unreach-call) .23  20 2.4  -16 true .19 17 1.5  2 aborted .14  7.7 1.1  0 true 2.8 270 26 2 true 4.4 280 33 2 true 3.7 280 35 2 true 4.5  280 41   2 true .16 23 1.9 2 out of memory 49     15000 590    0 true .11  23 .87 2 true .085 23 .75 2 true 6.2 340 47 2 true 1.5 73 18 2 true .18 9.5 1.3 2 true .14  19   1.5  2 true 170   730 2100 2 true 170   640 2200 2 true 160   570 1900 2 true 650   870 6000 2
loops/nec40_true-unreach-call_true-termination.i true .13  25 1.1  2 false(unreach-call) .27  21 2.4  -16 true .15 17 1.6  2 aborted .10  7.9 1.2  0 true 2.9 270 25 2 true 4.1 280 30 2 true 3.5 280 35 2 true 4.4  280 48   2 true .14 23 1.8 2 timeout 900     6800 13000    0 true .075 23 .81 2 true .076 23 .89 2 true 6.7 340 55 2 true 1.4 76 17 2 true .14 9.1 1.7 2 true .14  9.8 1.2  2 true 170   720 2000 2 true 170   680 1900 2 true 170   720 2200 2 true 650   910 6000 2
loops/string_true-unreach-call_true-termination.i true .13  23 .68 2 true .75  22 5.7  2 true .51 22 5.2  2 aborted .11  8.0 1.1  0 true 2.9 270 23 2 true 5.6 320 41 2 true 3.2 260 25 2 true 4.8  270 50   2 true 12    500 140   2 out of memory 660     15000 6300    0 true 3.1   39 8.4  2 true .083 23 .83 2 unknown 470   990 5900 0 true 1.5 89 17 2 true .18 9.3 2.0 2 true 8.2   30   110    2 true 8.0 380 67 2 true 8.3 390 66 2 true 20   600 160 2 true 11   270 89 2
loops/sum01_true-unreach-call_true-termination.i timeout 900     1700 11000    0 true 1.5   22 16    2 true 19    120 210    2 timeout 900     11000   13000    0 true 3.7 280 28 2 true 120   3900 1000 2 true 300   3600 3000 2 true 300    3300 2900   2 false(unreach-call) 1.4  130 17   -16 out of memory 290     15000 3500    0 out of memory 200     15000 2900    0 out of memory 200     15000 2100    0 true 8.1 370 60 2 true 880   960 11000 2 true .15 10   1.7 2 true .16  12   .87 2 true 8.6 430 70 1 true 7.0 340 54 1 true 9.5 470 81 1 true 14   470 100 2
loops/sum03_true-unreach-call_false-termination.i true .41  26 4.9  2 true .18  20 1.4  2 out of memory 320    15000 4200    0 true .48  7.6 6.2  2 true 5.6 400 47 2 true 3.9 280 27 2 true 180   2200 2200 2 true 180    1400 2100   2 true .27 41 3.6 2 timeout 900     9700 13000    0 out of memory 410     15000 5800    0 out of memory 120     15000 1400    0 true 6.7 340 52 2 timeout 900   190 10000 0 timeout (timeout) 880    15000   12000   0 true .057 9.9 .53 2 true 5.9 330 51 2 true 6.6 340 47 2 true 5.9 330 48 2 true 12   360 99 2
loops/sum04_true-unreach-call_true-termination.i true .32  27 3.7  2 true .76  23 8.0  2 true .40 17 5.4  2 unknown .039 7.9 .20 0 true 2.9 270 27 2 true 2.8 270 22 2 true 2.2 240 18 2 true 3.3  260 31   2 true .13 23 1.8 2 timeout 900     8700 12000    0 true .087 23 .88 2 true .41  23 1.4  2 true 14   480 130 2 true 1.1 68 14 2 true .19 18   2.2 2 true .053 9.9 .47 2 true 9.2 480 76 2 true 8.6 480 60 2 true 9.5 550 71 2 true 14   490 100 2
loops/sum_array_true-unreach-call.i timeout 900     12000 4900    0 false(unreach-call) .62  25 6.5  -16 error (42) 850    1500 3900    0 aborted .17  33   1.3  0 error 6.4 350 59 0 segmentation fault 210   4400 1700 0 timeout 910   5800 8100 0 unknown 890    240 8500   0 timeout 900    1300 11000   0 timeout 900     330 2800    0 timeout 900     790 9300    0 timeout 900     750 8600    0 timeout 900   1200 12000 0 true 880   550 12000 1 unknown .17 9.8 2.2 0 unknown .081 9.9 .47 0 timeout 900   1900 11000 0 timeout 900   650 10000 0 timeout 900   2300 10000 0 true 660   1100 7400 1
loops/terminator_02_true-unreach-call_true-termination.i true .12  22 .75 2 true .21  20 1.9  2 true .17 19 1.8  2 true 1.3   7.8 14    2 true 2.7 260 28 2 true 3.4 280 31 2 true 2.9 260 25 2 true 4.0  280 35   2 true 35    4700 370   2 out of memory 510     15000 5400    0 true .10  23 .89 2 true .29  23 .61 2 true 10   530 93 2 true 1.4 75 15 2 true .19 10   1.8 2 true .15  9.9 2.1  2 true 5.8 320 44 2 true 6.6 340 46 2 true 6.6 340 50 2 true 9.8 320 71 2
loops/terminator_03_true-unreach-call_true-termination.i true .10  22 1.0  2 true .40  22 2.0  2 error (42) 850    500 6200    0 timeout 900     990   10000    0 true 2.7 270 24 2 true 3.8 300 28 2 true 3.0 260 26 2 true 4.0  270 38   2 false(unreach-call) 43    320 490   -16 timeout 900     3700 9600    0 timeout 900     6700 10000    0 true .088 23 .79 2 true 7.6 350 60 2 true 1.3 82 18 2 timeout (timeout) 900    64   12000   0 timeout 900     1200   11000    0 true 6.0 320 48 2 true 6.1 340 46 2 true 6.8 340 52 2 true 12   470 89 2
loops/trex01_true-unreach-call_true-termination.i true 6.4   120 81    2 true .83  22 7.2  2 error (42) 850    6100 4300    0 timeout 900     8400   13000    0 true 6.0 320 52 2 true 5.9 320 44 2 true 160   2400 1900 2 unknown 820    160 8800   0 false(unreach-call) 42    1800 490   -16 timeout 900     13000 11000    0 timeout 900     7000 11000    0 timeout 900     8500 11000    0 true 9.5 540 86 2 true 1.5 75 17 2 timeout (timeout) 900    2400   12000   0 unknown .40  9.9 5.4  0 true 6.3 330 49 2 true 5.8 320 51 2 true 5.9 330 49 2 true 19   580 150 2
loops/trex02_true-unreach-call_true-termination.i true .12  22 .76 2 true .14  20 1.2  2 error (42) 850    1000 7900    0 aborted .10  7.8 1.2  0 true 2.6 270 26 2 true 3.5 280 26 2 true 2.8 260 24 2 true 3.6  260 35   2 false(unreach-call) 15    890 180   -16 timeout 900     4000 9300    0 timeout 900     12000 11000    0 true .11  23 .82 2 true 5.9 340 50 2 true 1.3 78 19 2 true .17 9.4 1.7 2 timeout 900     3200   9900    0 true 5.8 320 45 2 true 6.2 350 52 2 true 6.0 330 47 2 true 15   560 110 2
loops/trex03_true-unreach-call_true-termination.i true .12  22 .78 2 false(unreach-call) .068 18 .66 -16 error (42) 850    840 7000    0 true 1.9   7.9 23    2 error 3.0 280 27 0 true 4.1 280 28 2 true 2.9 260 22 2 true 3.9  260 36   2 false(unreach-call) 560    890 8000   -16 timeout 900     3800 9500    0 timeout 900     5300 11000    0 true .11  23 .89 2 timeout 900   1300 7100 0 true 880   410 10000 2 timeout (timeout) 900    3800   9800   0 unknown .28  9.6 2.9  0 true 6.4 320 47 2 true 5.9 320 50 2 true 6.1 340 49 2 true 31   690 230 2
loops/trex04_true-unreach-call_false-termination.i true .11  22 .74 2 true .35  29 3.3  2 error (42) 850    2700 7200    0 timeout 900     6600   13000    0 true 2.8 270 24 2 true 3.8 280 27 2 true 3.0 260 29 2 true 4.5  280 39   2 false(unreach-call) 22    300 250   -16 timeout 900     3900 10000    0 timeout 900     7300 12000    0 true .092 23 .86 2 timeout 900   1000 12000 0 true 1.4 82 15 2 true .18 9.4 2.0 2 unknown .085 9.9 .67 0 true 5.8 330 46 2 true 6.2 330 48 2 true 6.1 320 50 2 true 12   440 82 2
loops/veris.c_NetBSD-libc__loop_true-unreach-call_true-termination.i true .099 23 .95 2 true .29  21 1.6  2 true .29 17 3.2  2 unknown .083 7.8 .19 0 true 2.9 280 27 2 timeout 910   9600 6900 0 true 3.2 260 24 2 true 4.0  280 37   2 true 11    1200 140   2 out of memory 360     15000 4200    0 true .12  23 .87 2 true .086 23 .80 2 unknown 5.3 340 43 0 true 1.3 80 20 2 true .16 9.5 1.4 2 true .052 9.8 .49 2 true 8.6 390 61 2 true 7.3 380 66 2 true 8.3 370 60 2 true 13   460 89 2
loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i true .11  24 .88 2 true 1.0   23 8.6  2 true 1.6  35 20    2 aborted .11  7.9 1.1  0 true 16   720 120 2 true 27   1200 230 2 true 150   2400 2100 2 true 160    2400 2000   2 timeout 900    1800 11000   0 timeout 900     6900 12000    0 true .35  36 3.4  2 unknown .11  24 .90 0 unknown 5.5 360 50 0 true 5.0 110 63 2 true .52 11   6.5 2 unknown .14  9.7 1.3  0 true 7.8 370 60 2 true 6.6 330 48 2 true 7.1 350 60 2 true 20   270 190 2
loops/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call_true-termination.i true .083 22 .88 2 true .37  24 3.9  2 true .48 18 4.3  2 aborted .14  7.7 .94 0 true 3.1 280 30 2 true 4.0 290 31 2 true 4.0 270 39 2 true 5.1  290 44   2 true 2.0  290 21   2 out of memory 360     15000 4500    0 true .097 23 1.1  2 true .081 23 .82 2 true 38   700 370 2 true 1.7 85 21 2 true .14 9.2 1.5 2 true .15  9.8 1.2  2 true 6.0 320 52 2 true 6.1 320 45 2 true 6.5 340 54 2 true 12   420 82 2
loops/vogal_true-unreach-call.i true 5.5   89 64    2 timeout 900     300 11000    0 true .33 18 3.5  2 aborted .11  7.6 1.2  0 true 53   2800 460 2 segmentation fault 61   1800 460 0 true 330   2200 3800 2 true 330    2100 3500   2 true 290    14000 3300   2 timeout 900     14000 11000    0 true .30  24 3.9  2 true 2.8   38 6.5  2 unknown 6.1 330 57 0 true 3.6 89 50 2 true .17 9.4 1.7 2 true .48  9.7 5.5  2 timeout 900   5400 12000 0 timeout 900   2400 11000 0 timeout 900   5300 12000 0 true 660   1200 7100 2
loops/while_infinite_loop_1_true-unreach-call_false-termination.i true .11  22 .65 2 true .051 16 .62 2 out of memory 260    15000 3300    0 unknown .037 7.7 .33 0 true 2.6 270 24 2 true 2.9 280 22 2 true 2.2 250 19 2 true 3.1  260 29   2 false(unreach-call) .19 23 1.7 -16 out of memory 740     15000 9200    0 out of memory 430     15000 6700    0 true .099 23 .77 2 true 5.4 360 40 2 true 1.3 79 16 2 timeout (timeout) 900    15000   14000   0 true .053 9.9 .44 2 true 5.7 320 41 2 true 5.8 330 51 2 true 5.9 320 46 2 true 12   470 89 2
loops/while_infinite_loop_2_true-unreach-call_false-termination.i true .097 22 .77 2 true .057 15 .52 2 out of memory 260    15000 3200    0 unknown .034 7.8 .30 0 true 2.5 270 24 2 true 2.7 260 23 2 true 2.4 240 21 2 true 3.2  250 28   2 true .19 23 1.9 2 out of memory 740     15000 9900    0 out of memory 430     15000 6600    0 true .079 23 .84 2 true 5.4 340 40 2 true 1.3 72 16 2 true .13 9.3 1.3 2 true .065 9.9 .46 2 true 6.1 340 47 2 true 5.6 330 44 2 true 6.0 340 47 2 true 9.0 280 65 2
loops/while_infinite_loop_3_true-unreach-call_false-termination.i true .093 22 .83 2 true .054 17 .66 2 out of memory 230    15000 2800    0 unknown .037 7.9 .27 0 true 2.7 270 27 2 true 3.0 290 25 2 true 2.4 250 20 2 true 3.3  260 30   2 false(unreach-call) .20 23 2.2 -16 timeout 900     15000 13000    0 out of memory 420     15000 6000    0 true .10  23 .76 2 true 5.5 330 42 2 true 1.3 79 17 2 timeout (timeout) 890    15000   12000   0 true .098 11   .47 2 true 6.3 350 46 2 true 5.6 320 46 2 true 5.9 320 42 2 true 13   480 95 2
loop-acceleration/array_false-unreach-call1_true-termination.i timeout 900     10000 8900    0 timeout 900     260 8400    0 false(unreach-call) 29    1700 370    0 aborted .11  7.8 1.1  0 timeout 900   4000 11000 0 segmentation fault 680   7200 6300 0 timeout 900   15000 11000 0 unknown 900    230 9400   0 false(unreach-call) 140    160 1900   0 false(unreach-call) 300     510 3900    0 false(unreach-call) 310     2000 4800    0 timeout 900     590 10000    0 timeout 900   1000 8400 0 false(unreach-call) 15   280 210 0 false(unreach-call) .15 10   2.0 0 unknown .074 9.9 .47 0 timeout 900   2400 14000 0 timeout 900   3800 12000 0 timeout 900   2000 12000 0 witness invalid (false(unreach-call)) 340   3700 4100 0
loop-acceleration/array_false-unreach-call2_true-termination.i timeout 900     11000 10000    0 timeout 900     500 9300    0 false(unreach-call) 61    3500 830    0 aborted .099 7.6 1.2  0 timeout 900   4300 9300 0 timeout 930   14000 7300 0 out of memory 870   15000 9400 0 unknown 890    610 9000   0 false(unreach-call) 140    180 2000   0 false(unreach-call) 110     1200 1500    0 false(unreach-call) 180     9200 2400    0 timeout 900     640 9000    0 timeout 900   1100 11000 0 false(unreach-call) 140   3500 1700 0 false(unreach-call) .16 14   1.6 0 false(unreach-call) .058 9.9 .50 0 timeout 900   3400 12000 0 timeout 900   3700 14000 0 timeout 900   3200 13000 0 witness invalid (false(unreach-call)) 360   4000 4200 0
loop-acceleration/array_false-unreach-call3_true-termination.i timeout 900     10000 7300    0 timeout 900     360 10000    0 false(unreach-call) 23    930 310    0 aborted .11  7.8 1.1  0 timeout 900   4300 8900 0 timeout 920   4000 9600 0 timeout 920   10000 9700 0 timeout 900    8300 9300   0 false(unreach-call) 150    230 2000   0 false(unreach-call) 300     700 4000    0 false(unreach-call) 320     2300 4300    0 timeout 900     530 9500    0 timeout 900   1100 10000 0 timeout 880   820 8000 0 false(unreach-call) 2.0  12   32   0 false(unreach-call) 130     820   1800    0 timeout 900   1900 13000 0 timeout 900   2400 13000 0 timeout 900   1700 12000 0 witness invalid (false(unreach-call)) 350   3700 4100 0
loop-acceleration/const_false-unreach-call1.i timeout 900     1700 10000    0 timeout 900     340 8700    0 false(unreach-call) 1.3  20 16    1 unknown .035 7.8 .26 0 timeout 900   4200 8800 0 timeout 920   9300 8400 0 false(unreach-call) 68   1600 880 1 unknown 54    75 670   0 false(unreach-call) .14 23 1.7 1 false(unreach-call) 10     130 120    1 false(unreach-call) 21     1500 280    1 out of memory 150     15000 1700    0 timeout 900   1000 12000 0 false(unreach-call) 2.3 69 29 1 false(unreach-call) .17 11   1.4 1 false(unreach-call) .11  9.7 .97 1 timeout 900   1700 12000 0 timeout 900   880 12000 0 timeout 900   760 11000 0 witness invalid (false(unreach-call)) 340   3700 3500 0
loop-acceleration/diamond_false-unreach-call1.i false(unreach-call) .83  31 9.2  1 false(unreach-call) 54     40 520    0 false(unreach-call) 1.4  50 15    1 timeout 900     560   12000    0 false(unreach-call) 47   1700 460 0 false(unreach-call) 43   2000 360 1 false(unreach-call) 12   1200 110 1 false(unreach-call) 32    75 410   1 false(unreach-call) 1.3  130 17   0 false(unreach-call) 1.3   150 17    1 false(unreach-call) 2.2   260 29    1 false(unreach-call) 4.0   410 53    1 timeout 900   1000 11000 0 false(unreach-call) 260   120 3700 1 false(unreach-call) .16 9.9 1.9 1 false(unreach-call) 27     150   380    1 false(unreach-call) 150   1000 1800 1 false(unreach-call) 850   820 12000 1 false(unreach-call) 520   670 6800 1 false(unreach-call) 83   1900 820 1
loop-acceleration/functions_false-unreach-call1_true-termination.i timeout 900     1400 12000    0 timeout 900     250 12000    0 out of memory 260    15000 3400    0 unknown .035 7.7 .22 0 timeout 900   4400 8600 0 timeout 910   7900 8000 0 timeout 910   7200 8900 0 unknown 36    75 390   0 false(unreach-call) .16 23 1.8 0 out of memory 640     15000 9400    0 out of memory 260     15000 3800    0 out of memory 210     15000 2600    0 timeout 900   1000 12000 0 error (1) 880   1400 10000 0 false(unreach-call) .13 9.3 1.5 0 out of memory 120     15000   1400    0 timeout 900   2300 14000 0 timeout 900   1900 11000 0 timeout 900   1100 11000 0 unknown 24   220 210 0
loop-acceleration/multivar_false-unreach-call1_true-termination.i false(unreach-call) .098 22 .90 1 false(unreach-call) .10  20 .58 1 false(unreach-call) .13 17 .94 1 false(unreach-call) .19  7.9 1.7  1 false(unreach-call) 3.0 280 27 1 false(unreach-call) 3.9 310 29 1 false(unreach-call) 2.4 250 22 1 false(unreach-call) .53 75 6.5 1 false(unreach-call) 2.9  170 34   1 false(unreach-call) .11  23 .81 1 false(unreach-call) .088 23 .77 1 false(unreach-call) .11  23 .66 1 false(unreach-call) 5.0 330 37 1 false(unreach-call) 1.6 80 22 1 false(unreach-call) .17 9.4 1.4 1 false(unreach-call) .078 9.6 .53 1 false(unreach-call) 5.8 330 45 1 false(unreach-call) 6.6 340 47 1 false(unreach-call) 5.9 320 46 1 false(unreach-call) 22   280 260 1
loop-acceleration/nested_false-unreach-call1.i timeout 900     9600 10000    0 timeout 900     410 8800    0 out of memory 310    15000 4000    0 unknown .031 7.7 .32 0 timeout 900   3900 11000 0 segmentation fault 19   840 120 0 timeout 900   4000 8900 0 timeout 900    1400 8100   0 false(unreach-call) 3.3  450 33   0 timeout 900     8200 11000    0 out of memory 330     15000 4100    0 timeout 900     12000 10000    0 timeout 900   1100 11000 0 timeout 880   880 12000 0 false(unreach-call) .16 9.4 1.5 0 false(unreach-call) .050 9.8 .56 0 timeout 900   3600 13000 0 timeout 900   1500 12000 0 timeout 900   2200 11000 0 unknown 150   7100 1900 0
loop-acceleration/phases_false-unreach-call1.i timeout 900     1200 12000    0 exception (gremlins) .11  22 1.2  0 out of memory 310    15000 3700    0 unknown .035 7.9 .30 0 timeout 900   4100 9300 0 timeout 900   5100 8600 0 timeout 900   3600 8900 0 unknown 150    75 1800   0 false(unreach-call) .15 23 1.8 0 timeout 900     5700 11000    0 out of memory 510     15000 6700    0 timeout 900     4200 11000    0 timeout 900   1000 10000 0 timeout 880   380 11000 0 out of memory 230    15000   3500   0 out of memory 160     15000   1700    0 timeout 900   1600 13000 0 timeout 900   2300 12000 0 timeout 900   1000 13000 0 unknown 140   6000 1600 0
loop-acceleration/phases_false-unreach-call2.i false(unreach-call) .17  25 1.1  1 false(unreach-call) .075 16 .59 1 false(unreach-call) .13 17 .97 1 false(unreach-call) .23  7.9 2.2  1 false(unreach-call) 3.1 280 28 1 false(unreach-call) 4.7 300 35 1 false(unreach-call) 2.4 250 21 1 false(unreach-call) .55 76 7.0 1 false(unreach-call) 56    3200 640   1 false(unreach-call) .096 23 .78 1 false(unreach-call) .074 23 .83 1 false(unreach-call) .28  23 .55 1 false(unreach-call) 5.0 330 40 1 timeout 880   170 10000 0 false(unreach-call) .15 9.4 1.5 1 false(unreach-call) .086 9.9 .93 1 false(unreach-call) 5.5 320 47 1 false(unreach-call) 5.5 320 48 1 false(unreach-call) 5.6 320 48 1 false(unreach-call) 37   580 310 1
loop-acceleration/simple_false-unreach-call1.i timeout 900     1400 13000    0 exception (gremlins) 770     160 9300    0 error (1) 270    15000 3600    0 unknown .035 7.7 .19 0 timeout 900   4200 8200 0 segmentation fault 90   2900 650 0 timeout 910   8400 11000 0 unknown 54    75 660   0 false(unreach-call) .14 23 1.8 0 timeout 900     9100 11000    0 out of memory 310     15000 3800    0 out of memory 260     15000 2800    0 timeout 900   1000 9900 0 timeout 880   880 11000 0 false(unreach-call) .14 9.3 1.6 0 false(unreach-call) .079 9.8 .46 0 timeout 900   1500 13000 0 timeout 900   980 13000 0 timeout 900   830 12000 0 unknown 140   8700 2000 0
loop-acceleration/simple_false-unreach-call2_true-termination.i false(unreach-call) .12  22 .78 1 false(unreach-call) .085 16 .56 1 false(unreach-call) .13 17 1.1  1 false(unreach-call) .16  7.6 2.0  1 false(unreach-call) 2.9 280 29 1 false(unreach-call) 3.3 300 27 1 false(unreach-call) 2.4 250 20 1 false(unreach-call) .38 75 4.5 1 false(unreach-call) 2.6  120 27   1 false(unreach-call) .11  23 .66 1 false(unreach-call) .074 23 1.1  1 false(unreach-call) .072 23 .96 1 false(unreach-call) 5.0 340 46 1 false(unreach-call) 1.6 72 19 1 false(unreach-call) .16 9.4 1.7 1 false(unreach-call) .081 9.9 .40 1 false(unreach-call) 5.6 310 40 1 false(unreach-call) 5.5 320 47 1 false(unreach-call) 5.5 320 44 1 false(unreach-call) 8.9 280 63 1
loop-acceleration/simple_false-unreach-call3_true-termination.i false(unreach-call) .099 22 .87 1 false(unreach-call) .067 17 .71 1 false(unreach-call) .11 17 .86 1 false(unreach-call) .17  7.8 1.7  1 false(unreach-call) 2.9 270 29 1 false(unreach-call) 5.6 370 38 1 false(unreach-call) 2.5 250 21 1 false(unreach-call) .52 75 7.2 1 false(unreach-call) 1.3  83 14   1 false(unreach-call) .086 23 .79 1 false(unreach-call) .10  23 .83 1 false(unreach-call) .072 23 .92 1 false(unreach-call) 4.9 350 38 1 false(unreach-call) 1.6 79 22 1 false(unreach-call) .17 9.3 1.3 1 false(unreach-call) .062 16   .72 1 false(unreach-call) 5.5 320 45 1 false(unreach-call) 5.6 310 45 1 false(unreach-call) 5.6 320 52 1 false(unreach-call) 130   860 690 1
loop-acceleration/simple_false-unreach-call4.i timeout 900     1400 12000    0 exception (gremlins) 1.1   35 8.9  0 error (1) 290    15000 3000    0 unknown .036 7.8 .32 0 timeout 900   4300 7900 0 segmentation fault 200   3100 1900 0 timeout 910   7700 9300 0 unknown 53    75 670   0 false(unreach-call) .14 23 1.7 0 timeout 900     9000 13000    0 out of memory 310     15000 4100    0 out of memory 210     15000 2500    0 timeout 900   1000 11000 0 timeout 880   910 9900 0 false(unreach-call) .13 9.4 1.6 0 false(unreach-call) .078 9.5 .52 0 timeout 900   1400 14000 0 timeout 900   960 11000 0 timeout 900   880 13000 0 unknown 150   8400 1600 0
loop-acceleration/underapprox_false-unreach-call1_true-termination.i false(unreach-call) .23  25 2.1  1 false(unreach-call) .99  23 12    1 false(unreach-call) .40 17 3.3  1 unknown .034 7.9 .28 0 false(unreach-call) 3.3 290 30 1 false(unreach-call) 3.7 280 28 1 false(unreach-call) 2.6 250 22 1 false(unreach-call) 3.5  75 46   1 false(unreach-call) .14 23 1.5 1 false(unreach-call) .073 23 .89 1 false(unreach-call) .11  23 .66 1 false(unreach-call) .093 23 1.0  1 false(unreach-call) 9.1 380 69 0 false(unreach-call) 1.5 73 20 1 false(unreach-call) .16 9.3 1.5 1 false(unreach-call) .085 10   .54 1 false(unreach-call) 7.4 380 56 1 false(unreach-call) 7.0 360 49 1 false(unreach-call) 9.3 430 64 1 false(unreach-call) 10   290 80 1
loop-acceleration/underapprox_false-unreach-call2_true-termination.i false(unreach-call) .24  26 2.2  1 false(unreach-call) .72  23 7.2  1 false(unreach-call) .36 17 3.6  1 unknown .078 7.8 .23 0 false(unreach-call) 3.2 270 26 1 false(unreach-call) 3.6 280 27 1 false(unreach-call) 2.8 260 24 1 false(unreach-call) 3.5  75 44   1 false(unreach-call) .14 23 1.5 1 false(unreach-call) .075 23 .80 1 false(unreach-call) .29  23 1.1  1 false(unreach-call) .089 23 1.1  1 false(unreach-call) 9.0 360 72 0 false(unreach-call) 1.5 75 16 1 false(unreach-call) .13 9.2 1.5 1 false(unreach-call) .052 9.9 .44 1 false(unreach-call) 7.3 370 57 1 false(unreach-call) 7.4 350 50 1 false(unreach-call) 9.0 430 71 1 false(unreach-call) 10   290 76 1
loop-acceleration/array_true-unreach-call1_true-termination.i true 38     540 390    2 timeout 900     340 8700    0 true 10    1100 120    2 aborted .098 7.7 1.0  0 timeout 900   4000 11000 0 true 4.0 300 28 2 true 98   430 1000 2 true 99    550 1300   2 false(unreach-call) 140    160 1800   -16 out of memory 180     15000 2200    0 true 110     1600 200    2 true .089 23 .82 2 timeout 900   1000 9200 0 true 2.9 210 36 2 true .13 9.3 1.6 2 unknown .059 9.9 .56 0 timeout 900   3100 13000 0 timeout 900   2900 13000 0 timeout 900   2000 12000 0 true 640   840 6500 2
loop-acceleration/array_true-unreach-call2_true-termination.i timeout 900     12000 9300    0 timeout 900     500 9700    0 true 23    2200 260    1 aborted .14  7.8 1.0  0 timeout 900   4200 9000 0 timeout 940   14000 7100 0 out of memory 880   15000 8900 0 unknown 890    280 12000   0 false(unreach-call) 140    180 1900   -16 out of memory 270     15000 3400    0 true 140     8500 1800    1 timeout 900     570 8800    0 timeout 900   1000 11000 0 true 35   3100 410 1 true .15 10   1.6 1 true .057 9.9 .44 1 timeout 900   3100 13000 0 timeout 900   3100 12000 0 timeout 900   1900 14000 0 true 640   830 7500 1
loop-acceleration/array_true-unreach-call3_true-termination.i true 3.8   130 38    2 true .39  22 2.9  1 true 7.9  630 98    1 aborted .099 7.8 1.3  0 timeout 900   4300 11000 0 true 4.0 310 27 2 true 14   1200 130 1 true 14    1200 120   1 true .83 130 9.4 1 timeout 900     4600 11000    0 true 64     2100 810    1 timeout 900     720 9600    0 timeout 900   1000 9200 0 timeout 880   850 7400 0 true 6.6  13   79   1 true 370     1700   4800    1 timeout 900   1800 13000 0 timeout 900   4400 15000 0 true 7.8 360 61 1 true 640   860 6200 1
loop-acceleration/array_true-unreach-call4_true-termination.i timeout 900     10000 8700    0 timeout 900     350 8600    0 true 7.7  630 110    1 aborted .13  7.7 .91 0 timeout 900   4200 9500 0 timeout 900   5200 8000 0 true 13   1200 110 1 unknown 890    220 11000   0 true .82 130 10   1 timeout 900     4800 11000    0 true 65     2000 850    1 timeout 900     610 10000    0 timeout 900   1000 11000 0 timeout 880   830 6800 0 true 6.6  13   87   1 true 360     1700   4700    1 timeout 900   1800 12000 0 timeout 900   3400 12000 0 timeout 900   1700 11000 0 true 640   860 6300 1
loop-acceleration/const_true-unreach-call1.i true .19  24 1.8  2 true .24  21 1.9  1 true 1.6  19 15    2 unknown .078 7.7 .21 0 true 3.0 270 25 2 true 3.2 270 28 2 true 5.9 600 60 2 true 7.4  430 65   2 true .19 30 2.2 2 timeout 900     1700 2200    0 true 21     1500 270    2 true .090 23 .94 2 true 5.4 340 49 2 true 1.9 66 23 2 true .14 9.4 1.7 2 true .088 9.9 .81 2 timeout 900   1600 14000 0 timeout 900   870 12000 0 timeout 900   620 11000 0 true 11   420 89 2
loop-acceleration/diamond_true-unreach-call1_true-termination.i true .84  31 11    2 false(unreach-call) 47     41 600    -16 true 1.9  50 21    2 timeout 900     520   11000    0 error 57   2100 590 0 true 34   1800 280 2 true 150   2800 2200 2 true 270    2900 3500   2 true 1.4  180 17   2 out of memory 160     15000 2100    0 true 11     1100 140    2 true 56     1600 820    2 timeout 900   1000 9900 0 true 880   170 9500 2 true .16 9.8 1.9 2 true 180     1600   2400    2 true 500   980 6300 1 timeout 900   680 12000 0 timeout 900   810 13000 0 true 20   480 150 2
loop-acceleration/diamond_true-unreach-call2.i true .17  26 2.1  2 false(unreach-call) 77     41 820    -16 true .42 24 4.6  2 true 740     5800   8200    2 true 9.8 470 79 2 true 9.1 720 62 2 true 4.8 290 39 2 true 8.9  290 99   2 true 96    2600 1000   2 out of memory 550     15000 1400    0 true .25  37 3.3  2 true .45  45 5.8  2 timeout 900   1100 9000 0 true 2.0 100 25 2 true .20 17   2.4 2 true .21  10   2.6  2 true 30   600 310 1 true 13   470 120 1 true 220   630 3100 1 true 140   670 1700 2
loop-acceleration/functions_true-unreach-call1_true-termination.i timeout 900     1600 12000    0 timeout 900     290 12000    0 out of memory 260    15000 3100    0 unknown .038 7.8 .26 0 timeout 900   4400 9600 0 segmentation fault 44   1900 320 0 timeout 910   7600 9000 0 unknown 36    75 440   0 true .26 39 2.3 1 out of memory 640     15000 8900    0 out of memory 260     15000 3000    0 out of memory 200     15000 2300    0 timeout 900   1000 10000 0 true 880   1300 11000 1 true .13 9.5 2.0 1 out of memory 110     15000   1400    0 timeout 900   2600 14000 0 timeout 900   1800 12000 0 true 9.0 410 75 2 true 16   540 110 1
loop-acceleration/multivar_true-unreach-call1_true-termination.i timeout 900     1700 12000    0 true .13  19 .74 2 true 100    270 850    2 true .51  7.8 5.2  2 true 2.8 270 21 2 true 3.6 310 26 2 true 2.7 260 24 2 unknown 63    75 750   0 true 1.1  160 15   2 out of memory 210     15000 2700    0 out of memory 160     15000 1700    0 out of memory 180     15000 2100    0 true 5.8 340 43 2 true 880   1100 13000 2 true .14 9.1 1.5 2 true .061 9.7 .44 2 true 6.5 350 45 2 true 5.8 320 46 2 true 6.4 330 49 2 true 12   440 88 2
loop-acceleration/nested_true-unreach-call1.i true .17  24 1.3  2 timeout 900     280 9200    0 out of memory 310    15000 4300    0 unknown .078 7.8 .25 0 timeout 900   3900 11000 0 true 3.4 270 26 2 true 350   4500 4000 2 true 360    4200 4100   2 true 3.6  550 35   2 timeout 900     8200 11000    0 out of memory 330     15000 3800    0 true .11  23 .84 2 timeout 900   1000 9500 0 timeout 880   940 12000 0 true .16 9.4 1.4 2 true .050 9.9 .52 2 timeout 900   3700 14000 0 timeout 900   1500 13000 0 timeout 900   2500 12000 0 true 16   620 110 2
loop-acceleration/overflow_true-unreach-call1.i timeout 900     1400 13000    0 true .17  22 1.4  1 error (1) 280    15000 3400    0 unknown .036 7.8 .32 0 true 3.2 270 23 1 timeout 900   8700 7900 0 timeout 910   7800 8700 0 unknown 53    75 590   0 true .16 23 2.1 1 timeout 900     9200 11000    0 out of memory 320     15000 3600    0 out of memory 220     15000 2300    0 true 5.9 340 46 1 timeout 880   930 12000 0 true .15 9.5 1.4 1 true .053 9.9 .56 1 timeout 900   1800 13000 0 timeout 900   1100 14000 0 true 6.6 360 48 1 true 12   450 97 1
loop-acceleration/phases_true-unreach-call1.i timeout 900     1500 12000    0 exception (gremlins) .14  20 1.2  0 out of memory 310    15000 4900    0 unknown .045 7.6 .25 0 timeout 900   4100 10000 0 timeout 900   5000 7800 0 timeout 900   4300 8600 0 unknown 130    75 1900   0 false(unreach-call) .15 23 1.9 -16 timeout 900     5700 12000    0 out of memory 510     15000 6600    0 timeout 900     4400 9900    0 timeout 900   1000 10000 0 timeout 880   350 12000 0 true 210    15000   2900   1 out of memory 160     15000   2200    0 timeout 900   1500 13000 0 timeout 900   2400 12000 0 timeout 900   900 13000 0 unknown 140   6100 1900 0
loop-acceleration/phases_true-unreach-call2_false-termination.i true .12  24 1.1  2 exception (gremlins) .48  21 4.4  0 error (42) 850    5900 7900    0 true 1.4   11   16    2 error 3.1 290 31 0 true 4.7 310 36 2 true 2.8 260 25 2 true 5.3  280 53   2 false(unreach-call) 57    3200 540   -16 timeout 900     13000 7300    0 out of memory 740     15000 5200    0 true 110     83 1500    2 unknown 43   690 500 0 timeout 880   170 11000 0 timeout (timeout) 900    11000   8800   0 true .12  9.5 1.1  2 true 7.6 340 69 2 true 6.8 320 58 2 true 120   400 1400 2 true 11   440 90 2
loop-acceleration/simple_true-unreach-call1.i timeout 900     1600 10000    0 exception (gremlins) 770     160 9200    0 error (1) 280    15000 3500    0 unknown .065 7.8 .21 0 timeout 900   4200 7900 0 timeout 910   8600 7900 0 timeout 910   7900 8900 0 unknown 53    75 640   0 true .18 23 1.9 1 timeout 900     9200 11000    0 out of memory 310     15000 4200    0 out of memory 240     15000 2700    0 timeout 900   1000 12000 0 timeout 880   970 11000 0 true .13 9.5 1.5 1 true .049 9.9 .65 1 timeout 900   3800 15000 0 timeout 900   1000 13000 0 true 6.7 350 54 2 true 12   450 77 1
loop-acceleration/simple_true-unreach-call2_true-termination.i true .083 22 .77 2 exception (gremlins) .15  21 .62 0 error (42) 850    4600 7300    0 true .27  7.9 3.7  2 true 2.7 270 23 2 true 3.3 280 26 2 true 2.7 260 24 2 true 3.6  280 35   2 false(unreach-call) 2.6  120 33   -16 timeout 900     4300 11000    0 timeout 900     8200 10000    0 true .11  23 .81 2 true 5.5 340 44 2 true 1.3 80 15 2 true .13 9.3 1.7 2 true .073 9.7 .47 2 true 5.7 320 50 2 true 5.4 330 46 2 true 5.9 330 50 2 true 13   480 87 2
loop-acceleration/simple_true-unreach-call3_true-termination.i timeout 900     1200 9600    0 false(unreach-call) .065 20 .67 -16 error (42) 850    11000 3300    0 unknown .13  7.8 1.8  0 timeout 900   8800 8200 0 timeout 900   7300 8700 0 timeout 900   5800 9400 0 unknown 56    110 750   0 true .67 94 7.4 1 out of memory 130     15000 1800    0 out of memory 130     15000 1500    0 out of memory 140     15000 1900    0 true 6.7 350 54 1 true 880   400 11000 1 true .17 9.3 1.8 1 true .058 9.9 .48 1 timeout 900   770 10000 0 timeout 900   1200 12000 0 true 7.5 360 52 2 true 11   440 85 1
loop-acceleration/simple_true-unreach-call4.i true .12  22 .64 2 exception (gremlins) 1.4   35 18    0 error (1) 290    15000 3700    0 unknown .037 7.5 .29 0 timeout 900   4300 9100 0 true 3.0 270 24 2 true 150   2200 1700 2 true 150    1300 1600   2 true .19 23 2.1 2 timeout 900     9100 11000    0 out of memory 310     15000 4000    0 true .10  23 .82 2 timeout 900   1000 9600 0 timeout 880   960 11000 0 true .14 9.6 1.5 2 true .050 9.9 .56 2 true 5.9 330 48 2 timeout 900   1100 13000 0 true 6.9 360 52 2 true 12   450 85 2
loop-acceleration/underapprox_true-unreach-call1_true-termination.i true .22  25 2.6  2 true .58  22 4.0  2 true .41 17 3.8  2 unknown .079 7.7 .26 0 true 3.8 270 35 2 true 2.8 270 21 2 true 2.3 240 20 2 true 5.8  260 63   2 true .16 23 1.4 2 timeout 900     9100 11000    0 true .080 23 .98 2 true .11  23 1.4  2 true 11   450 92 2 true 1.2 69 14 2 true .16 9.2 1.4 2 true .080 9.7 .45 2 true 63   510 810 2 timeout 900   500 12000 0 true 190   570 2400 2 true 20   520 150 2
loop-acceleration/underapprox_true-unreach-call2_true-termination.i true .10  25 1.7  2 true .21  20 1.8  2 true .42 17 4.8  2 unknown .040 7.8 .24 0 true 2.7 270 23 2 true 2.8 270 24 2 true 2.3 240 21 2 true 3.2  260 30   2 true .14 24 1.6 2 timeout 900     9400 11000    0 true .081 23 .83 2 true .11  23 .79 2 true 9.7 370 83 2 true 1.1 66 14 2 true .14 9.5 1.4 2 true .055 9.9 .47 2 true 7.8 390 57 2 true 8.1 390 56 2 true 10   470 72 2 true 13   470 93 2
loop-invgen/id_trans_false-unreach-call_true-termination.i false(unreach-call) .10  23 .98 1 exception (gremlins) .21  23 2.0  0 false(unreach-call) .12 18 1.1  1 false(unreach-call) 8.6   110   100    1 false(unreach-call) 3.4 280 28 1 false(unreach-call) 9.5 530 74 1 false(unreach-call) 3.3 290 29 1 false(unreach-call) .59 76 6.9 1 false(unreach-call) 24    2300 300   0 false(unreach-call) .30  23 .99 1 false(unreach-call) .095 23 .90 1 false(unreach-call) .093 23 .84 1 false(unreach-call) 7.0 360 59 1 false(unreach-call) 1.8 79 22 1 false(unreach-call) .20 10   1.8 0 false(unreach-call) .10  11   1.2  1 false(unreach-call) 6.5 320 49 1 false(unreach-call) 7.2 340 56 1 false(unreach-call) 7.9 370 63 1 false(unreach-call) 10   280 70 1
loop-invgen/MADWiFi-encode_ie_ok_true-unreach-call_true-termination.i timeout 900     540 12000    0 true 1.6   31 21    2 error (42) 850    200 12000    0 timeout 900     4500   14000    0 true 3.2 270 30 2 timeout 900   5000 8200 0 timeout 900   1800 8700 0 unknown 900    76 12000   0 true 900    2400 10000   2 timeout 900     770 11000    0 timeout 900     1600 11000    0 timeout 900     2600 11000    0 true 12   530 110 2 true 56   170 630 2 timeout (timeout) 900    2200   11000   0 timeout 900     3500   10000    0 true 7.7 380 63 2 true 9.3 460 75 2 true 10   450 79 2 true 15   480 100 2
loop-invgen/NetBSD_loop_true-unreach-call_true-termination.i true .12  23 1.1  2 true .59  25 5.1  2 error (42) 850    11000 5700    0 timeout 900     12000   11000    0 true 5.4 330 45 2 true 330   5600 2900 2 timeout 910   8000 8600 0 unknown 54    76 670   0 true 9.3  870 120   2 out of memory 410     15000 4600    0 out of memory 220     15000 2700    0 out of memory 150     15000 2000    0 true 11   430 79 2 true 880   560 9700 2 timeout (timeout) 900    1200   11000   0 timeout 900     1300   12000    0 true 7.8 410 57 2 true 7.7 430 56 2 true 9.4 500 76 2 true 13   470 90 2
loop-invgen/SpamAssassin-loop_true-unreach-call_false-termination.i true 3.7   48 42    2 true 210     95 2300    2 error (42) 850    470 9400    0 timeout 900     5000   13000    0 true 130   3800 1500 1 segmentation fault 83   3000 690 0 true 9.0 360 87 2 unknown 890    120 13000   0 out of memory 34    15000 380   0 timeout 900     140 10000    0 timeout 900     170 9300    0 timeout 900     130 2300    0 timeout 900   1200 9300 0 timeout 880   370 7800 0 timeout (timeout) 900    1700   6700   0 timeout 900     2400   11000    0 true 12   490 100 2 true 21   710 180 2 true 280   1000 3800 1 true 55   800 400 2
loop-invgen/apache-escape-absolute_true-unreach-call_true-termination.i timeout 900     2000 9000    0 true 9.7   32 110    2 error (42) 850    470 9000    0 timeout 900     2800   11000    0 true 19   620 140 2 true 66   3700 440 2 true 4.1 280 37 2 unknown 890    100 13000   0 timeout 900    650 13000   0 timeout 900     110 1800    0 timeout 900     310 12000    0 timeout 900     420 11000    0 true 780   990 11000 2 true 880   340 9000 2 timeout (timeout) 900    3500   10000   0 timeout 900     990   14000    0 true 11   500 84 2 true 18   550 130 2 true 19   520 150 2 unknown 670   1200 5400 0
loop-invgen/apache-get-tag_true-unreach-call_true-termination.i true 3.4   43 43    2 true 5.5   33 52    2 error (42) 850    680 8900    0 timeout 900     12000   11000    0 true 19   850 160 2 timeout 910   5600 6900 0 timeout 910   6300 8100 0 unknown 900    100 12000   0 out of memory 140    15000 1500   0 timeout 900     220 13000    0 timeout 900     400 13000    0 timeout 900     640 11000    0 timeout 900   1200 11000 0 true 880   370 9200 2 timeout (timeout) 900    4400   8200   0 timeout 900     1500   13000    0 true 10   480 98 1 true 11   490 97 2 true 12   500 100 1 unknown 650   1400 5300 0
loop-invgen/down_true-unreach-call_true-termination.i timeout 900     1900 8900    0 timeout 900     280 9500    0 error (42) 850    3600 4800    0 timeout 900     9100   11000    0 timeout 900   4100 9000 0 timeout 910   4200 9100 0 timeout 910   12000 8300 0 unknown 89    100 1100   0 true 18    1000 250   1 timeout 900     6900 8800    0 timeout 900     14000 9900    0 out of memory 600     15000 6500    0 timeout 900   1000 12000 0 true 880   460 14000 1 timeout (timeout) 900    730   11000   0 timeout 900     6700   11000    0 timeout 900   4000 12000 0 timeout 900   3600 13000 0 true 9.0 360 71 1 true 19   640 150 1
loop-invgen/fragtest_simple_true-unreach-call_true-termination.i timeout 900     3200 9900    0 timeout 900     260 12000    0 error (42) 850    1600 6200    0 timeout 900     640   11000    0 timeout 900   4400 12000 0 timeout 930   3900 9300 0 timeout 910   15000 9600 0 unknown 91    130 1100   0 true 13    1400 130   1 timeout 900     15000 12000    0 out of memory 450     15000 5800    0 unknown .098 23 .85 0 timeout 900   1100 11000 0 true 880   580 9600 1 timeout (timeout) 900    3400   9400   0 out of memory 250     15000   2900    0 timeout 900   4200 13000 0 timeout 900   4200 12000 0 timeout 900   5100 13000 0 unknown 530   510 3500 0
loop-invgen/half_2_true-unreach-call_true-termination.i timeout 900     2100 12000    0 exception (gremlins) .11  20 .86 0 error (42) 850    1400 6700    0 timeout 900     3500   13000    0 timeout 900   4100 8800 0 timeout 900   5500 7400 0 timeout 910   7700 7500 0 unknown 170    110 2100   0 true 31    1000 410   1 timeout 900     4400 9400    0 timeout 900     9100 9700    0 timeout 900     5400 2500    0 timeout 900   1000 12000 0 true 600   270 8200 1 timeout (timeout) 900    2000   10000   0 timeout 900     5700   11000    0 timeout 900   1500 12000 0 timeout 900   760 15000 0 timeout 900   1400 15000 0 true 21   620 150 1
loop-invgen/heapsort_true-unreach-call_true-termination.i timeout 900     1400 7200    0 exception (gremlins) .22  24 2.1  0 error (42) 850    12000 7100    0 aborted .11  7.9 1.2  0 true 63   2700 600 2 exception 490   4300 3600 0 timeout 900   4900 7900 0 unknown 900    710 12000   0 out of memory 39    15000 370   0 timeout 900     1200 7600    0 timeout 900     2300 8700    0 timeout 900     3200 8000    0 timeout 900   1300 9900 0 true 880   380 7300 2 timeout (timeout) 900    1600   8300   0 timeout 900     730   10000    0 true 200   1100 2500 2 true 67   1000 840 2 error 850   12000 9500 0 timeout (true) 900   1500 4600 0
loop-invgen/id_build_true-unreach-call_true-termination.i true .18  25 1.5  2 true .38  23 3.8  2 error (134) 200    12000 1700    0 timeout 900     6200   11000    0 true 3.1 270 27 2 true 9.4 550 68 2 true 200   1100 2400 2 true 210    1000 2400   2 out of memory 70    15000 970   0 out of memory 420     15000 5300    0 out of memory 240     15000 2700    0 timeout 900     5700 2800    0 timeout 900   1600 7100 0 true 880   550 10000 2 timeout (timeout) 900    1900   9200   0 timeout 900     4100   13000    0 true 6.3 330 49 2 true 7.4 380 63 2 true 11   540 87 2 true 19   630 140 2
loop-invgen/large_const_true-unreach-call_true-termination.i true .23  26 2.3  2 true 41     38 490    2 true .20 17 1.8  2 aborted .11  7.8 1.2  0 true 4.2 300 40 2 true 5.5 310 38 2 true 3.4 270 29 2 true 4.5  310 41   2 true 31    2000 410   2 timeout 900     14000 8400    0 true .091 23 .97 2 true .13  23 .87 2 timeout 900   1500 7900 0 true 1.4 82 16 2 true .16 10   1.9 2 true .24  18   2.3  2 true 8.1 430 64 2 true 8.4 440 62 2 true 30   890 310 2 true 27   720 180 2
loop-invgen/nest-if3_true-unreach-call_true-termination.i true .70  32 8.1  2 true .23  21 2.2  2 error (134) 710    13000 4300    0 timeout 900     9700   11000    0 true 4.4 290 37 2 segmentation fault 23   870 160 0 timeout 900   2600 9100 0 unknown 900    320 7700   0 timeout 900    11000 8700   0 timeout 900     1200 7700    0 timeout 900     2400 8700    0 timeout 900     3400 7500    0 timeout 900   1600 6300 0 true 880   370 11000 2 timeout (timeout) 900    77   12000   0 timeout 900     23   11000    0 true 6.1 330 48 2 true 9.5 480 80 2 true 7.2 340 59 2 true 28   680 180 2
loop-invgen/nested6_true-unreach-call_true-termination.i timeout 900     3200 5300    0 exception (gremlins) 89     41 1000    0 error (42) 850    470 2900    0 timeout 900     5500   13000    0 true 130   4000 1400 2 timeout 960   4000 8800 0 timeout 910   6100 8100 0 unknown 900    4100 8400   0 out of memory 52    15000 540   0 timeout 900     1600 10000    0 timeout 900     2500 11000    0 timeout 900     4600 12000    0 timeout 910   1500 6100 0 true 880   320 9500 2 timeout (timeout) 900    4700   9000   0 timeout 900     2200   11000    0 true 9.0 490 72 2 true 9.5 470 80 2 true 17   520 140 2 unknown 900   2800 6000 0
loop-invgen/nested9_true-unreach-call_true-termination.i timeout 900     280 8400    0 true .27  21 3.2  2 error (134) 170    12000 1400    0 timeout 900     10000   12000    0 true 12   480 92 2 segmentation fault 72   3400 510 0 timeout 900   6100 7800 0 timeout 900    6100 10000   0 out of memory 32    15000 310   0 out of memory 330     15000 3900    0 out of memory 210     15000 2800    0 timeout 900     2500 2200    0 timeout 900   1600 7800 0 true 880   470 9900 2 timeout (timeout) 900    1100   12000   0 timeout 900     5000   10000    0 true 8.9 440 66 2 true 16   510 150 2 true 9.5 410 72 2 true 82   950 810 2
loop-invgen/sendmail-close-angle_true-unreach-call_true-termination.i timeout 900     2200 11000    0 exception (gremlins) 8.9   35 98    0 error (42) 850    4500 10000    0 timeout 900     9400   12000    0 true 16   610 120 2 segmentation fault 880   6500 6900 0 timeout 900   9700 8800 0 unknown 230    82 3000   0 true 38    3500 460   2 timeout 900     4100 12000    0 timeout 900     11000 12000    0 unknown .095 23 1.1  0 true 48   710 500 2 true 880   490 11000 2 timeout (timeout) 900    1000   11000   0 timeout 900     1900   11000    0 true 16   640 140 1 true 20   550 180 2 true 25   630 240 1 true 820   2000 7200 2
loop-invgen/seq_true-unreach-call_true-termination.i timeout 900     1500 10000    0 timeout 900     270 11000    0 error (42) 850    600 6100    0 timeout 900     9100   11000    0 timeout 900   4000 10000 0 timeout 960   3900 9300 0 timeout 900   10000 10000 0 timeout 900    10000 8800   0 true 92    1200 1000   1 timeout 900     690 11000    0 timeout 900     1400 11000    0 timeout 900     2500 13000    0 timeout 900   1000 9900 0 true 880   320 14000 1 timeout (timeout) 900    1900   10000   0 timeout 900     3300   11000    0 timeout 900   1600 12000 0 timeout 900   2500 11000 0 timeout 900   1600 12000 0 true 46   650 430 1
loop-invgen/string_concat-noarr_true-unreach-call_true-termination.i true .12  23 .75 1 timeout 900     250 11000    0 error (42) 850    9400 4600    0 timeout 900     660   9700    0 timeout 900   4300 8900 0 segmentation fault 530   3100 4600 0 timeout 910   7300 8800 0 unknown 900    15000 10000   0 timeout 900    2800 10000   0 out of memory 74     15000 810    0 out of memory 74     15000 780    0 out of memory 74     15000 780    0 timeout 900   1100 10000 0 true 880   670 9600 1 timeout (timeout) 900    120   11000   0 timeout 900     4900   12000    0 timeout 900   1800 13000 0 timeout 900   3300 14000 0 true 9.2 380 68 1 unknown 520   530 4300 0
loop-invgen/up_true-unreach-call_true-termination.i timeout 900     2100 9400    0 timeout 900     260 12000    0 error (42) 850    1400 9000    0 timeout 900     11000   9700    0 timeout 900   4100 11000 0 segmentation fault 23   1100 160 0 out of memory 900   15000 8500 0 unknown 71    100 860   0 true 17    1000 210   1 timeout 900     10000 13000    0 out of memory 570     15000 6900    0 out of memory 380     15000 5200    0 timeout 900   1000 12000 0 true 880   530 13000 1 timeout (timeout) 900    2000   9200   0 timeout 900     4400   11000    0 timeout 900   3100 12000 0 timeout 900   2700 13000 0 timeout 900   5400 13000 0 true 19   620 140 1
loop-lit/afnp2014_true-unreach-call_true-termination.c.i timeout 900     2200 11000    0 true 1.1   21 14    2 true 14    150 160    2 timeout 900     610   11000    0 true 9.3 450 73 2 true 77   3300 660 2 true 12   730 110 2 unknown 86    76 1100   0 true 2.5  230 29   2 timeout 900     3500 12000    0 timeout 900     7700 13000    0 out of memory 760     15000 8300    0 timeout 900   1000 10000 0 true 880   730 11000 2 true 6.2  13   83   2 true 47     200   580    2 true 6.6 330 49 2 timeout 900   1100 12000 0 true 7.4 350 54 2 true 15   520 110 2
loop-lit/bhmr2007_true-unreach-call_true-termination.c.i timeout 900     300 12000    0 true 27     36 290    2 error (42) 850    350 9200    0 timeout 900     11000   13000    0 true 2.8 270 25 1 timeout 960   3200 8500 0 timeout 900   2700 8300 0 timeout 900    2200 10000   0 false(unreach-call) 130    880 1600   -16 timeout 900     84 12000    0 timeout 900     130 13000    0 timeout 900     190 14000    0 true 29   670 250 2 true 880   120 11000 2 timeout (timeout) 900    50   11000   0 timeout 900     2300   11000    0 true 8.7 460 74 2 true 6.8 330 58 2 true 11   480 88 2 true 26   600 240 2
loop-lit/cggmp2005_true-unreach-call_true-termination.c.i true .34  27 3.5  2 true .36  22 3.6  2 true .28 17 2.9  2 true 6.3   10   69    2 true 2.8 270 26 2 true 2.8 270 22 2 true 2.3 240 20 2 true 3.2  270 29   2 true .14 23 1.6 2 timeout 900     9600 11000    0 true .28  23 .79 2 true .12  23 .75 2 true 9.2 380 77 2 true 1.3 82 15 2 true .13 9.4 1.6 2 true .079 9.8 .46 2 true 7.5 390 55 2 true 7.3 380 64 2 true 8.8 400 67 2 true 14   490 88 2
loop-lit/cggmp2005_variant_true-unreach-call_true-termination.c.i timeout 900     1700 9200    0 true .88  24 10    2 error (42) 850    4000 5200    0 timeout 900     6200   11000    0 true 2.9 270 28 2 timeout 900   9000 7500 0 timeout 910   8900 10000 0 timeout 900    8500 9100   0 false(unreach-call) 3.0  220 38   -16 timeout 900     3300 9200    0 timeout 900     7500 12000    0 timeout 900     11000 9700    0 true 8.2 350 71 2 true 330   630 4400 2 true .17 9.3 1.5 2 true .058 9.9 .49 2 true 8.2 390 65 2 true 6.9 330 57 2 true 8.8 410 77 2 true 17   600 110 2
loop-lit/cggmp2005b_true-unreach-call_true-termination.c.i true .95  35 13    2 true .57  20 5.2  2 true .96 17 11    2 timeout 900     330   14000    0 true 4.6 290 37 2 true 4.3 270 31 2 true 3.5 260 27 2 true 4.5  260 42   2 true 6.8  990 63   2 timeout 900     5800 11000    0 true .39  52 4.9  2 true .10  23 .88 2 timeout 910   1700 6000 0 true 54   1000 650 2 true .15 9.4 1.6 2 true .064 9.8 .72 2 true 6.9 350 57 2 true 8.1 370 65 2 true 7.7 350 58 2 true 13   450 93 2
loop-lit/css2003_true-unreach-call_true-termination.c.i timeout 900     260 10000    0 true 1.0   31 13    2 error (42) 850    820 5100    0 timeout 900     9800   12000    0 true 3.0 270 27 2 true 3.9 280 29 2 true 3.0 270 25 2 unknown 51    77 660   0 true 5.0  510 62   2 out of memory 450     15000 5400    0 out of memory 220     15000 2600    0 out of memory 150     15000 1800    0 timeout 900   1400 7100 0 true 410   470 6200 2 true 7.1  360   98   2 out of memory 510     15000   6300    0 true 6.4 340 49 2 true 6.3 330 46 2 true 5.9 330 49 2 true 16   560 110 2
loop-lit/ddlm2013_true-unreach-call.i timeout 900     2100 11000    0 false(unreach-call) 16     30 180    -16 error (42) 850    1300 9000    0 timeout 900     15000   13000    0 true 160   3700 1700 1 timeout 930   6200 9300 0 timeout 910   8400 9600 0 unknown 210    310 2200   0 true 4.7  440 62   1 out of memory 170     15000 1400    0 out of memory 330     15000 2600    0 unknown .30  23 .72 0 timeout 900   1100 11000 0 true 880   310 11000 1 timeout (timeout) 900    74   10000   0 timeout 900     3200   14000    0 timeout 900   2500 12000 0 timeout 900   1200 11000 0 true 11   520 90 1 unknown 310   1200 3600 0
loop-lit/gj2007_true-unreach-call_true-termination.c.i true 5.2   82 65    2 timeout 900     290 9800    0 true 1.0  17 11    2 timeout 900     590   11000    0 true 60   3000 670 2 true 4.1 280 30 2 true 3.1 270 25 2 unknown 36    76 420   0 true .15 23 2.0 2 timeout 900     5600 11000    0 true .45  43 5.5  2 true 58     680 130    2 timeout 900   1000 11000 0 timeout 880   580 10000 0 true .16 9.4 1.5 2 true .075 9.9 .46 2 true 69   1700 650 2 true 140   1300 1800 2 true 86   1400 780 2 true 21   520 150 2
loop-lit/gj2007b_true-unreach-call_true-termination.c.i timeout 900     1400 13000    0 true 2.6   32 21    2 error (42) 850    2800 9000    0 timeout 900     12000   11000    0 true 20   640 160 2 timeout 900   4300 6100 0 timeout 900   3400 9500 0 unknown 210    130 2800   0 true 8.1  380 94   2 timeout 900     5100 13000    0 timeout 900     11000 11000    0 out of memory 850     15000 11000    0 true 28   680 280 2 true 880   370 14000 2 timeout (timeout) 900    1700   9000   0 timeout 900     920   12000    0 true 7.7 390 56 2 true 7.2 370 63 2 true 11   520 81 1 true 15   500 110 2
loop-lit/gr2006_true-unreach-call_true-termination.c.i true 9.0   120 110    2 timeout 900     290 11000    0 true .97 19 11    2 timeout 900     650   11000    0 true 67   2400 640 2 true 4.9 290 38 2 true 3.2 260 28 2 unknown 140    120 1800   0 true .18 23 1.5 2 timeout 900     5000 11000    0 true .49  48 6.8  2 true 14     740 160    2 timeout 900   1300 9300 0 true 550   440 7100 2 true .15 9.3 1.7 2 true .058 9.7 .66 2 true 59   1600 560 2 true 750   1400 13000 2 true 71   1700 680 2 true 21   600 170 2
loop-lit/gsv2008_true-unreach-call_true-termination.c.i timeout 900     810 7200    0 true .27  20 1.6  2 true 220    620 2000    2 timeout 900     8400   13000    0 true 3.4 270 32 1 true 860   5200 7900 2 true 880   4900 9900 2 unknown 900    620 7100   0 false(unreach-call) 7.3  220 79   -16 timeout 900     1500 2300    0 timeout 900     6200 9400    0 timeout 900     8900 9200    0 true 17   520 170 2 true 880   330 12000 2 timeout (timeout) 900    60   11000   0 out of memory 610     15000   8900    0 true 7.0 340 54 2 true 7.3 360 58 2 true 7.1 370 50 2 true 130   540 1300 2
loop-lit/hhk2008_true-unreach-call_true-termination.c.i timeout 900     390 14000    0 true .80  23 9.9  2 error (42) 850    260 11000    0 timeout 900     5200   13000    0 true 3.2 270 27 2 segmentation fault 53   2000 430 0 timeout 910   8000 9100 0 timeout 900    8000 8800   0 false(unreach-call) 2.7  150 33   -16 timeout 900     420 11000    0 timeout 900     740 13000    0 timeout 900     1000 14000    0 true 7.0 350 61 2 true 140   390 1900 2 true .17 9.3 1.5 2 true .13  18   1.2  2 true 8.9 410 66 2 true 6.6 330 46 2 true 8.1 370 67 2 true 15   510 100 2
loop-lit/jm2006_true-unreach-call_true-termination.c.i timeout 900     1500 10000    0 exception (gremlins) 2.4   35 21    0 error (42) 850    6900 4400    0 timeout 900     5000   11000    0 true 2.8 280 25 2 true 4.8 300 32 2 true 2.8 260 24 2 true 3.8  270 38   2 false(unreach-call) 1.4  140 16   -16 timeout 900     2300 12000    0 timeout 900     4900 11000    0 timeout 900     7600 11000    0 true 6.8 330 57 2 true 880   1000 11000 2 true .16 9.8 1.7 2 true .097 9.9 .77 2 true 8.7 450 62 2 true 6.7 330 48 2 true 9.9 500 74 2 true 18   640 130 2
loop-lit/jm2006_variant_true-unreach-call_true-termination.c.i timeout 900     1700 11000    0 true 6.0   35 62    2 error (42) 850    5300 3900    0 timeout 900     5100   13000    0 true 4.0 280 32 2 timeout 900   8300 6800 0 timeout 910   10000 8400 0 timeout 900    10000 8300   0 false(unreach-call) 2.0  210 27   -16 timeout 900     2000 11000    0 timeout 900     4800 12000    0 timeout 900     8000 12000    0 true 9.2 380 75 2 true 290   620 3400 2 true .15 9.9 1.7 2 true .10  9.9 .96 2 true 8.8 450 63 2 true 6.5 320 50 2 true 11   470 88 2 true 16   610 110 2
loop-lit/mcmillan2006_true-unreach-call_true-termination.c.i out of memory 890     15000 6700    0 false(unreach-call) .33  21 2.9  -16 error (42) 850    6000 8000    0 aborted .10  7.8 1.1  0 false(unreach-call) 3.5 280 33 -16 timeout 900   3900 11000 0 timeout 960   1000 12000 0 unknown 890    100 11000   0 timeout 900    880 11000   0 timeout 900     150 9200    0 timeout 900     180 10000    0 timeout 900     210 10000    0 unknown 5.7 350 41 0 true 880   360 10000 1 unknown 140    330   1800   0 unknown .052 9.9 .64 0 timeout 900   960 13000 0 timeout 900   830 13000 0 timeout 900   1000 13000 0 true 640   800 6100 1
loop-lit/gcnr2008_false-unreach-call_false-termination.i false(unreach-call) .10  23 1.1  1 false(unreach-call) .066 20 .58 1 false(unreach-call) .14 17 .79 1 false(unreach-call) .18  7.8 2.1  1 false(unreach-call) 3.0 270 27 1 false(unreach-call) 5.5 310 36 1 false(unreach-call) 2.6 250 19 1 false(unreach-call) 16    79 190   1 false(unreach-call) 100    1900 1200   1 false(unreach-call) .093 23 .78 1 false(unreach-call) .28  23 .79 1 false(unreach-call) .088 23 .89 1 false(unreach-call) 5.9 350 48 1 false(unreach-call) 1.7 83 25 1 false(unreach-call) .16 9.4 1.8 1 false(unreach-call) .078 9.8 .62 1 false(unreach-call) 6.5 360 51 1 false(unreach-call) 6.1 320 46 1 false(unreach-call) 5.8 320 48 1 false(unreach-call) 9.9 280 73 1
loop-new/count_by_1_true-unreach-call_true-termination.i true .16  23 1.2  2 true .19  22 1.8  1 true 87    3100 1100    2 timeout 900     660   10000    0 timeout 900   4200 8800 0 true 3.0 270 25 2 true 350   3100 4000 2 true 350    3500 4000   2 false(unreach-call) .16 23 1.5 -16 timeout 900     10000 12000    0 out of memory 300     15000 3300    0 true .074 23 .80 2 timeout 900   1000 11000 0 true 1.2 66 17 2 true .15 9.4 1.3 2 true .049 9.7 .72 2 timeout 900   2800 13000 0 timeout 900   3200 13000 0 true 6.3 370 49 2 true 11   420 73 2
loop-new/count_by_1_variant_true-unreach-call_true-termination.i true .12  23 1.6  2 true .21  21 1.7  2 out of memory 130    15000 1400    0 true .61  7.8 8.4  2 true 3.9 280 36 2 true 3.2 270 26 2 true 350   3000 4100 2 unknown 37    75 430   0 true .23 30 3.0 2 timeout 900     14000 14000    0 out of memory 390     15000 5300    0 out of memory 120     15000 1500    0 timeout 900   1000 10000 0 true 37   160 470 2 true 2.9  370   48   2 true 64     4900   690    2 true 7.1 340 59 2 true 6.4 330 56 2 true 8.4 370 61 2 true 14   360 97 2
loop-new/count_by_2_true-unreach-call_true-termination.i timeout 900     1200 11000    0 exception (gremlins) 210     150 2300    0 true 44    1600 530    1 timeout 900     680   10000    0 timeout 900   4200 11000 0 timeout 910   5100 9200 0 timeout 910   8800 8900 0 unknown 57    75 690   0 false(unreach-call) .15 23 1.6 -16 timeout 900     10000 13000    0 out of memory 310     15000 3600    0 timeout 900     13000 8900    0 timeout 900   1100 10000 0 true 1.1 68 13 1 true .16 9.2 1.5 1 true .052 9.7 .47 1 timeout 900   2600 14000 0 timeout 900   3000 12000 0 timeout 900   1700 15000 0 true 12   440 86 1
loop-new/count_by_k_true-unreach-call_true-termination.i timeout 900     1200 12000    0 timeout 900     770 13000    0 error (42) 850    10000 3500    0 timeout 900     4400   11000    0 timeout 900   4100 11000 0 timeout 910   5300 7700 0 timeout 900   4500 9600 0 unknown 78    75 1100   0 false(unreach-call) 5.6  160 79   -16 out of memory 150     15000 1700    0 out of memory 150     15000 1800    0 timeout 900     10000 10000    0 timeout 900   1000 11000 0 true 400   360 5200 1 timeout (timeout) 900    11   12000   0 timeout 900     3100   12000    0 timeout 900   1200 11000 0 timeout 900   3500 15000 0 timeout 900   820 11000 0 true 13   470 110 1
loop-new/count_by_nondet_true-unreach-call_true-termination.i timeout 900     2100 12000    0 timeout 900     260 9700    0 error (42) 850    1500 7300    0 timeout 900     700   9500    0 timeout 900   4300 8700 0 timeout 910   3300 9000 0 timeout 900   3700 10000 0 timeout 900    3800 10000   0 out of memory 110    15000 1400   0 out of memory 330     15000 2900    0 timeout 900     2800 9800    0 timeout 900     3500 8800    0 timeout 900   1000 10000 0 true 59   220 730 1 timeout (timeout) 900    110   12000   0 timeout 900     89   11000    0 timeout 900   4800 12000 0 timeout 900   4800 14000 0 timeout 900   2900 14000 0 unknown 670   620 6500 0
loop-new/gauss_sum_true-unreach-call_true-termination.i timeout 900     1700 11000    0 exception (gremlins) .34  24 2.0  0 true 19    130 200    1 timeout 900     15000   14000    0 error 3.1 280 27 0 true 84   4200 640 2 true 280   3000 2600 2 unknown 550    120 6200   0 false(unreach-call) 1.8  140 24   -16 out of memory 530     15000 6200    0 out of memory 250     15000 3500    0 out of memory 310     15000 3500    0 timeout 900   1000 11000 0 true 880   650 12000 1 true .23 10   2.1 1 true .65  17   7.8  1 timeout 900   2900 12000 0 timeout 900   800 13000 0 true 14   560 130 1 true 37   560 290 1
loop-new/half_true-unreach-call_true-termination.i timeout 900     1800 10000    0 exception (gremlins) 1.2   22 15    0 error (42) 850    8200 3500    0 timeout 900     13000   13000    0 true 4.3 280 35 2 timeout 900   5500 8000 0 timeout 910   6100 8500 0 unknown 74    76 990   0 false(unreach-call) 1.3  110 14   -16 out of memory 400     15000 5500    0 out of memory 880     15000 2400    0 out of memory 470     15000 4500    0 timeout 900   1500 7300 0 true 880   260 12000 2 timeout (timeout) 900    2200   8800   0 unknown .074 9.5 .50 0 true 12   520 99 2 timeout 900   830 12000 0 true 17   530 170 2 unknown 220   300 2300 0
loop-new/nested_true-unreach-call_true-termination.i timeout 900     2500 5500    0 timeout 900     280 11000    0 error (42) 850    3800 6100    0 timeout 900     12000   12000    0 true 120   2300 1400 2 segmentation fault 39   2600 250 0 timeout 900   2600 9500 0 unknown 900    480 7400   0 out of memory 890    15000 10000   0 timeout 900     2900 7100    0 timeout 900     5400 8800    0 timeout 900     9200 9400    0 timeout 900   1100 12000 0 true 880   510 11000 2 true .16 11   1.7 2 unknown .068 9.7 .44 0 true 110   4600 1300 2 true 120   1400 1600 1 true 120   4500 1400 2 timeout 900   760 5500 0
loop-industry-pattern/aiob_1_true-unreach-call.c true .35  29 2.7  2 false(unreach-call) 48     100 490    -16 true 3.6  24 34    1 out of memory 20     15000   230    0 true 120   2300 1500 2 true 35   1100 280 2 true 25   670 210 2 true 58    620 710   2 true .21 25 2.5 2 out of memory 290     15000 4700    0 true .82  82 11    2 true 3.3   240 45    2 unknown 8.6 670 70 0 true 880   290 9800 2 true .17 9.9 2.0 2 unknown .055 10   .58 0 error 8.2 320 65 0 error 8.6 310 70 0 error 8.4 300 61 0 true 67   670 670 2
loop-industry-pattern/aiob_2_true-unreach-call.c true .35  30 3.4  2 false(unreach-call) 48     100 600    -16 true 3.9  24 35    1 out of memory 20     15000   220    0 true 130   2200 1300 2 true 32   920 230 2 true 24   650 280 2 true 59    640 690   2 true .25 25 2.2 2 out of memory 290     15000 3900    0 true .84  81 10    2 true 3.3   240 45    2 unknown 8.9 680 62 0 true 880   310 9800 2 true .19 9.9 1.9 2 unknown .075 10   .60 0 error 7.9 330 62 0 error 8.4 310 69 0 error 9.0 330 74 0 true 66   690 650 2
loop-industry-pattern/aiob_3_true-unreach-call.c true .38  29 3.6  2 false(unreach-call) 47     100 570    -16 true 3.7  24 33    1 out of memory 20     15000   240    0 true 130   2200 1600 2 true 36   1200 260 2 true 24   600 250 2 true 59    620 810   2 true .25 25 2.3 2 out of memory 290     15000 3900    0 true .83  81 9.5  2 true 3.3   240 48    2 unknown 8.3 670 72 0 true 880   290 10000 2 true .19 10   2.1 2 unknown .061 10   .50 0 error 8.0 300 63 0 error 7.9 310 59 0 error 8.7 320 68 0 true 66   670 620 2
loop-industry-pattern/aiob_4_true-unreach-call.c true .39  30 3.0  2 false(unreach-call) 46     88 590    -16 true 3.9  23 32    1 out of memory 20     15000   250    0 true 120   2100 1400 2 true 33   950 230 2 true 24   620 290 2 true 46    620 520   2 true .22 25 2.6 2 out of memory 300     15000 4000    0 true 3.4   81 7.9  2 unknown .11  25 1.4  0 unknown 8.4 660 68 0 true 880   240 9800 2 true .17 10   2.0 2 unknown .056 9.9 .59 0 error 8.6 310 69 0 error 8.1 300 67 0 error 8.3 310 65 0 true 76   710 880 2
loop-industry-pattern/mod3_true-unreach-call.c true .48  27 5.9  2 false(unreach-call) .066 17 .75 -16 error (42) 850    200 9900    0 unknown 1.6   19   19    0 true 3.2 280 28 2 true 14   380 110 2 true 69   340 770 2 unknown 890    90 11000   0 timeout 900    290 13000   0 timeout 900     130 12000    0 timeout 900     150 13000    0 unknown 2.5   23 31    0 unknown 6.6 340 52 0 true 1.4 78 17 2 timeout (timeout) 900    89   12000   0 timeout 900     6200   13000    0 true 26   330 280 2 timeout 900   510 12000 0 true 21   370 210 2 true 20   570 170 2
loop-industry-pattern/nested_true-unreach-call.c timeout 900     270 8800    0 true 230     110 2700    1 error (1) 360    15000 4000    0 aborted .12  7.9 1.6  0 timeout 900   4000 10000 0 segmentation fault 39   2200 270 0 timeout 900   4200 9700 0 unknown 900    530 7400   0 out of memory 62    15000 840   0 timeout 900     530 10000    0 out of memory 290     15000 3700    0 timeout 900     2600 6900    0 timeout 900   1300 6100 0 true 880   510 11000 1 error .50 78   6.9 0 out of memory 140     15000   1600    0 timeout 900   2300 15000 0 timeout 900   3100 14000 0 true 21   800 170 1 true 500   1000 5500 1
loop-industry-pattern/ofuf_1_true-unreach-call.c error (5) .24  30 2.3  0 false(unreach-call) 2.2   35 21    -16 error (42) 850    510 13000    0 out of memory 33     15000   440    0 error 12   490 99 0 error 9.3 450 66 0 error 9.0 460 66 0 unknown 500    600 6900   0 timeout 900    1800 12000   0 unknown .66  25 9.1  0 unknown .71  25 10    0 unknown .13  25 1.1  0 unknown 40   1300 260 0 true 2.9 160 35 1 timeout (timeout) 900    150   11000   0 unknown .090 10   .48 0 error 8.4 320 66 0 error 8.3 300 59 0 error 8.4 310 73 0 true 140   820 1500 1
loop-industry-pattern/ofuf_2_true-unreach-call.c error (5) .27  32 2.0  0 exception (gremlins) .10  22 .80 0 error (42) 850    380 9400    0 out of memory 32     15000   390    0 error 12   480 98 0 error 8.7 460 67 0 error 9.0 440 67 0 unknown 500    600 7500   0 timeout 900    1800 12000   0 unknown .69  25 7.8  0 unknown .71  25 8.9  0 unknown .10  25 1.1  0 unknown 38   1300 280 0 true 3.2 160 38 1 timeout (timeout) 900    160   11000   0 unknown .076 10   .61 0 error 8.5 310 67 0 error 8.2 300 66 0 error 9.8 340 72 0 true 110   810 1000 1
loop-industry-pattern/ofuf_3_true-unreach-call.c error (5) .28  30 1.8  0 exception (gremlins) .087 23 .95 0 error (42) 850    570 9500    0 out of memory 32     15000   400    0 error 12   480 91 0 error 8.5 450 66 0 error 9.3 450 74 0 unknown 490    600 5800   0 timeout 900    1800 11000   0 unknown .65  25 8.4  0 unknown .68  25 8.7  0 unknown .13  25 1.0  0 unknown 40   1300 270 0 true 2.7 160 35 1 timeout (timeout) 900    160   12000   0 unknown .084 9.8 .53 0 error 8.1 300 66 0 error 8.7 320 67 0 error 8.2 320 65 0 true 110   790 980 1
loop-industry-pattern/ofuf_4_true-unreach-call.c error (5) .25  30 2.4  0 false(unreach-call) 2.6   36 24    -16 error (42) 850    500 9200    0 out of memory 32     15000   390    0 error 11   490 92 0 error 9.3 500 58 0 error 8.6 440 67 0 unknown 480    590 5500   0 timeout 900    1700 11000   0 unknown .64  25 7.5  0 unknown .62  25 8.2  0 unknown .10  25 1.1  0 unknown 61   1400 370 0 true 2.6 160 31 1 timeout (timeout) 900    160   12000   0 unknown .080 10   .52 0 error 8.0 300 63 0 error 8.8 320 60 0 error 8.2 330 65 0 true 14   300 100 1
loop-industry-pattern/ofuf_5_true-unreach-call.c error (5) .25  30 2.0  0 exception (gremlins) .22  23 2.4  0 error (42) 850    530 9900    0 out of memory 32     15000   420    0 error 11   490 91 0 error 8.9 470 57 0 error 9.2 460 68 0 unknown 470    560 7000   0 timeout 900    1700 11000   0 unknown .60  25 8.1  0 unknown .62  25 7.0  0 unknown .13  25 1.2  0 unknown 42   1300 280 0 true 2.6 150 39 1 timeout (timeout) 900    160   9500   0 unknown .059 10   .64 0 error 8.3 320 66 0 error 8.2 310 70 0 error 8.4 320 69 0 true 14   280 94 1
loops/heavy_true-unreach-call.c out of memory 31     15000 380    0 true .051 15 .57 1 error (42) 850    3600 9500    0 aborted .14  18   1.4  0 true 2.7 270 21 1 true 3.9 280 29 2 true 93   2200 1300 1 true 330    5300 3700   1 out of memory 780    15000 3100   0 timeout 900     4400 11000    0 out of memory 860     15000 11000    0 true 19     4400 240    1 unknown 8.4 700 73 0 timeout 900   3400 10000 0 true .40 30   4.7 1 timeout 900     60   10000    0 timeout 900   7000 9500 0 timeout 900   7300 7000 0 timeout 900   6900 7300 0 true 15   1800 130 1
loops/compact_false-unreach-call.c timeout 900     3000 8800    0 timeout 900     340 10000    0 out of memory 130    15000 1700    0 aborted .098 7.9 1.2  0 timeout 900   4200 10000 0 timeout 910   4500 8600 0 timeout 900   6200 8900 0 unknown 78    100 990   0 timeout 900    4400 11000   0 timeout 900     7000 11000    0 out of memory 340     15000 4700    0 timeout 900     460 2500    0 timeout 900   1000 9000 0 timeout 880   940 12000 0 timeout (timeout) 900    60   11000   0 out of memory 860     15000   8700    0 timeout 900   5200 8000 0 timeout 900   5200 9700 0 timeout 900   5200 9400 0 out of memory 240   15000 1700 0
loops/heavy_false-unreach-call.c out of memory 31     15000 380    0 timeout 900     1400 9300    0 out of memory 410    15000 5200    0 aborted .14  18   1.5  0 timeout 900   4800 11000 0 timeout 910   4400 9300 0 timeout 900   4100 8900 0 unknown 890    5400 10000   0 out of memory 320    15000 3800   0 timeout 900     4400 12000    0 out of memory 870     15000 12000    0 out of memory 640     15000 7400    0 unknown 8.3 710 61 0 timeout 900   3400 11000 0 false(unreach-call) .37 29   4.7 0 timeout 900     56   11000    0 timeout 900   6800 7400 0 timeout 900   7300 7400 0 timeout 900   6800 7400 0 out of memory 520   15000 6000 0
../../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score
total 156 51000 220000 550000 145 156 27000 14000 310000 -214 156 49000 570000 430000 107 156 40000 440000 520000 33 156 32000   220000 340000 115 156 40000 370000 360000 151 156 51000 450000 520000 157 156 40000 140000 450000 120 156 27000 400000 300000 -295 156 78000 960000 910000 36 156 48000 820000 580000 96 156 44000 510000 450000 118 156 55000 120000 600000 98 156 60000 63000 720000 194 156 39000   170000 470000 136 156 28000 220000 350000 60 156 44000 200000 590000 156 156 49000 190000 650000 147 156 39000 210000 490000 162 156 24000   240000 220000 194
    correct results 89 550 12000 3500 142 72 430 1800 4700 115 67 500 8100 5000 96 24 910 6400 10000 33 94 1400   53000 14000 155 91 2300 66000 19000 149 94 5100 77000 57000 152 75 3400 36000 38000 117 67 4500 59000 52000 107 36 390 3600 3700 36 63 190 7700 1000 91 75 1100 9900 11000 116 60 1900 27000 22000 96 103 25000 23000 300000 170 76 29   1500 360 123 72 330 7600 4300 115 92 1800 45000 19000 150 89 3100 39000 40000 143 91 3100 46000 34000 148 101 8000   57000 78000 168
        correct true 53 89 2400 980 106 43 320 1100 3500 86 29 460 5900 4600 58 9 760 5800 8400 18 61 1300   43000 13000 122 58 2000 48000 17000 116 58 4600 58000 51000 116 42 2800 33000 32000 84 40 1500 38000 17000 80 0 28 160 5100 700 56 41 260 4700 2800 82 36 1300 16000 16000 72 67 25000 19000 300000 134 47 24   1200 310 94 43 300 7200 3800 86 58 1300 31000 14000 116 54 1800 24000 24000 108 57 1400 30000 15000 114 67 6600   39000 66000 134
        correct false 36 470 9400 2600 36 29 110 680 1200 29 38 40 2300 460 38 15 150 570 1700 15 33 140   11000 1300 33 33 350 19000 2500 33 36 550 19000 5900 36 33 580 3100 6700 33 27 3000 20000 35000 27 36 390 3600 3700 36 35 30 2500 350 35 34 820 5200 8100 34 24 650 10000 6400 24 36 430 3600 5800 36 29 4.9 280 50 29 29 30 440 410 29 34 510 14000 5100 34 35 1300 15000 16000 35 34 1700 15000 19000 34 34 1400   19000 12000 34
    correct-unconfimed results 3 310 4200 3300 3 13 340 460 3900 7 15 250 12000 3100 11 0 11 380   12000 4000 8 4 630 7000 6200 2 5 130 5200 1600 5 8 390 7900 4600 3 27 680 14000 9000 14 7 700 2600 9500 0 12 1100 26000 15000 5 6 33 4800 410 2 4 31 1400 240 2 29 13000 17000 170000 24 26 230   15000 3200 13 14 860 4400 11000 9 6 640 3600 7800 6 4 200 3200 2400 4 14 680 7600 8600 14 27 5300   19000 53000 26
        correct-unconfirmed true 3 310 4200 3300 3 7 280 280 3300 7 11 130 5500 1500 11 0 8 310   9400 3400 8 2 12 680 78 2 5 130 5200 1600 5 3 350 6900 4000 3 14 200 9700 2500 14 0 5 270 13000 3400 5 2 21 4400 260 2 2 13 690 100 2 24 13000 13000 170000 24 13 230   15000 3100 13 9 730 3500 9500 9 6 640 3600 7800 6 4 200 3200 2400 4 14 680 7600 8600 14 26 5300   18000 53000 26
        correct-unconfirmed false 0 6 64 180 620 0 4 120 6200 1600 0 0 3 63   2500 580 0 2 620 6300 6100 0 0 5 42 1100 590 0 13 470 4600 6500 0 7 700 2600 9500 0 7 810 14000 12000 0 4 12 380 150 0 2 18 750 140 0 5 170 4100 2000 0 13 4.4 150 59 0 5 130 860 1800 0 0 0 0 1 9.8 280 72 0
    incorrect results 0 21 350 860 4000 -336 0 0 2 25   1100 220 -48 0 0 0 26 1200 10000 16000 -416 0 0 0 0 0 0 2 89 640 1100 -64 0 0 0 0
        incorrect true 0 0 0 0 1 21   800 190 -32 0 0 0 0 0 0 0 0 0 0 2 89 640 1100 -64 0 0 0 0
        incorrect false 0 21 350 860 4000 -336 0 0 1 3.5 280 33 -16 0 0 0 26 1200 10000 16000 -416 0 0 0 0 0 0 0 0 0 0 0
score (156 tasks, max score: 261) 145 -214 107 33 115 151 157 120 -295 36 96 118 98 194 136 60 156 147 162 194
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