Tool DIVINE CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a CPA-witness2test 1.7-svn 29852 CProver witness2test 0.1 CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a
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.15.0-42-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33546 MB
Date of execution 2018-12-06 11:06:04 CET 2018-12-08 03:24:14 CET 2018-12-08 05:17:35 CET 2018-12-08 06:43:53 CET 2018-12-12 20:24:22 CET 2018-12-08 01:45:35 CET 2018-12-08 04:38:54 CET
Run set divine-smt.sv-comp19_prop-reachsafety.ReachSafety-ProductLines cpa-seq-validate-violation-witnesses-divine-smt.sv-comp19_prop-reachsafety.ReachSafety-ProductLines uautomizer-validate-violation-witnesses-divine-smt.sv-comp19_prop-reachsafety.ReachSafety-ProductLines cpa-witness2test-validate-violation-witnesses-divine-smt.sv-comp19_prop-reachsafety.ReachSafety-ProductLines fshell-witness2test-validate-violation-witnesses-divine-smt.sv-comp19_prop-reachsafety.ReachSafety-ProductLines cpa-seq-validate-correctness-witnesses-divine-smt.sv-comp19_prop-reachsafety.ReachSafety-ProductLines uautomizer-validate-correctness-witnesses-divine-smt.sv-comp19_prop-reachsafety.ReachSafety-ProductLines
Options -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -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 -witness ../../results-verified/divine-smt.2018-12-06_1106.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/divine-smt.2018-12-06_1106.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true -witness ../../results-verified/divine-smt.2018-12-06_1106.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/divine-smt.2018-12-06_1106.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/divine-smt.2018-12-06_1106.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/divine-smt.2018-12-06_1106.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/product-lines/ status score witness inspect witness cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB)
elevator_spec14_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.9 8.9 440 100 0      0     false(unreach-call) 1 wit inspect 9.0  4.8  280 0   0     true -32 --- inspect 18     9.9   460   .66 0     false(unreach-call) 1 --- inspect 6.9  3.8  280 0   0      false(unreach-call) 1 --- inspect .88   .88   20    .34 0     - --- inspect - --- inspect
elevator_spec14_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.8 8.8 440 110 0      0     false(unreach-call) 1 wit inspect 9.2  4.9  290 0   0     true -32 --- inspect 17     9.8   500   .66 0     false(unreach-call) 1 --- inspect 6.9  3.8  270 0   0      false(unreach-call) 1 --- inspect .91   .94   20    .34 0     - --- inspect - --- inspect
elevator_spec14_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.8 8.8 440 85 0      0     false(unreach-call) 1 wit inspect 8.6  4.6  280 0   0     true -32 --- inspect 18     10     500   .62 0     false(unreach-call) 1 --- inspect 6.4  3.5  270 0   .086  false(unreach-call) 1 --- inspect .84   .84   20    .34 0     - --- inspect - --- inspect
elevator_spec14_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.7 8.7 440 120 0      0     false(unreach-call) 1 wit inspect 8.0  4.3  290 0   0     true -32 --- inspect 15     8.8   510   .66 0     false(unreach-call) 1 --- inspect 7.7  4.2  270 0   .17   false(unreach-call) 1 --- inspect .86   .88   21    .25 0     - --- inspect - --- inspect
elevator_spec14_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 42   22   440 470 0      0     false(unreach-call) 1 wit inspect 11    6.1  440 0   0     true -32 --- inspect 21     12     470   .66 0     unknown 0 --- inspect 7.4  4.1  270 0   0      true -32 --- inspect .90   .90   20    .38 0     - --- inspect - --- inspect
elevator_spec1_product18_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.7 8.7 430 140 0      .049 false(unreach-call) 1 wit inspect 7.5  4.0  280 0   0     true -32 --- inspect 16     9.2   510   .62 0     false(unreach-call) 1 --- inspect 6.8  3.8  270 0   0      false(unreach-call) 1 --- inspect .86   .86   20    .34 .074 - --- inspect - --- inspect
elevator_spec1_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.7 8.7 430 120 0      0     false(unreach-call) 1 wit inspect 9.1  4.9  300 0   0     true -32 --- inspect 18     10     510   .66 0     false(unreach-call) 1 --- inspect 6.9  3.8  270 0   0      false(unreach-call) 1 --- inspect .88   .88   21    .36 .074 - --- inspect - --- inspect
elevator_spec1_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.9 9.0 430 120 0      0     false(unreach-call) 1 wit inspect 8.2  4.4  310 0   0     true -32 --- inspect 16     9.1   530   .66 0     false(unreach-call) 1 --- inspect 7.2  4.0  270 0   5.8    false(unreach-call) 1 --- inspect .90   .90   20    .35 0     - --- inspect - --- inspect
elevator_spec1_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.9 8.9 430 100 0      0     false(unreach-call) 1 wit inspect 9.5  5.1  290 0   0     true -32 --- inspect 16     9.4   530   .66 0     false(unreach-call) 1 --- inspect 7.0  3.8  270 0   0      false(unreach-call) 1 --- inspect .86   .86   20    .36 0     - --- inspect - --- inspect
elevator_spec1_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.7 8.7 430 100 0      0     false(unreach-call) 1 wit inspect 8.4  4.5  290 0   0     true -32 --- inspect 19     11     470   .66 0     false(unreach-call) 1 --- inspect 6.6  3.7  260 0   0      false(unreach-call) 1 --- inspect .89   .90   20    .35 0     - --- inspect - --- inspect
elevator_spec1_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.7 8.7 430 130 0      0     false(unreach-call) 1 wit inspect 9.0  4.9  280 0   0     true -32 --- inspect 20     11     500   .66 0     false(unreach-call) 1 --- inspect 6.9  3.8  260 0   0      false(unreach-call) 1 --- inspect .89   .90   20    .35 0     - --- inspect - --- inspect
elevator_spec1_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.7 8.8 430 110 0      0     false(unreach-call) 1 wit inspect 8.6  4.6  290 0   0     true -32 --- inspect 17     9.4   530   .66 0     false(unreach-call) 1 --- inspect 6.8  3.8  270 0   0      false(unreach-call) 1 --- inspect .85   .85   20    .36 .074 - --- inspect - --- inspect
elevator_spec1_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.7 8.8 430 110 0      0     false(unreach-call) 1 wit inspect 9.2  4.9  290 0   0     true -32 --- inspect 21     12     460   .62 0     false(unreach-call) 1 --- inspect 5.4  3.0  270 0   0      false(unreach-call) 1 --- inspect .85   .85   20    .36 0     - --- inspect - --- inspect
elevator_spec1_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 73   35   440 850 0      0     false(unreach-call) 1 wit inspect 40    25    1200 0   0     true -32 --- inspect 20     11     530   .66 0     unknown 0 --- inspect 7.3  4.1  270 0   0      true -32 --- inspect .88   .88   20    .39 0     - --- inspect - --- inspect
elevator_spec2_product18_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.6 8.6 430 110 0      0     false(unreach-call) 1 wit inspect 8.8  4.7  280 0   0     true -32 --- inspect 16     9.2   470   .66 0     false(unreach-call) 1 --- inspect 6.1  3.4  270 0   0      false(unreach-call) 1 --- inspect .85   .85   20    .34 0     - --- inspect - --- inspect
elevator_spec2_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.8 8.9 430 110 0      0     false(unreach-call) 1 wit inspect 8.4  4.5  290 0   0     true -32 --- inspect 18     10     520   .66 0     false(unreach-call) 1 --- inspect 7.1  3.9  270 0   0      false(unreach-call) 1 --- inspect .88   .87   20    .36 0     - --- inspect - --- inspect
elevator_spec2_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.8 8.8 430 100 0      0     false(unreach-call) 1 wit inspect 8.3  4.5  290 0   0     true -32 --- inspect 17     9.6   510   .66 0     false(unreach-call) 1 --- inspect 5.6  3.2  270 0   0      false(unreach-call) 1 --- inspect .84   .84   20    .35 0     - --- inspect - --- inspect
elevator_spec2_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.7 8.7 430 100 0      0     false(unreach-call) 1 wit inspect 9.9  5.3  290 0   0     true -32 --- inspect 18     10     510   .66 0     false(unreach-call) 1 --- inspect 6.9  3.8  270 0   0      false(unreach-call) 1 --- inspect .88   .88   20    .36 0     - --- inspect - --- inspect
elevator_spec2_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.7 8.7 430 100 0      0     false(unreach-call) 1 wit inspect 9.2  4.9  280 0   0     true -32 --- inspect 18     10     470   .66 0     false(unreach-call) 1 --- inspect 5.6  3.1  270 0   0      false(unreach-call) 1 --- inspect .87   .88   21    .35 0     - --- inspect - --- inspect
elevator_spec2_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.7 8.7 430 110 0      0     false(unreach-call) 1 wit inspect 7.0  3.7  280 0   0     true -32 --- inspect 21     11     460   .66 0     false(unreach-call) 1 --- inspect 6.4  3.6  270 0   0      false(unreach-call) 1 --- inspect .89   .90   20    .36 0     - --- inspect - --- inspect
elevator_spec2_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.8 8.8 430 110 0      0     false(unreach-call) 1 wit inspect 8.1  4.4  290 0   0     true -32 --- inspect 18     10     460   .66 0     false(unreach-call) 1 --- inspect 5.5  3.1  270 0   0      false(unreach-call) 1 --- inspect .87   .89   20    .36 0     - --- inspect - --- inspect
elevator_spec2_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.6 8.6 430 110 0      0     false(unreach-call) 1 wit inspect 9.9  5.3  290 0   0     true -32 --- inspect 19     11     520   .66 .078 false(unreach-call) 1 --- inspect 5.8  3.2  270 0   0      false(unreach-call) 1 --- inspect .88   .88   20    .36 0     - --- inspect - --- inspect
elevator_spec2_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 72   35   450 740 0      0     false(unreach-call) 1 wit inspect 42    25    1200 0   0     true -32 --- inspect 20     11     550   .66 0     unknown 0 --- inspect 7.0  3.9  270 0   0      true -32 --- inspect .88   .88   20    .39 .082 - --- inspect - --- inspect
elevator_spec3_product03_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.8 8.8 440 100 0      0     false(unreach-call) 1 wit inspect 9.8  5.2  290 0   0     true -32 --- inspect 16     9.3   500   .66 0     false(unreach-call) 1 --- inspect 7.3  4.0  270 0   0      false(unreach-call) 1 --- inspect .87   .87   20    .34 0     - --- inspect - --- inspect
elevator_spec3_product11_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.6 8.6 440 100 0      0     false(unreach-call) 1 wit inspect 9.1  4.9  290 0   0     true -32 --- inspect 15     8.7   510   .66 0     false(unreach-call) 1 --- inspect 7.6  4.2  260 0   0      false(unreach-call) 1 --- inspect .88   .88   21    .34 0     - --- inspect - --- inspect
elevator_spec3_product19_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.8 8.8 440 110 0      0     false(unreach-call) 1 wit inspect 11    5.6  310 0   0     true -32 --- inspect 19     11     470   .66 0     false(unreach-call) 1 --- inspect 7.1  3.9  260 0   0      false(unreach-call) 1 --- inspect .86   .86   21    .35 .074 - --- inspect - --- inspect
elevator_spec3_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.9 8.9 440 100 0      0     false(unreach-call) 1 wit inspect 8.3  4.4  310 0   0     true -32 --- inspect 18     10     510   .66 0     false(unreach-call) 1 --- inspect 5.9  3.3  270 0   .070  false(unreach-call) 1 --- inspect .85   .87   21    .26 0     - --- inspect - --- inspect
elevator_spec3_product23_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 9.0 9.0 440 120 0      0     false(unreach-call) 1 wit inspect 9.0  4.9  310 0   0     true -32 --- inspect 17     9.7   520   .66 0     false(unreach-call) 1 --- inspect 7.4  4.1  270 0   0      false(unreach-call) 1 --- inspect .87   .87   20    .36 0     - --- inspect - --- inspect
elevator_spec3_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.8 8.9 440 110 0      0     false(unreach-call) 1 wit inspect 8.3  4.5  320 0   0     true -32 --- inspect 17     9.7   520   .66 0     false(unreach-call) 1 --- inspect 5.7  3.1  270 0   0      false(unreach-call) 1 --- inspect .88   .88   21    .36 .078 - --- inspect - --- inspect
elevator_spec3_product27_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.7 8.8 440 120 0      0     false(unreach-call) 1 wit inspect 8.8  4.7  290 0   0     true -32 --- inspect 19     10     470   .66 0     false(unreach-call) 1 --- inspect 5.9  3.3  270 0   0      false(unreach-call) 1 --- inspect .85   .85   20    .35 0     - --- inspect - --- inspect
elevator_spec3_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.8 8.8 440 120 0      0     false(unreach-call) 1 wit inspect 11    5.6  310 0   0     true -32 --- inspect 15     8.9   510   .66 0     false(unreach-call) 1 --- inspect 6.2  3.4  270 0   0      false(unreach-call) 1 --- inspect .85   .85   20    .36 0     - --- inspect - --- inspect
elevator_spec3_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.7 8.7 440 110 0      0     false(unreach-call) 1 wit inspect 8.8  4.8  310 0   0     true -32 --- inspect 21     11     460   .66 0     false(unreach-call) 1 --- inspect 6.9  3.8  270 0   0      false(unreach-call) 1 --- inspect .88   .89   20    .36 0     - --- inspect - --- inspect
elevator_spec3_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.7 8.7 440 110 0      0     false(unreach-call) 1 wit inspect 8.7  4.7  320 0   0     true -32 --- inspect 18     10     470   .66 0     false(unreach-call) 1 --- inspect 7.2  4.0  270 0   0      false(unreach-call) 1 --- inspect .87   .87   20    .36 0     - --- inspect - --- inspect
elevator_spec3_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 200   85   460 2200 0      0     false(unreach-call) 1 wit inspect 20    11    610 0   0     true -32 --- inspect 21     12     530   .66 0     unknown 0 --- inspect 6.1  3.4  270 0   0      true -32 --- inspect .90   .90   20    .39 0     - --- inspect - --- inspect
elevator_spec9_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.8 8.8 430 100 0      0     false(unreach-call) 1 wit inspect 9.7  5.2  280 0   0     true -32 --- inspect 15     8.7   510   .66 0     false(unreach-call) 1 --- inspect 6.5  3.6  270 0   0      false(unreach-call) 1 --- inspect .87   .89   20    .34 0     - --- inspect - --- inspect
elevator_spec9_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.6 8.6 430 120 0      0     false(unreach-call) 1 wit inspect 8.0  4.3  290 0   0     true -32 --- inspect 15     8.5   520   .66 0     false(unreach-call) 1 --- inspect 5.6  3.1  270 0   0      false(unreach-call) 1 --- inspect .87   .87   20    .36 0     - --- inspect - --- inspect
elevator_spec9_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.9 8.9 430 110 0      0     false(unreach-call) 1 wit inspect 9.0  4.8  300 0   0     true -32 --- inspect 18     10     510   .66 0     false(unreach-call) 1 --- inspect 6.0  3.4  260 0   0      false(unreach-call) 1 --- inspect .85   .85   20    .36 0     - --- inspect - --- inspect
elevator_spec9_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 9.0 9.0 430 110 0      0     false(unreach-call) 1 wit inspect 9.9  5.3  290 0   0     true -32 --- inspect 16     9.3   530   .66 0     false(unreach-call) 1 --- inspect 7.6  4.2  290 0   0      false(unreach-call) 1 --- inspect .86   .86   20    .36 0     - --- inspect - --- inspect
elevator_spec9_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 84   39   450 940 0      0     false(unreach-call) 1 wit inspect 43    25    1300 0   0     true -32 --- inspect 22     12     560   .66 0     unknown 0 --- inspect 7.1  3.9  270 0   0      true -32 --- inspect .94   .93   20    .39 0     - --- inspect - --- inspect
elevator_spec13_product21_true-unreach-call_false-termination.cil.c true 1 wit inspect 8.9 8.9 370 120 0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    2700 0   0      out of memory 0 --- inspect 220     150     7000   .65 0    
elevator_spec13_product22_true-unreach-call_false-termination.cil.c true 1 wit inspect 8.5 8.5 370 110 0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    880    3300 0   0      out of memory 0 --- inspect 200     130     7000   .66 0    
elevator_spec13_product23_true-unreach-call_false-termination.cil.c true 1 wit inspect 8.7 8.7 370 110 0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    880    3700 0   0      out of memory 0 --- inspect 260     180     7000   .65 0    
elevator_spec13_product24_true-unreach-call_false-termination.cil.c true 1 wit inspect 8.6 8.6 370 100 0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    880    4300 0   0      out of memory 0 --- inspect 260     170     7000   1.7  0    
elevator_spec13_product29_true-unreach-call_false-termination.cil.c true 1 wit inspect 8.5 8.5 370 110 0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    880    2400 0   0      out of memory 0 --- inspect 230     150     7000   .68 0    
elevator_spec13_product30_true-unreach-call_false-termination.cil.c true 1 wit inspect 8.7 8.7 370 100 0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    880    3400 0   0      out of memory 0 --- inspect 210     140     7000   .65 0    
elevator_spec13_product31_true-unreach-call_false-termination.cil.c true 1 wit inspect 8.7 8.8 370 96 0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    3700 0   0      out of memory 0 --- inspect 200     130     7000   .65 0    
elevator_spec13_product32_true-unreach-call_false-termination.cil.c true 1 wit inspect 8.6 8.6 370 98 0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    880    4400 0   .0041 out of memory 0 --- inspect 240     170     7000   .65 0    
elevator_spec13_productSimulator_true-unreach-call_false-termination.cil.c true 1 wit inspect 44   17   380 400 0      0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    880    3400 0   0      out of memory 0 --- inspect 230     150     7000   .72 0    
elevator_spec14_product03_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.6 8.6 370 100 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 22    12    660 0   0      out of memory 0 --- inspect 270     190     7000   .72 0    
elevator_spec14_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.8 8.8 370 110 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 20    11    680 0   0      out of memory 0 --- inspect 280     200     7000   .65 0    
elevator_spec14_product19_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.6 8.6 370 110 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 22    12    700 0   0      out of memory 0 --- inspect 310     220     7000   1.6  .033
elevator_spec14_product23_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.9 8.9 370 110 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 31    18    1100 0   0      out of memory 0 --- inspect 240     160     7000   .66 0    
elevator_spec14_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.8 8.8 370 110 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 22    12    710 0   0      out of memory 0 --- inspect 330     240     7000   .79 0    
elevator_spec14_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.5 8.5 370 100 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 28    17    1100 0   0      out of memory 0 --- inspect 250     170     7000   .71 .041
elevator_spec1_product01_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.7 8.7 370 110 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 81    66    1600 0   0      out of memory 0 --- inspect 260     190     7000   .64 0    
elevator_spec1_product03_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.6 8.7 370 98 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 82    68    1700 0   0      out of memory 0 --- inspect 260     180     7000   .65 0    
elevator_spec1_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.8 8.8 370 110 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 91    75    1700 0   0      out of memory 0 --- inspect 260     180     7000   .64 0    
elevator_spec1_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.4 8.4 370 130 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 100    89    1700 0   0      out of memory 0 --- inspect 280     190     7000   1.6  0    
elevator_spec1_product17_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.6 8.6 370 110 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 80    69    1800 0   0      out of memory 0 --- inspect 250     180     7000   .64 0    
elevator_spec1_product19_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.7 8.7 370 100 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 97    85    1800 0   0      out of memory 0 --- inspect 330     230     7000   .66 0    
elevator_spec1_product21_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.7 8.7 370 96 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 170    160    2200 0   0      out of memory 0 --- inspect 260     190     7000   .72 0    
elevator_spec1_product23_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.6 8.6 370 90 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 160    150    2300 0   0      out of memory 0 --- inspect 340     240     7000   .64 0    
elevator_spec1_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.8 8.8 370 120 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 94    79    1800 0   0      out of memory 0 --- inspect 260     180     7000   .65 0    
elevator_spec1_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.5 8.5 370 97 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 110    98    2000 0   0      out of memory 0 --- inspect 250     180     7000   .66 0    
elevator_spec1_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.5 8.5 370 110 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 340    320    2300 0   0      out of memory 0 --- inspect 290     200     7000   .68 0    
elevator_spec1_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.6 8.6 370 99 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 200    180    2500 0   0      out of memory 0 --- inspect 290     200     7000   .64 0    
elevator_spec2_product01_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.6 8.7 370 120 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 37    25    1000 0   0      out of memory 0 --- inspect 180     120     7000   1.5  0    
elevator_spec2_product03_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.8 8.8 370 120 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 38    26    1100 0   0      out of memory 0 --- inspect 220     150     7000   .69 0    
elevator_spec2_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.5 8.5 370 110 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 35    23    1100 0   0      out of memory 0 --- inspect 160     100     7000   .66 0    
elevator_spec2_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.7 8.7 370 110 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 36    25    1100 0   0      out of memory 0 --- inspect 180     120     7000   1.3  0    
elevator_spec2_product17_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.8 8.8 370 110 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 40    27    1100 0   0      out of memory 0 --- inspect 160     100     7000   .65 0    
elevator_spec2_product19_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.6 8.6 370 120 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 46    32    1200 0   0      out of memory 0 --- inspect 200     140     7000   .66 0    
elevator_spec2_product21_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.6 8.6 370 120 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 56    42    1300 0   0      out of memory 0 --- inspect 200     130     7000   .64 0    
elevator_spec2_product23_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.7 8.7 370 120 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 59    45    1400 0   0      out of memory 0 --- inspect 300     210     7000   .64 0    
elevator_spec2_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.8 8.8 370 110 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 37    26    1200 0   0      out of memory 0 --- inspect 170     110     7000   .64 0    
elevator_spec2_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.7 8.7 370 120 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 50    36    1200 0   0      out of memory 0 --- inspect 220     140     7000   .65 0    
elevator_spec2_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.7 8.8 370 110 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 60    48    1500 0   0      out of memory 0 --- inspect 210     140     7000   .75 0    
elevator_spec2_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.8 8.8 370 110 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 56    42    1500 0   0      out of memory 0 --- inspect 230     160     7000   .70 0    
elevator_spec3_product01_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.9 8.9 370 110 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 17    9.4  670 0   0      out of memory 0 --- inspect 180     110     7000   .64 0    
elevator_spec3_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.8 8.8 370 120 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 18    9.8  650 0   0      out of memory 0 --- inspect 150     95     7000   .66 0    
elevator_spec3_product17_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.6 8.6 370 110 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 17    9.6  670 0   0      out of memory 0 --- inspect 200     120     7000   .65 .36 
elevator_spec3_product18_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.4 8.4 370 130 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 29    16    840 0   0      out of memory 0 --- inspect 200     130     7000   .91 0    
elevator_spec3_product21_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.8 8.8 370 100 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 24    13    930 0   0      out of memory 0 --- inspect 240     160     7000   .64 0    
elevator_spec3_product22_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.6 8.7 370 100 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 34    19    1300 0   0      out of memory 0 --- inspect 230     160     7000   .64 0    
elevator_spec3_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.7 8.7 370 99 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 19    10    700 0   0      out of memory 0 --- inspect 190     120     7000   1.5  0    
elevator_spec3_product26_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.8 8.8 370 110 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 25    14    930 0   0      out of memory 0 --- inspect 270     180     7000   .64 0    
elevator_spec3_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.8 8.8 370 110 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 23    13    910 0   0      out of memory 0 --- inspect 260     180     7000   .66 0    
elevator_spec3_product30_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.6 8.6 370 110 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 38    21    1500 0   0      out of memory 0 --- inspect 190     130     7000   .71 0    
elevator_spec9_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.7 8.7 370 96 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 40    27    1100 0   0      out of memory 0 --- inspect 210     140     7000   .71 0    
elevator_spec9_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.6 8.7 370 96 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 39    28    1100 0   0      out of memory 0 --- inspect 180     120     7000   .65 0    
elevator_spec9_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.6 8.6 370 120 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 39    27    1200 0   0      out of memory 0 --- inspect 210     140     7000   .70 0    
elevator_spec9_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.8 8.8 370 110 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 40    28    1200 0   0      out of memory 0 --- inspect 200     130     7000   .65 0    
elevator_spec9_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.9 8.9 370 120 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 85    70    1500 0   0      out of memory 0 --- inspect 220     150     7000   .82 0    
elevator_spec9_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.9 8.9 370 110 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 61    49    1600 0   0      out of memory 0 --- inspect 250     170     7000   .71 0    
email_spec0_product16_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 68   33   440 710 0      0     error (invalid witness file) 0 --- inspect .59 .37 42 0   0     error (2) 0 --- inspect .021 .022 5.7 0    0     error (invalid witness file) 0 --- inspect 1.2  .75 47 0   0      error (invalid witness file) 0 --- inspect .0048 .0060 .54 0    0     - --- inspect - --- inspect
email_spec0_product21_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 69   33   440 710 0      0     error (invalid witness file) 0 --- inspect .75 .45 41 0   0     error (2) 0 --- inspect .022 .023 5.6 0    0     error (invalid witness file) 0 --- inspect 1.0  .65 48 0   0      error (invalid witness file) 0 --- inspect .0053 .0064 .54 0    0     - --- inspect - --- inspect
email_spec0_product22_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 68   33   440 820 0      0     error (invalid witness file) 0 --- inspect .73 .44 41 0   0     error (2) 0 --- inspect .031 .032 5.6 0    0     error (invalid witness file) 0 --- inspect 1.4  .89 47 0   0      error (invalid witness file) 0 --- inspect .0046 .0074 .54 0    0     - --- inspect - --- inspect
email_spec0_product26_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 69   33   440 710 0      0     error (invalid witness file) 0 --- inspect .78 .47 42 0   0     error (2) 0 --- inspect .023 .024 5.6 0    0     error (invalid witness file) 0 --- inspect 1.0  .67 49 0   0      error (invalid witness file) 0 --- inspect .0023 .0029 .54 0    0     - --- inspect - --- inspect
email_spec0_product31_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 69   33   440 710 0      0     error (invalid witness file) 0 --- inspect .74 .44 40 0   0     error (2) 0 --- inspect .026 .027 5.6 0    0     error (invalid witness file) 0 --- inspect .97 .64 47 0   0      error (invalid witness file) 0 --- inspect .0055 .0068 .53 0    0     - --- inspect - --- inspect
email_spec0_product33_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 68   33   440 740 0      0     error (invalid witness file) 0 --- inspect .65 .40 41 0   0     error (2) 0 --- inspect .029 .030 5.5 0    0     error (invalid witness file) 0 --- inspect 1.1  .69 47 0   0      error (invalid witness file) 0 --- inspect .0055 .0072 .54 0    0     - --- inspect - --- inspect
email_spec0_product34_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 69   34   440 780 0      0     error (invalid witness file) 0 --- inspect .60 .37 41 0   0     error (2) 0 --- inspect .020 .022 5.6 0    0     error (invalid witness file) 0 --- inspect .99 .64 46 0   0      error (invalid witness file) 0 --- inspect .0055 .0065 .54 0    0     - --- inspect - --- inspect
email_spec0_product35_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 68   33   450 730 0      0     error (invalid witness file) 0 --- inspect .75 .45 40 0   0     error (2) 0 --- inspect .023 .024 5.6 0    0     error (invalid witness file) 0 --- inspect 1.1  .72 47 0   0      error (invalid witness file) 0 --- inspect .0016 .0021 .54 0    0     - --- inspect - --- inspect
email_spec0_productSimulator_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 21   14   440 230 0      0     error (invalid witness file) 0 --- inspect .64 .40 40 0   0     error (2) 0 --- inspect .024 .026 5.6 0    0     error (invalid witness file) 0 --- inspect .90 .59 47 0   0      error (invalid witness file) 0 --- inspect .0023 .0029 .53 0    0     - --- inspect - --- inspect
email_spec11_product15_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 68   33   440 760 0      0     error (invalid witness file) 0 --- inspect .74 .47 40 0   0     error (2) 0 --- inspect .022 .023 5.6 0    0     error (invalid witness file) 0 --- inspect 1.0  .67 48 0   0      error (invalid witness file) 0 --- inspect .0021 .0027 .41 0    0     - --- inspect - --- inspect
email_spec11_product20_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 68   33   440 710 0      0     error (invalid witness file) 0 --- inspect .77 .48 41 0   0     error (2) 0 --- inspect .036 .038 5.6 0    0     error (invalid witness file) 0 --- inspect 1.2  .77 47 0   0      error (invalid witness file) 0 --- inspect .0058 .0070 .52 0    0     - --- inspect - --- inspect
email_spec11_product22_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 68   33   440 730 0      0     error (invalid witness file) 0 --- inspect .61 .38 40 0   0     error (2) 0 --- inspect .026 .027 5.6 0    0     error (invalid witness file) 0 --- inspect .94 .59 48 0   0      error (invalid witness file) 0 --- inspect .0021 .0042 .61 0    0     - --- inspect - --- inspect
email_spec11_product26_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 68   33   440 710 0      0     error (invalid witness file) 0 --- inspect .75 .46 41 0   0     error (2) 0 --- inspect .022 .023 5.6 0    0     error (invalid witness file) 0 --- inspect .99 .64 48 0   0      error (invalid witness file) 0 --- inspect .0055 .0082 .53 0    0     - --- inspect - --- inspect
email_spec11_product30_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 68   33   440 720 0      0     error (invalid witness file) 0 --- inspect .78 .47 41 0   0     error (2) 0 --- inspect .025 .025 5.6 0    0     error (invalid witness file) 0 --- inspect 1.1  .71 49 0   0      error (invalid witness file) 0 --- inspect .0058 .018  .52 0    0     - --- inspect - --- inspect
email_spec11_product32_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 68   33   440 710 0      0     error (invalid witness file) 0 --- inspect .76 .46 41 0   0     error (2) 0 --- inspect .027 .027 5.6 0    0     error (invalid witness file) 0 --- inspect .95 .61 46 0   0      error (invalid witness file) 0 --- inspect .0020 .0025 .53 0    0     - --- inspect - --- inspect
email_spec11_product33_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 69   33   440 740 0      0     error (invalid witness file) 0 --- inspect .74 .46 41 0   0     error (2) 0 --- inspect .028 .028 5.6 0    0     error (invalid witness file) 0 --- inspect 1.2  .79 47 0   0      error (invalid witness file) 0 --- inspect .0016 .0020 .52 0    0     - --- inspect - --- inspect
email_spec11_product35_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 68   33   440 750 0      0     error (invalid witness file) 0 --- inspect .59 .36 40 0   0     error (2) 0 --- inspect .021 .021 5.6 0    0     error (invalid witness file) 0 --- inspect 1.2  .77 46 0   0      error (invalid witness file) 0 --- inspect .0064 .011  .48 0    0     - --- inspect - --- inspect
email_spec11_productSimulator_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 21   14   440 260 0      0     error (invalid witness file) 0 --- inspect .78 .47 42 0   0     error (2) 0 --- inspect .021 .021 5.6 0    0     error (invalid witness file) 0 --- inspect 1.2  .78 48 0   0      error (invalid witness file) 0 --- inspect .0059 .0075 .52 0    0     - --- inspect - --- inspect
email_spec1_product14_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 68   33   450 730 0      0     error (invalid witness file) 0 --- inspect .76 .45 40 0   0     error (2) 0 --- inspect .026 .027 5.6 0    0     error (invalid witness file) 0 --- inspect 1.2  .77 46 0   0      error (invalid witness file) 0 --- inspect .0047 .0058 .54 0    0     - --- inspect - --- inspect
email_spec1_product15_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 68   33   450 670 0      0     error (invalid witness file) 0 --- inspect .71 .43 41 0   0     error (2) 0 --- inspect .021 .022 5.6 0    0     error (invalid witness file) 0 --- inspect 1.4  .88 47 0   0    Ȁ