Tool 2LS 0.5.0 BLAST 2.7.3 CBMC 5.6 Ceagle Ceagle 1.3 @ 53cfa89 CPAchecker 1.6.1-svn 23987 CPAchecker 1.6.1-svn 24048 DepthK DepthK version 3.0 - Fri Jan 6 18:14:20 AMT 2017 ESBMC ESBMC version 3.1 64-bit x86_64 linux SMACK+Corral 1.7.2 symbiotic KLEE:7f3c74aa-dg:96e851cf-symbiotic:69a1d8e6-minisat:3db58943-stp:39fa956f-LLVMInstrumentation:f750b24a 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: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-Recursive blast.sv-comp17.ReachSafety-Recursive cbmc.sv-comp17.ReachSafety-Recursive ceagle.sv-comp17.ReachSafety-Recursive cpa-bam-bnb.sv-comp17.ReachSafety-Recursive cpa-kind.sv-comp17.ReachSafety-Recursive cpa-seq.sv-comp17.ReachSafety-Recursive depthk.sv-comp17.ReachSafety-Recursive esbmc.sv-comp17.ReachSafety-Recursive esbmc-falsi.sv-comp17.ReachSafety-Recursive esbmc-incr.sv-comp17.ReachSafety-Recursive esbmc-kind.sv-comp17.ReachSafety-Recursive smack.sv-comp17.ReachSafety-Recursive symbiotic4.sv-comp17.ReachSafety-Recursive symdivine.sv-comp17.ReachSafety-Recursive uautomizer.sv-comp17.ReachSafety-Recursive ukojak.sv-comp17.ReachSafety-Recursive utaipan.sv-comp17.ReachSafety-Recursive veriabs.sv-comp17.ReachSafety-Recursive
Options --graphml-witness witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/2ls.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/2ls.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/2ls.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/2ls.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] -alias empty -enable-recursion -noprofile -cref -sv-comp -lattice -include-lattice symb -nosserr -svcomp-witness error-witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/blast.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/blast.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/blast.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/blast.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] --graphml-witness witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cbmc.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cbmc.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cbmc.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cbmc.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] --compiler clang-3.7 [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ceagle.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ceagle.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ceagle.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ceagle.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] -sv-comp17-bam-bnb -disable-java-assertions -heap 10000m [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-bam-bnb.2017-01-10_2044.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-bam-bnb.2017-01-10_2044.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-bam-bnb.2017-01-10_2044.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-bam-bnb.2017-01-10_2044.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] -sv-comp17-k-induction -heap 10000M -disable-java-assertions [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-kind.2017-01-10_2204.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-kind.2017-01-10_2204.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-kind.2017-01-10_2204.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-kind.2017-01-10_2204.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] -sv-comp17 -heap 10000M -disable-java-assertions [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-seq.2017-01-11_1118.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-seq.2017-01-11_1118.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-seq.2017-01-11_1118.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-seq.2017-01-11_1118.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/depthk.2017-01-11_1124.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/depthk.2017-01-11_1124.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/depthk.2017-01-11_1124.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/depthk.2017-01-11_1124.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] -s fixed [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc.2017-01-11_1131.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc.2017-01-11_1131.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc.2017-01-11_1131.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc.2017-01-11_1131.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] -s falsi [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-falsi.2017-01-11_1509.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-falsi.2017-01-11_1509.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-falsi.2017-01-11_1509.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-falsi.2017-01-11_1509.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] -s incr [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-incr.2017-01-11_1616.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-incr.2017-01-11_1616.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-incr.2017-01-11_1616.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-incr.2017-01-11_1616.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] -s kinduction [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-kind.2017-01-12_1202.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-kind.2017-01-12_1202.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-kind.2017-01-12_1202.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-kind.2017-01-12_1202.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] -w error-witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/smack.2017-01-13_1109.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/smack.2017-01-13_1109.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/smack.2017-01-13_1109.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/smack.2017-01-13_1109.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] --witness witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/symbiotic4.2017-01-13_1110.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/symbiotic4.2017-01-13_1110.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/symbiotic4.2017-01-13_1110.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/symbiotic4.2017-01-13_1110.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] --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
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c error (5) .12  22 .67 0 exception (gremlins) 2.5   32   25    0 false(unreach-call) 1.3  91 17    1 unknown .34  7.9 3.8  0 error 2.8 280 26 0 error 3.0 270 27 0 false(unreach-call) 4.6 310 40 1 out of memory (false(no-overflow)) 710    15000 8800   0 out of memory 260    15000 3700    0 false(unreach-call) .47  23 1.3  1 false(unreach-call) .15  23 1.8  1 false(unreach-call) .16  25 2.1  1 false(unreach-call) 1.6 75 20 1 false(unreach-call) .19 10   1.6 1 false(unreach-call) 8.4   34   130    1 false(unreach-call) 7.3 370 55 1 timeout 900   1400 10000 0 false(unreach-call) 8.0 360 62 1 unknown 830   480 4500 0
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c error (5) .10  22 .68 0 false(unreach-call) 1.1   22   11    1 false(unreach-call) .13 19 1.1  1 false(unreach-call) .17  7.9 1.9  1 error 3.0 280 29 0 error 3.0 270 24 0 false(unreach-call) 3.5 300 28 1 false(unreach-call) 1.1  50 15   1 out of memory 230    15000 3000    0 false(unreach-call) .091 23 .93 1 false(unreach-call) .11  23 1.1  1 false(unreach-call) .13  23 1.1  1 false(unreach-call) 1.6 78 20 1 false(unreach-call) .15 9.9 1.7 1 timeout 900     28   7800    0 false(unreach-call) 6.4 320 53 1 false(unreach-call) 6.9 330 54 1 false(unreach-call) 7.1 340 58 1 error (124) 900   5100 6700 0
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c error (5) .11  22 .74 0 false(unreach-call) .27  21   2.6  1 false(unreach-call) .14 17 1.0  1 aborted .13  7.8 1.4  0 error 2.8 270 26 0 false(unreach-call) 3.9 330 32 1 false(unreach-call) 2.8 280 25 1 false(unreach-call) .86 49 12   1 false(unreach-call) 7.6  580 91    1 false(unreach-call) .073 23 .88 1 false(unreach-call) .081 23 .87 1 false(unreach-call) .10  23 .89 1 false(unreach-call) 1.5 76 21 0 false(unreach-call) .15 9.4 1.7 1 true .088 11   .73 -32 false(unreach-call) 6.6 330 51 1 false(unreach-call) 6.2 330 49 1 false(unreach-call) 6.9 350 58 1 witness invalid (false(unreach-call)) 5.6 270 45 0
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c error (5) .085 22 .95 0 false(unreach-call) .069 17   .66 1 false(unreach-call) .13 18 1.2  1 false(unreach-call) .098 7.9 1.0  1 error 3.0 280 26 0 error 3.2 280 27 0 false(unreach-call) 3.3 300 30 1 false(unreach-call) .59 50 7.2 1 false(unreach-call) 37    2900 470    0 false(unreach-call) .11  23 .73 1 false(unreach-call) .077 23 .85 1 false(unreach-call) .079 23 .75 1 false(unreach-call) 1.5 74 18 1 false(unreach-call) .15 10   1.7 1 timeout 900     350   13000    0 false(unreach-call) 6.5 330 54 1 false(unreach-call) 6.0 340 52 1 false(unreach-call) 5.4 310 46 1 unknown 5.2 150 48 0
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c error (5) .12  22 .63 0 exception (gremlins) 3.0   32   34    0 false(unreach-call) .53 30 5.0  1 unknown .24  7.9 3.3  0 error 2.8 270 22 0 error 3.2 270 26 0 false(unreach-call) 6.4 450 56 1 out of memory (false(no-overflow)) 610    15000 7100   0 out of memory 170    15000 2100    0 false(unreach-call) .12  23 1.2  1 false(unreach-call) .15  23 1.4  1 false(unreach-call) .15  25 1.8  1 false(unreach-call) 1.6 72 22 1 false(unreach-call) .20 10   1.9 1 timeout 900     430   13000    0 false(unreach-call) 11   500 120 1 false(unreach-call) 11   490 85 1 false(unreach-call) 38   1800 330 1 unknown 770   190 4600 0
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c error (5) .12  22 .65 0 exception (gremlins) 3.1   31   36    0 error (42) 850    260 4100    0 unknown .24  7.8 3.2  0 error 2.9 270 26 0 error 3.0 280 24 0 false(unreach-call) 14   620 130 1 out of memory (false(no-overflow)) 610    15000 6600   0 out of memory 170    15000 2200    0 false(unreach-call) 2.3   73 6.4  0 false(unreach-call) .79  95 8.9  0 false(unreach-call) 1.0   120 12    0 false(unreach-call) 2.0 82 25 1 false(unreach-call) .28 11   3.2 0 timeout 900     440   12000    0 false(unreach-call) 14   710 120 0 false(unreach-call) 21   1300 170 0 false(unreach-call) 42   1700 350 0 unknown 770   190 3600 0
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c error (5) .12  22 .62 0 false(unreach-call) .11  21   .58 1 false(unreach-call) .15 18 1.1  1 false(unreach-call) .098 7.7 1.0  1 error 2.8 280 26 0 error 2.9 280 21 0 false(unreach-call) 3.0 300 27 1 false(unreach-call) .64 82 6.7 1 out of memory 200    15000 2800    0 false(unreach-call) .074 23 .83 1 false(unreach-call) .082 23 .86 1 false(unreach-call) .087 23 .73 1 false(unreach-call) 1.5 70 19 1 false(unreach-call) .15 10   1.9 1 timeout 900     380   13000    0 false(unreach-call) 5.5 320 48 1 false(unreach-call) 5.6 320 47 1 false(unreach-call) 5.9 340 40 1 witness invalid (false(unreach-call)) 540   330 2800 0
recursive/Ackermann01_true-unreach-call_true-no-overflow.c error (5) .11  22 .72 0 exception (gremlins) 25     48   270    0 error (42) 850    370 3700    0 unknown .42  7.7 5.2  0 error 2.9 280 26 0 error 3.2 280 25 0 true 4.2 310 39 2 out of memory (false(no-overflow)) 720    15000 8300   0 out of memory 250    15000 3200    0 out of memory 260     15000 3000    0 timeout 900     3900 8300    0 timeout 900     2600 7000    0 true 880   500 8200 2 timeout (timeout) 900    15000   13000   0 unknown 13     52   170    0 true 9.2 490 70 2 timeout 900   1300 10000 0 timeout 900   13000 4000 0 unknown 740   370 3600 0
recursive/Ackermann03_true-unreach-call_true-no-overflow.c error (5) .12  22 .79 0 exception (gremlins) 4.4   34   47    0 error (42) 850    340 2000    0 unknown .34  7.8 4.0  0 error 2.8 270 23 0 error 3.2 280 23 0 true 43   1400 410 2 out of memory (false(no-overflow)) 720    15000 9000   0 out of memory 250    15000 3300    0 out of memory 290     15000 3500    0 timeout 900     3600 8800    0 timeout 900     2400 7500    0 true 1.4 72 18 2 timeout (timeout) 900    15000   14000   0 unknown 13     54   170    0 true 27   860 230 2 timeout 900   1900 11000 0 timeout 900   13000 4600 0 unknown 740   450 3900 0
recursive/Ackermann04_true-unreach-call_true-no-overflow.c error (5) .12  22 .65 0 exception (gremlins) 4.4   36   58    0 error (42) 850    370 4200    0 unknown .33  7.7 3.5  0 error 2.9 280 27 0 error 3.2 280 28 0 true 13   650 130 2 out of memory (false(no-overflow)) 720    15000 9300   0 out of memory 250    15000 2800    0 out of memory 380     15000 3900    0 timeout 900     3900 8400    0 timeout 900     1900 2500    0 true 880   390 8500 2 timeout (timeout) 900    15000   12000   0 unknown 13     52   260    0 true 20   720 170 2 timeout 900   2000 11000 0 timeout 900   13000 5200 0 unknown 740   400 3800 0
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c error (5) .10  22 .85 0 exception (gremlins) 8.5   35   110    0 error (42) 850    8800 5600    0 unknown .24  8.0 2.5  0 error 2.9 280 26 0 error 3.1 270 28 0 true 4.2 310 35 2 unknown 640    15000 9100   0 out of memory 210    15000 2600    0 out of memory 470     15000 3400    0 out of memory 870     15000 6100    0 out of memory 400     15000 3200    0 true 880   380 11000 2 timeout (timeout) 900    150   13000   0 timeout 900     9300   11000    0 true 7.9 430 66 2 true 8.0 460 59 2 true 11   510 72 2 timeout 900   5000 7900 0
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c error (5) .12  22 .70 0 exception (gremlins) 1.9   34   16    0 error (134) 660    15000 6800    0 unknown .43  7.8 4.9  0 error 2.9 270 24 0 error 3.2 280 25 0 timeout 900   10000 11000 0 timeout (false(no-overflow)) 900    15000 12000   0 out of memory 220    15000 3000    0 out of memory 240     15000 2200    0 out of memory 380     15000 3600    0 out of memory 400     15000 4100    0 true 880   400 11000 2 timeout (timeout) 900    230   10000   0 unknown .053 9.8 .58 0 true 230   3200 2500 2 timeout 900   2500 7700 0 timeout 900   1400 13000 0 timeout (error (124)) 900   8400 5900 0
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c error (5) .10  22 .70 0 false(unreach-call) .088 20   .74 -16 error (42) 850    8100 4600    0 unknown .44  8.0 5.0  0 error 2.9 270 25 0 error 3.2 270 27 0 true 4.8 310 39 1 unknown 6.0  320 55   0 true 38    2800 440    1 out of memory 800     15000 9500    0 out of memory 490     15000 6800    0 out of memory 410     15000 5100    0 true 880   150 10000 1 true .19 12   2.4 1 timeout 900     340   10000    0 timeout 900   1300 11000 0 timeout 900   850 12000 0 timeout 900   1100 13000 0 unknown 5.3 150 52 0
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c error (5) .12  22 .65 0 exception (gremlins) 5.3   34   67    0 error (42) 850    250 3300    0 unknown .28  7.8 3.0  0 error 3.1 280 26 0 error 3.1 270 25 0 true 7.4 480 68 2 timeout (false(no-overflow)) 900    10000 12000   0 out of memory 160    15000 2100    0 timeout 900     3200 11000    0 timeout 900     2300 8800    0 timeout 900     2200 8400    0 true 890   10000 8900 2 timeout (timeout) 900    15000   12000   0 timeout 900     440   14000    0 true 18   680 150 2 timeout 900   1100 9800 0 true 56   2100 510 2 unknown 770   190 3600 0
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c error (5) .099 22 .72 0 exception (gremlins) 22     34   260    0 true .48 17 5.2  2 unknown .15  7.8 1.4  0 error 2.8 280 25 0 error 2.9 280 25 0 true 4.8 440 38 2 unknown 6.1  440 51   0 true .15 23 2.0  2 timeout 900     11000 11000    0 true .33  26 3.7  2 true .48  33 7.5  2 true 1.7 78 23 2 true .16 9.2 1.4 2 true .074 9.9 .80 2 true 24   1500 210 2 timeout 900   5100 14000 0 timeout 910   13000 5500 0 true 7.6 290 63 2
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c error (5) .085 22 .92 0 exception (gremlins) 3.0   32   32    0 error (42) 850    260 3700    0 unknown .25  7.6 3.2  0 error 2.8 270 22 0 error 3.0 270 25 0 timeout 900   3700 10000 0 out of memory (false(no-overflow)) 600    15000 7600   0 out of memory 160    15000 2200    0 timeout 900     5800 12000    0 timeout 900     3200 11000    0 timeout 900     3900 10000    0 out of memory 440   15000 4500 0 timeout (timeout) 900    15000   13000   0 timeout 900     430   11000    0 true 24   1000 210 2 timeout 900   5300 12000 0 true 130   3900 1600 2 unknown 770   190 3000 0
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c error (5) .12  22 .73 0 false(unreach-call) 4.5   34   52    -16 error (42) 850    1300 3300    0 unknown .29  7.8 3.3  0 error 2.8 280 27 0 error 3.2 280 27 0 true 3.6 310 30 2 out of memory (false(no-overflow)) 740    15000 10000   0 out of memory 200    15000 2400    0 timeout 900     7000 10000    0 timeout 900     5000 8500    0 timeout 900     4700 8400    0 true 880   400 9000 2 timeout (timeout) 900    320   11000   0 timeout 900     360   12000    0 true 7.4 370 51 2 true 7.0 360 61 2 true 8.7 370 76 2 unknown 660   330 4100 0
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c error (5) .10  22 .78 0 exception (gremlins) 96     45   940    0 error (42) 850    410 3300    0 unknown .60  7.9 8.6  0 error 2.9 280 26 0 error 3.2 290 28 0 timeout 900   750 11000 0 out of memory (false(no-overflow)) 710    15000 9900   0 out of memory 250    15000 3300    0 timeout 900     9800 8100    0 timeout 900     2500 7000    0 timeout 900     2900 6400    0 true 880   110 11000 1 timeout (timeout) 900    140   11000   0 timeout 900     2800   11000    0 timeout 900   1200 10000 0 timeout 900   1500 12000 0 timeout 900   6700 10000 0 unknown 850   2500 6400 0
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c error (5) .12  22 .72 0 exception (gremlins) 78     610   900    0 error (42) 850    300 2500    0 unknown .66  7.8 7.9  0 error 3.4 280 26 0 error 3.6 280 29 0 timeout 900   1300 11000 0 out of memory (false(no-overflow)) 740    15000 8000   0 out of memory 270    15000 3400    0 out of memory 310     15000 3400    0 out of memory 330     15000 3200    0 out of memory 520     15000 4300    0 true 880   260 9400 1 timeout (timeout) 900    93   12000   0 timeout 900     120   13000    0 timeout 900   1200 14000 0 timeout 900   1100 12000 0 timeout 900   6000 11000 0 unknown 780   2500 6500 0
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c error (5) .089 22 .76 0 false(unreach-call) 5.2   34   61    -16 error (42) 850    3300 6700    0 unknown 1.1   7.6 15    0 error 2.9 270 24 0 error 3.2 280 24 0 true 4.0 300 35 2 unknown 570    15000 6500   0 out of memory 170    15000 2200    0 timeout 900     160 11000    0 timeout 900     160 12000    0 timeout 900     160 14000    0 true 880   370 12000 2 timeout (timeout) 900    100   11000   0 timeout 900     87   11000    0 true 9.4 500 75 2 true 7.7 410 67 2 true 9.1 480 72 2 timeout 900   6700 7400 0
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c error (5) .11  22 .64 0 unknown .077 8.2 .40 0 error (42) 850    180 8300    0 unknown 2.3   12   29    0 error 3.1 280 24 0 error 3.4 280 30 0 timeout 900   1100 11000 0 timeout (false(no-overflow)) 900    15000 11000   0 out of memory 96    15000 1100    0 timeout 900     850 12000    0 timeout 900     850 12000    0 timeout 900     850 11000    0 true 880   83 11000 1 timeout (timeout) 900    50   9800   0 timeout 900     72   12000    0 timeout 900   1300 11000 0 timeout 900   890 11000 0 timeout 900   2500 9400 0 timeout 900   5400 7300 0
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c error (5) .077 22 .89 0 exception (gremlins) 67     69   770    0 error (42) 850    800 3500    0 aborted .14  7.6 1.5  0 error 2.9 280 24 0 error 3.2 280 25 0 exception 4.9 320 40 0 out of memory (false(no-overflow)) 610    15000 8400   0 out of memory 180    15000 2100    0 out of memory 380     15000 3200    0 out of memory 360     15000 3000    0 out of memory 470     15000 5200    0 true 890   6800 8000 1 timeout (timeout) 900    15000   13000   0 timeout 900     8000   12000    0 timeout 900   8300 11000 0 timeout 900   1300 12000 0 timeout 910   13000 6200 0 unknown 650   180 3900 0
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c error (5) .098 22 .66 0 false(unreach-call) .97  23   13    -16 true 1.0  22 11    2 aborted .22  7.7 2.4  0 error 2.9 280 26 0 error 2.9 270 23 0 true 6.3 450 57 2 unknown 7.6  460 68   0 true 4.0  310 46    2 out of memory 440     15000 5400    0 true 1.2   79 15    2 true 1.5   110 21    2 true 1.7 66 22 2 true .20 10   2.3 2 timeout 900     350   11000    0 true 6.1 330 50 2 true 5.9 330 42 2 true 10   480 77 2 unknown 4.9 150 42 0
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c error (5) .10  22 .81 0 exception (gremlins) 3.3   31   44    0 true 1.1  21 11    1 aborted .20  7.8 2.2  0 error 2.8 270 26 0 error 3.2 280 26 0 true 9.8 480 84 1 unknown 10    490 110   0 true 16    310 32    1 out of memory 460     15000 5100    0 true 1.5   81 21    1 true 1.8   110 24    1 true 1.9 70 27 1 true .21 10   2.1 1 timeout 900     350   13000    0 timeout 900   2500 9900 0 true 9.2 460 81 1 timeout 900   2600 11000 0 unknown 4.7 150 38 0
recursive-simple/afterrec_2calls_false-unreach-call_true-termination.c error (5) .11  22 .61 0 unknown .047 8.2 .42 0 false(unreach-call) .14 17 .95 1 false(unreach-call) .057 7.8 .47 1 error 2.8 280 27 0 false(unreach-call) 3.5 280 27 1 false(unreach-call) 2.7 260 23 1 false(unreach-call) 1.1  48 13   1 false(unreach-call) .13 23 1.5  1 false(unreach-call) .074 23 .74 1 false(unreach-call) .074 23 .88 1 false(unreach-call) .094 23 .76 1 false(unreach-call) 1.5 77 21 1 false(unreach-call) .15 9.6 1.4 1 false(unreach-call) .081 9.8 .54 1 false(unreach-call) 6.9 350 53 1 false(unreach-call) 6.0 320 47 1 false(unreach-call) 5.8 330 45 1 witness invalid (false(unreach-call)) 5.5 220 52 0
recursive-simple/afterrec_false-unreach-call_true-termination.c error (5) .081 22 .82 0 false(unreach-call) .059 17   .75 1 false(unreach-call) .13 17 .90 1 false(unreach-call) .063 13   .64 1 error 2.9 280 26 0 false(unreach-call) 3.1 270 23 1 false(unreach-call) 2.4 250 21 1 false(unreach-call) 1.0  48 13   1 false(unreach-call) .14 23 1.5  1 false(unreach-call) .11  23 .57 1 false(unreach-call) .074 23 .80 1 false(unreach-call) .074 23 .95 1 false(unreach-call) 1.5 73 17 1 false(unreach-call) .13 9.2 1.5 1 false(unreach-call) .079 9.7 .50 1 false(unreach-call) 6.2 340 52 1 false(unreach-call) 6.4 330 47 1 false(unreach-call) 5.6 320 42 1 witness invalid (false(unreach-call)) 5.4 220 46 0
recursive-simple/fibo_10_false-unreach-call.c error (5) .11  22 .86 0 exception (gremlins) 27     34   290    0 false(unreach-call) .48 19 4.1  0 unknown .12  7.7 1.2  0 error 2.9 270 27 0 error 3.1 270 26 0 false(unreach-call) 5.7 400 51 1 false(unreach-call) 1.2  49 14   0 false(unreach-call) .15 23 1.8  1 false(unreach-call) .54  23 1.5  1 false(unreach-call) .64  30 7.4  1 false(unreach-call) 1.1   39 12    1 false(unreach-call) 3.1 91 46 1 false(unreach-call) .14 9.3 1.5 0 false(unreach-call) .097 9.5 .82 1 false(unreach-call) 22   1900 190 0 timeout 900   1800 11000 0 timeout 900   13000 6500 0 witness invalid (false(unreach-call)) 5.7 220 45 0
recursive-simple/fibo_15_false-unreach-call.c error (5) .11  22 .66 0 exception (gremlins) 22     31   230    0 false(unreach-call) 1.8  61 22    0 unknown .11  7.9 1.3  0 error 2.7 270 24 0 error 3.1 280 26 0 false(unreach-call) 34   1700 360 0 false(unreach-call) 2.5  61 36   0 false(unreach-call) .43 24 5.4  1 false(unreach-call) .96  33 15    1 false(unreach-call) 190     150 2200    1 false(unreach-call) 390     270 4900    1 false(unreach-call) 110   570 960 1 false(unreach-call) .17 17   1.9 0 false(unreach-call) .66  77   8.7  1 false(unreach-call) 330   4900 4600 0 timeout 900   2000 11000 0 timeout 910   13000 6400 0 witness invalid (false(unreach-call)) 12   230 140 0
recursive-simple/fibo_20_false-unreach-call.c error (5) .084 22 .78 0 exception (gremlins) 22     35   260    0 false(unreach-call) 180    660 1100    0 unknown .14  7.8 1.2  0 error 2.8 270 28 0 error 3.1 290 24 0 timeout 960   5400 8800 0 false(unreach-call) 18    520 270   0 false(unreach-call) 3.9  82 47    0 false(unreach-call) 63     260 120    0 timeout 900     380 11000    0 timeout 900     310 9200    0 error (1) 890   2800 7800 0 false(unreach-call) .60 110   7.9 0 false(unreach-call) 8.6   790   94    0 timeout 900   5500 11000 0 timeout 900   2100 11000 0 timeout 910   13000 6300 0 unknown 720   200 5100 0
recursive-simple/fibo_25_false-unreach-call.c error (5) .11  22 .71 0 exception (gremlins) 27     35   310    0 error (42) 850    390 4300    0 unknown .15  7.8 1.3  0 error 3.1 280 26 0 error 3.0 270 22 0 timeout 910   7200 5200 0 false(unreach-call) 240    5400 3100   0 false(unreach-call) 45    820 670    0 false(unreach-call) 210     3000 2900    0 timeout 900     380 10000    0 timeout 900     310 9700    0 error (1) 890   2900 10000 0 false(unreach-call) 5.3  1200   64   0 false(unreach-call) 120     15000   1400    0 timeout 900   5400 11000 0 timeout 900   1800 12000 0 timeout 910   13000 6000 0 unknown 4.6 150 40 0
recursive-simple/fibo_2calls_10_false-unreach-call.c error (5) .088 33 .86 0 exception (gremlins) 21     41   240    0 false(unreach-call) .32 19 2.9  0 unknown .23  7.8 2.4  0 error 2.9 280 26 0 error 3.1 280 27 0 false(unreach-call) 6.1 400 49 1 false(unreach-call) 1.3  50 16   0 false(unreach-call) .15 23 2.0  1 false(unreach-call) .13  23 1.4  1 false(unreach-call) .45  25 5.2  1 false(unreach-call) .73  29 8.3  1 false(unreach-call) 3.1 92 38 1 false(unreach-call) .16 9.3 1.8 0 false(unreach-call) .14  11   1.0  1 false(unreach-call) 46   3800 410 0 timeout 900   1700 9600 0 timeout 900   13000 6900 0 witness invalid (false(unreach-call)) 5.7 220 46 0
recursive-simple/fibo_2calls_15_false-unreach-call.c error (5) .086 22 .75 0 exception (gremlins) 42     40   490    0 false(unreach-call) 1.6  67 22    0 unknown .22  7.7 2.3  0 error 3.0 280 29 0 error 3.2 280 28 0 false(unreach-call) 28   1600 270 0 false(unreach-call) 2.7  69 36   0 false(unreach-call) .45 24 5.2  1 false(unreach-call) .65  25 7.5  1 false(unreach-call) 97     100 1100    1 false(unreach-call) 200     150 2400    1 false(unreach-call) 110   570 1000 1 false(unreach-call) .17 11   1.5 0 false(unreach-call) .75  78   8.9  1 false(unreach-call) 780   5400 11000 0 timeout 900   1100 12000 0 timeout 910   13000 6200 0 witness invalid (false(unreach-call)) 12   230 130 0
recursive-simple/fibo_2calls_20_false-unreach-call.c error (5) .086 22 .84 0 exception (gremlins) 66     43   770    0 false(unreach-call) 210    710 1100    0 unknown .21  7.8 2.5  0 error 2.9 270 29 0 error 3.2 270 23 0 timeout 960   5400 8500 0 false(unreach-call) 20    610 280   0 false(unreach-call) 4.1  82 51    0 false(unreach-call) 7.8   170 99    0 timeout 900     530 11000    0 timeout 900     240 8600    0 timeout 890   2700 8100 0 false(unreach-call) .30 45   3.4 0 false(unreach-call) 11     1500   120    0 timeout 900   5500 13000 0 timeout 900   1500 12000 0 timeout 900   13000 5500 0 unknown 720   200 6100 0
recursive-simple/fibo_2calls_25_false-unreach-call.c error (5) .089 22 .79 0 exception (gremlins) 63     46   890    0 error (42) 850    390 3900    0 unknown .25  7.9 2.3  0 error 3.0 270 26 0 error 3.1 280 27 0 timeout 910   7700 1200 0 false(unreach-call) 230    6400 2700   0 false(unreach-call) 48    820 680    0 false(unreach-call) 130     2000 1600    0 timeout 900     560 10000    0 timeout 900     240 11000    0 timeout 900   2900 11000 0 false(unreach-call) 1.8  420   25   0 false(unreach-call) 140     14000   1800    0 timeout 900   5400 11000 0 timeout 900   1600 10000 0 timeout 910   13000 6700 0 unknown 840   200 6600 0
recursive-simple/fibo_2calls_2_false-unreach-call_true-termination.c error (5) .10  22 .64 0 false(unreach-call) .072 20   .64 1 false(unreach-call) .12 17 .97 1 false(unreach-call) .13  7.8 1.4  1 false(unreach-call) 3.2 280 29 1 false(unreach-call) 3.5 280 27 1 false(unreach-call) 2.5 250 24 1 false(unreach-call) .35 48 4.1 1 false(unreach-call) .16 23 1.4  1 false(unreach-call) .082 23 .74 1 false(unreach-call) .078 23 .71 1 false(unreach-call) .075 23 .80 1 false(unreach-call) 1.5 69 20 1 false(unreach-call) .13 9.1 2.0 1 false(unreach-call) .090 9.9 .32 1 false(unreach-call) 7.5 350 56 1 false(unreach-call) 6.9 330 51 1 false(unreach-call) 7.6 380 56 1 witness invalid (false(unreach-call)) 5.7 230 49 0
recursive-simple/fibo_2calls_4_false-unreach-call_true-termination.c error (5) .11  22 .72 0 true 7.9   30   95    -32 false(unreach-call) .15 17 .78 1 false(unreach-call) .31  7.8 4.0  1 error 3.1 280 25 0 error 3.2 280 26 0 false(unreach-call) 3.4 300 31 1 false(unreach-call) 1.1  50 13   1 false(unreach-call) .16 23 1.5  1 false(unreach-call) .10  23 .83 1 false(unreach-call) .077 23 .83 1 false(unreach-call) .078 23 .98 1 false(unreach-call) 1.6 72 21 1 false(unreach-call) .16 9.2 1.4 1 false(unreach-call) .078 9.5 .56 1 false(unreach-call) 8.9 480 77 1 timeout 900   1100 12000 0 false(unreach-call) 16   530 140 1 witness invalid (false(unreach-call)) 5.6 230 51 0
recursive-simple/fibo_2calls_5_false-unreach-call_true-termination.c error (5) .10  22 .73 0 true 3.9   24   50    -32 false(unreach-call) .15 17 1.1  1 false(unreach-call) .48  9.3 5.2  1 error 3.2 270 29 0 error 3.1 280 26 0 false(unreach-call) 3.6 300 29 1 false(unreach-call) 1.1  52 12   1 false(unreach-call) .13 23 1.4  1 false(unreach-call) .076 23 .95 1 false(unreach-call) .085 23 .90 1 false(unreach-call) .083 23 1.1  1 false(unreach-call) 1.6 74 22 1 false(unreach-call) .14 9.4 1.7 0 false(unreach-call) .056 9.8 .55 1 false(unreach-call) 13   500 100 1 timeout 900   1100 11000 0 false(unreach-call) 18   560 160 1 witness invalid (false(unreach-call)) 5.5 230 54 0
recursive-simple/fibo_2calls_6_false-unreach-call_true-termination.c error (5) .10  22 .79 0 true 5.3   30   67    -32 false(unreach-call) .14 17 .88 1 false(unreach-call) 1.0   20   8.5  1 error 2.9 270 26 0 error 3.0 280 26 0 false(unreach-call) 3.9 300 36 1 false(unreach-call) 1.2  50 15   1 false(unreach-call) .13 23 1.6  1 false(unreach-call) .095 23 .80 1 false(unreach-call) .094 23 1.1  1 false(unreach-call) .13  23 1.3  1 false(unreach-call) 1.7 81 20 1 false(unreach-call) .16 9.4 1.7 0 false(unreach-call) .085 9.7 .57 1 false(unreach-call) 16   540 120 1 timeout 900   1700 11000 0 false(unreach-call) 32   860 300 1 witness invalid (false(unreach-call)) 5.5 230 47 0
recursive-simple/fibo_2calls_8_false-unreach-call.c error (5) .072 22 1.3  0 exception (gremlins) 22     36   280    0 false(unreach-call) .28 18 2.5  0 unknown .22  7.8 2.5  0 error 2.8 280 24 0 error 3.1 270 24 0 false(unreach-call) 4.5 310 39 1 false(unreach-call) 1.2  50 15   1 false(unreach-call) .14 23 1.5  1 false(unreach-call) .12  23 .76 1 false(unreach-call) .15  23 1.5  1 false(unreach-call) .15  23 1.8  1 false(unreach-call) 2.0 89 27 1 false(unreach-call) .15 9.2 1.4 0 false(unreach-call) .092 9.6 .63 1 false(unreach-call) 26   930 230 0 timeout 900   1100 14000 0 false(unreach-call) 140   5400 1500 0 witness invalid (false(unreach-call)) 5.6 220 56 0
recursive-simple/fibo_5_false-unreach-call_true-termination.c error (5) .099 22 .74 0 exception (gremlins) 5.6   32   58    0 false(unreach-call) .25 17 3.2  1 unknown .11  7.8 1.1  0 error 2.9 280 24 0 error 3.1 270 25 0 false(unreach-call) 3.5 300 29 1 false(unreach-call) 1.1  49 11   1 false(unreach-call) .13 23 1.9  1 false(unreach-call) .078 23 .82 1 false(unreach-call) .096 23 .91 1 false(unreach-call) .10  23 1.2  1 false(unreach-call) 1.6 69 19 1 false(unreach-call) .16 9.5 1.4 1 false(unreach-call) .056 9.8 .54 1 false(unreach-call) 9.8 490 81 1 timeout 900   1900 10000 0 false(unreach-call) 13   510 100 1 witness invalid (false(unreach-call)) 5.5 230 47 0
recursive-simple/fibo_7_false-unreach-call.c error (5) .11  22 .65 0 exception (gremlins) 13     31   160    0 false(unreach-call) .29 17 2.4  1 unknown .11  7.9 1.4  0 error 2.8 280 23 0 error 3.0 260 23 0 false(unreach-call) 3.9 310 33 1 false(unreach-call) 1.1  49 14   1 false(unreach-call) .13 23 2.6  1 false(unreach-call) .091 23 .97 1 false(unreach-call) .16  23 1.4  1 false(unreach-call) .16  25 1.9  1 false(unreach-call) 1.7 72 25 1 false(unreach-call) .14 9.3 1.4 0 false(unreach-call) .059 9.8 .57 1 false(unreach-call) 13   520 110 1 timeout 900   1900 10000 0 false(unreach-call) 25   920 200 1 witness invalid (false(unreach-call)) 5.5 230 54 0
recursive-simple/id2_b3_o2_false-unreach-call.c error (5) .10  22 .71 0 false(unreach-call) .52  21   3.8  1 false(unreach-call) .13 18 .91 1 false(unreach-call) .20  7.9 1.8  1 error 2.8 270 25 0 error 3.2 280 24 0 false(unreach-call) 3.6 300 31 1 false(unreach-call) 1.1  50 13   1 false(unreach-call) 35    1300 440    1 false(unreach-call) .081 23 .87 1 false(unreach-call) .11  23 .75 1 false(unreach-call) .085 23 .82 1 false(unreach-call) 1.5 77 20 1 false(unreach-call) .16 9.9 1.9 0 timeout 900     370   12000    0 false(unreach-call) 6.5 330 50 1 false(unreach-call) 6.8 330 53 1 false(unreach-call) 7.6 350 61 1 witness invalid (false(unreach-call)) 6.0 270 56 0
recursive-simple/id2_i5_o5_false-unreach-call_true-termination.c error (5) .086 22 .70 0 false(unreach-call) .087 19   .61 1 false(unreach-call) .12 17 .98 1 false(unreach-call) .14  7.9 1.7  1 error 2.9 280 27 0 error 3.1 270 29 0 false(unreach-call) 3.4 300 27 1 false(unreach-call) 1.1  49 14   1 false(unreach-call) .49 23 .99 1 false(unreach-call) .11  23 .65 1 false(unreach-call) .11  23 .76 1 false(unreach-call) .078 23 .91 1 false(unreach-call) 1.6 77 18 1 false(unreach-call) .13 9.4 1.5 1 false(unreach-call) .053 9.9 .57 1 false(unreach-call) 7.9 410 65 1 false(unreach-call) 9.5 500 66 1 false(unreach-call) 11   480 88 1 witness invalid (false(unreach-call)) 5.5 230 49 0
recursive-simple/id_b3_o2_false-unreach-call.c error (5) .10  22 .77 0 false(unreach-call) .32  22   3.6  1 false(unreach-call) .12 17 .98 1 false(unreach-call) .19  43   2.6  1 error 2.8 270 22 0 error 2.9 270 23 0 false(unreach-call) 3.3 300 27 1 false(unreach-call) 1.1  50 14   1 false(unreach-call) 11    370 120    1 false(unreach-call) .10  23 .86 1 false(unreach-call) .082 23 .87 1 false(unreach-call) .091 23 .91 1 false(unreach-call) 1.5 78 20 1 false(unreach-call) .17 9.4 1.6 1 timeout 900     370   12000    0 false(unreach-call) 6.4 330 59 1 false(unreach-call) 7.2 330 61 1 false(unreach-call) 7.6 360 62 1 unknown 4.7 160 42 0
recursive-simple/id_i10_o10_false-unreach-call_true-termination.c error (5) .12  22 .71 0 false(unreach-call) .10  18   .61 0 false(unreach-call) .38 17 4.1  1 unknown .080 7.6 .66 0 error 3.0 270 25 0 error 3.1 280 27 0 false(unreach-call) 3.4 300 29 1 false(unreach-call) 1.1  49 13   1 false(unreach-call) .16 23 1.5  1 false(unreach-call) .087 23 .97 1 false(unreach-call) .11  23 1.2  1 false(unreach-call) .11  23 1.4  1 false(unreach-call) 1.6 73 20 1 false(unreach-call) .16 9.3 1.2 1 false(unreach-call) .072 9.7 .52 1 false(unreach-call) 12   490 97 1 false(unreach-call) 20   600 190 1 false(unreach-call) 26   740 270 1 witness invalid (false(unreach-call)) 5.5 220 50 0
recursive-simple/id_i15_o15_false-unreach-call_true-termination.c error (5) .10  22 .77 0 false(unreach-call) .071 21   .74 0 false(unreach-call) .50 17 6.3  1 unknown .091 7.5 .58 0 error 2.7 270 24 0 error 3.1 270 24 0 false(unreach-call) 3.6 310 30 1 false(unreach-call) 1.0  49 13   1 false(unreach-call) .14 23 1.6  1 false(unreach-call) .093 23 .99 1 false(unreach-call) .13  23 1.2  1 false(unreach-call) .54  25 1.2  1 false(unreach-call) 1.6 69 22 1 false(unreach-call) .13 9.2 1.7 1 false(unreach-call) .069 9.6 .51 1 false(unreach-call) 18   610 160 1 false(unreach-call) 36   830 350 1 false(unreach-call) 70   1200 940 1 witness invalid (false(unreach-call)) 5.7 230 51 0
recursive-simple/id_i20_o20_false-unreach-call_true-termination.c error (5) .10  22 .62 0 false(unreach-call) .074 20   .79 0 false(unreach-call) .74 30 7.6  1 unknown .073 7.5 .68 0 error 2.7 270 22 0 error 3.0 280 24 0 false(unreach-call) 3.5 300 33 1 false(unreach-call) 1.0  49 13   1 false(unreach-call) .14 23 1.5  1 false(unreach-call) .12  23 1.0  1 false(unreach-call) .16  24 1.4  1 false(unreach-call) .17  30 2.2  1 false(unreach-call) 1.7 77 23 1 false(unreach-call) .13 9.2 1.4 1 false(unreach-call) .098 9.8 .35 1 false(unreach-call) 23   790 230 1 false(unreach-call) 83   1600 1200 1 false(unreach-call) 190   1100 2600 1 witness invalid (false(unreach-call)) 5.4 230 51 0
recursive-simple/id_i25_o25_false-unreach-call_true-termination.c error (5) .12  22 .62 0 false(unreach-call) .11  18   .59 0 false(unreach-call) .87 17 7.0  1 unknown .082 7.8 .65 0 error 2.7 280 25 0 error 3.0 280 26 0 false(unreach-call) 3.6 310 30 1 unknown 4.9  310 43   0 false(unreach-call) .13 23 1.5  1 false(unreach-call) .12  23 1.3  1 false(unreach-call) .19  26 1.9  1 false(unreach-call) .20  35 2.5  1 false(unreach-call) 1.9 75 21 1 false(unreach-call) .15 9.2 1.6 1 false(unreach-call) .053 9.9 .49 1 false(unreach-call) 27   910 210 1 false(unreach-call) 140   1300 1800 1 false(unreach-call) 430   1100 5600 1 unknown 4.7 150 39 0
recursive-simple/id_i5_o5_false-unreach-call_true-termination.c error (5) .12  22 .70 0 false(unreach-call) .075 17   .74 1 false(unreach-call) .27 17 2.6  1 unknown .075 7.9 .70 0 error 2.8 270 26 0 error 3.0 270 23 0 false(unreach-call) 3.3 300 29 1 false(unreach-call) 1.0  52 13   1 false(unreach-call) .13 23 1.3  1 false(unreach-call) .078 23 .81 1 false(unreach-call) .12  23 .87 1 false(unreach-call) .089 23 .89 1 false(unreach-call) 1.5 78 20 1 false(unreach-call) .15 9.3 1.4 1 false(unreach-call) .052 9.6 .54 1 false(unreach-call) 7.8 410 66 1 false(unreach-call) 8.8 470 65 1 false(unreach-call) 11   490 92 1 witness invalid (false(unreach-call)) 5.3 230 50 0
recursive-simple/id_o1000_false-unreach-call.c error (5) .098 22 .74 0 false(unreach-call) 1.1   22   12    0 false(unreach-call) 39    390 400    0 unknown .12  7.8 1.3  0 error 2.8 280 23 0 error 3.0 270 21 0 false(unreach-call) 380   4300 4600 0 unknown 400    4300 4200   0 true 3.8  290 45    -32 timeout 900     6200 13000    0 timeout 900     13000 13000    0 out of memory 740     15000 8500    0 timeout 880   220 11000 0 false(unreach-call) .17 9.5 1.6 0 false(unreach-call) .062 9.8 .43 0 timeout 900   2900 12000 0 timeout 900   3900 13000 0 timeout 900   1200 12000 0 unknown 4.6 160 41 0
recursive-simple/id_o100_false-unreach-call.c error (5) .091 22 .72 0 false(unreach-call) 1.1   23   14    0 false(unreach-call) 1.8  41 21    0 unknown .16  7.8 1.3  0 error 2.8 280 24 0 error 3.1 280 27 0 false(unreach-call) 6.7 480 53 0 unknown 8.7  490 69   0 false(unreach-call) 3.7  290 49    0 false(unreach-call) 8.8   250 130    0 false(unreach-call) 12     530 140    0 false(unreach-call) 16     810 210    0 false(unreach-call) 16   110 200 0 false(unreach-call) .14 9.4 1.7 1 false(unreach-call) .059 9.5 .55 1 false(unreach-call) 250   2000 3900 0 false(unreach-call) 290   1800 3900 0 timeout 900   1300 14000 0 unknown 4.7 150 40 0
recursive-simple/id_o10_false-unreach-call.c error (5) .083 22 .88 0 false(unreach-call) 1.1   22   12    0 false(unreach-call) .44 20 3.9  1 unknown .11  7.7 1.3  0 error 2.7 270 23 0 error 2.9 270 22 0 false(unreach-call) 3.4 300 28 1 false(unreach-call) 1.1  49 13   1 false(unreach-call) 3.7  290 52    1 false(unreach-call) .11  23 1.4  1 false(unreach-call) .15  25 1.8  1 false(unreach-call) .17  29 2.5  1 false(unreach-call) 1.6 77 17 0 false(unreach-call) .14 9.2 1.7 1 false(unreach-call) .054 9.8 .73 1 false(unreach-call) 11   480 80 1 false(unreach-call) 12   480 100 1 false(unreach-call) 23   820 250 1 unknown 4.9 160 42 0
recursive-simple/id_o200_false-unreach-call.c error (5) .11  22 .70 0 false(unreach-call) 1.1   24   12    0 false(unreach-call) 1.6  41 18    0 unknown .14  7.9 1.4  0 error 2.9 280 24 0 error 3.0 270 25 0 false(unreach-call) 11   680 90 0 unknown 13    660 110   0 false(unreach-call) 3.8  290 45    0 false(unreach-call) 67     1000 940    0 false(unreach-call) 86     2400 1200    0 false(unreach-call) 110     3700 1600    0 false(unreach-call) 160   240 2000 0 false(unreach-call) .16 9.4 1.4 1 false(unreach-call) .072 9.9 .54 1 timeout 900   2400 15000 0 timeout 900   3600 13000 0 timeout 900   1200 14000 0 unknown 4.8 150 49 0
recursive-simple/id_o20_false-unreach-call.c error (5) .090 22 .72 0 false(unreach-call) 1.2   26   11    0 false(unreach-call) .78 20 7.6  1 unknown .13  7.8 1.2  0 error 2.9 270 25 0 error 3.0 270 26 0 false(unreach-call) 4.0 300 33 1 false(unreach-call) 1.1  49 13   1 false(unreach-call) 3.7  290 43    1 false(unreach-call) .26  28 2.5  1 false(unreach-call) 1.3   41 2.6  1 false(unreach-call) .46  56 5.0  1 false(unreach-call) 1.8 74 20 0 false(unreach-call) .17 9.4 1.4 1 false(unreach-call) .084 9.8 .37 1 false(unreach-call) 18   590 140 1 false(unreach-call) 22   790 180 1 false(unreach-call) 160   1300 2100 1 unknown 4.7 160 44 0
recursive-simple/id_o3_false-unreach-call.c error (5) .097 22 .75 0 false(unreach-call) .53  22   5.2  1 false(unreach-call) .27 17 2.7  1 unknown .16  7.8 1.2  0 error 2.9 270 25 0 error 2.9 270 22 0 false(unreach-call) 3.2 290 27 1 false(unreach-call) 1.1  49 14   1 false(unreach-call) 3.7  280 48    1 false(unreach-call) .11  23 .89 1 false(unreach-call) .086 23 .88 1 false(unreach-call) .10  23 1.2  1 false(unreach-call) 1.5 84 19 0 false(unreach-call) .14 9.4 1.5 1 false(unreach-call) .11  12   .63 1 false(unreach-call) 6.3 320 49 1 false(unreach-call) 7.7 350 57 1 false(unreach-call) 7.9 370 62 1 unknown 4.6 160 43 0
recursive-simple/sum_10x0_false-unreach-call_true-termination.c error (5) .12  22 .63 0 false(unreach-call) .074 19   .81 0 false(unreach-call) .42 17 4.3  1 false(unreach-call) .058 7.7 .49 1 error 2.8 270 24 0 error 3.1 280 23 0 false(unreach-call) 3.4 300 29 1 false(unreach-call) 1.0  49 13   1 false(unreach-call) .13 23 1.9  1 false(unreach-call) .12  23 .82 1 false(unreach-call) .10  23 1.0  1 false(unreach-call) .13  23 1.3  1 false(unreach-call) 1.5 75 19 1 false(unreach-call) .15 9.3 1.6 1 false(unreach-call) .080 9.5 .53 1 false(unreach-call) 11   490 93 1 false(unreach-call) 10   480 77 1 false(unreach-call) 27   840 270 1 witness invalid (false(unreach-call)) 5.3 230 57 0
recursive-simple/sum_15x0_false-unreach-call_true-termination.c error (5) .12  22 .70 0 false(unreach-call) .073 19   .67 0 false(unreach-call) .55 19 5.3  1 false(unreach-call) .059 7.8 .59 1 error 2.8 270 24 0 error 3.0 270 27 0 false(unreach-call) 3.6 300 33 1 false(unreach-call) 1.1  49 12   1 false(unreach-call) .17 23 1.2  1 false(unreach-call) .36  23 .94 1 false(unreach-call) .12  23 1.2  1 false(unreach-call) .14  25 1.8  1 false(unreach-call) 1.6 68 19 1 false(unreach-call) .16 9.4 1.5 1 false(unreach-call) .078 10   .47 1 false(unreach-call) 14   620 110 1 false(unreach-call) 13   500 110 1 false(unreach-call) 67   1100 750 1 witness invalid (false(unreach-call)) 5.4 230 44 0
recursive-simple/sum_20x0_false-unreach-call_true-termination.c error (5) .099 22 .67 0 false(unreach-call) .076 18   .65 0 false(unreach-call) .72 17 7.2  1 false(unreach-call) .088 7.8 .40 1 error 2.9 270 23 0 error 2.9 280 23 0 false(unreach-call) 3.5 300 28 1 false(unreach-call) 1.0  49 15   1 false(unreach-call) .17 23 1.7  1 false(unreach-call) .12  23 1.4  1 false(unreach-call) .14  24 1.4  1 false(unreach-call) .21  30 2.1  1 false(unreach-call) 1.7 74 22 1 false(unreach-call) .13 9.4 1.6 1 false(unreach-call) .078 9.6 .60 1 false(unreach-call) 18   700 140 1 false(unreach-call) 17   540 120 1 false(unreach-call) 180   1400 2500 1 witness invalid (false(unreach-call)) 5.5 230 57 0
recursive-simple/sum_25x0_false-unreach-call_true-termination.c error (5) .11  22 .67 0 false(unreach-call) .068 18   .71 0 false(unreach-call) .85 17 8.6  1 false(unreach-call) .053 7.7 .58 1 error 2.8 270 27 0 error 3.0 280 23 0 false(unreach-call) 3.8 310 37 1 unknown 5.0  310 50   0 false(unreach-call) .17 23 1.3  1 false(unreach-call) .48  23 1.2  1 false(unreach-call) .20  27 2.0  1 false(unreach-call) .22  35 2.6  1 false(unreach-call) 1.8 73 21 1 false(unreach-call) .13 9.1 1.7 1 false(unreach-call) .052 9.9 .47 1 false(unreach-call) 22   830 200 1 false(unreach-call) 20   620 170 1 false(unreach-call) 420   1400 6000 1 unknown 4.9 150 40 0
recursive-simple/sum_2x3_false-unreach-call_true-termination.c error (5) .12  22 .66 0 false(unreach-call) .094 17   .60 1 false(unreach-call) .14 17 .91 1 false(unreach-call) .12  7.9 .37 1 error 2.9 270 29 0 error 2.9 270 22 0 false(unreach-call) 3.2 300 29 1 false(unreach-call) 1.0  50 12   1 false(unreach-call) .13 23 1.4  1 false(unreach-call) .10  23 .82 1 false(unreach-call) .082 23 .84 1 false(unreach-call) .090 23 1.1  1 false(unreach-call) 1.5 74 19 1 false(unreach-call) .16 9.3 1.5 1 false(unreach-call) .060 9.5 .41 1 false(unreach-call) 6.7 330 51 1 false(unreach-call) 6.9 340 54 1 false(unreach-call) 7.8 370 62 1 witness invalid (false(unreach-call)) 5.5 220 48 0
recursive-simple/sum_non_eq_false-unreach-call.c error (5) .11  22 .72 0 false(unreach-call) .091 20   .59 1 false(unreach-call) .13 17 .92 1 false(unreach-call) .069 7.9 .55 1 error 2.8 280 27 0 error 2.9 270 25 0 false(unreach-call) 3.0 300 28 1 false(unreach-call) .53 49 6.4 1 false(unreach-call) 7.8  500 98    0 false(unreach-call) .073 23 .89 1 false(unreach-call) .073 23 .97 1 false(unreach-call) .10  23 .83 1 false(unreach-call) 1.5 76 23 1 false(unreach-call) .15 9.5 1.9 1 false(unreach-call) .083 9.7 .48 1 false(unreach-call) 5.8 330 45 1 false(unreach-call) 5.5 320 43 1 false(unreach-call) 5.3 310 40 1 witness invalid (false(unreach-call)) 5.8 280 46 0
recursive-simple/sum_non_false-unreach-call_true-termination.c error (5) .083 22 .82 0 false(unreach-call) .065 21   .67 1 false(unreach-call) .12 17 1.1  1 false(unreach-call) .091 7.7 .40 1 error 2.9 280 24 0 error 3.0 290 25 0 false(unreach-call) 3.1 290 28 1 false(unreach-call) .55 50 6.9 1 false(unreach-call) 12    610 140    1 false(unreach-call) .077 23 .79 1 false(unreach-call) .072 23 .90 1 false(unreach-call) .11  23 .72 1 false(unreach-call) 1.5 70 18 1 false(unreach-call) .14 9.2 1.6 1 false(unreach-call) .12  17   .85 1 false(unreach-call) 5.7 320 45 1 false(unreach-call) 5.9 350 43 1 false(unreach-call) 5.6 320 47 1 witness invalid (false(unreach-call)) 5.8 280 54 0
recursive-simple/afterrec_2calls_true-unreach-call_true-termination.c error (5) .098 22 .79 0 unknown .051 8.0 .46 0 true .18 17 1.7  2 true .057 7.8 .37 2 true 2.7 280 23 2 true 2.8 270 22 2 true 2.3 250 19 2 true 3.2  250 29   2 true .16 23 1.3  2 out of memory 880     15000 11000    0 true .072 23 .84 2 true .085 23 .82 2 true 1.2 72 16 2 true .13 9.2 1.8 2 true .050 9.9 .62 2 true 6.0 340 51 2 true 5.6 330 41 2 true 5.9 330 45 2 true 7.3 290 53 2
recursive-simple/afterrec_true-unreach-call_true-termination.c error (5) .085 22 .73 0 true .057 16   .52 2 true .21 17 1.6  2 true .064 7.8 .45 2 true 2.5 260 23 2 true 2.8 270 22 2 true 2.2 240 17 2 true 3.0  250 29   2 true .15 23 1.2  2 out of memory 880     15000 11000    0 true .085 23 .76 2 true .072 23 .77 2 true 1.2 69 15 2 true .15 9.1 1.3 2 true .051 11   .78 2 true 6.0 330 50 2 true 5.6 320 44 2 true 6.1 340 49 2 true 6.8 290 55 2
recursive-simple/fibo_10_true-unreach-call.c error (5) .11  22 .67 0 exception (gremlins) 27     34   320    0 true .54 17 5.2  2 unknown .12  7.8 1.2  0 error 2.9 270 25 0 error 3.1 270 27 0 true 6.8 490 53 2 unknown 8.1  430 64   0 true .19 23 1.8  2 timeout 900     11000 12000    0 true .59  31 6.7  2 true 1.0   43 12    2 true 2.2 93 30 2 true .15 9.4 1.6 2 true .083 9.8 1.1  2 true 31   2500 260 2 timeout 900   5200 12000 0 timeout 900   13000 5600 0 true 7.5 290 61 2
recursive-simple/fibo_15_true-unreach-call.c error (5) .085 22 .88 0 exception (gremlins) 21     32   240    0 true 2.7  34 29    2 unknown .12  7.9 1.4  0 error 2.9 270 27 0 error 3.1 290 22 0 true 46   2300 540 2 unknown 49    2300 570   0 true .64 59 7.7  2 timeout 900     9800 12000    0 true 220     190 3100    2 true 450     310 5300    2 true 110   590 1100 2 true .17 9.3 1.6 2 true .68  77   8.0  2 true 580   6300 8500 2 timeout 900   5200 13000 0 timeout 910   13000 5800 0 true 9.8 290 95 2
recursive-simple/fibo_20_true-unreach-call.c error (5) .097 22 .92 0 exception (gremlins) 21     35   260    0 true 360    350 2700    1 unknown .13  7.7 1.1  0 error 3.0 280 25 0 error 2.9 270 22 0 timeout 910   3900 11000 0 timeout 900    3900 12000   0 true 6.2  560 96    1 timeout 900     8400 11000    0 timeout 900     380 10000    0 timeout 900     310 13000    0 true 890   2700 8100 1 true .21 15   2.0 1 true 8.6   800   100    1 timeout 900   5500 13000 0 timeout 900   5200 15000 0 timeout 910   13000 6700 0 unknown 720   200 5400 0
recursive-simple/fibo_25_true-unreach-call.c error (5) .12  22 .59 0 exception (gremlins) 28     35   280    0 error (42) 850    390 3100    0 unknown .12  7.6 1.2  0 error 2.9 270 25 0 error 3.0 290 29 0 timeout 930   5000 11000 0 timeout 900    4400 11000   0 true 71    6100 990    1 timeout 900     8500 11000    0 timeout 900     210 2000    0 timeout 900     310 11000    0 true 890   2900 11000 1 true .78 77   11   1 true 120     15000   1200    1 timeout 900   5400 11000 0 timeout 900   5300 11000 0 timeout 910   13000 6000 0 unknown 4.7 150 43 0
recursive-simple/fibo_2calls_10_true-unreach-call.c error (5) .11  22 .77 0 exception (gremlins) 21     41   270    0 true .42 17 4.0  2 unknown .22  7.7 2.5  0 error 3.1 270 24 0 error 3.2 270 25 0 true 7.3 510 56 2 unknown 8.8  490 83   0 true .18 23 2.1  2 timeout 900     11000 12000    0 true .38  25 4.5  2 true .64  30 6.8  2 true 2.3 93 30 2 true .16 9.3 1.3 2 true .096 11   1.1  2 true 75   3800 740 2 timeout 900   5100 12000 0 timeout 900   13000 5700 0 true 7.6 300 56 2
recursive-simple/fibo_2calls_15_true-unreach-call.c error (5) .098 22 .72 0 exception (gremlins) 42     37   550    0 true 2.5  35 33    1 unknown .26  7.8 2.2  0 error 3.0 280 28 0 error 3.1 280 25 0 true 63   2400 820 1 unknown 65    2600 920   0 true .75 81 8.8  1 timeout 900     9500 12000    0 true 130     150 1600    1 true 270     210 3700    1 true 66   550 550 1 true .30 18   2.0 1 true .76  78   9.0  1 timeout 900   5400 11000 0 timeout 900   5300 12000 0 timeout 910   13000 6200 0 true 10   290 88 1
recursive-simple/fibo_2calls_20_true-unreach-call.c error (5) .12  22 .65 0 exception (gremlins) 65     43   750    0 true 380    360 2100    1 unknown .21  7.7 2.2  0 error 3.2 280 26 0 error 3.2 280 25 0 timeout 910   3900 14000 0 timeout 900    3900 13000   0 true 7.3  800 97    1 timeout 900     8200 11000    0 timeout 900     520 11000    0 timeout 900     240 12000    0 timeout 890   2700 7400 0 true .18 11   1.8 1 true 11     1500   120    1 timeout 900   5300 12000 0 timeout 900   5200 12000 0 timeout 900   13000 5800 0 unknown 720   200 5900 0
recursive-simple/fibo_2calls_25_true-unreach-call.c error (5) .11  22 .75 0 exception (gremlins) 63     47   730    0 error (42) 850    390 3500    0 unknown .26  7.7 2.1  0 error 3.0 280 27 0 error 3.2 270 26 0 timeout 960   5500 12000 0 timeout 900    4500 11000   0 true 84    8800 1000    1 timeout 900     7900 11000    0 timeout 900     580 13000    0 timeout 900     240 11000    0 timeout 890   2900 10000 0 true .50 42   5.3 1 true 140     14000   1600    1 timeout 900   5500 12000 0 timeout 900   5200 12000 0 timeout 900   13000 6200 0 unknown 840   200 6700 0
recursive-simple/fibo_2calls_2_true-unreach-call_true-termination.c error (5) .10  22 .70 0 true .056 16   .57 2 true .21 17 1.6  2 true .12  7.6 1.4  2 true 2.8 260 25 2 true 2.9 270 24 2 true 2.3 250 22 2 true 13    260 21   2 true .16 23 1.3  2 timeout 900     11000 12000    0 true .098 23 .74 2 true .086 23 .65 2 true 1.2 67 16 2 true .13 9.2 1.4 2 true .051 9.8 .65 2 true 8.8 460 64 2 timeout 900   1300 12000 0 true 10   500 76 2 true 7.2 290 54 2
recursive-simple/fibo_2calls_4_true-unreach-call_true-termination.c error (5) .10  22 .78 0 exception (gremlins) 5.6   32   70    0 true .18 17 1.9  2 true .31  7.7 3.7  2 error 2.9 280 26 0 error 3.0 270 22 0 true 3.6 290 31 2 unknown 4.9  300 45   0 true .13 23 1.4  2 timeout 900     11000 14000    0 true .30  23 .84 2 true .13  23 .86 2 true 1.2 73 17 2 true .14 9.3 1.7 2 true .059 9.9 .42 2 true 14   500 110 2 timeout 900   1100 13000 0 true 18   680 170 2 true 8.1 320 71 2
recursive-simple/fibo_2calls_5_true-unreach-call_true-termination.c error (5) .12  22 .68 0 exception (gremlins) 9.7   32   120    0 true .17 17 1.9  2 true .47  9.2 6.7  2 error 3.0 280 28 0 error 3.1 270 25 0 true 3.5 290 31 2 unknown 4.9  300 48   0 true .16 23 1.6  2 timeout 900     12000 13000    0 true .12  23 .77 2 true .12  23 .94 2 true 1.3 71 15 2 true .13 9.3 1.4 2 true .078 9.6 .54 2 true 17   530 130 2 timeout 900   1100 13000 0 true 28   700 250 2 true 7.4 300 64 2
recursive-simple/fibo_2calls_6_true-unreach-call_true-termination.c error (5) .12  22 .68 0 exception (gremlins) 18     33   230    0 true .21 17 1.7  2 true .78  20   9.7  2 error 3.0 280 28 0 error 3.1 290 26 0 true 4.0 300 33 2 unknown 5.3  300 56   0 true .13 23 2.4  2 timeout 900     11000 13000    0 true .12  23 .87 2 true .13  23 1.0  2 true 1.3 73 15 2 true .13 9.2 1.4 2 true .058 9.8 .62 2 true 25   900 210 2 timeout 900   1800 12000 0 true 45   1200 420 2 true 7.9 290 63 2
recursive-simple/fibo_2calls_8_true-unreach-call_true-termination.c error (5) .11  22 .66 0 exception (gremlins) 21     37   270    0 true .34 17 3.5  2 unknown .32  44   2.5  0 error 3.0 270 27 0 error 3.2 280 27 0 true 5.2 370 40 2 unknown 6.2  350 50   0 true .16 23 1.6  2 timeout 900     11000 14000    0 true .16  23 1.3  2 true .16  23 4.3  2 true 1.4 73 18 2 true .14 9.2 1.5 2 true .066 9.9 .68 2 true 39   1300 310 2 timeout 900   2900 12000 0 true 170   5300 1500 2 true 7.9 290 61 2
recursive-simple/fibo_5_true-unreach-call_true-termination.c error (5) .12  22 .69 0 exception (gremlins) 5.6   32   59    0 true .32 17 3.0  2 unknown .12  7.9 1.3  0 error 2.9 280 23 0 error 3.1 280 26 0 true 3.3 290 30 2 unknown 4.7  300 42   0 true .15 23 1.3  2 timeout 900     12000 12000    0 true .099 23 1.2  2 true .10  23 1.2  2 true 1.3 70 17 2 true .13 9.3 1.7 2 true .051 9.7 .72 2 true 12   490 100 2 timeout 900   1800 12000 0 true 20   730 180 2 true 7.8 290 65 2
recursive-simple/fibo_7_true-unreach-call.c error (5) .11  22 .76 0 exception (gremlins) 13     33   170    0 true .35 17 3.4  2 unknown .12  7.9 1.3  0 error 2.9 280 24 0 error 3.0 280 22 0 true 3.9 300 35 2 unknown 5.2  300 54   0 true .16 24 1.3  2 timeout 900     12000 12000    0 true .17  23 1.7  2 true .22  25 2.6  2 true 1.3 66 15 2 true .16 9.3 1.3 2 true .055 9.9 .72 2 true 18   710 140 2 timeout 900   3300 13000 0 true 42   1300 400 2 true 7.8 290 59 2
recursive-simple/id2_b2_o3_true-unreach-call.c error (5) .12  22 .57 0 true .41  22   4.1  2 error (42) 850    4900 5400    0 unknown .43  7.9 5.0  0 true 2.9 270 26 2 error 3.1 280 25 0 true 3.2 290 27 2 unknown 4.8  300 42   0 true 35    1400 370    2 out of memory 570     15000 6900    0 out of memory 440     15000 5300    0 out of memory 410     15000 4500    0 true 1.2 68 15 2 timeout (timeout) 900    2400   12000   0 timeout 900     360   9900    0 true 6.7 340 53 2 true 6.6 340 51 2 true 7.1 340 50 2 unknown 5.1 150 48 0
recursive-simple/id2_b3_o5_true-unreach-call.c error (5) .089 22 .81 0 true .43  22   2.6  2 error (42) 850    4900 6100    0 unknown .43  8.0 6.2  0 true 2.8 270 27 2 error 3.0 280 24 0 true 3.3 300 24 2 unknown 4.8  300 45   0 true 35    1400 420    2 timeout 900     12000 11000    0 out of memory 510     15000 6400    0 out of memory 450     15000 6600    0 true 1.2 70 15 2 timeout (timeout) 900    2300   13000   0 timeout 900     360   11000    0 true 6.9 340 50 2 true 6.2 330 49 2 true 7.6 350 59 2 unknown 5.2 150 52 0
recursive-simple/id2_b5_o10_true-unreach-call.c error (5) .11  22 .66 0 true .45  22   3.8  2 error (42) 850    6800 3500    0 unknown .45  7.9 5.2  0 true 2.8 270 26 2 error 3.2 280 27 0 true 3.4 300 30 2 unknown 5.0  300 52   0 true 35    1400 390    2 timeout 900     14000 11000    0 out of memory 460     15000 6200    0 out of memory 410     15000 5000    0 true 1.2 67 14 2 timeout (timeout) 900    2200   11000   0 timeout 900     370   12000    0 true 6.9 330 55 2 true 6.2 330 45 2 true 8.0 340 62 2 unknown 5.2 150 51 0
recursive-simple/id2_i5_o5_true-unreach-call_true-termination.c error (5) .10  22 .81 0 true .077 16   .47 2 true .18 17 1.6  2 true .13  7.8 1.3  2 error 2.8 270 24 0 error 3.2 280 24 0 true 3.3 300 29 2 unknown 4.6  300 46   0 true .13 23 1.3  2 timeout 900     13000 11000    0 true .090 23 .97 2 true .092 23 .90 2 true 1.2 72 18 2 true .16 9.4 1.6 2 true .050 9.8 .57 2 true 11   480 79 2 timeout 900   1100 13000 0 true 14   540 110 2 true 7.6 290 54 2
recursive-simple/id_b2_o3_true-unreach-call.c error (5) .12  22 .71 0 true .27  20   2.2  2 error (42) 850    6700 6200    0 unknown .16  7.8 1.7  0 true 2.7 270 23 2 error 3.1 280 24 0 true 3.2 290 24 2 unknown 4.6  300 49   0 true 11    440 140    2 out of memory 540     15000 6600    0 out of memory 430     15000 5100    0 out of memory 400     15000 5600    0 true 1.2 66 14 2 timeout (timeout) 900    2200   10000   0 timeout 900     370   10000    0 true 6.4 330 58 2 true 6.0 330 48 2 true 9.6 470 76 2 unknown 5.0 150 43 0
recursive-simple/id_b3_o5_true-unreach-call.c error (5) .11  22 .79 0 true .24  20   2.3  2 error (42) 850    6700 6600    0 unknown .15  7.7 2.0  0 true 2.6 270 26 2 error 3.1 270 27 0 true 3.1 300 28 2 unknown 4.5  300 45   0 true 11    440 130    2 out of memory 820     15000 9900    0 out of memory 510     15000 6900    0 out of memory 460     15000 6900    0 true 1.2 62 14 2 timeout (timeout) 900    2400   9400   0 timeout 900     370   13000    0 true 6.4 330 52 2 true 6.0 330 49 2 true 9.3 420 76 2 unknown 5.0 150 45 0
recursive-simple/id_b5_o10_true-unreach-call.c error (5) .11  22 .77 0 true .31  20   2.1  2 out of memory 780    15000 3300    0 unknown .16  7.8 1.7  0 true 2.7 270 26 2 error 3.0 270 23 0 true 3.2 290 27 2 unknown 4.8  300 45   0 true 11    440 140    2 out of memory 630     15000 7700    0 out of memory 460     15000 5800    0 out of memory 420     15000 5600    0 true 1.2 61 16 2 timeout (timeout) 900    2200   11000   0 timeout 900     390   13000    0 true 6.4 330 54 2 true 6.4 340 48 2 true 9.8 470 75 2 unknown 4.9 150 49 0
recursive-simple/id_i10_o10_true-unreach-call_true-termination.c error (5) .10  22 .60 0 false(unreach-call) .071 21   .70 -16 true .46 17 4.5  2 unknown .099 7.6 .61 0 error 2.8 280 25 0 error 3.0 280 27 0 true 3.0 280 28 2 unknown 4.6  300 39   0 true .15 23 1.2  2 timeout 900     13000 13000    0 true .38  23 .72 2 true .11  23 1.3  2 true 1.2 68 18 2 true .15 9.2 1.6 2 true .068 9.7 .56 2 true 12   490 99 2 true 12   570 110 2 true 28   730 300 2 true 7.6 300 64 2
recursive-simple/id_i15_o15_true-unreach-call_true-termination.c error (5) .11  22 .85 0 false(unreach-call) .076 20   .77 -16 true .61 17 7.0  2 unknown .11  43   .97 0 error 2.8 280 25 0 error 3.0 270 26 0 true 3.3 300 28 2 unknown 4.8  300 45   0 true .13 23 1.5  2 timeout 900     12000 12000    0 true .11  23 1.3  2 true .15  25 1.5  2 true 1.3 70 16 2 true .16 9.4 1.4 2 true .053 9.9 .54 2 true 15   540 130 2 true 18   600 140 2 true 70   1400 810 2 true 7.5 290 61 2
recursive-simple/id_i20_o20_true-unreach-call_true-termination.c error (5) .10  22 .64 0 false(unreach-call) .065 17   1.1  -16 true .76 17 7.6  2 unknown .070 7.8 .70 0 error 2.8 280 29 0 error 3.0 280 23 0 true 3.5 310 30 2 unknown 4.7  300 45   0 true .15 23 1.3  2 timeout 900     12000 12000    0 true .17  24 1.4  2 true .17  30 2.2  2 true 1.4 70 18 2 true .15 9.5 1.8 2 true .050 9.9 .58 2 true 21   620 170 2 true 23   720 210 2 true 180   1100 2200 2 true 8.0 290 70 2
recursive-simple/id_i25_o25_true-unreach-call_true-termination.c error (5) .12  22 .65 0 false(unreach-call) .089 18   .73 -16 true .91 17 9.7  2 unknown .080 7.8 .65 0 error 2.6 270 24 0 error 3.0 270 24 0 true 3.4 300 29 2 unknown 4.8  300 43   0 true .13 23 1.4  2 timeout 900     11000 14000    0 true .67  27 1.3  2 true .21  36 2.4  2 true 1.5 68 17 2 true .13 9.2 1.5 2 true .049 9.8 .55 2 true 25   820 200 2 true 29   800 290 2 true 430   1100 5800 2 unknown 4.9 160 46 0
recursive-simple/id_i5_o5_true-unreach-call_true-termination.c error (5) .10  22 .74 0 false(unreach-call) .069 17   .69 -16 true .32 17 2.8  2 unknown .069 7.8 .70 0 error 2.8 270 24 0 error 3.1 280 26 0 true 3.1 290 25 2 unknown 4.5  300 42   0 true .12 23 1.4  2 timeout 900     13000 14000    0 true .084 23 .79 2 true .34  23 .64 2 true 1.2 69 13 2 true .13 9.3 2.0 2 true .053 9.9 .45 2 true 9.1 490 66 2 true 9.8 480 84 2 true 12   490 96 2 true 7.4 290 65 2
recursive-simple/sum_10x0_true-unreach-call_true-termination.c error (5) .12  22 .65 0 false(unreach-call) .068 19   .88 -16 true .51 17 4.2  2 true .084 17   .56 2 error 2.8 270 24 0 error 3.1 280 21 0 true 3.6 300 30 2 unknown 5.0  300 46   0 true .16 23 1.3  2 timeout 900     14000 12000    0 true .11  23 1.0  2 true .14  23 1.3  2 true 1.2 68 16 2 true .15 9.4 1.3 2 true .068 9.9 .47 2 true 14   490 110 2 timeout 900   1000 14000 0 true 36   830 410 2 true 7.7 290 69 2
recursive-simple/sum_15x0_true-unreach-call_true-termination.c error (5) .099 22 .75 0 false(unreach-call) .070 18   .86 -16 true .63 17 5.2  2 true .064 7.8 .42 2 error 2.9 270 24 0 error 3.0 270 26 0 true 3.6 300 32 2 unknown 4.9  300 41   0 true .13 23 1.7  2 timeout 900     13000 11000    0 true .12  23 1.3  2 true .15  25 1.6  2 true 1.3 74 15 2 true .13 9.5 1.5 2 true .067 9.8 .51 2 true 19   560 140 2 timeout 900   1000 13000 0 true 95   1400 1100 2 true 7.6 300 61 2
recursive-simple/sum_20x0_true-unreach-call_true-termination.c error (5) .10  22 .73 0 false(unreach-call) .071 17   .89 -16 true .80 17 8.0  2 true .082 7.6 .46 2 error 2.8 280 24 0 error 3.1 270 28 0 true 3.7 300 30 2 unknown 5.4  310 55   0 true .13 23 1.5  2 timeout 900     12000 14000    0 true .16  24 1.6  2 true .19  30 2.7  2 true 1.3 68 18 2 true .15 9.3 1.5 2 true .054 9.9 .47 2 true 24   670 200 2 timeout 900   1100 13000 0 true 230   1200 3000 2 true 7.9 290 61 2
recursive-simple/sum_25x0_true-unreach-call_true-termination.c error (5) .12  22 .71 0 false(unreach-call) .099 18   .74 -16 true .90 17 9.8  2 true .077 7.6 .40 2 error 2.9 280 24 0 error 3.1 290 26 0 true 4.2 300 32 2 unknown 5.4  300 47   0 true .17 23 1.6  2 timeout 900     11000 12000    0 true .18  27 2.2  2 true .25  36 3.0  2 true 1.3 66 16 2 true .13 9.5 1.3 2 true .068 9.9 .42 2 true 31   970 270 2 timeout 900   1300 13000 0 true 530   1400 6900 2 unknown 4.6 160 45 0
recursive-simple/sum_2x3_true-unreach-call_true-termination.c error (5) .090 22 .85 0 true .053 16   .55 2 true .20 17 1.6  2 true .065 7.8 .42 2 error 2.8 280 25 0 error 3.0 280 26 0 true 3.1 290 27 2 unknown 4.6  300 39   0 true .12 23 1.8  2 timeout 900     13000 11000    0 true .10  23 .80 2 true .077 23 1.0  2 true 1.2 68 15 2 true .16 9.3 1.4 2 true .080 9.7 .44 2 true 8.3 410 63 2 timeout 900   930 9900 0 true 12   570 95 2 true 7.4 290 59 2
recursive-simple/sum_non_eq_true-unreach-call.c error (5) .085 22 .77 0 exception (gremlins) 8.1   35   110    0 error (42) 850    320 10000    0 unknown .13  7.6 1.2  0 error 3.0 290 26 0 error 2.9 260 24 0 true 3.3 310 28 2 unknown 5.2  310 51   0 true 150    660 2000    2 timeout 900     1100 11000    0 timeout 900     2200 13000    0 timeout 900     3200 13000    0 true 880   530 12000 2 true .16 9.4 1.4 2 true .063 9.8 .46 2 true 7.0 350 60 2 true 6.7 330 52 2 true 8.6 370 68 2 unknown 4.7 150 43 0
recursive-simple/sum_non_true-unreach-call_true-termination.c error (5) .12  22 .68 0 exception (gremlins) 8.4   33   84    0 error (42) 850    260 11000    0 unknown .12  7.7 1.3  0 error 2.8 280 26 0 error 3.0 280 24 0 true 3.3 310 26 2 unknown 4.7  310 46   0 true 780    840 7800    2 out of memory 580     15000 7700    0 out of memory 350     15000 4100    0 out of memory 300     15000 4200    0 true 880   260 11000 2 true .21 17   1.9 2 true .082 9.7 .86 2 true 7.2 370 52 2 true 6.6 330 50 2 true 8.5 390 66 2 unknown 4.9 160 48 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
total 98 10 2200 72 0 98 1100   3200 13000 -270 98 24000 91000 140000 86 98 23   920 250 43 98 280   27000 2500 19 98 300   27000 2500 10 98 13000 100000 140000 119 98 16000 290000 210000 35 98 5300   310000 65000 72 98 43000   620000 550000 37 98 23000 230000 260000 89 98 23000 230000 260000 89 98 22000 66000 240000 125 98 17000   110000 220000 91 98 23000     91000 300000    57 98 19000 140000 240000 116 98 46000   140000 600000 65 98 31000 370000 280000 100 98 19000 57000 130000 45
    correct results 0 24 5.8 470 51 34 57 25 1100 250 82 31 5.8 320 59 43 10 28   2700 260 19 7 22   2000 180 10 76 390 28000 3500 116 32 47 2200 430 35 64 1200   12000 12000 97 37 6.6 870 57 37 62 520 1900 6500 87 62 1000 2400 13000 87 75 8400 20000 96000 116 57 8.6 540 90 84 58 14     810 190    84 74 1800 53000 19000 116 45 670   22000 6700 64 66 4100 55000 50000 100 22 170 6500 1400 44
        correct true 0 10 2.4 190 19 20 25 14 450 140 50 12 2.3 120 26 24 9 24   2400 230 18 3 8.5 810 68 6 40 240 16000 2300 80 3 19 770 80 6 33 1100   7800 11000 66 0 25 220 830 3100 50 25 460 1000 5400 50 41 8100 16000 94000 82 27 4.1 260 42 54 26 2.3   320 24    52 42 1500 37000 16000 84 19 180   8000 1500 38 34 2300 33000 27000 68 22 170 6500 1400 44
        correct false 0 14 3.4 280 32 14 32 11 660 110 32 19 3.5 200 34 19 1 3.2 280 29 1 4 14   1200 110 4 36 140 11000 1200 36 29 28 1500 350 29 31 81   4200 980 31 37 6.6 870 57 37 37 290 1100 3400 37 37 590 1300 7400 37 34 280 3600 2700 34 30 4.5 280 47 30 32 12     480 160    32 32 350 15000 2900 32 26 490   14000 5100 26 32 1800 22000 23000 32 0
    correct-unconfimed results 0 13 6.3 270 66 0 14 1200 2800 7600 4 0 0 0 8 530 12000 6300 3 8 520 13000 6500 0 15 380   25000 4800 7 7 490   6700 5800 0 5 240 3200 3000 2 5 390 5000 5500 2 15 6400 14000 71000 9 22 12   2100 150 7 10 550     63000 6500    5 7 1500 20000 20000 0 3 320   3500 4200 1 2 180 7100 1900 0 1 10 290 88 1
        correct-unconfirmed true 0 0 4 750 770 4900 4 0 0 0 3 77 3200 940 3 0 7 220   19000 2700 7 0 2 140 230 1700 2 2 270 330 3700 2 9 6300 14000 69000 9 7 2.4 180 26 7 5 280     31000 3100    5 0 1 9.2 460 81 1 0 1 10 290 88 1
        correct-unconfirmed false 0 13 6.3 270 66 0 10 440 2000 2700 0 0 0 0 5 460 8800 5400 0 8 520 13000 6500 0 8 150   5800 2100 0 7 490   6700 5800 0 3 100 3000 1300 0 3 120 4600 1800 0 6 180 660 2300 0 15 9.9 1900 120 0 5 270     31000 3500    0 7 1500 20000 20000 0 2 310   3000 4100 0 2 180 7100 1900 0 0
    incorrect results 0 16 29   360 350 -304 0 0 0 0 0 0 1 3.8 290 45 -32 0 0 0 0 0 1 .088 11 .73 -32 0 0 0 0
        incorrect true 0 3 17   83 210 -96 0 0 0 0 0 0 1 3.8 290 45 -32 0 0 0 0 0 1 .088 11 .73 -32 0 0 0 0
        incorrect false 0 13 11   280 130 -208 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
