Tool VeriAbs 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* [apollon020; apollon077; apollon078; apollon084; apollon149; apollon164] apollon* [apollon037; apollon065; apollon077; apollon078; apollon155; apollon159] 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-12-02 18:04:04 CET 2017-12-03 04:46:33 CET 2017-12-03 06:08:30 CET 2017-12-03 06:21:09 CET 2017-12-03 06:27:12 CET 2017-12-03 03:55:53 CET 2017-12-03 04:55:47 CET
Run set veriabs.sv-comp18.ReachSafety-ProductLines cpa-seq-validate-violation-witnesses-veriabs.sv-comp18-violation-witness.ReachSafety-ProductLines uautomizer-validate-violation-witnesses-veriabs.sv-comp18-violation-witness.ReachSafety-ProductLines cpa-witness2test-validate-violation-witnesses-veriabs.sv-comp18-violation-witness.ReachSafety-ProductLines fshell-witness2test-validate-violation-witnesses-veriabs.sv-comp18-violation-witness.ReachSafety-ProductLines cpa-seq-validate-correctness-witnesses-veriabs.sv-comp18-correctness-witness.ReachSafety-ProductLines uautomizer-validate-correctness-witnesses-veriabs.sv-comp18-correctness-witness.ReachSafety-ProductLines
Options -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/veriabs.2017-12-02_1804.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/veriabs.2017-12-02_1804.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/veriabs.2017-12-02_1804.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/veriabs.2017-12-02_1804.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/veriabs.2017-12-02_1804.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/veriabs.2017-12-02_1804.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 unknown 0 wit inspect 380 1200 2800 error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .68 50 error (invalid witness file) 0 wit inspect .0011 .31 - wit inspect - wit inspect
elevator_spec14_product24_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 400 1400 3800 error (invalid witness file) 0 wit inspect .59 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .68 49 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect - wit inspect
elevator_spec14_product28_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 400 1200 2800 error (invalid witness file) 0 wit inspect .58 44 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .66 49 error (invalid witness file) 0 wit inspect .0028 .26 - wit inspect - wit inspect
elevator_spec14_product32_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 400 1400 3500 error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .022 4.9 error (invalid witness file) 0 wit inspect .86 49 error (invalid witness file) 0 wit inspect .0030 .26 - wit inspect - wit inspect
elevator_spec14_productSimulator_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900 5900 6900 error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .85 49 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
elevator_spec1_product18_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 210 750 2000 error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .020 5.0 error (invalid witness file) 0 wit inspect .64 49 error (invalid witness file) 0 wit inspect .0013 .28 - wit inspect - wit inspect
elevator_spec1_product20_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 210 770 2000 error (invalid witness file) 0 wit inspect .59 44 error (2) 0 wit inspect .021 4.8 error (invalid witness file) 0 wit inspect .66 50 error (invalid witness file) 0 wit inspect .0017 .26 - wit inspect - wit inspect
elevator_spec1_product22_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 210 760 2200 error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .70 49 error (invalid witness file) 0 wit inspect .0012 .33 - wit inspect - wit inspect
elevator_spec1_product24_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 210 760 2300 error (invalid witness file) 0 wit inspect .59 42 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .83 49 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
elevator_spec1_product26_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 210 760 2400 error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .84 49 error (invalid witness file) 0 wit inspect .0013 .29 - wit inspect - wit inspect
elevator_spec1_product28_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 220 780 1900 error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .68 50 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect - wit inspect
elevator_spec1_product30_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 210 780 2100 error (invalid witness file) 0 wit inspect .40 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .85 49 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
elevator_spec1_product32_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 210 760 2400 error (invalid witness file) 0 wit inspect .51 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .86 50 error (invalid witness file) 0 wit inspect .0037 .26 - wit inspect - wit inspect
elevator_spec1_productSimulator_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 690 6800 4800 error (invalid witness file) 0 wit inspect .59 42 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .83 49 error (invalid witness file) 0 wit inspect .0011 .29 - wit inspect - wit inspect
elevator_spec2_product18_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 210 850 2500 error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .020 5.0 error (invalid witness file) 0 wit inspect .81 47 error (invalid witness file) 0 wit inspect .0010 .34 - wit inspect - wit inspect
elevator_spec2_product20_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 210 810 2100 error (invalid witness file) 0 wit inspect .42 41 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .67 50 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
elevator_spec2_product22_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 210 790 1900 error (invalid witness file) 0 wit inspect .56 42 error (2) 0 wit inspect .026 4.9 error (invalid witness file) 0 wit inspect .80 47 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
elevator_spec2_product24_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 210 820 2300 error (invalid witness file) 0 wit inspect .41 41 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .85 49 error (invalid witness file) 0 wit inspect .0011 .30 - wit inspect - wit inspect
elevator_spec2_product26_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 210 760 2000 error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .66 50 error (invalid witness file) 0 wit inspect .0023 .35 - wit inspect - wit inspect
elevator_spec2_product28_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 210 760 2200 error (invalid witness file) 0 wit inspect .40 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .67 49 error (invalid witness file) 0 wit inspect .0015 .29 - wit inspect - wit inspect
elevator_spec2_product30_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 210 840 2600 error (invalid witness file) 0 wit inspect .40 44 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .66 50 error (invalid witness file) 0 wit inspect .0014 .29 - wit inspect - wit inspect
elevator_spec2_product32_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 210 830 2300 error (invalid witness file) 0 wit inspect .39 43 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .82 47 error (invalid witness file) 0 wit inspect .0018 .26 - wit inspect - wit inspect
elevator_spec2_productSimulator_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 890 7900 6000 error (invalid witness file) 0 wit inspect .54 45 error (2) 0 wit inspect .023 4.9 error (invalid witness file) 0 wit inspect .69 51 error (invalid witness file) 0 wit inspect .0011 .30 - wit inspect - wit inspect
elevator_spec3_product03_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 220 790 1400 error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .68 49 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
elevator_spec3_product11_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 210 770 1600 error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .021 4.9 error (invalid witness file) 0 wit inspect .86 50 error (invalid witness file) 0 wit inspect .0023 .29 - wit inspect - wit inspect
elevator_spec3_product19_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 210 760 1900 error (invalid witness file) 0 wit inspect .63 42 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .76 49 error (invalid witness file) 0 wit inspect .0013 .27 - wit inspect - wit inspect
elevator_spec3_product20_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 220 770 1400 error (invalid witness file) 0 wit inspect .65 43 error (2) 0 wit inspect .021 4.8 error (invalid witness file) 0 wit inspect .65 49 error (invalid witness file) 0 wit inspect .0014 .26 - wit inspect - wit inspect
elevator_spec3_product23_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 220 780 1500 error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .021 5.0 error (invalid witness file) 0 wit inspect .86 47 error (invalid witness file) 0 wit inspect .0044 .26 - wit inspect - wit inspect
elevator_spec3_product24_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 210 770 1400 error (invalid witness file) 0 wit inspect .62 44 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .66 50 error (invalid witness file) 0 wit inspect .0011 .34 - wit inspect - wit inspect
elevator_spec3_product27_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 220 760 1500 error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .020 5.0 error (invalid witness file) 0 wit inspect .85 49 error (invalid witness file) 0 wit inspect .0028 .26 - wit inspect - wit inspect
elevator_spec3_product28_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 220 760 1600 error (invalid witness file) 0 wit inspect .43 43 error (2) 0 wit inspect .045 4.8 error (invalid witness file) 0 wit inspect .65 49 error (invalid witness file) 0 wit inspect .0015 .26 - wit inspect - wit inspect
elevator_spec3_product31_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 210 750 1600 error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .020 5.0 error (invalid witness file) 0 wit inspect .87 51 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
elevator_spec3_product32_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 220 810 1500 error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .71 49 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect - wit inspect
elevator_spec3_productSimulator_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 810 7900 6400 error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .68 50 error (invalid witness file) 0 wit inspect .0012 .34 - wit inspect - wit inspect
elevator_spec9_product26_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 440 1400 3200 error (invalid witness file) 0 wit inspect .63 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .89 49 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect - wit inspect
elevator_spec9_product28_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 440 1600 3700 error (invalid witness file) 0 wit inspect .60 41 error (2) 0 wit inspect .023 4.9 error (invalid witness file) 0 wit inspect .84 47 error (invalid witness file) 0 wit inspect .0036 .34 - wit inspect - wit inspect
elevator_spec9_product30_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 440 1400 2900 error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .83 49 error (invalid witness file) 0 wit inspect .0013 .34 - wit inspect - wit inspect
elevator_spec9_product32_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 440 1500 3100 error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .030 4.8 error (invalid witness file) 0 wit inspect .65 49 error (invalid witness file) 0 wit inspect .0018 .26 - wit inspect - wit inspect
elevator_spec9_productSimulator_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900 3100 6700 error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .021 4.9 error (invalid witness file) 0 wit inspect .65 49 error (invalid witness file) 0 wit inspect .0017 .26 - wit inspect - wit inspect
elevator_spec13_product21_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 480 1600 2900 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .022 4.8
elevator_spec13_product22_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 470 1600 3800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .020 5.0
elevator_spec13_product23_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 460 2100 2500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 41 error (2) 0 wit inspect .020 4.9
elevator_spec13_product24_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 460 2000 2700 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 44 error (2) 0 wit inspect .019 4.9
elevator_spec13_product29_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 480 1600 2900 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .019 4.9
elevator_spec13_product30_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 480 1600 3100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 42 error (2) 0 wit inspect .024 4.8
elevator_spec13_product31_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 460 2100 2600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .020 4.9
elevator_spec13_product32_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 470 2000 3300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 44 error (2) 0 wit inspect .025 5.0
elevator_spec13_productSimulator_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900 2500 8000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .76 41 error (2) 0 wit inspect .019 4.9
elevator_spec14_product03_true-unreach-call_true-termination.cil.c true 2 wit inspect 120 1000 1300 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 19    570 out of memory 0 wit inspect 240     7000  
elevator_spec14_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect 120 1000 1100 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 18    640 out of memory 0 wit inspect 320     7000  
elevator_spec14_product19_true-unreach-call_true-termination.cil.c true 2 wit inspect 120 1100 1100 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 20    660 out of memory 0 wit inspect 320     7000  
elevator_spec14_product23_true-unreach-call_true-termination.cil.c true 2 wit inspect 160 1300 1600 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 29    1100 out of memory 0 wit inspect 200     7000  
elevator_spec14_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect 130 1100 1100 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 21    720 out of memory 0 wit inspect 310     7000  
elevator_spec14_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect 160 1300 1500 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 26    1100 out of memory 0 wit inspect 230     7000  
elevator_spec1_product01_true-unreach-call_true-termination.cil.c true 2 wit inspect 160 1500 1100 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 86    1500 timeout 0 wit inspect 960     5300  
elevator_spec1_product03_true-unreach-call_true-termination.cil.c true 2 wit inspect 170 1700 1400 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 86    1500 timeout 0 wit inspect 960     4600  
elevator_spec1_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect 170 1700 1400 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 69    1400 out of memory 0 wit inspect 220     7000  
elevator_spec1_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect 170 1700 1100 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 100    1600 out of memory 0 wit inspect 250     7000  
elevator_spec1_product17_true-unreach-call_true-termination.cil.c true 2 wit inspect 160 1600 1200 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 81    1500 out of memory 0 wit inspect 200     7000  
elevator_spec1_product19_true-unreach-call_true-termination.cil.c true 2 wit inspect 170 1700 1200 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 86    1700 out of memory 0 wit inspect 210     7000  
elevator_spec1_product21_true-unreach-call_true-termination.cil.c true 2 wit inspect 170 1700 1200 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 170    1900 out of memory 0 wit inspect 210     7000  
elevator_spec1_product23_true-unreach-call_true-termination.cil.c true 2 wit inspect 160 1700 1200 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 120    2000 out of memory 0 wit inspect 240     7000  
elevator_spec1_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect 160 1700 1200 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 67    1600 out of memory 0 wit inspect 170     7000  
elevator_spec1_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect 170 1700 1300 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 92    1800 out of memory 0 wit inspect 280     7000  
elevator_spec1_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect 170 1500 1300 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 200    2000 out of memory 0 wit inspect 190     7000  
elevator_spec1_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect 160 1800 1400 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 140    2100 out of memory 0 wit inspect 220     7000  
elevator_spec2_product01_true-unreach-call_true-termination.cil.c true 2 wit inspect 110 980 800 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 27    890 out of memory 0 wit inspect 140     7000  
elevator_spec2_product03_true-unreach-call_true-termination.cil.c true 2 wit inspect 120 1000 890 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 47    1100 timeout 0 wit inspect 960     4600  
elevator_spec2_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect 110 1000 720 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 30    890 out of memory 0 wit inspect 100     7000  
elevator_spec2_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect 120 1100 930 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 46    1100 timeout 0 wit inspect 960     4600  
elevator_spec2_product17_true-unreach-call_true-termination.cil.c true 2 wit inspect 110 1000 810 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 34    910 out of memory 0 wit inspect 140     7000  
elevator_spec2_product19_true-unreach-call_true-termination.cil.c true 2 wit inspect 120 1100 790 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 24    1000 out of memory 0 wit inspect 150     7000  
elevator_spec2_product21_true-unreach-call_true-termination.cil.c true 2 wit inspect 130 1200 1000 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 53    1000 out of memory 0 wit inspect 130     7000  
elevator_spec2_product23_true-unreach-call_true-termination.cil.c true 2 wit inspect 120 1200 910 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 37    1200 out of memory 0 wit inspect 230     7000  
elevator_spec2_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect 110 1000 860 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 33    950 out of memory 0 wit inspect 140     7000  
elevator_spec2_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect 120 1100 910 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 35    1000 out of memory 0 wit inspect 150     7000  
elevator_spec2_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect 130 1200 890 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 54    1200 out of memory 0 wit inspect 150     7000  
elevator_spec2_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect 130 1300 940 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 49    1100 out of memory 0 wit inspect 220     7000  
elevator_spec3_product01_true-unreach-call_true-termination.cil.c true 2 wit inspect 93 750 640 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 12    660 out of memory 0 wit inspect 190     7000  
elevator_spec3_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect 100 770 780 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 18    650 out of memory 0 wit inspect 150     7000  
elevator_spec3_product17_true-unreach-call_true-termination.cil.c true 2 wit inspect 95 780 700 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 22    620 out of memory 0 wit inspect 160     7000  
elevator_spec3_product18_true-unreach-call_true-termination.cil.c true 2 wit inspect 100 860 800 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 29    990 out of memory 0 wit inspect 160     7000  
elevator_spec3_product21_true-unreach-call_true-termination.cil.c true 2 wit inspect 110 840 780 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 27    780 out of memory 0 wit inspect 130     7000  
elevator_spec3_product22_true-unreach-call_true-termination.cil.c true 2 wit inspect 110 1000 790 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 30    1300 out of memory 0 wit inspect 200     7000  
elevator_spec3_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect 95 770 700 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 23    730 out of memory 0 wit inspect 160     7000  
elevator_spec3_product26_true-unreach-call_true-termination.cil.c true 2 wit inspect 110 920 740 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 30    1100 out of memory 0 wit inspect 180     7000  
elevator_spec3_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect 100 830 810 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 24    920 out of memory 0 wit inspect 120     7000  
elevator_spec3_product30_true-unreach-call_true-termination.cil.c true 2 wit inspect 110 1000 830 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 38    1700 out of memory 0 wit inspect 210     7000  
elevator_spec9_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect 350 1000 2000 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 30    810 out of memory 0 wit inspect 160     7000  
elevator_spec9_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect 340 1100 2000 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 32    930 out of memory 0 wit inspect 100     7000  
elevator_spec9_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect 350 1100 2300 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 30    940 out of memory 0 wit inspect 140     7000  
elevator_spec9_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect 360 1100 2000 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 36    1100 out of memory 0 wit inspect 170     7000  
elevator_spec9_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect 350 1200 2200 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 37    1200 out of memory 0 wit inspect 190     7000  
elevator_spec9_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect 360 1300 2200 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 38    1200 out of memory 0 wit inspect 140     7000  
email_spec0_product16_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 500 3800 5500 error (invalid witness file) 0 wit inspect .61 42 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .89 49 error (invalid witness file) 0 wit inspect .0013 .28 - wit inspect - wit inspect
email_spec0_product21_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 530 3900 5900 error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .87 49 error (invalid witness file) 0 wit inspect .0015 .28 - wit inspect - wit inspect
email_spec0_product22_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 500 3900 5900 error (invalid witness file) 0 wit inspect .41 41 error (2) 0 wit inspect .024 5.0 error (invalid witness file) 0 wit inspect .84 49 error (invalid witness file) 0 wit inspect .0011 .28 - wit inspect - wit inspect
email_spec0_product26_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 520 4000 5500 error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .023 5.0 error (invalid witness file) 0 wit inspect .67 49 error (invalid witness file) 0 wit inspect .0012 .34 - wit inspect - wit inspect
email_spec0_product31_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 510 3800 5800 error (invalid witness file) 0 wit inspect .43 41 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .83 49 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
email_spec0_product33_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 510 3800 5800 error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .66 49 error (invalid witness file) 0 wit inspect .0040 .26 - wit inspect - wit inspect
email_spec0_product34_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 540 3900 5600 error (invalid witness file) 0 wit inspect .41 43 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .66 49 error (invalid witness file) 0 wit inspect .0012 .34 - wit inspect - wit inspect
email_spec0_product35_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 550 4000 6200 error (invalid witness file) 0 wit inspect .51 42 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .81 48 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
email_spec0_productSimulator_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900 2500 6300 error (invalid witness file) 0 wit inspect .61 42 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .72 50 error (invalid witness file) 0 wit inspect .0017 .30 - wit inspect - wit inspect
email_spec11_product15_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 500 3800 6100 error (invalid witness file) 0 wit inspect .58 41 error (2) 0 wit inspect .024 5.0 error (invalid witness file) 0 wit inspect .85 47 error (invalid witness file) 0 wit inspect .0010 .26 - wit inspect - wit inspect
email_spec11_product20_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 510 3900 6800 error (invalid witness file) 0 wit inspect .56 42 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .65 49 error (invalid witness file) 0 wit inspect .0033 .28 - wit inspect - wit inspect
email_spec11_product22_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 500 3900 5300 error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .65 49 error (invalid witness file) 0 wit inspect .0011 .28 - wit inspect - wit inspect
email_spec11_product26_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 530 3900 5700 error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .65 49 error (invalid witness file) 0 wit inspect .0012 .28 - wit inspect - wit inspect
email_spec11_product30_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 510 3800 5700 error (invalid witness file) 0 wit inspect .39 41 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .65 49 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
email_spec11_product32_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 540 3900 5100 error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .81 47 error (invalid witness file) 0 wit inspect .0019 .29 - wit inspect - wit inspect
email_spec11_product33_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 510 3900 5400 error (invalid witness file) 0 wit inspect .41 43 error (2) 0 wit inspect .020 5.0 error (invalid witness file) 0 wit inspect .85 49 error (invalid witness file) 0 wit inspect .0012 .34 - wit inspect - wit inspect
email_spec11_product35_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 550 3900 6600 error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .022 4.8 error (invalid witness file) 0 wit inspect .84 50 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect - wit inspect
email_spec11_productSimulator_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900 2500 5700 error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .67 49 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
email_spec1_product14_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 500 3900 4900 error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .023 5.0 error (invalid witness file) 0 wit inspect .81 51 error (invalid witness file) 0 wit inspect .0018 .28 - wit inspect - wit inspect
email_spec1_product15_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 510 3800 5800 error (invalid witness file) 0 wit inspect .59 45 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .67 50 error (invalid witness file) 0 wit inspect .0010 .29 - wit inspect - wit inspect
email_spec1_product16_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 500 3800 5200 error (invalid witness file) 0 wit inspect .40 43 error (2) 0 wit inspect .021 4.9 error (invalid witness file) 0 wit inspect .64 49 error (invalid witness file) 0 wit inspect .0035 .26 - wit inspect - wit inspect
email_spec1_product20_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 520 3900 6600 error (invalid witness file) 0 wit inspect .60 43 error (2) 0 wit inspect .020 5.0 error (invalid witness file) 0 wit inspect .88 49 error (invalid witness file) 0 wit inspect .0012 .28 - wit inspect - wit inspect
email_spec1_product21_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 530 3900 6100 error (invalid witness file) 0 wit inspect .40 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .81 47 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
email_spec1_product22_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 500 3900 6200 error (invalid witness file) 0 wit inspect .56 42 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .70 49 error (invalid witness file) 0 wit inspect .0028 .26 - wit inspect - wit inspect
email_spec1_product26_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 520 3900 6500 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .86 47 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect - wit inspect
email_spec1_product29_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 510 3900 5700 error (invalid witness file) 0 wit inspect .43 43 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .86 49 error (invalid witness file) 0 wit inspect .0012 .27 - wit inspect - wit inspect
email_spec1_product30_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 500 3800 5300 error (invalid witness file) 0 wit inspect .41 44 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .70 49 error (invalid witness file) 0 wit inspect .0015 .26 - wit inspect - wit inspect
email_spec1_product31_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 510 3800 5400 error (invalid witness file) 0 wit inspect .41 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .65 52 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect - wit inspect
email_spec1_product32_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 530 3900 5700 error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .017 4.9 error (invalid witness file) 0 wit inspect .83 50 error (invalid witness file) 0 wit inspect .0033 .30 - wit inspect - wit inspect
email_spec1_product33_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 510 3900 5800 error (invalid witness file) 0 wit inspect .59 41 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .86 47 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
email_spec1_product34_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 540 3900 5800 error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .023 4.9 error (invalid witness file) 0 wit inspect .86 49 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
email_spec1_product35_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 550 4000 6500 error (invalid witness file) 0 wit inspect .58 42 error (2) 0 wit inspect .017 4.8 error (invalid witness file) 0 wit inspect .69 49 error (invalid witness file) 0 wit inspect .0042 .34 - wit inspect - wit inspect
email_spec1_productSimulator_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900 4500 8100 error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .68 49 error (invalid witness file) 0 wit inspect .0036 .31 - wit inspect - wit inspect
email_spec27_product17_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 510 3900 5500 error (invalid witness file) 0 wit inspect .58 41 error (2) 0 wit inspect .022 4.9 error (invalid witness file) 0 wit inspect .82 47 error (invalid witness file) 0 wit inspect .0013 .27 - wit inspect - wit inspect
email_spec27_product18_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 500 3800 6200 error (invalid witness file) 0 wit inspect .57 42 error (2) 0 wit inspect .021 4.8 error (invalid witness file) 0 wit inspect .84 49 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
email_spec27_product19_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 510 3800 5300 error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .021 4.9 error (invalid witness file) 0 wit inspect .83 49 error (invalid witness file) 0 wit inspect .0014 .29 - wit inspect - wit inspect
email_spec27_product23_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 520 3900 5600 error (invalid witness file) 0 wit inspect .57 42 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .66 49 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
email_spec27_product24_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 510 3800 5500 error (invalid witness file) 0 wit inspect .62 41 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .86 49 error (invalid witness file) 0 wit inspect .0013 .31 - wit inspect - wit inspect
email_spec27_product25_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 530 3900 5500 error (invalid witness file) 0 wit inspect .69 42 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .88 47 error (invalid witness file) 0 wit inspect .0015 .29 - wit inspect - wit inspect
email_spec27_product27_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 540 4000 6500 error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .93 49 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
email_spec27_product29_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 510 3900 5300 error (invalid witness file) 0 wit inspect .39 42