Tool CBMC 5.8 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:26:01 CET 2017-12-01 07:56:00 CET 2017-12-01 08:08:00 CET 2017-12-01 08:15:34 CET 2017-12-01 04:22:29 CET 2017-12-01 07:31:28 CET
Run set cbmc.sv-comp18.ReachSafety-ProductLines cpa-seq-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.ReachSafety-ProductLines uautomizer-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.ReachSafety-ProductLines cpa-witness2test-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.ReachSafety-ProductLines fshell-witness2test-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.ReachSafety-ProductLines cpa-seq-validate-correctness-witnesses-cbmc.sv-comp18-correctness-witness.ReachSafety-ProductLines uautomizer-validate-correctness-witnesses-cbmc.sv-comp18-correctness-witness.ReachSafety-ProductLines
Options --graphml-witness witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cbmc.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/cbmc.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cbmc.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/cbmc.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cbmc.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/cbmc.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 .45 42 4.5 true -32 wit inspect 8.7  410 true -32 wit inspect 10     450   unknown 0 wit inspect 25    1600 false(unreach-call) 1 wit inspect 1.3    20    - wit inspect - wit inspect
elevator_spec14_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .51 42 4.9 true -32 wit inspect 9.2  410 true -32 wit inspect 10     450   unknown 0 wit inspect 26    1500 false(unreach-call) 1 wit inspect 1.2    20    - wit inspect - wit inspect
elevator_spec14_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .47 42 4.3 true -32 wit inspect 9.5  430 true -32 wit inspect 10     450   unknown 0 wit inspect 27    1600 false(unreach-call) 1 wit inspect 1.0    20    - wit inspect - wit inspect
elevator_spec14_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .47 42 4.6 true -32 wit inspect 9.0  410 true -32 wit inspect 10     460   unknown 0 wit inspect 26    1500 false(unreach-call) 1 wit inspect 1.4    20    - wit inspect - wit inspect
elevator_spec14_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 11    450 110   true -32 wit inspect 5.6  280 true -32 wit inspect 9.1   420   unknown 0 wit inspect 29    2000 false(unreach-call) 1 wit inspect 1.2    21    - wit inspect - wit inspect
elevator_spec1_product18_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.2  42 13   true -32 wit inspect 6.5  280 true -32 wit inspect 8.2   370   unknown 0 wit inspect 18    1300 false(unreach-call) 1 wit inspect 1.1    20    - wit inspect - wit inspect
elevator_spec1_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.2  42 13   true -32 wit inspect 7.1  300 true -32 wit inspect 9.7   410   unknown 0 wit inspect 35    1700 false(unreach-call) 1 wit inspect 1.5    20    - wit inspect - wit inspect
elevator_spec1_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.2  42 12   true -32 wit inspect 6.2  280 true -32 wit inspect 8.6   410   unknown 0 wit inspect 25    1700 false(unreach-call) 1 wit inspect 1.1    20    - wit inspect - wit inspect
elevator_spec1_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.3  43 16   true -32 wit inspect 7.2  280 true -32 wit inspect 9.6   400   unknown 0 wit inspect 31    2000 false(unreach-call) 1 wit inspect 1.2    20    - wit inspect - wit inspect
elevator_spec1_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.2  42 14   true -32 wit inspect 6.4  290 true -32 wit inspect 8.8   380   unknown 0 wit inspect 28    1600 false(unreach-call) 1 wit inspect 1.1    20    - wit inspect - wit inspect
elevator_spec1_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.2  42 13   true -32 wit inspect 6.3  280 true -32 wit inspect 10     390   unknown 0 wit inspect 29    2000 false(unreach-call) 1 wit inspect 1.1    20    - wit inspect - wit inspect
elevator_spec1_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.2  42 12   true -32 wit inspect 6.6  300 true -32 wit inspect 9.5   380   unknown 0 wit inspect 26    1700 false(unreach-call) 1 wit inspect 1.4    20    - wit inspect - wit inspect
elevator_spec1_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.3  43 16   true -32 wit inspect 7.4  300 true -32 wit inspect 9.0   420   unknown 0 wit inspect 30    2100 false(unreach-call) 1 wit inspect 1.2    21    - wit inspect - wit inspect
elevator_spec1_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 85    1200 760   true -32 wit inspect 6.3  280 true -32 wit inspect 10     430   unknown 0 wit inspect 34    1900 false(unreach-call) 1 wit inspect 1.1    20    - wit inspect - wit inspect
elevator_spec2_product18_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.2  42 12   true -32 wit inspect 8.4  340 true -32 wit inspect 9.0   390   unknown 0 wit inspect 24    1200 false(unreach-call) 1 wit inspect 1.2    20    - wit inspect - wit inspect
elevator_spec2_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.2  42 12   true -32 wit inspect 9.7  430 true -32 wit inspect 11     410   unknown 0 wit inspect 28    1800 false(unreach-call) 1 wit inspect 1.2    20    - wit inspect - wit inspect
elevator_spec2_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.2  42 12   true -32 wit inspect 9.8  320 true -32 wit inspect 10     380   unknown 0 wit inspect 29    1600 false(unreach-call) 1 wit inspect 1.2    20    - wit inspect - wit inspect
elevator_spec2_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.3  43 13   true -32 wit inspect 12    430 true -32 wit inspect 8.7   410   unknown 0 wit inspect 39    1900 false(unreach-call) 1 wit inspect 1.4    20    - wit inspect - wit inspect
elevator_spec2_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.2  42 11   true -32 wit inspect 7.9  320 true -32 wit inspect 8.9   380   unknown 0 wit inspect 23    1600 false(unreach-call) 1 wit inspect 1.1    20    - wit inspect - wit inspect
elevator_spec2_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.2  42 13   true -32 wit inspect 10    410 true -32 wit inspect 9.5   410   unknown 0 wit inspect 31    1900 false(unreach-call) 1 wit inspect 1.1    20    - wit inspect - wit inspect
elevator_spec2_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.2  42 14   true -32 wit inspect 7.7  300 true -32 wit inspect 9.1   390   unknown 0 wit inspect 27    1800 false(unreach-call) 1 wit inspect 1.3    20    - wit inspect - wit inspect
elevator_spec2_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.2  43 14   true -32 wit inspect 9.4  430 true -32 wit inspect 9.2   410   unknown 0 wit inspect 33    2200 false(unreach-call) 1 wit inspect 1.1    21    - wit inspect - wit inspect
elevator_spec2_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 48    930 380   true -32 wit inspect 5.4  280 true -32 wit inspect 8.3   430   unknown 0 wit inspect 32    2100 false(unreach-call) 1 wit inspect 1.5    21    - wit inspect - wit inspect
elevator_spec3_product03_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .65 43 6.4 true -32 wit inspect 8.1  280 true -32 wit inspect 9.3   460   unknown 0 wit inspect 39    2000 false(unreach-call) 1 wit inspect 1.1    21    - wit inspect - wit inspect
elevator_spec3_product11_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .61 43 5.7 true -32 wit inspect 6.9  280 true -32 wit inspect 12     450   unknown 0 wit inspect 32    2200 false(unreach-call) 1 wit inspect 1.1    21    - wit inspect - wit inspect
elevator_spec3_product19_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .66 43 7.3 true -32 wit inspect 6.6  280 true -32 wit inspect 8.8   460   unknown 0 wit inspect 32    2000 false(unreach-call) 1 wit inspect 1.1    21    - wit inspect - wit inspect
elevator_spec3_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .67 43 7.1 true -32 wit inspect 6.6  280 true -32 wit inspect 12     460   unknown 0 wit inspect 43    2300 false(unreach-call) 1 wit inspect 1.1    22    - wit inspect - wit inspect
elevator_spec3_product23_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .68 44 6.4 true -32 wit inspect 7.5  280 true -32 wit inspect 9.0   460   unknown 0 wit inspect 48    2200 false(unreach-call) 1 wit inspect 1.2    21    - wit inspect - wit inspect
elevator_spec3_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .69 44 8.0 true -32 wit inspect 7.2  310 true -32 wit inspect 9.9   460   unknown 0 wit inspect 39    2100 false(unreach-call) 1 wit inspect 1.3    22    - wit inspect - wit inspect
elevator_spec3_product27_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .64 43 6.4 true -32 wit inspect 6.8  280 true -32 wit inspect 9.2   460   unknown 0 wit inspect 41    2200 false(unreach-call) 1 wit inspect 1.4    21    - wit inspect - wit inspect
elevator_spec3_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .64 43 7.5 true -32 wit inspect 7.4  280 true -32 wit inspect 9.2   450   unknown 0 wit inspect 31    2300 false(unreach-call) 1 wit inspect 1.2    22    - wit inspect - wit inspect
elevator_spec3_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .68 44 7.2 true -32 wit inspect 7.3  280 true -32 wit inspect 12     460   unknown 0 wit inspect 36    2300 false(unreach-call) 1 wit inspect 1.2    21    - wit inspect - wit inspect
elevator_spec3_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .65 44 8.1 true -32 wit inspect 6.9  290 true -32 wit inspect 9.9   460   unknown 0 wit inspect 48    2500 false(unreach-call) 1 wit inspect 1.2    22    - wit inspect - wit inspect
elevator_spec3_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 43    950 410   true -32 wit inspect 6.4  280 true -32 wit inspect 9.1   470   unknown 0 wit inspect 51    2500 false(unreach-call) 1 wit inspect 1.2    22    - wit inspect - wit inspect
elevator_spec9_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.2  44 13   true -32 wit inspect 9.9  350 true -32 wit inspect 11     400   unknown 0 wit inspect 27    1800 false(unreach-call) 1 wit inspect 1.1    20    - wit inspect - wit inspect
elevator_spec9_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.3  42 14   true -32 wit inspect 10    430 true -32 wit inspect 9.1   390   unknown 0 wit inspect 31    1800 false(unreach-call) 1 wit inspect 1.1    21    - wit inspect - wit inspect
elevator_spec9_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.2  42 13   true -32 wit inspect 8.6  310 true -32 wit inspect 8.6   380   unknown 0 wit inspect 29    1800 false(unreach-call) 1 wit inspect 1.2    20    - wit inspect - wit inspect
elevator_spec9_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.3  42 13   true -32 wit inspect 9.8  410 true -32 wit inspect 9.0   390   unknown 0 wit inspect 31    2200 false(unreach-call) 1 wit inspect 1.6    21    - wit inspect - wit inspect
elevator_spec9_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 47    930 450   true -32 wit inspect 7.1  270 true -32 wit inspect 12     450   unknown 0 wit inspect 51    2400 true -32 wit inspect 1.3    21    - wit inspect - wit inspect
elevator_spec13_product21_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    12000 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .023 4.8
elevator_spec13_product22_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    12000 14000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .018 4.8
elevator_spec13_product23_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 750    15000 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 44 error (2) 0 wit inspect .023 4.9
elevator_spec13_product24_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 760    15000 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .024 4.8
elevator_spec13_product29_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 880    12000 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .018 4.8
elevator_spec13_product30_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 880    12000 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 42 error (2) 0 wit inspect .042 4.8
elevator_spec13_product31_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 750    15000 9700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 41 error (2) 0 wit inspect .020 4.9
elevator_spec13_product32_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 750    15000 9800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .020 4.9
elevator_spec13_productSimulator_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    460 9900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 44 error (2) 0 wit inspect .048 4.8
elevator_spec14_product03_true-unreach-call_true-termination.cil.c true 1 wit inspect 3.3  47 37   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5500 out of memory 0 wit inspect 300     7000  
elevator_spec14_product11_true-unreach-call_true-termination.cil.c true 1 wit inspect 3.3  47 42   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5500 out of memory 0 wit inspect 280     7000  
elevator_spec14_product19_true-unreach-call_true-termination.cil.c true 1 wit inspect 3.4  47 37   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5500 out of memory 0 wit inspect 280     7000  
elevator_spec14_product23_true-unreach-call_true-termination.cil.c true 1 wit inspect 3.5  47 44   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5500 out of memory 0 wit inspect 220     7000  
elevator_spec14_product27_true-unreach-call_true-termination.cil.c true 1 wit inspect 3.5  47 40   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5500 out of memory 0 wit inspect 290     7000  
elevator_spec14_product31_true-unreach-call_true-termination.cil.c true 1 wit inspect 3.4  47 44   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5500 out of memory 0 wit inspect 200     7000  
elevator_spec1_product01_true-unreach-call_true-termination.cil.c true 1 wit inspect 2.8  45 27   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5500 out of memory 0 wit inspect 270     7000  
elevator_spec1_product03_true-unreach-call_true-termination.cil.c true 1 wit inspect 3.0  45 34   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5500 out of memory 0 wit inspect 250     7000  
elevator_spec1_product09_true-unreach-call_true-termination.cil.c true 1 wit inspect 2.8  45 36   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    5500 out of memory 0 wit inspect 340     7000  
elevator_spec1_product11_true-unreach-call_true-termination.cil.c true 1 wit inspect 3.1  45 33   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    5500 out of memory 0 wit inspect 260     7000  
elevator_spec1_product17_true-unreach-call_true-termination.cil.c true 1 wit inspect 2.9  45 30   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5500 out of memory 0 wit inspect 270     7000  
elevator_spec1_product19_true-unreach-call_true-termination.cil.c true 1 wit inspect 3.1  46 45   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    5500 out of memory 0 wit inspect 230     7000  
elevator_spec1_product21_true-unreach-call_true-termination.cil.c true 1 wit inspect 3.0  45 39   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5500 out of memory 0 wit inspect 240     7000  
elevator_spec1_product23_true-unreach-call_true-termination.cil.c true 1 wit inspect 3.2  47 39   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5500 out of memory 0 wit inspect 240     7000  
elevator_spec1_product25_true-unreach-call_true-termination.cil.c true 1 wit inspect 3.0  45 33   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5400 out of memory 0 wit inspect 200     7000  
elevator_spec1_product27_true-unreach-call_true-termination.cil.c true 1 wit inspect 3.1  46 37   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5500 out of memory 0 wit inspect 270     7000  
elevator_spec1_product29_true-unreach-call_true-termination.cil.c true 1 wit inspect 3.1  46 39   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5500 out of memory 0 wit inspect 190     7000  
elevator_spec1_product31_true-unreach-call_true-termination.cil.c true 1 wit inspect 3.3  47 41   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5500 out of memory 0 wit inspect 270     7000  
elevator_spec2_product01_true-unreach-call_true-termination.cil.c true 1 wit inspect 1.6  42 18   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5500 out of memory 0 wit inspect 150     7000  
elevator_spec2_product03_true-unreach-call_true-termination.cil.c true 1 wit inspect 1.6  42 22   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960    5500 out of memory 0 wit inspect 160     7000  
elevator_spec2_product09_true-unreach-call_true-termination.cil.c true 1 wit inspect 1.5  42 16   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5500 out of memory 0 wit inspect 140     7000  
elevator_spec2_product11_true-unreach-call_true-termination.cil.c true 1 wit inspect 1.7  43 18   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5500 out of memory 0 wit inspect 170     7000  
elevator_spec2_product17_true-unreach-call_true-termination.cil.c true 1 wit inspect 1.6  42 16   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 940    5500 out of memory 0 wit inspect 130     7000  
elevator_spec2_product19_true-unreach-call_true-termination.cil.c true 1 wit inspect 1.6  43 20   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5500 out of memory 0 wit inspect 200     7000  
elevator_spec2_product21_true-unreach-call_true-termination.cil.c true 1 wit inspect 1.6  43 18   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5500 out of memory 0 wit inspect 140     7000  
elevator_spec2_product23_true-unreach-call_true-termination.cil.c true 1 wit inspect 1.7  43 16   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    5500 out of memory 0 wit inspect 230     7000  
elevator_spec2_product25_true-unreach-call_true-termination.cil.c true 1 wit inspect 1.6  42 18   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 940    5500 out of memory 0 wit inspect 140     7000  
elevator_spec2_product27_true-unreach-call_true-termination.cil.c true 1 wit inspect 1.7  43 17   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5500 out of memory 0 wit inspect 150     7000  
elevator_spec2_product29_true-unreach-call_true-termination.cil.c true 1 wit inspect 1.7  43 17   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5500 out of memory 0 wit inspect 130     7000  
elevator_spec2_product31_true-unreach-call_true-termination.cil.c true 1 wit inspect 1.8  43 18   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5500 out of memory 0 wit inspect 150     7000  
elevator_spec3_product01_true-unreach-call_true-termination.cil.c true 1 wit inspect 3.5  47 40   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5500 out of memory 0 wit inspect 150     7000  
elevator_spec3_product09_true-unreach-call_true-termination.cil.c true 1 wit inspect 3.5  47 40   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5500 out of memory 0 wit inspect 160     7000  
elevator_spec3_product17_true-unreach-call_true-termination.cil.c true 1 wit inspect 3.5  47 37   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5500 out of memory 0 wit inspect 190     7000  
elevator_spec3_product18_true-unreach-call_true-termination.cil.c true 1 wit inspect 3.6  47 41   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5400 out of memory 0 wit inspect 160     7000  
elevator_spec3_product21_true-unreach-call_true-termination.cil.c true 1 wit inspect 3.9  50 42   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5500 out of memory 0 wit inspect 140     7000  
elevator_spec3_product22_true-unreach-call_true-termination.cil.c true 1 wit inspect 4.0  49 46   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    5500 out of memory 0 wit inspect 240     7000  
elevator_spec3_product25_true-unreach-call_true-termination.cil.c true 1 wit inspect 3.6  47 44   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5500 out of memory 0 wit inspect 170     7000  
elevator_spec3_product26_true-unreach-call_true-termination.cil.c true 1 wit inspect 3.6  48 50   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    5400 out of memory 0 wit inspect 200     7000  
elevator_spec3_product29_true-unreach-call_true-termination.cil.c true 1 wit inspect 3.9  50 47   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5500 out of memory 0 wit inspect 110     7000  
elevator_spec3_product30_true-unreach-call_true-termination.cil.c true 1 wit inspect 4.0  50 52   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5500 out of memory 0 wit inspect 210     7000  
elevator_spec9_product09_true-unreach-call_true-termination.cil.c true 1 wit inspect 1.5  42 18   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 930    5500 out of memory 0 wit inspect 190     7000  
elevator_spec9_product11_true-unreach-call_true-termination.cil.c true 1 wit inspect 1.7  44 17   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5500 out of memory 0 wit inspect 140     7000  
elevator_spec9_product25_true-unreach-call_true-termination.cil.c true 1 wit inspect 1.6  42 19   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 930    5500 out of memory 0 wit inspect 180     7000  
elevator_spec9_product27_true-unreach-call_true-termination.cil.c true 1 wit inspect 1.7  43 18   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5500 out of memory 0 wit inspect 130     7000  
elevator_spec9_product29_true-unreach-call_true-termination.cil.c true 1 wit inspect 1.7  43 16   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    5500 out of memory 0 wit inspect 180     7000  
elevator_spec9_product31_true-unreach-call_true-termination.cil.c true 1 wit inspect 1.8  43 17   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5500 out of memory 0 wit inspect 140     7000  
email_spec0_product16_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 3.1  55 25   true -32 wit inspect 13    410 true -32 wit inspect 8.9   400   unknown 0 wit inspect 9.3  310 true -32 wit inspect 1.2    20    - wit inspect - wit inspect
email_spec0_product21_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 4.5  64 70   true -32 wit inspect 5.9  280 true -32 wit inspect 9.2   430   unknown 0 wit inspect 9.6  400 true -32 wit inspect 1.3    21    - wit inspect - wit inspect
email_spec0_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.1  56 32   true -32 wit inspect 12    410 true -32 wit inspect 9.8   410   unknown 0 wit inspect 10    420 false(unreach-call) 1 wit inspect 1.2    20    - wit inspect - wit inspect
email_spec0_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 5.0  65 57   true -32 wit inspect 6.7  270 true -32 wit inspect 9.8   440   unknown 0 wit inspect 9.5  430 true -32 wit inspect 1.5    21    - wit inspect - wit inspect
email_spec0_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 3.4  57 37   true -32 wit inspect 13    440 true -32 wit inspect 10     420   unknown 0 wit inspect 8.3  420 true -32 wit inspect 1.3    20    - wit inspect - wit inspect
email_spec0_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 3.6  60 41   true -32 wit inspect 5.8  280 true -32 wit inspect 8.9   440   unknown 0 wit inspect 7.4  430 true -32 wit inspect 1.2    20    - wit inspect - wit inspect
email_spec0_product34_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 6.0  76 64   true -32 wit inspect 6.5  280 true -32 wit inspect 11     470   unknown 0 wit inspect 12    470 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 6.4  77 73   true -32 wit inspect 17    590 true -32 wit inspect 7.7   470   unknown 0 wit inspect 9.2  430 false(unreach-call) 1 wit inspect 1.1    20    - wit inspect - wit inspect
email_spec0_productSimulator_false-unreach-call_true-termination.cil.c error (42) 0 wit inspect 870    1800 5200   error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .022 4.8 error (invalid witness file) 0 wit inspect .92 49 error (invalid witness file) 0 wit inspect .0019 .29 - wit inspect - wit inspect
email_spec11_product15_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 3.0  56 34   true -32 wit inspect 6.4  260 true -32 wit inspect 8.5   370   unknown 0 wit inspect 7.2  290 true -32 wit inspect 1.3    20    - wit inspect - wit inspect
email_spec11_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 4.1  63 42   true -32 wit inspect 5.6  260 true -32 wit inspect 9.3   410   unknown 0 wit inspect 9.2  430 false(unreach-call) 1 wit inspect 1.1    20    - wit inspect - wit inspect
email_spec11_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 3.1  56 31   true -32 wit inspect 7.5  290 true -32 wit inspect 10     420   unknown 0 wit inspect 8.8  310 true -32 wit inspect 1.1    20    - wit inspect - wit inspect
email_spec11_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 4.9  65 54   true -32 wit inspect 6.9  270 true -32 wit inspect 9.0   410   unknown 0 wit inspect 11    410 false(unreach-call) 1 wit inspect 1.4    20    - wit inspect - wit inspect
email_spec11_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 3.2  57 41   true -32 wit inspect 6.7  290 true -32 wit inspect 8.1   410   unknown 0 wit inspect 8.4  420 true -32 wit inspect 1.1    20    - wit inspect - wit inspect
email_spec11_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 5.3  70 62   true -32 wit inspect 6.0  280 true -32 wit inspect 11     450   unknown 0 wit inspect 11    420 false(unreach-call) 1 wit inspect 1.5    21    - wit inspect - wit inspect
email_spec11_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.5  58 38   true -32 wit inspect 5.9  270 true -32 wit inspect 11     420   unknown 0 wit inspect 7.7  360 false(unreach-call) 1 wit inspect 1.2    20    - wit inspect - wit inspect
email_spec11_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 6.5  77 77   true -32 wit inspect 7.0  270 true -32 wit inspect 9.4   470   unknown 0 wit inspect 11    480 true -32 wit inspect 1.2    20    - wit inspect - wit inspect
email_spec11_productSimulator_false-unreach-call_true-termination.cil.c error (42) 0 wit inspect 870    2200 5000   error (invalid witness file) 0 wit inspect .52 44 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 .26 - wit inspect - wit inspect
email_spec1_product14_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 2.8  55 37   true -32 wit inspect 6.3  270 true -32 wit inspect 8.8   400   unknown 0 wit inspect 8.7  420 true -32 wit inspect 1.1    20    - wit inspect - wit inspect
email_spec1_product15_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 2.8  54 29   true -32 wit inspect 5.8  270 true -32 wit inspect 8.7   400   unknown 0 wit inspect 10    450 true -32 wit inspect 1.5    20    - wit inspect - wit inspect
email_spec1_product16_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 3.0  54 35   true -32 wit inspect 9.2  280 true -32 wit inspect 8.7   410   unknown 0 wit inspect 12    470 true -32 wit inspect 1.3    21    - wit inspect - wit inspect
email_spec1_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 4.1  61 46   true -32 wit inspect 15    490 true -32 wit inspect 8.5   420   unknown 0 wit inspect 12    410 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 4.6  63 50   true -32 wit inspect 20    580 true -32 wit inspect 9.5   430   unknown 0 wit inspect 11    470 false(unreach-call) 1 wit inspect 1.5    21    - wit inspect - wit inspect
email_spec1_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.1  56 32   true -32 wit inspect 6.8  270 true -32 wit inspect 11     400   unknown 0 wit inspect 8.9  420 false(unreach-call) 1 wit inspect 1.1    20    - wit inspect - wit inspect
email_spec1_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 4.9  64 62   true -32 wit inspect 6.2  290 true -32 wit inspect 11     420   unknown 0 wit inspect 11    370 false(unreach-call) 1 wit inspect 1.5    20    - wit inspect - wit inspect
email_spec1_product29_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.3  56 42   true -32 wit inspect 7.5  280 true -32 wit inspect 9.3   440   unknown 0 wit inspect 11    380 false(unreach-call) 1 wit inspect 1.2    21    - wit inspect - wit inspect
email_spec1_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.2  54 33   true -32 wit inspect 5.8  270 true -32 wit inspect 9.8   390   unknown 0 wit inspect 9.5  420 false(unreach-call) 1 wit inspect 1.3    20    - wit inspect - wit inspect
email_spec1_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 3.4  56 41   true -32 wit inspect 15    390 true -32 wit inspect 8.5   430   unknown 0 wit inspect 11    470 error (2) 0 wit inspect 1.4    21    - wit inspect - wit inspect
email_spec1_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 5.2  67 60   true -32 wit inspect 6.1  280 true -32 wit inspect 9.6   430   unknown 0 wit inspect 15    470 true -32 wit inspect 1.2    21    - wit inspect - wit inspect
email_spec1_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.6  56 41   true -32 wit inspect 6.0  270 true -32 wit inspect 11     440   unknown 0 wit inspect 12    460 false(unreach-call) 1 wit inspect 1.2    20    - wit inspect - wit inspect
email_spec1_product34_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 6.0  72 66   true -32 wit inspect 5.9  280 true -32 wit inspect 9.9   460   unknown 0 wit inspect 11    470 true -32 wit inspect 1.5    20    - wit inspect - wit inspect
email_spec1_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 6.4  74 94   true -32 wit inspect 7.4  280 true -32 wit inspect 8.8   450   unknown 0 wit inspect 19    880 true -32 wit inspect 1.5    22    - wit inspect - wit inspect
email_spec1_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 130    640 1700   true -32 wit inspect 5.9  280 true -32 wit inspect 11     460   unknown 0 wit inspect 15    610 false(unreach-call) 1 wit inspect 1.2    21    - wit inspect - wit inspect
email_spec27_product17_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.1  57 34   true -32 wit inspect 6.1  270 unknown 0 wit inspect 50     640   unknown 0 wit inspect 9.4  430 false(unreach-call) 1 wit inspect 1.5    21    - wit inspect - wit inspect
email_spec27_product18_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.0  55 34   true -32 wit inspect 6.0  270 true -32 wit inspect 8.1   380   unknown 0 wit inspect 9.5  370 false(unreach-call) 1 wit inspect 1.4    20    - wit inspect - wit inspect
email_spec27_product19_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.1  57 34   true -32 wit inspect 6.4  270 true -32 wit inspect 10     420   unknown 0 wit inspect 12    420 false(unreach-call) 1 wit inspect 1.2    21    - wit inspect - wit inspect
email_spec27_product23_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 4.4  63 46   true -32 wit inspect 20    400 unknown 0 wit inspect 42     790   unknown 0 wit inspect 12    370 true -32 wit inspect 1.5    21    - wit inspect - wit inspect
email_spec27_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.2  57 35   true -32 wit inspect 13    420 true -32 wit