score (98 tasks, max score: 151) 0 -270 86 43 19 10 119 35 72 37 89 89 125 91 57 116 65 100 45
Run set 2ls.sv-comp17.ReachSafety-Recursive blast.sv-comp17.ReachSafety-Recursive cbmc.sv-comp17.ReachSafety-Recursive ceagle.sv-comp17.ReachSafety-Recursive cpa-bam-bnb.sv-comp17.ReachSafety-Recursive cpa-kind.sv-comp17.ReachSafety-Recursive cpa-seq.sv-comp17.ReachSafety-Recursive depthk.sv-comp17.ReachSafety-Recursive esbmc.sv-comp17.ReachSafety-Recursive esbmc-falsi.sv-comp17.ReachSafety-Recursive esbmc-incr.sv-comp17.ReachSafety-Recursive esbmc-kind.sv-comp17.ReachSafety-Recursive smack.sv-comp17.ReachSafety-Recursive symbiotic4.sv-comp17.ReachSafety-Recursive symdivine.sv-comp17.ReachSafety-Recursive uautomizer.sv-comp17.ReachSafety-Recursive ukojak.sv-comp17.ReachSafety-Recursive utaipan.sv-comp17.ReachSafety-Recursive veriabs.sv-comp17.ReachSafety-Recursive