Tool CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741 CPA-witness2test 1.6.1-svn 26773 CProver witness2test 0.1 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon*
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB]
Date of execution 2017-11-30 11:20:26 CET 2017-12-01 07:29:20 CET 2017-12-01 08:07:14 CET 2017-12-01 08:15:38 CET 2017-12-01 08:19:10 CET 2017-12-01 04:11:27 CET 2017-12-01 07:35:08 CET
Run set cpa-seq.sv-comp18.ReachSafety-ProductLines cpa-seq-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.ReachSafety-ProductLines uautomizer-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.ReachSafety-ProductLines cpa-witness2test-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.ReachSafety-ProductLines fshell-witness2test-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.ReachSafety-ProductLines cpa-seq-validate-correctness-witnesses-cpa-seq.sv-comp18-correctness-witness.ReachSafety-ProductLines uautomizer-validate-correctness-witnesses-cpa-seq.sv-comp18-correctness-witness.ReachSafety-ProductLines
Options -svcomp18 -heap 10000M -benchmark -timelimit 900s -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-seq.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop cpa.smg.memoryAllocationFunctions=malloc,__kmalloc,kmalloc,kzalloc,kzalloc_node,ldv_zalloc,ldv_malloc -setprop cpa.smg.arrayAllocationFunctions=calloc,kmalloc_array,kcalloc -setprop cpa.smg.zeroingMemoryAllocation=calloc,kzalloc,kcalloc,kzalloc_node,ldv_zalloc -setprop cpa.smg.deallocationFunctions=free,kfree,kfree_const --full-output --validate ../../results-verified/cpa-seq.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-seq.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true --graphml-witness ../../results-verified/cpa-seq.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-seq.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/cpa-seq.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/product-lines/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
elevator_spec14_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 7.4 310 53 false(unreach-call) 1 wit inspect 6.9 290 false(unreach-call) 1 wit inspect 18   550 unknown 0 wit inspect 5.4 270 false(unreach-call) 1 wit inspect .94 22 - wit inspect - wit inspect
elevator_spec14_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 7.2 310 66 false(unreach-call) 1 wit inspect 7.1 310 false(unreach-call) 1 wit inspect 20   810 unknown 0 wit inspect 6.5 270 false(unreach-call) 1 wit inspect 1.2  22 - wit inspect - wit inspect
elevator_spec14_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 7.3 320 66 false(unreach-call) 1 wit inspect 6.7 300 false(unreach-call) 1 wit inspect 16   720 unknown 0 wit inspect 6.6 280 false(unreach-call) 1 wit inspect .97 22 - wit inspect - wit inspect
elevator_spec14_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 7.1 310 57 false(unreach-call) 1 wit inspect 7.3 300 false(unreach-call) 1 wit inspect 24   800 unknown 0 wit inspect 5.9 280 false(unreach-call) 1 wit inspect 1.0  22 - wit inspect - wit inspect
elevator_spec14_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.4 360 75 false(unreach-call) 1 wit inspect 7.4 320 false(unreach-call) 1 wit inspect 30   1400 unknown 0 wit inspect 7.5 270 true -32 wit inspect 1.2  22 - wit inspect - wit inspect
elevator_spec1_product18_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 7.5 330 58 false(unreach-call) 1 wit inspect 6.7 290 false(unreach-call) 1 wit inspect 39   1000 unknown 0 wit inspect 6.6 270 false(unreach-call) 1 wit inspect .97 22 - wit inspect - wit inspect
elevator_spec1_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 7.7 330 64 false(unreach-call) 1 wit inspect 7.2 290 false(unreach-call) 1 wit inspect 30   1100 unknown 0 wit inspect 5.9 270 false(unreach-call) 1 wit inspect .99 23 - wit inspect - wit inspect
elevator_spec1_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 7.4 330 68 false(unreach-call) 1 wit inspect 7.0 300 false(unreach-call) 1 wit inspect 48   1200 unknown 0 wit inspect 6.5 280 false(unreach-call) 1 wit inspect 1.1  23 - wit inspect - wit inspect
elevator_spec1_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 7.6 340 58 false(unreach-call) 1 wit inspect 7.0 300 false(unreach-call) 1 wit inspect 38   970 unknown 0 wit inspect 6.3 270 false(unreach-call) 1 wit inspect 1.0  23 - wit inspect - wit inspect
elevator_spec1_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 7.3 320 58 false(unreach-call) 1 wit inspect 7.3 310 false(unreach-call) 1 wit inspect 26   1200 unknown 0 wit inspect 5.5 270 false(unreach-call) 1 wit inspect .98 22 - wit inspect - wit inspect
elevator_spec1_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 7.6 330 59 false(unreach-call) 1 wit inspect 7.9 290 false(unreach-call) 1 wit inspect 32   1200 unknown 0 wit inspect 5.9 280 false(unreach-call) 1 wit inspect .99 23 - wit inspect - wit inspect
elevator_spec1_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 7.6 330 64 false(unreach-call) 1 wit inspect 6.9 310 false(unreach-call) 1 wit inspect 33   1000 unknown 0 wit inspect 5.9 270 false(unreach-call) 1 wit inspect 1.1  23 - wit inspect - wit inspect
elevator_spec1_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 7.8 340 52 false(unreach-call) 1 wit inspect 8.1 310 false(unreach-call) 1 wit inspect 31   1000 unknown 0 wit inspect 6.1 290 false(unreach-call) 1 wit inspect 1.0  23 - wit inspect - wit inspect
elevator_spec1_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 9.8 380 83 false(unreach-call) 1 wit inspect 8.0 310 false(unreach-call) 1 wit inspect 28   1200 unknown 0 wit inspect 6.8 270 true -32 wit inspect 1.1  23 - wit inspect - wit inspect
elevator_spec2_product18_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 7.1 320 59 false(unreach-call) 1 wit inspect 6.8 290 false(unreach-call) 1 wit inspect 30   1100 unknown 0 wit inspect 7.1 270 false(unreach-call) 1 wit inspect 1.2  22 - wit inspect - wit inspect
elevator_spec2_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 7.9 320 62 false(unreach-call) 1 wit inspect 7.0 290 false(unreach-call) 1 wit inspect 42   1100 unknown 0 wit inspect 5.4 270 false(unreach-call) 1 wit inspect .99 22 - wit inspect - wit inspect
elevator_spec2_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 7.3 320 61 false(unreach-call) 1 wit inspect 7.2 310 false(unreach-call) 1 wit inspect 28   1100 unknown 0 wit inspect 5.5 280 false(unreach-call) 1 wit inspect 1.0  22 - wit inspect - wit inspect
elevator_spec2_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 7.5 330 59 false(unreach-call) 1 wit inspect 6.7 300 false(unreach-call) 1 wit inspect 23   980 unknown 0 wit inspect 6.0 270 false(unreach-call) 1 wit inspect 1.2  23 - wit inspect - wit inspect
elevator_spec2_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 7.3 310 57 false(unreach-call) 1 wit inspect 7.6 290 false(unreach-call) 1 wit inspect 27   1000 unknown 0 wit inspect 5.5 270 false(unreach-call) 1 wit inspect 1.0  22 - wit inspect - wit inspect
elevator_spec2_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 7.7 330 57 false(unreach-call) 1 wit inspect 6.9 310 false(unreach-call) 1 wit inspect 38   1000 unknown 0 wit inspect 5.8 270 false(unreach-call) 1 wit inspect .97 22 - wit inspect - wit inspect
elevator_spec2_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 7.4 330 58 false(unreach-call) 1 wit inspect 7.2 300 false(unreach-call) 1 wit inspect 31   1000 unknown 0 wit inspect 6.9 280 false(unreach-call) 1 wit inspect 1.0  22 - wit inspect - wit inspect
elevator_spec2_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 7.5 330 65 false(unreach-call) 1 wit inspect 7.8 310 false(unreach-call) 1 wit inspect 36   1000 unknown 0 wit inspect 6.8 270 false(unreach-call) 1 wit inspect 1.1  23 - wit inspect - wit inspect
elevator_spec2_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 9.7 370 85 false(unreach-call) 1 wit inspect 7.0 290 false(unreach-call) 1 wit inspect 34   1200 unknown 0 wit inspect 5.7 270 true -32 wit inspect 1.3  23 - wit inspect - wit inspect
elevator_spec3_product03_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.2 350 76 false(unreach-call) 1 wit inspect 7.9 320 false(unreach-call) 1 wit inspect 47   1400 unknown 0 wit inspect 5.8 270 false(unreach-call) 1 wit inspect 1.0  24 - wit inspect - wit inspect
elevator_spec3_product11_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.3 350 71 false(unreach-call) 1 wit inspect 5.3 300 false(unreach-call) 1 wit inspect 44   1200 unknown 0 wit inspect 7.2 280 false(unreach-call) 1 wit inspect 1.2  24 - wit inspect - wit inspect
elevator_spec3_product19_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.2 350 57 false(unreach-call) 1 wit inspect 8.1 300 false(unreach-call) 1 wit inspect 45   1500 unknown 0 wit inspect 6.7 280 false(unreach-call) 1 wit inspect 1.2  24 - wit inspect - wit inspect
elevator_spec3_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.3 390 72 false(unreach-call) 1 wit inspect 7.8 300 false(unreach-call) 1 wit inspect 46   1500 unknown 0 wit inspect 6.5 270 false(unreach-call) 1 wit inspect 1.0  25 - wit inspect - wit inspect
elevator_spec3_product23_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.8 380 69 false(unreach-call) 1 wit inspect 8.0 320 false(unreach-call) 1 wit inspect 31   1400 unknown 0 wit inspect 7.3 280 false(unreach-call) 1 wit inspect 1.1  25 - wit inspect - wit inspect
elevator_spec3_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.8 380 74 false(unreach-call) 1 wit inspect 8.4 320 false(unreach-call) 1 wit inspect 33   1500 unknown 0 wit inspect 6.2 280 false(unreach-call) 1 wit inspect 1.4  25 - wit inspect - wit inspect
elevator_spec3_product27_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.0 360 64 false(unreach-call) 1 wit inspect 8.1 300 false(unreach-call) 1 wit inspect 45   1500 unknown 0 wit inspect 6.9 270 false(unreach-call) 1 wit inspect 1.0  24 - wit inspect - wit inspect
elevator_spec3_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.2 370 68 false(unreach-call) 1 wit inspect 8.6 300 false(unreach-call) 1 wit inspect 44   1500 unknown 0 wit inspect 7.6 280 false(unreach-call) 1 wit inspect 1.3  25 - wit inspect - wit inspect
elevator_spec3_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.6 370 72 false(unreach-call) 1 wit inspect 7.8 320 false(unreach-call) 1 wit inspect 39   1200 unknown 0 wit inspect 7.9 280 false(unreach-call) 1 wit inspect 1.2  25 - wit inspect - wit inspect
elevator_spec3_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.2 400 65 false(unreach-call) 1 wit inspect 7.6 320 false(unreach-call) 1 wit inspect 39   1800 unknown 0 wit inspect 6.1 280 false(unreach-call) 1 wit inspect 1.3  25 - wit inspect - wit inspect
elevator_spec3_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 11   480 80 false(unreach-call) 1 wit inspect 8.5 320 false(unreach-call) 1 wit inspect 58   2000 unknown 0 wit inspect 6.1 270 true -32 wit inspect 1.1  25 - wit inspect - wit inspect
elevator_spec9_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 7.5 330 63 false(unreach-call) 1 wit inspect 7.1 300 false(unreach-call) 1 wit inspect 31   1000 unknown 0 wit inspect 5.4 270 false(unreach-call) 1 wit inspect 1.2  22 - wit inspect - wit inspect
elevator_spec9_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 7.7 340 72 false(unreach-call) 1 wit inspect 7.3 290 false(unreach-call) 1 wit inspect 30   1100 unknown 0 wit inspect 6.9 270 false(unreach-call) 1 wit inspect 1.0  23 - wit inspect - wit inspect
elevator_spec9_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 7.6 330 60 false(unreach-call) 1 wit inspect 7.5 310 false(unreach-call) 1 wit inspect 33   1000 unknown 0 wit inspect 6.0 270 false(unreach-call) 1 wit inspect 1.3  23 - wit inspect - wit inspect
elevator_spec9_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 7.6 340 62 false(unreach-call) 1 wit inspect 9.3 300 false(unreach-call) 1 wit inspect 34   1300 unknown 0 wit inspect 5.7 270 false(unreach-call) 1 wit inspect 1.1  23 - wit inspect - wit inspect
elevator_spec9_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 9.5 400 84 false(unreach-call) 1 wit inspect 9.1 290 false(unreach-call) 1 wit inspect 39   1200 unknown 0 wit inspect 5.7 270 true -32 wit inspect 1.2  23 - wit inspect - wit inspect
elevator_spec13_product21_true-unreach-call_false-termination.cil.c true 1 wit inspect 5.2 280 44 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900   1800 out of memory 0 wit inspect 310   7000
elevator_spec13_product22_true-unreach-call_false-termination.cil.c true 1 wit inspect 5.6 280 52 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910   2100 out of memory 0 wit inspect 190   7000
elevator_spec13_product23_true-unreach-call_false-termination.cil.c true 1 wit inspect 5.2 280 40 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900   1900 out of memory 0 wit inspect 200   7000
elevator_spec13_product24_true-unreach-call_false-termination.cil.c true 1 wit inspect 5.3 280 44 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900   2100 out of memory 0 wit inspect 180   7000
elevator_spec13_product29_true-unreach-call_false-termination.cil.c true 1 wit inspect 5.3 280 43 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910   1900 out of memory 0 wit inspect 200   7000
elevator_spec13_product30_true-unreach-call_false-termination.cil.c true 1 wit inspect 5.5 280 43 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900   2100 out of memory 0 wit inspect 170   7000
elevator_spec13_product31_true-unreach-call_false-termination.cil.c true 1 wit inspect 5.4 280 44 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900   2100 out of memory 0 wit inspect 240   7000
elevator_spec13_product32_true-unreach-call_false-termination.cil.c true 1 wit inspect 5.3 290 42 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900   2100 out of memory 0 wit inspect 230   7000
elevator_spec13_productSimulator_true-unreach-call_false-termination.cil.c true 1 wit inspect 7.2 300 60 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910   2300 out of memory 0 wit inspect 240   7000
elevator_spec14_product03_true-unreach-call_true-termination.cil.c true 2 wit inspect 6.1 290 49 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 28   780 out of memory 0 wit inspect 170   7000
elevator_spec14_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect 6.2 290 52 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 23   800 out of memory 0 wit inspect 250   7000
elevator_spec14_product19_true-unreach-call_true-termination.cil.c true 2 wit inspect 5.8 290 51 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 24   820 out of memory 0 wit inspect 290   7000
elevator_spec14_product23_true-unreach-call_true-termination.cil.c true 2 wit inspect 6.1 290 52 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 48   1400 out of memory 0 wit inspect 220   7000
elevator_spec14_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect 6.6 290 53 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 27   960 out of memory 0 wit inspect 230   7000
elevator_spec14_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect 6.1 290 52 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 43   1400 out of memory 0 wit inspect 210   7000
elevator_spec1_product01_true-unreach-call_true-termination.cil.c true 2 wit inspect 5.7 290 51 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 240   3300 out of memory 0 wit inspect 250   7000
elevator_spec1_product03_true-unreach-call_true-termination.cil.c true 2 wit inspect 5.7 280 50 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 330   3300 out of memory 0 wit inspect 260   7000
elevator_spec1_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect 5.8 290 48 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 280   3300 out of memory 0 wit inspect 200   7000
elevator_spec1_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect 6.0 290 47 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 280   3600 out of memory 0 wit inspect 280   7000
elevator_spec1_product17_true-unreach-call_true-termination.cil.c true 2 wit inspect 5.8 290 47 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 300   3300 out of memory 0 wit inspect 310   7000
elevator_spec1_product19_true-unreach-call_true-termination.cil.c true 2 wit inspect 6.1 290 51 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 340   3800 out of memory 0 wit inspect 310   7000
elevator_spec1_product21_true-unreach-call_true-termination.cil.c true 2 wit inspect 6.0 290 49 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 720   4200 out of memory 0 wit inspect 260   7000
elevator_spec1_product23_true-unreach-call_true-termination.cil.c true 2 wit inspect 6.4 290 51 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 600   4400 out of memory 0 wit inspect 210   7000
elevator_spec1_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect 6.2 290 52 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 300   3400 out of memory 0 wit inspect 180   7000
elevator_spec1_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect 5.8 290 43 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 310   3900 out of memory 0 wit inspect 210   7000
elevator_spec1_product29_true-unreach-call_true-termination.cil.c true 1 wit inspect 6.0 290 48 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900   4200 out of memory 0 wit inspect 220   7000
elevator_spec1_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect 6.0 300 44 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 580   4700 out of memory 0 wit inspect 270   7000
elevator_spec2_product01_true-unreach-call_true-termination.cil.c true 2 wit inspect 5.3 280 43 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 60   1400 out of memory 0 wit inspect 140   7000
elevator_spec2_product03_true-unreach-call_true-termination.cil.c true 2 wit inspect 5.6 290 51 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 71   1400 out of memory 0 wit inspect 210   7000
elevator_spec2_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect 5.3 280 42 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 59   1400 out of memory 0 wit inspect 140   7000
elevator_spec2_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect 5.3 290 39 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 96   1500 out of memory 0 wit inspect 180   7000
elevator_spec2_product17_true-unreach-call_true-termination.cil.c true 2 wit inspect 5.8 280 45 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 86   1600 out of memory 0 wit inspect 130   7000
elevator_spec2_product19_true-unreach-call_true-termination.cil.c true 2 wit inspect 5.2 280 50 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 86   1700 out of memory 0 wit inspect 140   7000
elevator_spec2_product21_true-unreach-call_true-termination.cil.c true 2 wit inspect 5.3 280 45 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 140   1900 out of memory 0 wit inspect 130   7000
elevator_spec2_product23_true-unreach-call_true-termination.cil.c true 2 wit inspect 5.5 280 44 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 130   2200 out of memory 0 wit inspect 230   7000
elevator_spec2_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect 5.3 280 40 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 80   1500 out of memory 0 wit inspect 170   7000
elevator_spec2_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect 5.9 290 43 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 86   1700 out of memory 0 wit inspect 150   7000
elevator_spec2_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect 5.6 280 38 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 180   2200 out of memory 0 wit inspect 130   7000
elevator_spec2_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect 5.6 280 46 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 150   2300 out of memory 0 wit inspect 150   7000
elevator_spec3_product01_true-unreach-call_true-termination.cil.c true 2 wit inspect 5.9 290 48 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 24   710 out of memory 0 wit inspect 200   7000
elevator_spec3_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect 5.9 290 45 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 24   770 out of memory 0 wit inspect 120   7000
elevator_spec3_product17_true-unreach-call_true-termination.cil.c true 2 wit inspect 6.2 290 50 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 23   840 out of memory 0 wit inspect 160   7000
elevator_spec3_product18_true-unreach-call_true-termination.cil.c true 2 wit inspect 6.1 290 53 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 30   1100 out of memory 0 wit inspect 170   7000
elevator_spec3_product21_true-unreach-call_true-termination.cil.c true 2 wit inspect 6.2 290 49 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 28   1100 out of memory 0 wit inspect 150   7000
elevator_spec3_product22_true-unreach-call_true-termination.cil.c true 2 wit inspect 6.2 290 55 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 37   1500 out of memory 0 wit inspect 190   7000
elevator_spec3_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect 6.0 290 51 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 27   830 out of memory 0 wit inspect 180   7000
elevator_spec3_product26_true-unreach-call_true-termination.cil.c true 2 wit inspect 6.1 290 55 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 33   1200 out of memory 0 wit inspect 220   7000
elevator_spec3_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect 6.4 290 48 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 34   1100 out of memory 0 wit inspect 160   7000
elevator_spec3_product30_true-unreach-call_true-termination.cil.c true 2 wit inspect 6.6 290 57 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 44   1400 out of memory 0 wit inspect 250   7000
elevator_spec9_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect 5.4 280 40 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 65   1400 out of memory 0 wit inspect 120   7000
elevator_spec9_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect 5.6 280 46 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 69   1600 out of memory 0 wit inspect 150   7000
elevator_spec9_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect 5.3 280 44 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 71   1600 out of memory 0 wit inspect 160   7000
elevator_spec9_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect 5.6 280 49 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 88   1700 out of memory 0 wit inspect 120   7000
elevator_spec9_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect 5.4 290 40 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 160   2300 out of memory 0 wit inspect 150   7000
elevator_spec9_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect 5.4 280 51 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 130   2200 out of memory 0 wit inspect 130   7000
email_spec0_product16_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 14   510 110 false(unreach-call) 1 wit inspect 6.8 300 unknown 0 wit inspect 48   910 unknown 0 wit inspect 6.6 280 true -32 wit inspect .99 21 - wit inspect - wit inspect
email_spec0_product21_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 12   490 97 false(unreach-call) 1 wit inspect 6.7 290 unknown 0 wit inspect 59   930 unknown 0 wit inspect 6.3 270 true -32 wit inspect 1.2  21 - wit inspect - wit inspect
email_spec0_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 14   510 130 false(unreach-call) 1 wit inspect 7.7 290 unknown 0 wit inspect 44   780 unknown 0 wit inspect 6.9 270 true -32 wit inspect 1.1  21 - wit inspect - wit inspect
email_spec0_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 14   520 120 false(unreach-call) 1 wit inspect 7.0 310 unknown 0 wit inspect 39   750 unknown 0 wit inspect 5.5 280 true -32 wit inspect 1.0  21 - wit inspect - wit inspect
email_spec0_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 15   530 140 false(unreach-call) 1 wit inspect 6.7 310 unknown 0 wit inspect 53   960 unknown 0 wit inspect 5.5 270 true -32 wit inspect 1.2  21 - wit inspect - wit inspect
email_spec0_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 14   520 130 false(unreach-call) 1 wit inspect 7.5 290 unknown 0 wit inspect 50   960 unknown 0 wit inspect 5.7 280 true -32 wit inspect 1.0  21 - wit inspect - wit inspect
email_spec0_product34_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 15   530 140 false(unreach-call) 1 wit inspect 8.8 310 unknown 0 wit inspect 65   1400 unknown 0 wit inspect 7.3 290 true -32 wit inspect 1.2  21 - wit inspect - wit inspect
email_spec0_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 18   800 140 false(unreach-call) 1 wit inspect 6.9 310 unknown 0 wit inspect 51   1300 unknown 0 wit inspect 5.7 280 true -32 wit inspect 1.3  21 - wit inspect - wit inspect
email_spec0_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 560   6200 6800 false(unreach-call) 1 wit inspect 7.7 300 unknown 0 wit inspect 48   890 unknown 0 wit inspect 5.5 270 false(unreach-call) 1 wit inspect 1.1  22 - wit inspect - wit inspect
email_spec11_product15_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 12   480 110 false(unreach-call) 1 wit inspect 6.8 310 unknown 0 wit inspect 42   750 unknown 0 wit inspect 5.3 270 false(unreach-call) 1 wit inspect 1.0  21 - wit inspect - wit inspect
email_spec11_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 11   430 99 false(unreach-call) 1 wit inspect 7.6 290 unknown 0 wit inspect 46   880 unknown 0 wit inspect 6.1 280 false(unreach-call) 1 wit inspect 1.3  21 - wit inspect - wit inspect
email_spec11_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 12   480 98 false(unreach-call) 1 wit inspect 6.6 290 unknown 0 wit inspect 40   790 unknown 0 wit inspect 6.6 280 false(unreach-call) 1 wit inspect 1.0  21 - wit inspect - wit inspect
email_spec11_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 13   490 100 false(unreach-call) 1 wit inspect 8.6 310 unknown 0 wit inspect 55   870 unknown 0 wit inspect 5.4 280 false(unreach-call) 1 wit inspect 1.1  21 - wit inspect - wit inspect
email_spec11_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 12   480 100 false(unreach-call) 1 wit inspect 6.6 290 unknown 0 wit inspect 55   840 unknown 0 wit inspect 5.6 270 false(unreach-call) 1 wit inspect 1.1  21 - wit inspect - wit inspect
email_spec11_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 13   510 100 false(unreach-call) 1 wit inspect 6.9 290 unknown 0 wit inspect 50   860 unknown 0 wit inspect 5.7 270 false(unreach-call) 1 wit inspect 1.0  21 - wit inspect - wit inspect
email_spec11_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 12   480 110 false(unreach-call) 1 wit inspect 7.7 290 unknown 0 wit inspect 47   860 unknown 0 wit inspect 5.5 280 false(unreach-call) 1 wit inspect 1.1  21 - wit inspect - wit inspect
email_spec11_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 12   480 99 false(unreach-call) 1 wit inspect 6.8 290 unknown 0 wit inspect 52   1200 unknown 0 wit inspect 5.5 280 false(unreach-call) 1 wit inspect 1.1  21 - wit inspect - wit inspect
email_spec11_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 550   6300 5500 false(unreach-call) 1 wit inspect 7.3 300 unknown 0 wit inspect 57   1100 unknown 0 wit inspect 6.6 280 false(unreach-call) 1 wit inspect 1.1  22 - wit inspect - wit inspect
email_spec1_product14_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 14   530 110 false(unreach-call) 1 wit inspect 8.6 310 true -32 wit inspect 9.4 430 unknown 0 wit inspect 5.7 280 true -32 wit inspect 1.0  22 - wit inspect - wit inspect
email_spec1_product15_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 12   450 100 false(unreach-call) 1 wit inspect 8.3 300 true -32 wit inspect 8.6 400 unknown 0 wit inspect 5.7 280 true -32 wit inspect 1.0  21 - wit inspect - wit inspect
email_spec1_product16_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 13   480 110 false(unreach-call) 1 wit inspect 7.5 300 true -32 wit inspect 8.5 390 unknown 0 wit inspect 7.2 270 true -32 wit inspect 1.3  21 - wit inspect - wit inspect
email_spec1_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 14   510 100 false(unreach-call) 1 wit inspect 7.2 300 true -32 wit inspect 11   420 unknown 0 wit inspect 5.6 270 true -32 wit inspect 1.1  21 - wit inspect - wit inspect
email_spec1_product21_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 17   790 160 false(unreach-call) 1 wit inspect 7.8 320 true -32 wit inspect 11   430 unknown 0 wit inspect 5.7 270 true -32 wit inspect 1.1  22 - wit inspect - wit inspect
email_spec1_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 12   490 110 false(unreach-call) 1 wit inspect 8.1 300 true -32 wit inspect 9.2 400 unknown 0 wit inspect 5.4 270 true -32 wit inspect 1.1  21 - wit inspect - wit inspect
email_spec1_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 14   530 130 false(unreach-call) 1 wit inspect 7.8 300 true -32 wit inspect 8.9 420 unknown 0 wit inspect 5.7 280 true -32 wit inspect 1.1  22 - wit inspect - wit inspect
email_spec1_product29_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 17   740 150 false(unreach-call) 1 wit inspect 7.5 300 true -32 wit inspect 9.3 440 unknown 0 wit inspect 5.7 270 true -32 wit inspect 1.3  22 - wit inspect - wit inspect
email_spec1_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 17   800 150 false(unreach-call) 1 wit inspect 9.3 300 true -32 wit inspect 11   410 unknown 0 wit inspect 7.2 270 true -32 wit inspect 1.1  22 - wit inspect - wit inspect
email_spec1_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 22   900 230 false(unreach-call) 1 wit inspect 7.7 310 true -32 wit inspect 9.6 440 unknown 0 wit inspect 6.4 280 true -32 wit inspect 1.2  22 - wit inspect - wit inspect
email_spec1_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 15   540 120 false(unreach-call) 1 wit inspect 7.6 310 true -32 wit inspect 11   450 unknown 0 wit inspect 5.5 270 true -32 wit inspect 1.4  22 - wit inspect - wit inspect
email_spec1_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 19   810 170 false(unreach-call) 1 wit inspect 7.9 300 true -32 wit inspect 8.6 430 unknown 0 wit inspect 6.9 280 true -32 wit inspect 1.1  22 - wit inspect - wit inspect
email_spec1_product34_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 16   580 160 false(unreach-call) 1 wit inspect 8.0 320 true -32 wit inspect 9.9 480 unknown 0 wit inspect 4.2 280 true -32 wit inspect 1.2  22 - wit inspect - wit inspect
email_spec1_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 16   580 150 false(unreach-call) 1 wit inspect 8.2 310 true -32 wit inspect 9.5 450 unknown 0 wit inspect 5.7 280 true -32 wit inspect 1.1  22 - wit inspect - wit inspect
email_spec1_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 17   730 140 false(unreach-call) 1 wit inspect 7.2 300 true -32 wit inspect 10   470 unknown 0 wit inspect 5.7 280 true -32 wit inspect 1.4  22 - wit inspect - wit inspect
email_spec27_product17_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 18   800 160 false(unreach-call) 1 wit inspect 7.7 290 true -32 wit inspect 9.5 440 unknown 0 wit inspect 6.8 270 true -32 wit inspect 1.2  22 - wit inspect - wit inspect
email_spec27_product18_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 15   540 130 false(unreach-call) 1 wit inspect 9.2 300 true -32 wit inspect 8.3 390 unknown 0 wit inspect 6.8 280 true -32 wit inspect 1.0  22 - wit inspect - wit inspect
email_spec27_product19_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 18   810 170 false(unreach-call) 1 wit inspect 7.1 300 true -32 wit inspect 9.5 410 unknown 0 wit inspect 7.6 280 true -32 wit inspect 1.1  22 - wit inspect - wit inspect
email_spec27_product23_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 14   520 120 false(unreach-call) 1 wit inspect 7.2 300 true -32 wit inspect 11   420 unknown 0 wit inspect 5.8 270 true -32 wit inspect 1.1  22 - wit inspect - wit inspect
email_spec27_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 16   550 110 false(unreach-call) 1 wit inspect 7.4 300 true -32 wit inspect 8.3 410 unknown 0 wit inspect 5.9 280 true -32 wit inspect 1.1  22 - wit inspect - wit inspect
email_spec27_product25_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 17   810 150 false(unreach-call) 1 wit