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-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-ProductLines blast.sv-comp17.ReachSafety-ProductLines cbmc.sv-comp17.ReachSafety-ProductLines ceagle.sv-comp17.ReachSafety-ProductLines cpa-bam-bnb.sv-comp17.ReachSafety-ProductLines cpa-kind.sv-comp17.ReachSafety-ProductLines cpa-seq.sv-comp17.ReachSafety-ProductLines depthk.sv-comp17.ReachSafety-ProductLines esbmc.sv-comp17.ReachSafety-ProductLines esbmc-falsi.sv-comp17.ReachSafety-ProductLines esbmc-incr.sv-comp17.ReachSafety-ProductLines esbmc-kind.sv-comp17.ReachSafety-ProductLines smack.sv-comp17.ReachSafety-ProductLines symbiotic4.sv-comp17.ReachSafety-ProductLines symdivine.sv-comp17.ReachSafety-ProductLines uautomizer.sv-comp17.ReachSafety-ProductLines ukojak.sv-comp17.ReachSafety-ProductLines utaipan.sv-comp17.ReachSafety-ProductLines veriabs.sv-comp17.ReachSafety-ProductLines
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 --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/product-lines/ 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
elevator_spec14_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 5.7  1200 63    1 false(unreach-call) 350     320 3700    1 false(unreach-call) .24 27 2.3 1 false(unreach-call) .11  9.2 1.2  1 false(unreach-call) 100   4300 620 1 false(unreach-call) 10   500 76 0 false(unreach-call) 6.4 290 53 1 false(unreach-call) 480    370 6300   0 false(unreach-call) 18   7300 140 1 false(unreach-call) .16  36 2.1  1 false(unreach-call) .18  36 2.3  1 false(unreach-call) .22  36 2.1  1 false(unreach-call) 5.9 190 70 1 false(unreach-call) .36 19   5.0 1 true .89 160 9.8 -32 timeout 900   13000 6300 0 timeout 900   1800 13000 0 timeout 900   3400 13000 0 false(unreach-call) 230 1400 2700 1
elevator_spec14_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 9.6  1900 110    1 exception (gremlins) 1.2   40 17    0 false(unreach-call) .21 27 2.4 1 false(unreach-call) .11  9.4 1.3  1 false(unreach-call) 140   5700 970 1 false(unreach-call) 10   560 74 0 false(unreach-call) 6.2 290 54 1 false(unreach-call) 480    520 4300   0 false(unreach-call) 19   7300 130 1 false(unreach-call) .17  37 2.0  1 false(unreach-call) .20  36 1.6  1 false(unreach-call) .23  36 2.3  1 false(unreach-call) 5.9 200 71 1 false(unreach-call) .36 19   4.2 1 true 1.0  160 13   -32 timeout 910   13000 5400 0 timeout 900   2000 11000 0 timeout 900   2900 14000 0 false(unreach-call) 380 1400 4200 1
elevator_spec14_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 6.2  1200 57    1 false(unreach-call) 380     320 4600    1 false(unreach-call) .22 27 2.3 1 false(unreach-call) .12  18   1.5  1 false(unreach-call) 110   4400 790 1 false(unreach-call) 9.7 450 68 0 false(unreach-call) 6.5 290 48 1 false(unreach-call) 480    450 5200   0 false(unreach-call) 18   7300 130 1 false(unreach-call) .16  36 1.9  1 false(unreach-call) .20  36 1.8  1 false(unreach-call) .23  36 2.2  1 false(unreach-call) 6.5 200 79 1 false(unreach-call) .36 19   4.2 1 true .91 160 11   -32 timeout 900   11000 7100 0 timeout 900   1700 11000 0 timeout 900   2800 12000 0 false(unreach-call) 240 1200 2700 1
elevator_spec14_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 10    2000 93    1 exception (gremlins) 1.2   40 14    0 false(unreach-call) .21 27 1.9 1 false(unreach-call) .11  9.4 1.3  1 false(unreach-call) 130   5600 910 1 false(unreach-call) 10   560 77 0 false(unreach-call) 6.5 310 61 1 false(unreach-call) 6.1  540 57   0 false(unreach-call) 19   7300 130 1 false(unreach-call) .17  36 2.5  1 false(unreach-call) .17  36 1.9  1 false(unreach-call) .21  37 2.6  1 false(unreach-call) 6.6 220 83 1 false(unreach-call) .39 20   4.7 1 true 1.1  160 12   -32 timeout 900   13000 6000 0 timeout 900   2400 11000 0 timeout 900   3000 13000 0 false(unreach-call) 340 1400 3300 1
elevator_spec14_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 34    6700 400    1 exception (gremlins) 99     280 1200    0 false(unreach-call) 8.8  440 110   1 unknown .15  16   1.4  0 timeout 900   11000 4600 0 false(unreach-call) 15   830 120 0 false(unreach-call) 6.8 320 55 1 false(unreach-call) 530    1400 5400   0 timeout 900   1000 11000 0 false(unreach-call) 550     250 1300    0 false(unreach-call) 130     250 1600    0 false(unreach-call) 130     250 1600    0 false(unreach-call) 12   270 130 1 false(unreach-call) .43 24   5.2 1 true 23    640 280   -32 timeout 900   13000 7000 0 timeout 900   2000 13000 0 timeout 900   4200 13000 0 timeout (false(unreach-call)) 900 2000 7600 0
elevator_spec1_product18_false-unreach-call_true-termination.cil.c false(unreach-call) 38    800 420    0 timeout 900     690 11000    0 false(unreach-call) .59 27 5.3 1 false(unreach-call) .20  65   2.0  1 timeout 910   11000 5600 0 false(unreach-call) 11   570 88 0 false(unreach-call) 6.5 310 46 1 false(unreach-call) 490    180 5900   0 false(unreach-call) 18   7300 130 1 false(unreach-call) .23  36 2.5  1 false(unreach-call) .23  36 3.2  1 false(unreach-call) 2.4   63 31    1 false(unreach-call) 5.7 190 76 1 false(unreach-call) .38 19   4.6 1 true .29 42 3.6 -32 timeout 910   13000 6700 0 timeout 900   3500 14000 0 timeout 900   1900 14000 0 witness invalid (false(unreach-call)) 380 2700 4500 0
elevator_spec1_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 35    840 350    0 timeout 900     150 12000    0 false(unreach-call) .59 27 6.1 1 false(unreach-call) .12  9.7 1.3  1 timeout 910   11000 5200 0 false(unreach-call) 10   580 82 0 false(unreach-call) 7.1 320 50 1 false(unreach-call) 490    200 5600   0 false(unreach-call) 19   7300 140 1 false(unreach-call) .21  37 2.4  1 false(unreach-call) .24  36 3.2  1 false(unreach-call) 2.6   65 33    1 false(unreach-call) 6.6 210 89 1 false(unreach-call) .38 19   5.6 1 true .32 42 3.3 -32 timeout 900   13000 8100 0 timeout 900   2400 12000 0 timeout 900   2200 13000 0 witness invalid (false(unreach-call)) 380 3500 5200 0
elevator_spec1_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 43    1100 440    0 exception (gremlins) 2.3   61 27    0 false(unreach-call) .60 27 5.6 1 false(unreach-call) .16  16   1.1  1 timeout 910   11000 5700 0 false(unreach-call) 11   580 84 0 false(unreach-call) 6.6 320 55 1 false(unreach-call) 500    240 5700   0 false(unreach-call) 18   7300 130 1 false(unreach-call) .21  37 2.5  1 false(unreach-call) .24  37 2.9  1 false(unreach-call) 5.6   81 71    1 false(unreach-call) 6.7 200 83 1 false(unreach-call) .39 19   4.3 1 true .31 42 3.4 -32 timeout 900   13000 6700 0 timeout 900   2100 12000 0 timeout 900   1800 13000 0 witness invalid (false(unreach-call)) 390 3200 4100 0
elevator_spec1_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 46    1200 410    0 exception (gremlins) 2.2   54 26    0 false(unreach-call) .61 28 5.6 1 false(unreach-call) .20  65   1.6  1 timeout 910   11000 5500 0 false(unreach-call) 11   590 74 0 false(unreach-call) 7.0 340 59 1 false(unreach-call) 500    330 5800   0 false(unreach-call) 19   7300 140 1 false(unreach-call) .25  37 2.9  1 false(unreach-call) .28  37 3.1  1 false(unreach-call) 6.1   84 73    1 false(unreach-call) 7.7 220 110 1 false(unreach-call) .38 20   4.7 1 true .30 43 3.9 -32 timeout 900   14000 5900 0 timeout 900   4500 12000 0 timeout 900   2100 13000 0 witness invalid (false(unreach-call)) 380 3100 4700 0
elevator_spec1_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 37    830 360    0 timeout 900     450 12000    0 false(unreach-call) .52 27 6.3 1 false(unreach-call) .11  9.5 1.2  1 timeout 900   11000 5100 0 false(unreach-call) 11   590 84 0 false(unreach-call) 6.6 300 58 1 false(unreach-call) 490    200 5700   0 false(unreach-call) 19   7300 140 1 false(unreach-call) .20  36 2.7  1 false(unreach-call) .25  36 2.7  1 false(unreach-call) 2.6   66 33    1 false(unreach-call) 5.4 170 69 1 false(unreach-call) .39 20   4.9 1 true .31 42 3.3 -32 timeout 910   13000 6300 0 timeout 900   2400 12000 0 timeout 900   1900 14000 0 witness invalid (false(unreach-call)) 380 3100 4300 0
elevator_spec1_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 37    890 510    0 timeout 900     710 11000    0 false(unreach-call) .62 27 5.0 1 false(unreach-call) .13  16   1.4  1 timeout 910   11000 5400 0 false(unreach-call) 11   600 94 0 false(unreach-call) 6.8 320 58 1 false(unreach-call) 490    210 6100   0 false(unreach-call) 19   7300 130 1 false(unreach-call) .21  37 2.4  1 false(unreach-call) .27  37 2.8  1 false(unreach-call) 12     70 28    1 false(unreach-call) 6.7 210 84 1 false(unreach-call) .40 20   4.5 1 true .34 43 3.4 -32 timeout 910   14000 6100 0 timeout 900   3400 11000 0 timeout 900   1900 11000 0 witness invalid (false(unreach-call)) 380 3300 4500 0
elevator_spec1_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 41    1200 490    0 exception (gremlins) 2.7   74 32    0 false(unreach-call) .59 27 5.7 1 false(unreach-call) .11  9.7 1.4  1 timeout 910   11000 6000 0 false(unreach-call) 10   600 85 0 false(unreach-call) 6.6 320 57 1 false(unreach-call) 500    330 6000   0 false(unreach-call) 19   7300 140 1 false(unreach-call) .21  37 2.4  1 false(unreach-call) .24  37 2.8  1 false(unreach-call) 6.0   84 81    1 false(unreach-call) 6.9 210 72 1 false(unreach-call) .40 20   4.2 1 true .31 42 3.5 -32 timeout 900   13000 6700 0 timeout 900   2400 11000 0 timeout 900   1800 14000 0 witness invalid (false(unreach-call)) 380 2400 4300 0
elevator_spec1_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 46    1200 470    0 exception (gremlins) 2.5   63 33    0 false(unreach-call) .56 28 7.7 1 false(unreach-call) .14  9.8 1.1  1 timeout 900   11000 5800 0 false(unreach-call) 11   590 82 0 false(unreach-call) 6.9 340 54 1 false(unreach-call) 500    340 5900   0 false(unreach-call) 18   7300 140 1 false(unreach-call) .21  37 2.8  1 false(unreach-call) .28  37 3.4  1 false(unreach-call) 6.6   87 81    1 false(unreach-call) 7.1 210 91 1 false(unreach-call) .40 21   5.5 1 true .32 42 3.8 -32 timeout 900   13000 5300 0 timeout 900   3800 12000 0 timeout 900   1800 15000 0 witness invalid (false(unreach-call)) 390 3400 4100 0
elevator_spec1_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 110    3600 1000    0 timeout 900     1000 10000    0 false(unreach-call) 76    1200 580   1 unknown .17  18   1.5  0 timeout 900   11000 5900 0 false(unreach-call) 100   4700 670 1 false(unreach-call) 7.2 360 59 1 false(unreach-call) 700    760 7700   0 timeout 900   1200 10000 0 false(unreach-call) 310     420 4400    0 false(unreach-call) 410     710 5500    0 false(unreach-call) 500     890 6300    0 false(unreach-call) 12   280 140 1 false(unreach-call) .44 25   4.7 1 true 12    220 150   -32 timeout 900   14000 6100 0 timeout 900   1900 11000 0 timeout 900   3100 11000 0 unknown 640 850 4800 0
elevator_spec2_product18_false-unreach-call_true-termination.cil.c false(unreach-call) 32    800 300    0 timeout 900     350 12000    0 false(unreach-call) .55 27 5.5 1 false(unreach-call) .15  18   1.3  1 timeout 910   11000 5300 0 false(unreach-call) 10   570 78 0 false(unreach-call) 6.4 290 52 1 false(unreach-call) 490    180 6100   0 false(unreach-call) 18   7300 140 1 false(unreach-call) .21  36 2.9  1 false(unreach-call) .23  36 2.7  1 false(unreach-call) 2.4   64 33    1 false(unreach-call) 6.2 200 76 1 false(unreach-call) .37 19   4.2 1 true .26 42 3.4 -32 timeout 900   13000 6100 0 timeout 900   3200 14000 0 timeout 900   4700 12000 0 witness invalid (false(unreach-call)) 380 2400 4100 0
elevator_spec2_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 33    860 320    0 timeout 900     450 10000    0 false(unreach-call) .54 27 6.8 1 false(unreach-call) .11  9.6 1.3  1 timeout 900   11000 5300 0 false(unreach-call) 12   680 77 0 false(unreach-call) 6.5 320 51 1 false(unreach-call) 490    200 6000   0 false(unreach-call) 18   7300 150 1 false(unreach-call) .22  37 2.5  1 false(unreach-call) .24  37 2.7  1 false(unreach-call) 2.7   65 30    1 false(unreach-call) 6.2 190 77 1 false(unreach-call) .40 20   4.4 1 true .30 43 3.0 -32 timeout 910   13000 5500 0 timeout 900   2600 14000 0 timeout 900   4800 14000 0 witness invalid (false(unreach-call)) 380 2800 4800 0
elevator_spec2_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 39    1100 380    0 exception (gremlins) 2.2   58 27    0 false(unreach-call) .58 27 5.3 1 false(unreach-call) .11  9.5 1.3  1 timeout 900   11000 4900 0 false(unreach-call) 11   520 77 0 false(unreach-call) 6.7 310 50 1 false(unreach-call) 500    240 5500   0 false(unreach-call) 19   7300 120 1 false(unreach-call) .20  37 2.8  1 false(unreach-call) .27  37 2.7  1 false(unreach-call) 5.7   82 80    1 false(unreach-call) 7.3 220 93 1 false(unreach-call) .39 19   4.3 1 true .29 42 3.0 -32 timeout 910   13000 5800 0 timeout 900   3100 13000 0 timeout 900   3700 12000 0 witness invalid (false(unreach-call)) 380 2400 5000 0
elevator_spec2_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 35    1200 380    0 exception (gremlins) 2.2   54 27    0 false(unreach-call) .57 28 7.4 1 false(unreach-call) .12  9.7 1.3  1 timeout 900   11000 5000 0 false(unreach-call) 11   560 80 0 false(unreach-call) 7.4 330 56 1 false(unreach-call) 500    330 6000   0 false(unreach-call) 18   7300 120 1 false(unreach-call) .25  37 2.3  1 false(unreach-call) .26  37 2.9  1 false(unreach-call) 6.2   84 75    1 false(unreach-call) 8.5 240 95 1 false(unreach-call) .40 20   4.3 1 true .30 43 3.0 -32 timeout 900   14000 5700 0 timeout 900   2400 11000 0 timeout 900   5200 10000 0 witness invalid (false(unreach-call)) 380 2800 4100 0
elevator_spec2_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 35    840 300    0 false(unreach-call) 880     760 10000    0 false(unreach-call) .53 27 6.5 1 false(unreach-call) .13  9.4 1.2  1 timeout 900   11000 5800 0 false(unreach-call) 11   550 84 0 false(unreach-call) 6.6 300 51 1 false(unreach-call) 490    200 6500   0 false(unreach-call) 19   7300 120 1 false(unreach-call) .19  36 2.5  1 false(unreach-call) .24  36 3.3  1 false(unreach-call) 2.7   68 35    1 false(unreach-call) 6.5 190 77 1 false(unreach-call) .40 28   4.7 1 true .28 42 3.0 -32 timeout 910   14000 7100 0 timeout 900   3400 13000 0 timeout 900   4300 12000 0 witness invalid (false(unreach-call)) 380 2700 4800 0
elevator_spec2_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 35    900 310    0 timeout 900     570 9500    0 false(unreach-call) .62 27 5.2 1 false(unreach-call) .11  9.5 1.4  1 timeout 900   11000 5800 0 false(unreach-call) 12   680 93 0 false(unreach-call) 7.2 310 53 1 false(unreach-call) 490    220 6000   0 false(unreach-call) 19   7300 130 1 false(unreach-call) .23  37 2.4  1 false(unreach-call) .27  37 3.2  1 false(unreach-call) 3.0   70 45    1 false(unreach-call) 6.7 210 92 1 false(unreach-call) .37 20   4.5 1 true .26 43 3.4 -32 timeout 900   12000 6600 0 timeout 900   4300 13000 0 timeout 900   4100 11000 0 witness invalid (false(unreach-call)) 380 2400 4500 0
elevator_spec2_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 44    1200 390    0 exception (gremlins) 2.5   67 27    0 false(unreach-call) .58 27 6.1 1 false(unreach-call) .12  9.5 1.2  1 timeout 910   11000 5200 0 false(unreach-call) 11   590 90 0 false(unreach-call) 6.6 310 51 1 false(unreach-call) 500    320 6000   0 false(unreach-call) 18   7300 140 1 false(unreach-call) .21  37 2.3  1 false(unreach-call) .26  37 2.6  1 false(unreach-call) 6.1   85 75    1 false(unreach-call) 6.6 210 88 1 false(unreach-call) .37 20   4.8 1 true .29 42 2.8 -32 timeout 910   13000 5600 0 timeout 900   2400 12000 0 timeout 900   4800 11000 0 witness invalid (false(unreach-call)) 380 2100 4500 0
elevator_spec2_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 46    1300 370    0 exception (gremlins) 2.5   61 30    0 false(unreach-call) .66 28 5.4 1 false(unreach-call) .12  9.5 1.4  1 timeout 900   11000 5200 0 false(unreach-call) 11   610 84 0 false(unreach-call) 7.2 330 52 1 false(unreach-call) 500    340 6500   0 false(unreach-call) 19   7300 130 1 false(unreach-call) .23  37 3.1  1 false(unreach-call) .28  37 2.9  1 false(unreach-call) 6.8   88 88    1 false(unreach-call) 6.8 210 90 1 false(unreach-call) .40 21   4.4 1 true .31 43 3.1 -32 timeout 900   13000 5300 0 timeout 900   2400 14000 0 timeout 900   3900 12000 0 witness invalid (false(unreach-call)) 380 3200 4400 0
elevator_spec2_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 100    3600 840    0 timeout 900     740 11000    0 false(unreach-call) 40    910 420   1 unknown .14  9.9 1.2  0 timeout 910   11000 5300 0 false(unreach-call) 92   4600 630 1 false(unreach-call) 7.2 350 53 1 false(unreach-call) 700    730 9400   0 timeout 900   1200 12000 0 false(unreach-call) 310     430 3700    0 false(unreach-call) 420     710 6000    0 false(unreach-call) 500     900 7100    0 false(unreach-call) 14   290 160 1 false(unreach-call) .42 25   5.3 1 true 9.5  190 140   -32 timeout 910   13000 5700 0 timeout 900   3700 13000 0 timeout 900   5700 11000 0 witness invalid (false(unreach-call)) 670 1700 6300 0
elevator_spec3_product03_false-unreach-call_true-termination.cil.c false(unreach-call) 3.0  550 26    1 false(unreach-call) .48  47 5.7  1 false(unreach-call) .28 28 3.0 1 false(unreach-call) .11  9.3 1.2  1 timeout 910   10000 6200 0 false(unreach-call) 11   610 90 0 false(unreach-call) 7.1 390 62 1 false(unreach-call) 480    250 6700   0 false(unreach-call) 18   7300 140 1 false(unreach-call) .18  36 2.0  1 false(unreach-call) .18  36 2.0  1 false(unreach-call) .23  36 2.2  1 false(unreach-call) 10   290 100 1 false(unreach-call) .36 20   4.5 1 true .56 72 7.4 -32 timeout 910   14000 4900 0 timeout 900   2200 11000 0 timeout 900   3100 11000 0 false(unreach-call) 120 870 1100 1
elevator_spec3_product11_false-unreach-call_true-termination.cil.c false(unreach-call) 3.2  590 29    1 false(unreach-call) .43  50 5.7  1 false(unreach-call) .31 28 2.8 1 false(unreach-call) .11  9.4 1.0  1 timeout 910   11000 8000 0 false(unreach-call) 11   590 86 0 false(unreach-call) 7.1 400 56 1 false(unreach-call) 480    270 5700   0 false(unreach-call) 17   7300 150 1 false(unreach-call) .19  36 2.6  1 false(unreach-call) .21  36 2.0  1 false(unreach-call) .22  36 2.3  1 false(unreach-call) 11   260 120 1 false(unreach-call) .40 21   4.1 1 true .56 73 6.3 -32 timeout 910   13000 5300 0 timeout 900   2300 10000 0 timeout 900   3100 12000 0 false(unreach-call) 130 1100 1200 1
elevator_spec3_product19_false-unreach-call_true-termination.cil.c false(unreach-call) 3.3  630 30    1 false(unreach-call) .48  50 5.8  1 false(unreach-call) .28 28 2.4 1 false(unreach-call) .15  9.4 1.2  1 timeout 900   11000 6900 0 false(unreach-call) 12   610 86 0 false(unreach-call) 7.1 390 63 1 false(unreach-call) 480    420 6100   0 false(unreach-call) 17   7300 170 1 false(unreach-call) .22  36 1.9  1 false(unreach-call) .18  36 2.6  1 false(unreach-call) .23  37 1.9  1 false(unreach-call) 8.7 240 110 1 false(unreach-call) .37 21   4.2 1 true .56 74 6.9 -32 timeout 910   13000 6200 0 timeout 900   3800 9700 0 timeout 900   3200 13000 0 false(unreach-call) 130 1200 1000 1
elevator_spec3_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 6.0  1200 73    1 false(unreach-call) .49  50 6.9  1 false(unreach-call) .31 28 2.6 1 false(unreach-call) .15  16   1.2  1 timeout 910   11000 6000 0 false(unreach-call) 11   590 85 0 false(unreach-call) 7.2 420 63 1 false(unreach-call) 480    390 4500   0 false(unreach-call) 19   7300 140 1 false(unreach-call) .21  37 2.3  1 false(unreach-call) .18  37 2.4  1 false(unreach-call) .79  37 1.9  1 false(unreach-call) 11   260 130 1 false(unreach-call) .41 22   5.1 1 true .63 77 6.6 -32 timeout 900   13000 5900 0 timeout 900   2200 9900 0 timeout 900   3300 12000 0 false(unreach-call) 270 1200 2800 1
elevator_spec3_product23_false-unreach-call_true-termination.cil.c false(unreach-call) 5.2  1000 49    1 exception (gremlins) .82  38 9.1  0 false(unreach-call) .27 29 3.3 1 false(unreach-call) .11  9.6 1.4  1 timeout 910   11000 6900 0 false(unreach-call) 12   580 84 0 false(unreach-call) 7.3 420 59 1 false(unreach-call) 480    320 5500   0 false(unreach-call) 18   7300 150 1 false(unreach-call) .19  37 2.0  1 false(unreach-call) .22  37 2.0  1 false(unreach-call) .20  37 2.4  1 false(unreach-call) 10   270 120 1 false(unreach-call) .39 22   4.4 1 true .64 80 7.0 -32 timeout 910   13000 5500 0 timeout 900   2300 11000 0 timeout 900   3400 13000 0 false(unreach-call) 180 1300 1900 1
elevator_spec3_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 11    1900 91    1 exception (gremlins) .81  37 10    0 false(unreach-call) .27 29 2.9 1 false(unreach-call) .14  16   1.3  1 timeout 910   11000 6100 0 false(unreach-call) 12   650 87 0 false(unreach-call) 7.7 420 57 1 false(unreach-call) 480    540 4900   0 false(unreach-call) 18   7300 160 1 false(unreach-call) .19  37 2.5  1 false(unreach-call) .21  37 1.9  1 false(unreach-call) .23  37 2.4  1 false(unreach-call) 13   270 140 1 false(unreach-call) .42 23   6.2 1 true .72 88 7.8 -32 timeout 910   13000 6800 0 timeout 900   2100 11000 0 timeout 900   3300 14000 0 witness invalid (false(unreach-call)) 370 1100 4200 0
elevator_spec3_product27_false-unreach-call_true-termination.cil.c false(unreach-call) 3.4  670 30    1 false(unreach-call) .47  47 5.5  1 false(unreach-call) .28 28 2.7 1 false(unreach-call) .17  19   1.2  1 timeout 910   11000 6700 0 false(unreach-call) 11   600 83 0 false(unreach-call) 7.3 400 59 1 false(unreach-call) 480    430 6000   0 false(unreach-call) 18   7300 150 1 false(unreach-call) .19  37 1.8  1 false(unreach-call) .18  37 1.9  1 false(unreach-call) .19  37 2.6  1 false(unreach-call) 6.9 210 87 1 false(unreach-call) .37 22   4.5 1 true .55 74 6.3 -32 timeout 900   14000 5900 0 timeout 900   2200 13000 0 timeout 900   3700 12000 0 false(unreach-call) 150 1200 1600 1
elevator_spec3_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 6.5  1300 68    1 false(unreach-call) .49  50 6.5  1 false(unreach-call) .27 29 2.9 1 false(unreach-call) .15  19   1.3  1 timeout 900   11000 6400 0 false(unreach-call) 11   590 82 0 false(unreach-call) 7.1 410 59 1 false(unreach-call) 480    420 5600   0 false(unreach-call) 17   7300 150 1 false(unreach-call) .19  37 2.1  1 false(unreach-call) .20  37 2.2  1 false(unreach-call) .22  37 2.8  1 false(unreach-call) 12   260 130 1 false(unreach-call) .48 31   4.6 1 true .59 77 7.5 -32 timeout 910   13000 6300 0 timeout 900   2100 11000 0 timeout 900   2900 12000 0 false(unreach-call) 360 1100 3700 1
elevator_spec3_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 5.6  1000 57    1 exception (gremlins) .79  38 9.4  0 false(unreach-call) .28 29 3.1 1 false(unreach-call) .13  9.5 1.3  1 timeout 900   11000 7200 0 false(unreach-call) 12   570 84 0 false(unreach-call) 7.5 420 63 1 false(unreach-call) 480    330 5500   0 false(unreach-call) 18   7300 130 1 false(unreach-call) .23  37 2.0  1 false(unreach-call) .21  37 2.0  1 false(unreach-call) .20  37 3.1  1 false(unreach-call) 12   270 130 1 false(unreach-call) .41 23   4.8 1 true .65 80 8.1 -32 timeout 900   13000 5200 0 timeout 900   2300 11000 0 timeout 900   3300 11000 0 false(unreach-call) 210 1100 2200 1
elevator_spec3_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 11    2000 88    1 exception (gremlins) .80  37 9.7  0 false(unreach-call) .30 29 2.7 1 false(unreach-call) .14  16   1.4  1 timeout 910   11000 5900 0 false(unreach-call) 11   580 89 0 false(unreach-call) 7.5 420 63 1 false(unreach-call) 480    560 5500   0 false(unreach-call) 19   7300 130 1 false(unreach-call) .20  37 2.6  1 false(unreach-call) .20  37 2.3  1 false(unreach-call) .25  37 2.3  1 false(unreach-call) 15   290 160 1 false(unreach-call) .39 24   4.4 1 true .70 88 8.8 -32 timeout 900   13000 6100 0 timeout 900   2500 11000 0 timeout 900   3600 13000 0 witness invalid (false(unreach-call)) 370 1200 5000 0
elevator_spec3_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 38    6700 420    1 exception (gremlins) 340     410 4300    0 false(unreach-call) 37    920 360   1 unknown .13  17   1.8  0 timeout 910   11000 5700 0 timeout 960   8700 6000 0 false(unreach-call) 9.8 460 74 1 false(unreach-call) 620    1400 4200   0 timeout 900   1500 11000 0 false(unreach-call) 390     400 5300    0 false(unreach-call) 390     400 4800    0 false(unreach-call) 390     400 6000    0 false(unreach-call) 37   330 320 1 false(unreach-call) .43 28   4.8 1 true 28    590 340   -32 timeout 910   13000 5900 0 timeout 900   2600 11000 0 timeout 900   4000 11000 0 unknown 650 910 5500 0
elevator_spec9_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 34    840 320    0 timeout 900     570 9100    0 false(unreach-call) .56 27 5.0 1 false(unreach-call) .11  9.4 1.2  1 timeout 910   11000 5700 0 false(unreach-call) 11   570 79 0 false(unreach-call) 6.6 310 52 1 false(unreach-call) 490    190 6500   0 false(unreach-call) 17   7300 150 1 false(unreach-call) .20  36 2.6  1 false(unreach-call) .90  36 2.0  1 false(unreach-call) 2.7   67 33    1 false(unreach-call) 6.9 210 93 1 false(unreach-call) .39 20   4.5 1 true .27 42 3.4 -32 timeout 910   14000 5600 0 timeout 900   2900 13000 0 timeout 910   14000 4600 0 witness invalid (false(unreach-call)) 610 2700 5900 0
elevator_spec9_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 35    900 350    0 timeout 900     460 11000    0 false(unreach-call) .58 27 5.5 1 false(unreach-call) .14  9.4 1.3  1 timeout 910   11000 4900 0 false(unreach-call) 10   590 87 0 false(unreach-call) 6.8 330 55 1 false(unreach-call) 490    220 5400   0 false(unreach-call) 18   7300 140 1 false(unreach-call) .24  37 2.4  1 false(unreach-call) .26  37 2.9  1 false(unreach-call) 3.0   70 36    1 false(unreach-call) 6.8 220 85 1 false(unreach-call) .40 21   4.5 1 true .28 43 2.7 -32 timeout 910   14000 5400 0 timeout 900   2700 13000 0 timeout 900   14000 4900 0 witness invalid (false(unreach-call)) 610 2900 5800 0
elevator_spec9_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 42    1200 390    0 exception (gremlins) 50     170 540    0 false(unreach-call) .60 27 6.2 1 false(unreach-call) .12  9.4 1.1  1 timeout 910   11000 5400 0 false(unreach-call) 11   590 85 0 false(unreach-call) 6.6 320 53 1 false(unreach-call) 500    320 5800   0 false(unreach-call) 17   7300 140 1 false(unreach-call) .21  37 2.4  1 false(unreach-call) .27  37 2.5  1 false(unreach-call) 6.2   86 78    1 false(unreach-call) 8.0 220 92 1 false(unreach-call) .40 21   4.6 1 true .27 42 3.9 -32 timeout 900   14000 4800 0 timeout 900   2800 11000 0 timeout 900   14000 4700 0 witness invalid (false(unreach-call)) 620 2600 6000 0
elevator_spec9_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 46    1300 470    0 exception (gremlins) 71     190 840    0 false(unreach-call) .57 28 6.4 1 false(unreach-call) .11  9.5 1.4  1 timeout 900   11000 5800 0 false(unreach-call) 11   580 83 0 false(unreach-call) 6.8 330 54 1 false(unreach-call) 500    340 5100   0 false(unreach-call) 18   7300 130 1 false(unreach-call) .21  37 3.0  1 false(unreach-call) .26  37 3.4  1 false(unreach-call) 6.8   88 87    1 false(unreach-call) 7.4 220 89 1 false(unreach-call) .40 21   4.4 1 true .30 43 4.0 -32 timeout 900   14000 4900 0 timeout 900   3200 13000 0 timeout 910   14000 4900 0 witness invalid (false(unreach-call)) 610 2900 5700 0
elevator_spec9_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 87    3600 1100    0 timeout 900     1300 10000    0 false(unreach-call) 40    910 340   1 unknown .12  10   1.2  0 timeout 900   11000 4600 0 false(unreach-call) 86   4400 540 1 false(unreach-call) 7.2 360 53 1 false(unreach-call) 700    720 7300   0 timeout 900   1200 11000 0 false(unreach-call) 310     420 3900    0 false(unreach-call) 410     700 5600    0 false(unreach-call) 500     890 6200    0 false(unreach-call) 14   290 180 1 false(unreach-call) .45 25   5.5 1 true 10    190 130   -32 timeout 910   14000 4800 0 timeout 900   3400 12000 0 timeout 900   5100 13000 0 witness invalid (false(unreach-call)) 890 1700 7500 0
elevator_spec13_product21_true-unreach-call_false-termination.cil.c error (134) 4.6  960 43    0 exception (gremlins) 1.4   48 15    0 error (42) 850    13000 9800   0 true 120     9.3 1300    1 timeout 910   11000 5000 0 true 7.6 430 60 1 true 4.2 280 35 1 unknown 890    1500 11000   0 true 150   7900 1700 1 timeout 900     670 10000    0 timeout 900     3100 11000    0 timeout 900     680 10000    0 true 870   850 6600 1 timeout (timeout) 880    15000   11000   0 true .90 160 10   1 timeout 900   13000 5800 0 timeout 900   3400 11000 0 timeout 900   1700 11000 0 unknown 430 1100 3900 0
elevator_spec13_product22_true-unreach-call_false-termination.cil.c error (134) 8.9  1800 84    0 exception (gremlins) 1.3   45 17    0 error (42) 850    13000 11000   0 true 120     16   1600    1 timeout 910   11000 5700 0 true 7.8 490 60 1 true 4.5 280 35 1 unknown 890    2100 11000   0 true 260   7900 3300 1 timeout 900     670 11000    0 timeout 900     3200 13000    0 timeout 900     900 11000    0 true 890   820 5800 1 timeout (timeout) 900    15000   12000   0 true .96 160 11   1 timeout 900   14000 5300 0 timeout 900   2300 13000 0 timeout 900   2000 12000 0 unknown 430 1100 4200 0
elevator_spec13_product23_true-unreach-call_false-termination.cil.c error (134) 4.9  1100 54    0 exception (gremlins) 1.4   45 14    0 out of memory 610    15000 7700   0 true 120     9.5 1800    1 timeout 900   11000 6300 0 true 7.8 440 61 1 true 4.4 280 36 1 unknown 890    660 12000   0 true 280   7900 3400 1 timeout 900     930 11000    0 timeout 900     5000 12000    0 timeout 900     700 10000    0 true 780   860 5200 1 timeout (timeout) 890    15000   12000   0 true 1.0  160 14   1 timeout 900   14000 5400 0 timeout 900   1900 14000 0 timeout 900   2700 14000 0 unknown 420 1200 3700 0
elevator_spec13_product24_true-unreach-call_false-termination.cil.c error (134) 10    2000 93    0 exception (gremlins) 1.4   45 16    0 out of memory 610    15000 8800   0 true 120     9.2 1300    1 timeout 910   11000 5900 0 true 7.8 680 59 1 true 4.5 280 36 1 unknown 890    2400 13000   0 true 290   7900 3700 1 timeout 900     880 11000    0 timeout 900     4900 12000    0 timeout 900     550 10000    0 true 890   850 7800 1 timeout (timeout) 890    15000   12000   0 true 1.1  160 13   1 timeout 900   14000 6100 0 timeout 900   2400 11000 0 timeout 900   1800 11000 0 unknown 430 1100 3000 0
elevator_spec13_product29_true-unreach-call_false-termination.cil.c error (134) 4.8  1000 45    0 exception (gremlins) 1.6   50 19    0 error (42) 850    13000 11000   0 true 120     16   1600    1 timeout 900   11000 5300 0 true 7.9 440 66 1 true 4.2 280 34 1 unknown 890    1700 11000   0 true 250   7900 3300 1 timeout 900     320 4400    0 timeout 900     3100 9800    0 timeout 900     690 11000    0 true 880   810 6100 1 timeout (timeout) 890    15000   12000   0 true .96 150 9.6 1 timeout 910   13000 6000 0 timeout 900   2800 9500 0 timeout 900   1700 12000 0 unknown 440 1100 5000 0
elevator_spec13_product30_true-unreach-call_false-termination.cil.c error (134) 9.4  1900 79    0 exception (gremlins) 1.6   49 23    0 error (42) 850    13000 12000   0 true 120     9.4 1200    1 timeout 910   11000 5800 0 true 7.8 430 58 1 true 4.4 280 39 1 unknown 890    770 9000   0 true 280   7900 3300 1 timeout 900     670 11000    0 timeout 900     3100 11000    0 timeout 900     550 12000    0 true 890   810 5900 1 timeout (timeout) 900    15000   12000   0 true .99 160 11   1 timeout 910   13000 5600 0 timeout 900   2500 10000 0 timeout 900   1700 11000 0 unknown 430 1100 4300 0
elevator_spec13_product31_true-unreach-call_false-termination.cil.c error (134) 5.0  1100 55    0 exception (gremlins) 1.6   50 20    0 out of memory 620    15000 8100   0 true 120     9.6 1700    1 timeout 900   11000 5800 0 true 8.2 440 68 1 true 4.4 270 35 1 unknown 890    670 12000   0 true 310   7900 3400 1 timeout 900     880 11000    0 timeout 900     4800 10000    0 timeout 900     720 14000    0 true 890   870 6900 1 - 0 true 1.0  160 15   1 timeout 910   13000 5100 0 timeout 900   4100 14000 0 timeout 900   2800 13000 0 unknown 420 1200 3200 0
elevator_spec13_product32_true-unreach-call_false-termination.cil.c error (134) 9.7  2100 110    0 exception (gremlins) 1.6   47 23    0 out of memory 630    15000 7800   0 true 120     17   1300    1 timeout 910   11000 5700 0 true 8.6 440 64 1 true 4.4 280 35 1 unknown 890    750 10000   0 true 270   7900 3000 1 timeout 900     900 13000    0 timeout 900     4800 11000    0 timeout 900     580 12000    0 true 890   840 6000 1 - 0 true 1.1  160 16   1 timeout 910   14000 6600 0 timeout 900   2500 11000 0 timeout 900   1900 11000 0 unknown 420 1100 2900 0
elevator_spec13_productSimulator_true-unreach-call_true-termination.cil.c error (134) 41    7000 400    0 exception (gremlins) 2.0   76 24    0 error (42) 850    450 7400   0 unknown .12  9.8 1.2  0 timeout 910   11000 6100 0 true 10   660 75 1 true 5.7 290 50 1 unknown 890    1500 9100   0 out of memory 75   15000 930 0 timeout 900     670 11000    0 timeout 900     840 11000    0 timeout 900     840 11000    0 true 890   780 6700 1 timeout (timeout) 890    15000   12000   0 true 17    610 220   1 timeout 900   13000 6300 0 timeout 900   2700 12000 0 timeout 900   3000 13000 0 timeout 900 1000 11000 0
elevator_spec14_product03_true-unreach-call_true-termination.cil.c true 18    780 200    2 timeout 900     740 9600    0 true 1.5  31 18   1 true .14  9.2 1.3  2 true 110   4400 830 2 true 8.9 470 68 2 true 4.9 290 39 2 true 540    290 6700   2 true 18   7300 150 2 timeout 900     2300 11000    0 true 1.1   47 13    2 true 33     330 450    2 true 92   620 790 2 true .37 17   3.8 2 true .76 87 7.6 2 timeout 910   13000 7900 0 timeout 900   3200 11000 0 timeout 900   2500 13000 0 true 36 1100 300 2
elevator_spec14_product11_true-unreach-call_true-termination.cil.c true 18    830 210    2 timeout 900     750 10000    0 true 1.5  31 16   1 true .12  13   1.1  2 true 110   4500 780 2 true 8.0 430 61 2 true 4.7 290 39 2 true 550    290 6500   2 true 18   7300 160 2 timeout 900     2200 14000    0 true 1.2   47 14    2 true 37     370 460    2 true 81   550 600 2 true .35 18   4.6 2 true .82 150 10   2 timeout 910   13000 6200 0 timeout 900   2700 11000 0 timeout 900   2800 11000 0 true 35 1100 270 2
elevator_spec14_product19_true-unreach-call_true-termination.cil.c true 19    940 200    2 timeout 900     590 9500    0 true 1.6  31 16   1 true .11  9.3 1.1  2 true 110   4500 760 2 true 9.2 440 74 2 true 4.8 290 42 2 true 550    300 6600   2 true 19   7300 130 2 timeout 900     2200 13000    0 true 1.2   48 17    2 true 36     350 480    2 true 86   570 760 2 true .35 18   4.6 2 true .84 150 9.6 2 timeout 910   13000 8100 0 timeout 900   3100 10000 0 timeout 900   2500 11000 0 true 34 1100 300 2
elevator_spec14_product23_true-unreach-call_true-termination.cil.c true 19    1300 160    2 exception (gremlins) 1.2   38 14    0 true 1.6  31 16   1 true .14  9.5 1.1  2 true 160   5700 940 2 true 8.4 430 66 2 true 5.0 290 43 2 true 660    350 7400   2 true 19   7300 140 2 timeout 900     2300 12000    0 true 1.7   59 21    2 true 240     970 2900    2 true 95   620 910 2 true .36 19   5.0 2 true .95 160 11   2 timeout 900   13000 7900 0 timeout 900   1600 11000 0 timeout 900   2900 12000 0 true 41 1300 320 2
elevator_spec14_product27_true-unreach-call_true-termination.cil.c true 22    940 310    2 timeout 900     660 9900    0 true 1.6  32 15   1 true .12  16   1.6  2 true 96   4700 820 2 true 8.7 440 59 2 true 4.8 280 35 2 true 550    290 6300   2 true 19   7300 160 2 timeout 900     2200 13000    0 true 1.2   48 17    2 true 41     380 520    2 true 100   560 730 2 true .38 19   5.1 2 true .87 150 10   2 timeout 900   13000 6400 0 timeout 900   3000 11000 0 timeout 900   2600 11000 0 true 37 1100 300 2
elevator_spec14_product31_true-unreach-call_true-termination.cil.c true 10    1200 98    2 exception (gremlins) 1.2   40 15    0 true 1.6  32 18   1 true .11  9.2 1.2  2 true 140   5700 850 2 true 9.0 450 63 2 true 5.2 290 42 2 true 660    330 8600   2 true 19   7300 130 2 timeout 900     2300 14000    0 true 1.7   59 22    2 true 260     1100 3200    2 true 97   630 800 2 true .36 20   4.7 2 true 1.0  160 13   2 timeout 900   13000 6900 0 timeout 900   1800 12000 0 timeout 900   3100 13000 0 true 42 1300 360 2
elevator_spec1_product01_true-unreach-call_true-termination.cil.c true 67    1000 660    2 timeout 900     420 8300    0 true 1.3  32 15   1 true .14  9.3 1.1  2 timeout 900   11000 5100 0 true 8.2 470 68 2 true 4.8 280 37 2 true 520    280 6100   2 true 18   7300 150 2 timeout 900     2000 11000    0 true .88  42 12    2 true 31     310 380    2 true 41   430 400 2 true .36 17   3.8 2 true .26 40 5.4 2 timeout 910   13000 5500 0 timeout 900   2600 12000 0 timeout 900   2000 14000 0 true 48 540 340 2
elevator_spec1_product03_true-unreach-call_true-termination.cil.c true 72    1100 680    2 timeout 900     1200 9900    0 true 1.4  30 19   1 true .13  9.5 1.1  2 timeout 900   11000 5000 0 true 8.1 450 69 2 true 4.8 290 38 2 true 540    290 5600   2 true 18   7300 170 2 timeout 900     2000 14000    0 true 1.0   45 11    2 true 36     340 530    2 true 65   550 650 2 true .35 18   4.1 2 true .26 41 3.3 2 timeout 900   12000 6200 0 timeout 900   2200 13000 0 timeout 900   2000 11000 0 true 49 590 380 2
elevator_spec1_product09_true-unreach-call_true-termination.cil.c true 86    1100 960    2 timeout 900     560 9200    0 true 1.4  29 12   1 true .12  9.4 1.1  2 timeout 900   11000 4800 0 true 8.5 440 67 2 true 4.8 280 35 2 true 540    290 7000   2 true 18   7300 140 2 timeout 900     1900 11000    0 true .87  43 11    2 true 36     350 430    2 true 40   460 510 2 true .35 18   3.9 2 true .26 41 3.1 2 timeout 900   13000 6800 0 timeout 900   2300 12000 0 timeout 900   1700 11000 0 true 51 550 430 2
elevator_spec1_product11_true-unreach-call_true-termination.cil.c true 82    1100 750    2 timeout 900     1200 9700    0 true 1.5  30 14   1 true .16  29   2.0  2 timeout 900   11000 4600 0 true 9.0 440 77 2 true 4.9 290 40 2 true 550    300 6900   2 true 19   7300 160 2 timeout 900     2000 11000    0 true 1.0   45 12    2 true 41     380 480    2 true 61   530 520 2 true .36 19   4.6 2 true .27 40 3.2 2 timeout 900   11000 7300 0 timeout 900   2000 11000 0 timeout 900   1600 13000 0 true 50 520 370 2
elevator_spec1_product17_true-unreach-call_true-termination.cil.c true 80    1100 780    2 timeout 900     570 8900    0 true 1.4  29 14   1 true .11  9.3 1.1  2 timeout 900   11000 4700 0 true 8.3 440 66 2 true 5.0 290 42 2 true 530    290 6600   2 true 19   7300 120 2 timeout 900     1900 12000    0 true .91  43 12    2 true 34     320 440    2 true 36   470 380 2 true .37 18   3.9 2 true .28 41 3.0 2 timeout 900   13000 7000 0 timeout 900   2100 11000 0 timeout 900   1700 14000 0 true 50 600 410 2
elevator_spec1_product19_true-unreach-call_true-termination.cil.c true 86    1200 780    2 timeout 900     560 9000    0 true 1.5  30 18   1 true .12  9.2 1.1  2 timeout 910   11000 4900 0 true 8.3 440 73 2 true 5.1 300 39 2 true 550    300 7200   2 true 18   7300 170 2 timeout 900     1900 14000    0 true 1.0   46 13    2 true 39     350 500    2 true 48   500 430 2 true .36 19   4.1 2 true .29 41 3.7 2 timeout 900   11000 6400 0 timeout 900   2300 12000 0 timeout 900   1800 15000 0 true 51 570 350 2
elevator_spec1_product21_true-unreach-call_true-termination.cil.c true 110    1500 970    2 exception (gremlins) 2.9   86 43    0 true 1.4  30 13   1 true .11  9.4 1.3  2 timeout 910   11000 4800 0 true 8.2 450 60 2 true 4.7 270 39 2 true 570    300 6600   2 true 19   7300 150 2 timeout 900     1900 12000    0 true 1.0   45 12    2 true 92     490 1100    2 true 81   520 650 2 true .37 19   4.2 2 true .27 41 3.6 2 timeout 910   13000 6600 0 timeout 900   3500 14000 0 timeout 900   2100 12000 0 true 51 520 390 2
elevator_spec1_product23_true-unreach-call_true-termination.cil.c true 110    1600 1300    2 exception (gremlins) 20     180 220    0 true 1.6  31 16   1 true .14  9.6 1.2  2 timeout 900   11000 5400 0 true 8.6 430 65 2 true 5.1 290 37 2 true 580    290 7600   2 true 18   7300 150 2 timeout 900     1900 11000    0 true 1.1   48 13    2 true 100     530 1600    2 true 140   590 1100 2 true .37 19   4.1 2 true .30 41 3.8 2 timeout 900   13000 5400 0 timeout 900   3200 11000 0 timeout 900   2100 12000 0 true 52 590 380 2
elevator_spec1_product25_true-unreach-call_true-termination.cil.c true 90    1100 810    2 timeout 900     450 11000    0 true 1.3  30 15   1 true .14  9.2 1.1  2 timeout 900   11000 5200 0 true 8.0 450 60 2 true 4.6 280 39 2 true 550    300 7700   2 true 18   7300 140 2 timeout 900     1900 13000    0 true .94  43 12    2 true 39     360 530    2 true 51   510 520 2 true .36 19   4.2 2 true .28 41 2.9 2 timeout 900   13000 6100 0 timeout 900   1900 13000 0 timeout 900   2000 13000 0 true 50 580 330 2
elevator_spec1_product27_true-unreach-call_true-termination.cil.c true 85    1200 860    2 timeout 900     740 8900    0 true 1.5  30 15   1 true .11  9.5 1.2  2 timeout 900   11000 5300 0 true 8.0 430 57 2 true 4.8 280 40 2 true 550    290 6000   2 true 18   7300 140 2 timeout 900     1900 13000    0 true 1.1   46 13    2 true 43     390 560    2 true 61   520 500 2 true .38 19   5.2 2 true .28 41 4.0 2 timeout 900   12000 7200 0 timeout 900   2200 12000 0 timeout 900   2000 14000 0 true 49 580 380 2
elevator_spec1_product29_true-unreach-call_true-termination.cil.c true 100    1500 990    2 exception (gremlins) 3.0   88 40    0 true 1.4  30 15   1 true .12  9.7 1.1  2 timeout 900   11000 4700 0 true 8.3 430 67 2 true 4.8 290 37 2 true 580    310 7000   2 true 18   7300 150 2 timeout 900     1900 12000    0 true 1.0   46 13    2 true 100     520 1400    2 true 95   520 850 2 true .36 20   4.3 2 true .27 41 3.2 2 timeout 910   13000 5800 0 timeout 900   2200 11000 0 timeout 900   2200 12000 0 true 50 590 330 2
elevator_spec1_product31_true-unreach-call_true-termination.cil.c true 100    1600 920    2 exception (gremlins) 21     180 240    0 true 1.5  32 19   1 true .12  9.5 1.2  2 timeout 900   11000 4900 0 true 8.6 440 65 2 true 4.8 290 42 2 true 590    300 6800   2 true 19   7300 140 2 timeout 900     1900 9900    0 true 1.1   48 14    2 true 110     560 1500    2 true 94   550 790 2 true .37 20   4.4 2 true .28 41 3.5 2 timeout 900   13000 6800 0 timeout 900   2200 12000 0 timeout 900   2000 13000 0 true 51 570 370 2
elevator_spec2_product01_true-unreach-call_true-termination.cil.c true 59    770 570    2 timeout 900     450 9700    0 true .83 27 7.3 1 true .12  9.3 .94 2 timeout 900   11000 5600 0 true 8.2 430 66 2 true 4.5 280 33 2 true 440    280 5200   2 true 20   7300 140 2 timeout 900     1900 12000    0 true .42  36 4.9  2 true 5.4   100 63    2 true 19   380 190 2 true .37 18   4.3 2 true .23 24 2.3 2 timeout 910   13000 5100 0 timeout 900   2000 13000 0 timeout 910   13000 4900 0 true 49 560 330 2
elevator_spec2_product03_true-unreach-call_true-termination.cil.c true 59    810 640    2 timeout 900     560 9000    0 true .86 28 8.3 1 true .11  9.3 1.5  2 timeout 900   11000 5200 0 true 7.4 420 62 2 true 4.7 280 46 2 true 500    280 7200   2 true 19   7300 130 2 timeout 900     2000 11000    0 true .44  36 5.0  2 true 6.0   110 92    2 true 22   340 180 2 true .37 18   4.7 2 true .22 25 3.0 2 timeout 910   13000 6400 0 timeout 900   3600 12000 0 timeout 900   5300 11000 0 true 48 520 370 2
elevator_spec2_product09_true-unreach-call_true-termination.cil.c true 66    800 740    2 timeout 900     460 10000    0 true .77 27 8.2 1 true .13  17   1.3  2 timeout 910   11000 5100 0 true 8.0 440 60 2 true 4.5 280 36 2 true 500    280 5500   2 true 19   7300 120 2 timeout 900     1900 10000    0 true .43  36 5.1  2 true 6.1   110 84    2 true 18   340 180 2 true .36 18   4.7 2 true .22 24 2.6 2 timeout 900   13000 4600 0 timeout 900   2200 11000 0 timeout 910   14000 4700 0 true 48 560 340 2
elevator_spec2_product11_true-unreach-call_true-termination.cil.c true 62    840 620    2 timeout 900     640 9600    0 true .76 28 9.1 1 true .15  9.4 1.2  2 timeout 900   11000 5100 0 true 8.1 480 67 2 true 4.5 280 38 2 true 500    290 5800   2 true 17   7300 140 2 timeout 900     1900 11000    0 true .45  36 5.7  2 true 6.8   120 83    2 true 22   350 220 2 true .44 27   4.5 2 true .23 25 2.8 2 timeout 900   12000 6100 0 timeout 900   2900 12000 0 timeout 900   4700 13000 0 true 49 570 390 2
elevator_spec2_product17_true-unreach-call_true-termination.cil.c true 74    840 670    2 timeout 900     450 9600    0 true .74 27 9.8 1 true .14  9.4 1.1  2 timeout 900   11000 4600 0 true 7.4 440 59 2 true 4.4 270 33 2 true 480    280 6000   2 true 19   7300 140 2 timeout 900     1900 11000    0 true .42  36 5.0  2 true 5.8   100 78    2 true 22   360 230 2 true .36 18   5.2 2 true .25 26 2.3 2 timeout 910   13000 4700 0 timeout 900   2400 13000 0 timeout 910   13000 5600 0 true 49 520 390 2
elevator_spec2_product19_true-unreach-call_true-termination.cil.c true 68    870 590    2 timeout 900     570 8400    0 true .85 28 8.3 1 true .22  54   1.5  2 timeout 910   11000 4800 0 true 8.0 490 56 2 true 4.5 280 33 2 true 500    290 6900   2 true 19   7300 150 2 timeout 900     470 2000    0 true .46  36 5.3  2 true 6.4   110 72    2 true 24   370 230 2 true .36 19   4.6 2 true .25 41 2.8 2 timeout 910   13000 6100 0 timeout 900   2700 11000 0 timeout 900   4500 12000 0 true 51 530 390 2
elevator_spec2_product21_true-unreach-call_true-termination.cil.c true 72    1100 870    2 exception (gremlins) 2.9   78 33    0 true .83 28 7.7 1 true .12  16   1.4  2 timeout 900   11000 5600 0 true 8.0 500 67 2 true 4.4 280 40 2 true 510    280 6300   2 true 17   7300 180 2 timeout 900     1900 11000    0 true .46  36 5.0  2 true 59     150 160    2 true 25   350 330 2 true .38 19   4.4 2 true .23 25 3.2 2 timeout 910   14000 4700 0 timeout 900   2300 12000 0 timeout 900   9400 10000 0 true 49 540 380 2
elevator_spec2_product23_true-unreach-call_true-termination.cil.c true 80    1200 890    2 exception (gremlins) 29     270 290    0 true .83 28 11   1 true .13  17   1.4  2 timeout 900   11000 4800 0 true 7.8 430 55 2 true 4.3 280 34 2 true 510    320 6300   2 true 19   7300 130 2 timeout 900     1800 10000    0 true .48  38 6.0  2 true 15     150 180    2 true 20   330 210 2 true .36 20   4.3 2 true .28 41 3.1 2 timeout 910   14000 5700 0 timeout 900   2100 12000 0 timeout 900   4800 13000 0 true 51 530 350 2
elevator_spec2_product25_true-unreach-call_true-termination.cil.c true 74    860 600    2 timeout 900     580 10000    0 true .82 27 7.7 1 true .12  9.4 1.2  2 timeout 910   11000 5700 0 true 8.1 440 63 2 true 4.2 280 34 2 true 500    280 7200   2 true 18   7300 140 2 timeout 900     1800 11000    0 true .43  36 5.1  2 true 6.5   120 74    2 true 19   340 180 2 true .38 19   5.0 2 true .22 25 2.8 2 timeout 910   13000 4400 0 timeout 900   1900 12000 0 timeout 910   13000 5100 0 true 47 560 350 2
elevator_spec2_product27_true-unreach-call_true-termination.cil.c true 72    910 650    2 timeout 900     570 12000    0 true .88 28 8.3 1 true .22  54   1.5  2 timeout 900   11000 5300 0 true 8.3 440 64 2 true 4.4 280 39 2 true 510    290 6100   2 true 19   7300 130 2 timeout 900     1900 11000    0 true .47  37 5.8  2 true 7.2   120 100    2 true 25   340 250 2 true .36 20   4.7 2 true .24 26 2.4 2 timeout 900   13000 6600 0 timeout 900   2600 12000 0 timeout 900   4500 13000 0 true 50 540 370 2
elevator_spec2_product29_true-unreach-call_true-termination.cil.c true 90    1200 780    2 exception (gremlins) 3.0   79 36    0 true .81 28 6.9 1 true .11  9.5 1.5  2 timeout 900   11000 4800 0 true 8.0 430 62 2 true 4.5 280 38 2 true 510    280 6400   2 true 18   7300 130 2 timeout 900     1900 11000    0 true .45  37 5.2  2 true 15     160 190    2 true 19   340 220 2 true .39 20   4.6 2 true .23 26 2.7 2 timeout 910   13000 4200 0 timeout 900   3200 12000 0 timeout 900   12000 9400 0 true 49 510 390 2
elevator_spec2_product31_true-unreach-call_true-termination.cil.c true 90    1200 800    2 exception (gremlins) 29     210 320    0 true .88 28 7.9 1 true .12  9.7 1.1  2 timeout 900   11000 5700 0 true 8.0 430 68 2 true 4.6 280 35 2 true 510    280 6100   2 true 19   7300 130 2 timeout 900     1800 11000    0 true .50  38 6.0  2 true 16     170 190    2 true 30   370 270 2 true .40 20   4.2 2 true .27 41 2.8 2 timeout 910   13000 5200 0 timeout 900   2800 15000 0 timeout 900   4700 14000 0 true 50 590 360 2
elevator_spec3_product01_true-unreach-call_true-termination.cil.c true 3.0  580 26    2 timeout 900     410 11000    0 true 1.6  32 18   1 true .13  18   1.3  2 timeout 910   11000 6500 0 true 8.5 460 69 2 true 5.0 290 48 2 true 490    300 6000   2 true 19   7300 140 2 timeout 900     2100 9900    0 true 1.7   54 25    2 true 1.3   100 18    2 true 69   520 620 2 true .37 20   4.0 2 true .48 72 6.0 2 timeout 910   14000 4900 0 timeout 900   2500 10000 0 timeout 900   2700 12000 0 true 48 580 360 2
elevator_spec3_product09_true-unreach-call_true-termination.cil.c true 3.2  630 30    2 timeout 900     390 9200    0 true 1.6  32 18   1 true .14  9.3 1.0  2 timeout 910   11000 6400 0 true 8.9 460 64 2 true 5.1 290 41 2 true 490    330 6900   2 true 19   7300 130 2 timeout 900     2300 12000    0 true 1.6   54 21    2 true 1.4   110 18    2 true 63   520 600 2 true .36 20   4.2 2 true .51 72 5.5 2 timeout 900   14000 5000 0 timeout 900   2500 12000 0 timeout 900   3300 11000 0 true 48 560 340 2
elevator_spec3_product17_true-unreach-call_true-termination.cil.c true 3.4  670 32    2 timeout 900     410 10000    0 true 1.7  32 18   1 true .15  9.4 1.1  2 timeout 910   11000 5500 0 true 8.9 460 72 2 true 5.2 290 44 2 true 490    290 5800   2 true 19   7300 140 2 timeout 900     2100 11000    0 true 1.7   54 21    2 true 1.4   110 18    2 true 64   500 550 2 true .36 21   4.4 2 true .52 73 6.9 2 timeout 910   14000 4900 0 timeout 900   2400 12000 0 timeout 900   3000 13000 0 true 49 550 330 2
elevator_spec3_product18_true-unreach-call_true-termination.cil.c true 6.4  1200 54    2 timeout 900     540 9700    0 true 1.7  32 22   1 true .12  18   1.5  2 timeout 910   11000 6500 0 true 9.3 470 81 2 true 5.2 290 39 2 true 490    350 5200   2 true 19   7300 120 2 timeout 900     2100 13000    0 true 1.8   56 24    2 true 2.8   170 33    2 true 57   440 520 2 true .38 21   4.2 2 true .56 75 6.5 2 timeout 910   13000 6400 0 timeout 900   3100 9700 0 timeout 900   2900 13000 0 true 49 560 390 2
elevator_spec3_product21_true-unreach-call_true-termination.cil.c true 5.6  1100 51    2 exception (gremlins) 2.3   51 29    0 true 1.9  34 23   1 true .12  9.5 1.2  2 timeout 910   11000 7900 0 true 8.6 460 61 2 true 5.3 290 41 2 true 490    610 6400   2 true 19   7300 140 2 timeout 900     2200 14000    0 true 1.9   59 27    2 true 11     150 21    2 true 93   530 1000 2 true .37 21   4.9 2 true .60 73 6.2 2 timeout 910   13000 5200 0 timeout 900   3000 11000 0 timeout 900   4500 11000 0 true 50 570 350 2
elevator_spec3_product22_true-unreach-call_true-termination.cil.c true 11    2100 120    2 exception (gremlins) 2.3   53 31    0 true 1.9  34 20   1 true .12  9.5 1.2  2 timeout 910   11000 5800 0 true 9.0 460 70 2 true 5.0 290 41 2 true 500    460 4800   2 true 18   7300 130 2 timeout 900     2000 14000    0 true 2.1   61 24    2 true 6.4   250 81    2 true 78   440 670 2 true .37 22   4.5 2 true .63 78 7.1 2 timeout 910   13000 5100 0 timeout 900   2100 9700 0 timeout 900   3000 14000 0 true 52 530 380 2
elevator_spec3_product25_true-unreach-call_true-termination.cil.c true 3.6  710 31    2 timeout 900     400 9400    0 true 1.7  32 20   1 true .11  9.8 1.3  2 timeout 910   11000 7700 0 true 8.8 460 64 2 true 4.9 290 42 2 true 490    330 6200   2 true 19   7300 130 2 timeout 900     2100 13000    0 true 1.7   55 23    2 true 1.5   120 20    2 true 79   540 640 2 true .37 22   4.6 2 true .51 73 5.6 2 timeout 910   14000 5100 0 timeout 900   2500 10000 0 timeout 900   2900 13000 0 true 50 540 420 2
elevator_spec3_product26_true-unreach-call_true-termination.cil.c true 6.9  1300 73    2 timeout 900     580 9200    0 true 1.6  32 20   1 true .15  9.3 1.2  2 timeout 910   11000 6300 0 true 8.4 590 66 2 true 5.0 290 37 2 true 490    400 5400   2 true 18   7300 110 2 timeout 900     2100 11000    0 true 1.8   56 21    2 true 3.1   190 40    2 true 74   480 580 2 true .38 22   4.6 2 true .57 75 6.1 2 timeout 910   14000 5800 0 timeout 900   3000 11000 0 timeout 900   3100 13000 0 true 48 520 390 2
elevator_spec3_product29_true-unreach-call_true-termination.cil.c true 5.7  1100 55    2 exception (gremlins) 2.2   51 28    0 true 1.8  33 21   1 true .11  9.4 1.1  2 timeout 900   10000 6900 0 true 9.3 460 66 2 true 5.0 290 43 2 true 490    320 5800   2 true 18   7300 150 2 timeout 900     2100 12000    0 true 2.0   60 25    2 true 2.8   160 33    2 true 140   580 1300 2 true .39 22   4.2 2 true .56 73 6.5 2 timeout 910   13000 5100 0 timeout 900   2900 12000 0 timeout 900   3500 13000 0 true 49 570 330 2
elevator_spec3_product30_true-unreach-call_true-termination.cil.c true 11    2200 120    2 exception (gremlins) 2.3   51 30    0 true 1.8  33 24   1 true .11  9.8 1.5  2 timeout 910   11000 7000 0 true 9.6 520 69 2 true 5.1 290 45 2 true 500    520 6800   2 true 19   7300 140 2 timeout 900     2000 11000    0 true 2.1   61 29    2 true 6.9   270 100    2 true 90   500 820 2 true .39 23   5.7 2 true .63 78 7.0 2 timeout 910   14000 5100 0 timeout 900   2800 12000 0 timeout 900   3400 12000 0 true 48 570 400 2
elevator_spec9_product09_true-unreach-call_true-termination.cil.c true 62    800 620    2 timeout 900     430 9400    0 true .76 27 7.5 1 true .15  18   1.3  2 timeout 910   11000 5400 0 true 7.6 440 60 2 true 4.3 280 35 2 true 500    280 6800   2 true 18   7300 140 2 timeout 900     1800 11000    0 true .42  36 5.2  2 true 6.1   110 74    2 true 22   390 200 2 true .38 19   4.3 2 true .25 25 2.3 2 timeout 900   13000 5200 0 timeout 900   2600 13000 0 timeout 900   10000 9400 0 true 280 540 1800 2
elevator_spec9_product11_true-unreach-call_true-termination.cil.c true 59    830 740    2 timeout 900     440 10000    0 true .80 28 8.6 1 true .18  16   1.2  2 timeout 900   11000 6300 0 true 7.5 510 58 2 true 4.5 280 36 2 true 500    290 6800   2 true 18   7300 110 2 timeout 900     1800 12000    0 true .46  36 6.1  2 true 6.8   120 76    2 true 25   420 230 2 true .38 19   4.8 2 true .28 41 2.7 2 timeout 900   13000 5800 0 timeout 900   3000 11000 0 timeout 900   2800 12000 0 true 280 550 1900 2
elevator_spec9_product25_true-unreach-call_true-termination.cil.c true 65    860 600    2 timeout 900     470 11000    0 true .80 27 7.4 1 true .16  18   1.3  2 timeout 900   11000 6500 0 true 7.9 680 61 2 true 4.2 280 33 2 true 500    280 5500   2 true 19   7300 110 2 timeout 900     1800 12000    0 true .46  36 6.2  2 true 6.6   120 80    2 true 20   340 210 2 true .36 19   5.5 2 true .30 41 3.2 2 timeout 910   14000 4500 0 timeout 900   2400 13000 0 timeout 900   12000 10000 0 true 280 570 1900 2
elevator_spec9_product27_true-unreach-call_true-termination.cil.c true 77    910 770    2 timeout 900     610 9200    0 true .83 28 9.8 1 true .11  9.6 1.2  2 timeout 910   11000 6000 0 true 8.2 450 59 2 true 4.6 290 37 2 true 510    280 7200   2 true 17   7300 170 2 timeout 900     1800 11000    0 true .47  37 6.1  2 true 7.3   120 85    2 true 27   430 250 2 true .39 20   4.2 2 true .28 41 3.0 2 timeout 910   14000 5100 0 timeout 900   3400 10000 0 timeout 900   3200 12000 0 true 280 570 1600 2
elevator_spec9_product29_true-unreach-call_true-termination.cil.c true 92    1200 800    2 exception (gremlins) 16     110 180    0 true .82 28 8.4 1 true .12  9.8 1.0  2 timeout 900   11000 5700 0 true 8.0 430 58 2 true 4.2 280 33 2 true 510    280 6200   2 true 19   7300 130 2 timeout 900     1800 13000    0 true .45  36 5.2  2 true 15     160 200    2 true 20   350 190 2 true .36 20   4.2 2 true .29 46 2.6 2 timeout 910   14000 5200 0 timeout 900   2800 13000 0 timeout 900   5400 13000 0 true 280 570 1500 2
elevator_spec9_product31_true-unreach-call_true-termination.cil.c true 84    1200 790    2 exception (gremlins) 26     290 300    0 true .79 28 9.2 1 true .15  18   1.3  2 timeout 910   11000 7300 0 true 8.1 440 62 2 true 4.3 280 38 2 true 510    280 5700   2 true 19   7300 140 2 timeout 900     1800 11000    0 true .53  38 6.9  2 true 16     170 210    2 true 24   360 220 2 true .38 21   4.2 2 true .27 41 3.2 2 timeout 910   13000 5800 0 timeout 900   3600 11000 0 timeout 900   3200 14000 0 true 280 630 2000 2
email_spec0_product16_false-unreach-call_true-termination.cil.c false(unreach-call) 38    310 340    1 false(unreach-call) 300     270 3100    0 false(unreach-call) 1.6  41 20   1 unknown .13  9.5 1.2  0 false(unreach-call) 68   3000 470 0 timeout 960   8200 4600 0 false(unreach-call) 23   1200 220 1 false(unreach-call) 490    150 5100   0 false(unreach-call) 4.1 220 50 0 false(unreach-call) 1.2   77 16    0 false(unreach-call) 1.9   110 22    0 false(unreach-call) 2.5   140 33    0 false(unreach-call) 36   210 530 1 false(unreach-call) .37 16   4.4 1 out of memory 250    15000 3400   0 timeout 900   13000 7800 0 timeout 900   2900 13000 0 timeout 900   8100 11000 0 false(unreach-call) 340 5900 3100 1
email_spec0_product21_false-unreach-call_true-termination.cil.c false(unreach-call) 57    530 840    1 timeout 900     580 12000    0 false(unreach-call) 2.7  57 33   1 unknown .12  9.6 1.3  0 false(unreach-call) 200   6800 1300 0 timeout 960   8900 4700 0 false(unreach-call) 25   1500 210 1 false(unreach-call) 500    170 5900   0 false(unreach-call) 5.6 230 64 0 false(unreach-call) 2.6   97 37    0 false(unreach-call) 4.1   150 56    0 false(unreach-call) 5.5   200 59    0 false(unreach-call) 46   250 560 1 false(unreach-call) .41 19   4.5 1 out of memory 310    15000 3800   0 timeout 900   13000 6400 0 timeout 900   2100 13000 0 timeout 900   10000 9000 0 false(unreach-call) 360 5400 3100 1
email_spec0_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 43    330 390    1 timeout 900     570 11000    0 false(unreach-call) 1.7  43 15   1 unknown .13  19   1.8  0 false(unreach-call) 150   6100 990 0 timeout 960   8400 5900 0 false(unreach-call) 25   1400 240 1 false(unreach-call) 490    150 5600   0 false(unreach-call) 4.5 220 60 0 false(unreach-call) 1.3   81 15    0 false(unreach-call) 2.1   120 26    0 false(unreach-call) 2.7   150 34    0 false(unreach-call) 42   220 500 1 false(unreach-call) .41 17   5.2 1 out of memory 260    15000 3400   0 timeout 900   13000 8200 0 timeout 900   2600 13000 0 timeout 900   10000 7100 0 false(unreach-call) 340 5900 2800 1
email_spec0_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 73    590 710    1 timeout 900     560 9700    0 false(unreach-call) 2.8  60 40   1 unknown .12  9.7 1.3  0 timeout 910   11000 4900 0 timeout 960   9300 5100 0 false(unreach-call) 25   1500 230 1 false(unreach-call) 500    320 5900   0 false(unreach-call) 6.1 240 89 0 false(unreach-call) 2.9   100 34    0 false(unreach-call) 4.7   170 62    0 false(unreach-call) 6.3   210 87    0 false(unreach-call) 68   280 570 1 false(unreach-call) .42 20   4.7 1 out of memory 310    15000 3400   0 timeout 900   12000 7000 0 timeout 900   3500 12000 0 timeout 900   11000 6700 0 false(unreach-call) 370 5700 4200 1
email_spec0_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 35    340 460    1 timeout 900     450 9800    0 false(unreach-call) 1.8  45 23   1 unknown .11  9.6 1.2  0 false(unreach-call) 160   5800 1100 0 timeout 960   8400 4200 0 false(unreach-call) 25   1400 240 1 false(unreach-call) 490    160 5300   0 false(unreach-call) 5.3 230 65 0 false(unreach-call) 1.5   90 18    1 false(unreach-call) 2.5   140 34    1 false(unreach-call) 3.4   170 40    1 false(unreach-call) 24   220 270 1 false(unreach-call) .41 18   4.1 1 out of memory 290    15000 3400   0 timeout 900   14000 6000 0 timeout 900   4500 12000 0 timeout 900   4600 13000 0 false(unreach-call) 350 5700 3000 1
email_spec0_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 42    370 410    1 timeout 900     510 10000    0 false(unreach-call) 1.9  48 20   1 unknown .12  9.5 1.5  0 false(unreach-call) 360   9100 2200 0 timeout 960   9000 4700 0 false(unreach-call) 26   1500 250 1 false(unreach-call) 490    200 5200   0 false(unreach-call) 5.8 230 76 0 false(unreach-call) 1.7   95 18    1 false(unreach-call) 2.7   140 31    1 false(unreach-call) 15     180 34    1 false(unreach-call) 49   250 700 1 false(unreach-call) .41 19   6.2 1 out of memory 300    15000 4000   0 timeout 910   13000 7200 0 timeout 900   1900 12000 0 timeout 900   5600 11000 0 false(unreach-call) 340 5700 2900 1
email_spec0_product34_false-unreach-call_true-termination.cil.c false(unreach-call) 64    620 610    1 timeout 900     580 11000    0 false(unreach-call) 3.6  72 35   1 unknown .12  9.7 1.4  0 false(unreach-call) 360   8800 2400 0 timeout 960   9500 4900 0 false(unreach-call) 27   1500 270 1 false(unreach-call) 500    260 5800   0 false(unreach-call) 7.4 250 110 0 false(unreach-call) 3.8   120 48    0 false(unreach-call) 6.2   190 90    0 false(unreach-call) 8.4   240 120    0 false(unreach-call) 110   300 980 1 false(unreach-call) .41 21   4.9 1 out of memory 330    15000 4300   0 timeout 910   14000 6500 0 timeout 900   2700 15000 0 timeout 900   4900 12000 0 false(unreach-call) 360 5300 3300 1
email_spec0_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 70    670 740    1 timeout 900     540 11000    0 false(unreach-call) 3.8  75 43   1 unknown .15  16   1.3  0 timeout 910   11000 4700 0 timeout 960   9700 5000 0 false(unreach-call) 28   1500 240 1 false(unreach-call) 500    310 5200   0 false(unreach-call) 8.0 260 99 0 false(unreach-call) 4.3   130 57    0 false(unreach-call) 7.1   210 96    0 false(unreach-call) 9.4   270 120    0 false(unreach-call) 69   310 570 1 false(unreach-call) .46 22   5.6 1 out of memory 340    15000 5000   0 timeout 910   14000 7900 0 timeout 900   3200 13000 0 timeout 900   5900 12000 0 false(unreach-call) 440 5600 3600 1
email_spec0_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 280    7500 2200    1 timeout 900     5900 9700    0 false(unreach-call) 770    1700 6600   1 unknown .15  17   1.3  0 timeout 910   11000 5400 0 timeout 960   9900 6100 0 false(unreach-call) 54   2900 510 1 unknown 890    1600 9000   0 false(unreach-call) 220   800 3100 0 false(unreach-call) 420     1100 5300    0 false(unreach-call) 710     2700 9800    0 timeout 900     3700 11000    0 false(unreach-call) 400   380 3200 1 false(unreach-call) 1.5  45   18   1 timeout 900    11000 12000   0 timeout 900   13000 4900 0 timeout 900   5800 12000 0 timeout 900   14000 6600 0 timeout 900 1700 6100 0
email_spec11_product15_false-unreach-call_true-termination.cil.c false(unreach-call) 37    290 430    1 timeout 900     470 9200    0 false(unreach-call) 1.5  41 18   1 unknown .13  9.2 1.4  0 false(unreach-call) 120   4200 700 0 timeout 960   8200 4500 0 false(unreach-call) 23   1300 200 1 false(unreach-call) 490    130 5100   0 false(unreach-call) 2.6 200 31 0 false(unreach-call) 1.0   58 13    0 false(unreach-call) 1.5   82 18    0 false(unreach-call) 2.0   100 31    0 false(unreach-call) 41   210 450 1 false(unreach-call) .36 16   5.1 1 out of memory 230    15000 3200   0 timeout 900   13000 6500 0 timeout 900   4600 15000 0 timeout 900   8500 11000 0 false(unreach-call) 330 5800 2600 1
email_spec11_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 64    500 700    1 timeout 900     450 9100    0 false(unreach-call) 2.3  53 29   1 unknown .14  16   1.1  0 timeout 900   11000 5100 0 timeout 960   7700 4500 0 false(unreach-call) 24   1400 220 1 false(unreach-call) 490    220 6400   0 false(unreach-call) 3.7 210 41 1 false(unreach-call) 2.1   78 27    0 false(unreach-call) 3.3   120 40    0 false(unreach-call) 4.4   150 59    0 false(unreach-call) 80   250 880 1 false(unreach-call) .38 18   4.7 1 out of memory 280    15000 3500   0 timeout 900   13000 6100 0 timeout 900   3300 13000 0 timeout 900   8900 9000 0 false(unreach-call) 360 5600 3500 1
email_spec11_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 44    340 410    1 timeout 900     350 10000    0 false(unreach-call) 1.6  42 20   1 unknown .16  16   1.3  0 timeout 910   11000 4300 0 timeout 960   8000 4700 0 false(unreach-call) 24   1400 230 1 false(unreach-call) 490    280 6900   0 false(unreach-call) 4.5 220 54 0 false(unreach-call) 1.3   81 15    0 false(unreach-call) 2.0   120 28    0 false(unreach-call) 2.8   150 35    0 false(unreach-call) 48   220 500 1 false(unreach-call) .39 17   4.4 1 out of memory 260    15000 3100   0 timeout 900   13000 6100 0 timeout 900   2300 13000 0 timeout 900   9900 10000 0 false(unreach-call) 350 5500 2400 1
email_spec11_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 75    580 640    1 timeout 900     570 10000    0 false(unreach-call) 2.9  60 31   1 unknown .12  9.6 1.3  0 timeout 900   11000 5100 0 timeout 960   8900 5200 0 false(unreach-call) 27   1500 230 1 false(unreach-call) 500    410 6400   0 false(unreach-call) 7.7 240 92 0 false(unreach-call) 2.9   100 36    0 false(unreach-call) 4.7   170 56    0 false(unreach-call) 6.3   210 83    0 false(unreach-call) 89   280 890 1 false(unreach-call) .42 19   5.1 1 out of memory 300    15000 3900   0 timeout 910   13000 5900 0 timeout 900   3700 13000 0 timeout 900   10000 9400 0 false(unreach-call) 440 5700 3500 1
email_spec11_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 38    320 400    1 timeout 900     600 9800    0 false(unreach-call) 1.7  44 23   1 unknown .12  9.5 1.2  0 false(unreach-call) 110   4400 690 0 timeout 960   8000 4500 0 false(unreach-call) 26   1500 230 1 false(unreach-call) 490    190 5700   0 false(unreach-call) 2.8 200 31 0 false(unreach-call) 1.2   62 16    0 false(unreach-call) 1.9   89 24    0 false(unreach-call) 2.5   110 32    0 false(unreach-call) 36   230 480 1 false(unreach-call) .39 17   5.5 1 out of memory 260    15000 3400   0 timeout 900   13000 6800 0 timeout 900   2200 12000 0 timeout 900   4600 12000 0 false(unreach-call) 340 6000 3500 1
email_spec11_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 66    560 690    1 timeout 900     440 11000    0 false(unreach-call) 3.2  67 34   1 unknown .12  9.8 1.6  0 timeout 910   11000 5500 0 timeout 960   8800 5900 0 false(unreach-call) 27   1500 280 1 false(unreach-call) 500    200 5400   0 false(unreach-call) 4.3 220 44 1 false(unreach-call) 3.0   86 34    0 false(unreach-call) 4.8   140 59    0 false(unreach-call) 6.4   180 73    0 false(unreach-call) 98   280 1300 1 false(unreach-call) .39 19   5.0 1 out of memory 310    15000 3800   0 timeout 900   12000 6500 0 timeout 900   1800 15000 0 timeout 900   4800 14000 0 false(unreach-call) 520 5500 5100 1
email_spec11_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 47    370 390    1 timeout 900     420 9100    0 false(unreach-call) 1.9  45 20   1 unknown .12  9.7 1.2  0 timeout 910   11000 4600 0 timeout 960   8400 5200 0 false(unreach-call) 28   1500 240 1 false(unreach-call) 490    260 5800   0 false(unreach-call) 5.7 240 73 0 false(unreach-call) 1.6   95 20    0 false(unreach-call) 2.7   140 29    0 false(unreach-call) 3.6   180 46    0 false(unreach-call) 62   250 620 1 false(unreach-call) .39 19   4.7 1 out of memory 290    15000 4000   0 timeout 900   11000 7300 0 timeout 900   3000 12000 0 timeout 900   4900 12000 0 false(unreach-call) 350 5800 3500 1
email_spec11_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 78    680 630    1 timeout 900     560 12000    0 false(unreach-call) 3.8  75 52   1 unknown .23  54   1.8  0 timeout 910   11000 4400 0 timeout 960   9600 4700 0 false(unreach-call) 29   1600 260 1 false(unreach-call) 500    240 5100   0 false(unreach-call) 8.0 260 100 0 false(unreach-call) 4.3   130 54    1 false(unreach-call) 7.0   210 90    1 false(unreach-call) 9.4   270 110    1 false(unreach-call) 200   340 1500 1 false(unreach-call) .42 22   5.1 1 out of memory 340    15000 3700   0 timeout 900   12000 6800 0 timeout 900   2500 12000 0 timeout 900   4800 11000 0 false(unreach-call) 460 5700 4200 1
email_spec11_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 380    8000 2100    1 timeout 900     5300 11000    0 error (42) 850    2000 5100   0 unknown .13  10   1.3  0 timeout 900   11000 4600 0 timeout 960   11000 5900 0 false(unreach-call) 57   3000 530 1 unknown 890    1600 10000   0 false(unreach-call) 270   870 3700 0 false(unreach-call) 520     1200 6300    0 false(unreach-call) 880     3000 11000    0 timeout 900     3400 11000    0 false(unreach-call) 470   380 4500 1 false(unreach-call) .82 28   10   1 timeout 900    11000 11000   0 timeout 900   13000 5200 0 timeout 900   5700 12000 0 timeout 900   12000 6300 0 timeout 900 1700 6100 0
email_spec1_product14_false-unreach-call_true-termination.cil.c false(unreach-call) 28    350 380    1 timeout 900     1000 10000    0 false(unreach-call) 1.5  41 15   1 unknown .11  9.3 1.2  0 false(unreach-call) 440   7400 3700 0 timeout 960   8400 5400 0 false(unreach-call) 13   490 90 1 false(unreach-call) 490    260 5400   0 false(unreach-call) 2.8 200 31 0 false(unreach-call) .71  51 8.1  0 false(unreach-call) .97  67 10    0 false(unreach-call) 1.2   76 14    0 false(unreach-call) 11   190 130 1 false(unreach-call) .42 17   4.8 1 out of memory 250    15000 3400   0 timeout 900   13000 8300 0 timeout 900   5600 12000 0 timeout 900   11000 7200 0 false(unreach-call) 330 5700 2900 1
email_spec1_product15_false-unreach-call_true-termination.cil.c false(unreach-call) 18    230 180    1 timeout 900     560 10000    0 false(unreach-call) 1.5  40 16   1 unknown .12  9.5 1.2  0 false(unreach-call) 110   4300 840 0 timeout 960   7800 6900 0 false(unreach-call) 12   500 100 1 false(unreach-call) 490    170 5800   0 false(unreach-call) 2.6 200 27 0 false(unreach-call) .69  49 8.4  0 false(unreach-call) .95  64 13    0 false(unreach-call) 1.2   72 16    0 false(unreach-call) 6.0 160 73 1 false(unreach-call) .48 16   5.9 1 out of memory 220    15000 3300   0 timeout 900   12000 7000 0 timeout 900   5600 11000 0 timeout 900   10000 8900 0 false(unreach-call) 320 5800 2700 1
email_spec1_product16_false-unreach-call_true-termination.cil.c false(unreach-call) 19    240 240    1 timeout 900     430 9900    0 false(unreach-call) 1.6  40 16   1 unknown .12  9.5 1.1  0 false(unreach-call) 68   2900 470 0 timeout 970   8000 6700 0 false(unreach-call) 13   490 89 1 false(unreach-call) 490    370 5700   0 false(unreach-call) 4.1 220 45 0 false(unreach-call) .79  64 10    0 false(unreach-call) 1.2   86 15    0 false(unreach-call) 1.5   99 19    0 false(unreach-call) 8.2 170 120 1 false(unreach-call) .43 16   4.9 1 out of memory 250    15000 2900   0 timeout 900   14000 7000 0 timeout 900   5600 13000 0 timeout 900   12000 8300 0 false(unreach-call) 320 5900 2500 1
email_spec1_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 36    390 390    1 timeout 900     430 10000    0 false(unreach-call) 2.3  51 25   1 unknown .17  16   1.1  0 false(unreach-call) 130   5100 820 0 timeout 960   8400 5500 0 false(unreach-call) 12   490 110 1 false(unreach-call) 490    240 5500   0 false(unreach-call) 3.7 210 42 0 false(unreach-call) 1.4   64 17    0 false(unreach-call) 2.1   90 27    0 false(unreach-call) 2.7   100 39    0 false(unreach-call) 13   210 140 1 false(unreach-call) .44 18   5.7 1 out of memory 280    15000 3700   0 timeout 900   12000 9200 0 timeout 900   5600 13000 0 timeout 900   10000 7700 0 false(unreach-call) 350 5700 2600 1
email_spec1_product21_false-unreach-call_true-termination.cil.c false(unreach-call) 31    430 380    1 timeout 900     550 10000    0 false(unreach-call) 2.5  55 36   1 unknown .15  16   1.3  0 false(unreach-call) 210   6400 1400 0 timeout 960   8600 4900 0 false(unreach-call) 12   490 98 1 false(unreach-call) 490    210 5400   0 false(unreach-call) 5.6 230 62 0 false(unreach-call) 1.8   81 22    0 false(unreach-call) 2.7   120 33    0 false(unreach-call) 3.3   140 47    0 false(unreach-call) 14   220 160 1 false(unreach-call) .41 18   5.1 1 out of memory 310    15000 4200   0 timeout 900   13000 8000 0 timeout 900   5600 11000 0 timeout 910   11000 8500 0 false(unreach-call) 350 5600 2900 1
email_spec1_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 23    270 230    1 timeout 900     410 11000    0 false(unreach-call) 1.6  41 19   1 unknown .12  9.5 1.5  0 false(unreach-call) 160   6000 1100 0 timeout 960   8000 6200 0 false(unreach-call) 13   500 110 1 false(unreach-call) 490    180 5300   0 false(unreach-call) 4.5 220 55 0 false(unreach-call) .87  68 11    0 false(unreach-call) 1.3   92 18    0 false(unreach-call) 1.6   110 21    0 false(unreach-call) 7.5 180 82 1 false(unreach-call) .46 17   5.4 1 out of memory 260    15000 3300   0 timeout 910   11000 7300 0 timeout 900   5600 13000 0 timeout 900   12000 7500 0 false(unreach-call) 330 5900 2800 1
email_spec1_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 43    480 440    1 timeout 900     560 13000    0 false(unreach-call) 2.8  58 29   1 unknown .12  9.4 1.4  0 false(unreach-call) 240   6900 1600 0 timeout 960   9100 4300 0 false(unreach-call) 12   490 98 1 false(unreach-call) 490    230 6000   0 false(unreach-call) 6.2 240 64 0 false(unreach-call) 2.0   88 21    0 false(unreach-call) 3.0   130 40    0 false(unreach-call) 3.8   150 45    0 false(unreach-call) 13   220 150 1 false(unreach-call) .45 20   6.3 1 out of memory 310    15000 4200   0 timeout 900   11000 8100 0 timeout 900   5600 14000 0 timeout 900   11000 8000 0 false(unreach-call) 350 5600 2500 1
email_spec1_product29_false-unreach-call_true-termination.cil.c false(unreach-call) 34    420 330    1 timeout 900     800 11000    0 false(unreach-call) 1.7  42 22   1 unknown .12  16   1.8  0 timeout 900   11000 5100 0 timeout 960   8600 5600 0 false(unreach-call) 12   480 100 1 false(unreach-call) 490    210 6400   0 false(unreach-call) 3.0 210 36 0 false(unreach-call) .87  54 11    0 false(unreach-call) 1.3   72 16    0 false(unreach-call) 1.5   82 16    0 false(unreach-call) 11   220 130 1 false(unreach-call) .42 19   5.3 1 out of memory 290    15000 3600   0 timeout 910   13000 6500 0 timeout 900   5400 13000 0 timeout 900   2700 13000 0 false(unreach-call) 340 5800 3200 1
email_spec1_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 21    260 210    1 timeout 900     680 9500    0 false(unreach-call) 1.7  41 18   1 unknown .11  9.5 1.4  0 false(unreach-call) 68   3300 550 0 timeout 960   8200 6600 0 false(unreach-call) 14   530 110 1 false(unreach-call) 490    250 5300   0 false(unreach-call) 2.8 200 34 0 false(unreach-call) .83  53 11    0 false(unreach-call) 1.2   69 15    0 false(unreach-call) 1.5   79 21    0 false(unreach-call) 6.4 180 75 1 false(unreach-call) .51 17   5.8 1 out of memory 260    15000 3300   0 timeout 910   13000 7600 0 timeout 900   5600 12000 0 timeout 900   2800 11000 0 false(unreach-call) 330 5800 2700 1
email_spec1_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 22    280 210    1 timeout 900     520 10000    0 false(unreach-call) 1.8  42 19   1 unknown .14  16   1.4  0 false(unreach-call) 130   5400 880 0 timeout 960   8300 6200 0 false(unreach-call) 13   530 110 1 false(unreach-call) 490    190 4700   0 false(unreach-call) 5.3 230 64 0 false(unreach-call) 1.0   75 12    0 false(unreach-call) 1.6   100 19    0 false(unreach-call) 1.9   120 23    0 false(unreach-call) 7.5 180 100 1 false(unreach-call) .51 26   5.5 1 out of memory 260    15000 3100   0 timeout 900   13000 6400 0 timeout 900   5500 12000 0 timeout 900   2200 12000 0 false(unreach-call) 330 5900 3000 1
email_spec1_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 35    460 350    1 timeout 900     820 9200    0 false(unreach-call) 3.0  77 38   1 unknown .12  9.5 1.6  0 false(unreach-call) 170   5900 1300 0 timeout 960   9200 4500 0 false(unreach-call) 13   500 120 1 false(unreach-call) 490    440 5000   0 false(unreach-call) 4.3 220 53 0 false(unreach-call) 2.1   72 27    0 false(unreach-call) 3.2   100 50    0 false(unreach-call) 3.9   120 48    0 false(unreach-call) 21   250 210 1 false(unreach-call) .48 20   5.8 1 out of memory 310    15000 3700   0 timeout 900   12000 6900 0 timeout 900   5400 13000 0 timeout 900   3100 13000 0 false(unreach-call) 350 5700 2900 1
email_spec1_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 23    300 230    1 timeout 900     680 9900    0 false(unreach-call) 1.9  43 20   1 unknown .21  54   1.4  0 false(unreach-call) 200   6200 1300 0 timeout 960   8800 5900 0 false(unreach-call) 14   550 110 1 false(unreach-call) 490    190 4900   0 false(unreach-call) 5.7 240 74 0 false(unreach-call) 1.1   79 16    0 false(unreach-call) 1.7   110 21    0 false(unreach-call) 2.2   130 29    0 false(unreach-call) 8.9 200 110 1 false(unreach-call) .51 19   6.7 1 out of memory 300    15000 3600   0 timeout 900   12000 6000 0 timeout 900   5600 12000 0 timeout 900   2600 11000 0 false(unreach-call) 340 5900 2700 1
email_spec1_product34_false-unreach-call_true-termination.cil.c false(unreach-call) 40    530 410    1 timeout 900     800 9800    0 false(unreach-call) 3.5  69 46   1 unknown .15  9.9 1.3  0 timeout 910   11000 5800 0 timeout 960   9500 4700 0 false(unreach-call) 14   500 110 1 false(unreach-call) 490    360 5400   0 false(unreach-call) 7.5 250 86 0 false(unreach-call) 2.6   98 30    0 false(unreach-call) 4.1   150 54    0 false(unreach-call) 5.1   170 63    0 false(unreach-call) 20   250 220 1 false(unreach-call) .44 21   6.3 1 out of memory 340    15000 4000   0 timeout 900   12000 7000 0 timeout 900   5600 13000 0 timeout 900   3000 11000 0 false(unreach-call) 370 5800 3300 1
email_spec1_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 41    570 390    1 timeout 900     950 9400    0 false(unreach-call) 3.8  71 54   1 unknown .14  16   1.5  0 timeout 900   11000 5000 0 timeout 960   10000 4800 0 false(unreach-call) 14   510 110 1 false(unreach-call) 490    320 5600   0 false(unreach-call) 8.1 260 99 0 false(unreach-call) 3.0   110 40    0 false(unreach-call) 4.6   160 57    0 false(unreach-call) 5.7   190 71    0 false(unreach-call) 17   260 200 1 false(unreach-call) .49 22   5.0 1 out of memory 340    15000 4300   0 timeout 900   11000 6700 0 timeout 900   5400 13000 0 timeout 900   3700 12000 0 false(unreach-call) 380 5600 3000 1
email_spec1_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 140    7100 1100    1 timeout 900     2400 10000    0 false(unreach-call) 100    600 870   1 unknown .15  17   1.6  0 timeout 900   11000 5300 0 timeout 960   11000 4800 0 false(unreach-call) 19   890 170 1 false(unreach-call) 620    1600 7400   0 false(unreach-call) 69   480 960 0 false(unreach-call) 90     440 1100    0 false(unreach-call) 140     890 1900    0 false(unreach-call) 700     1100 1500    0 false(unreach-call) 57   310 490 1 false(unreach-call) 1.4  44   17   1 out of memory 770    15000 10000   0 timeout 910   13000 6200 0 timeout 900   4400 15000 0 timeout 900   13000 6700 0 witness invalid (false(unreach-call)) 760 4000 6600 0
email_spec27_product17_false-unreach-call_true-termination.cil.c false(unreach-call) 30    370 320    1 false(unreach-call) 46     130 470    0 false(unreach-call) 1.6  42 17   1 unknown .12  9.4 1.2  0 timeout 910   11000 5800 0 timeout 960   8100 4800 0 false(unreach-call) 9.9 410 80 1 false(unreach-call) 490    190 4800   0 false(unreach-call) 2.9 200 29 0 false(unreach-call) .78  52 9.2  0 false(unreach-call) 1.1   69 14    0 false(unreach-call) 1.4   79 19    0 false(unreach-call) 14   200 170 1 false(unreach-call) .61 19   6.5 1 out of memory 270    15000 3500   0 timeout 900   12000 6400 0 timeout 900   1800 13000 0 timeout 900   2500 12000 0 false(unreach-call) 340 5700 2700 1
email_spec27_product18_false-unreach-call_true-termination.cil.c false(unreach-call) 22    230 200    1 false(unreach-call) 5.9   90 44    0 false(unreach-call) 1.5  41 17   1 unknown .11  9.4 1.3  0 false(unreach-call) 230   5900 1600 0 timeout 960   8100 6300 0 false(unreach-call) 14   530 110 1 false(unreach-call) 490    130 6600   0 false(unreach-call) 2.6 200 34 0 false(unreach-call) .72  50 8.2  0 false(unreach-call) 1.0   65 13    0 false(unreach-call) 1.3   74 17    0 false(unreach-call) 13   190 180 1 false(unreach-call) .62 21   7.9 1 out of memory 230    15000 3000   0 timeout 900   13000 8300 0 timeout 900   1600 14000 0 timeout 900   2500 14000 0 false(unreach-call) 330 5800 2700 1
email_spec27_product19_false-unreach-call_true-termination.cil.c false(unreach-call) 21    250 270    1 false(unreach-call) 46     120 490    0 false(unreach-call) 1.6  42