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-10 10:00:20 CET 2018-12-10 10:48:16 CET 2018-12-10 11:10:44 CET 2018-12-10 11:13:11 CET 2018-12-12 20:23:24 CET 2018-12-10 10:29:49 CET 2018-12-10 10:51:28 CET
Run set divine-explicit.sv-comp19_prop-reachsafety.ReachSafety-ProductLines cpa-seq-validate-violation-witnesses-divine-explicit.sv-comp19_prop-reachsafety.ReachSafety-ProductLines uautomizer-validate-violation-witnesses-divine-explicit.sv-comp19_prop-reachsafety.ReachSafety-ProductLines cpa-witness2test-validate-violation-witnesses-divine-explicit.sv-comp19_prop-reachsafety.ReachSafety-ProductLines fshell-witness2test-validate-violation-witnesses-divine-explicit.sv-comp19_prop-reachsafety.ReachSafety-ProductLines cpa-seq-validate-correctness-witnesses-divine-explicit.sv-comp19_prop-reachsafety.ReachSafety-ProductLines uautomizer-validate-correctness-witnesses-divine-explicit.sv-comp19_prop-reachsafety.ReachSafety-ProductLines
Options --no-symbolic -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-explicit.2018-12-10_1000.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/divine-explicit.2018-12-10_1000.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-explicit.2018-12-10_1000.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/divine-explicit.2018-12-10_1000.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-explicit.2018-12-10_1000.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/divine-explicit.2018-12-10_1000.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.7 8.7 440 110 0   0     false(unreach-call) 1 wit inspect 7.2  3.9  280 0   0     true -32 --- inspect 14     8.0   460   .62  0     false(unreach-call) 1 --- inspect 5.5  3.0  270 0   0      false(unreach-call) 1 --- inspect .92   .92   20    .34 0     - --- inspect - --- inspect
elevator_spec14_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.6 8.6 440 120 0   0     false(unreach-call) 1 wit inspect 7.6  4.1  290 0   0     true -32 --- inspect 15     8.4   470   .62  0     false(unreach-call) 1 --- inspect 5.7  3.1  270 0   0      false(unreach-call) 1 --- inspect .87   .88   21    .35 .074 - --- inspect - --- inspect
elevator_spec14_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.5 8.5 440 130 0   0     false(unreach-call) 1 wit inspect 7.0  3.8  280 0   0     true -32 --- inspect 15     8.7   470   .62  0     false(unreach-call) 1 --- inspect 5.5  3.1  270 0   .086  false(unreach-call) 1 --- inspect .87   .87   20    .30 0     - --- inspect - --- inspect
elevator_spec14_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.6 8.7 440 110 0   0     false(unreach-call) 1 wit inspect 7.6  4.1  290 0   0     true -32 --- inspect 15     8.6   510   .62  0     false(unreach-call) 1 --- inspect 5.5  3.1  270 0   0      false(unreach-call) 1 --- inspect .88   .88   20    .35 0     - --- inspect - --- inspect
elevator_spec14_productSimulator_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 8.7 8.8 430 110 0   0     error (invalid witness file) 0 --- inspect .62 .39 41 0   0     error (2) 0 --- inspect .026 .026 5.6 0     0     error (invalid witness file) 0 --- inspect .93 .59 47 0   0      error (invalid witness file) 0 --- inspect .0054 .0074 .52 0    0     - --- inspect - --- inspect
elevator_spec1_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 6.9  3.7  280 0   0     true -32 --- inspect 14     8.0   510   .62  0     false(unreach-call) 1 --- inspect 5.1  2.9  270 0   0      false(unreach-call) 1 --- inspect .87   .89   20    .34 0     - --- inspect - --- inspect
elevator_spec1_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.6 8.6 430 110 0   .20  false(unreach-call) 1 wit inspect 7.5  4.0  280 0   .074 true -32 --- inspect 14     7.8   460   .62  0     false(unreach-call) 1 --- inspect 5.2  2.9  270 0   0      false(unreach-call) 1 --- inspect .87   .87   20    .36 0     - --- inspect - --- inspect
elevator_spec1_product22_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 7.1  3.9  290 0   0     true -32 --- inspect 16     8.8   460   .62  0     false(unreach-call) 1 --- inspect 5.2  2.9  270 0   0      false(unreach-call) 1 --- inspect .88   .87   20    .35 0     - --- inspect - --- inspect
elevator_spec1_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.5 8.5 430 120 0   .070 false(unreach-call) 1 wit inspect 7.8  4.2  290 0   0     true -32 --- inspect 15     8.7   520   .62  0     false(unreach-call) 1 --- inspect 5.2  2.9  270 0   0      false(unreach-call) 1 --- inspect .87   .87   20    .36 0     - --- inspect - --- inspect
elevator_spec1_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.5 8.5 430 100 0   0     false(unreach-call) 1 wit inspect 7.3  3.9  280 0   0     true -32 --- inspect 14     8.3   510   .62  0     false(unreach-call) 1 --- inspect 5.5  3.1  260 0   0      false(unreach-call) 1 --- inspect .87   .87   20    .35 0     - --- inspect - --- inspect
elevator_spec1_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.6 8.6 430 100 0   0     false(unreach-call) 1 wit inspect 6.9  3.8  290 0   0     true -32 --- inspect 15     8.4   520   .62  0     false(unreach-call) 1 --- inspect 5.3  2.9  270 0   .0041 false(unreach-call) 1 --- inspect .85   .85   20    .36 0     - --- inspect - --- inspect
elevator_spec1_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.6 8.6 430 130 0   0     false(unreach-call) 1 wit inspect 7.6  4.1  290 0   0     true -32 --- inspect 15     8.4   510   .62  0     false(unreach-call) 1 --- inspect 5.2  2.9  260 0   0      false(unreach-call) 1 --- inspect .86   .85   20    .36 0     - --- inspect - --- inspect
elevator_spec1_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.6 8.6 430 100 0   0     false(unreach-call) 1 wit inspect 7.5  4.0  300 0   0     true -32 --- inspect 14     8.3   460   .62  0     false(unreach-call) 1 --- inspect 5.3  3.0  270 0   0      false(unreach-call) 1 --- inspect .89   .89   20    .36 .078 - --- inspect - --- inspect
elevator_spec1_productSimulator_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 8.6 8.6 430 120 0   0     error (invalid witness file) 0 --- inspect .60 .38 40 0   0     error (2) 0 --- inspect .052 .053 5.5 0     0     error (invalid witness file) 0 --- inspect 1.0  .68 48 0   0      error (invalid witness file) 0 --- inspect .0046 .0059 .41 0    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 6.7  3.6  280 0   0     true -32 --- inspect 15     8.6   460   .62  0     false(unreach-call) 1 --- inspect 5.2  2.9  260 0   0      false(unreach-call) 1 --- inspect .85   .85   21    .34 0     - --- inspect - --- inspect
elevator_spec2_product20_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 7.4  4.0  280 0   0     true -32 --- inspect 17     9.7   460   .62  .074 false(unreach-call) 1 --- inspect 5.3  3.0  260 0   0      false(unreach-call) 1 --- inspect .89   .89   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 120 0   0     false(unreach-call) 1 wit inspect 7.5  4.0  300 0   0     true -32 --- inspect 15     8.6   520   .62  0     false(unreach-call) 1 --- inspect 5.4  3.0  270 0   0      false(unreach-call) 1 --- inspect .86   .86   20    .35 0     - --- inspect - --- inspect
elevator_spec2_product24_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.8  4.7  290 0   0     true -32 --- inspect 14     8.3   490   .62  0     false(unreach-call) 1 --- inspect 5.3  3.0  270 0   .078  false(unreach-call) 1 --- inspect .86   .86   21    .36 0     - --- inspect - --- inspect
elevator_spec2_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 6.8  3.6  280 0   0     true -32 --- inspect 16     8.9   470   .62  0     false(unreach-call) 1 --- inspect 5.4  3.0  260 0   0      false(unreach-call) 1 --- inspect .85   .85   20    .35 0     - --- inspect - --- inspect
elevator_spec2_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.5 8.5 430 97 0   0     false(unreach-call) 1 wit inspect 7.2  3.9  280 0   0     true -32 --- inspect 15     8.8   520   .62  0     false(unreach-call) 1 --- inspect 5.5  3.1  270 0   0      false(unreach-call) 1 --- inspect .87   .87   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 93 0   0     false(unreach-call) 1 wit inspect 7.3  3.9  300 0   0     true -32 --- inspect 15     8.6   510   .62  0     false(unreach-call) 1 --- inspect 5.4  3.0  270 0   0      false(unreach-call) 1 --- inspect .88   .88   20    .36 0     - --- inspect - --- inspect
elevator_spec2_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.4 8.5 430 99 0   0     false(unreach-call) 1 wit inspect 7.7  4.1  290 0   .078 true -32 --- inspect 17     10     520   .62  0     false(unreach-call) 1 --- inspect 5.4  3.0  270 0   0      false(unreach-call) 1 --- inspect .86   .86   20    .36 0     - --- inspect - --- inspect
elevator_spec2_productSimulator_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 8.8 8.8 430 110 0   0     error (invalid witness file) 0 --- inspect .59 .38 40 0   0     error (2) 0 --- inspect .028 .029 5.7 0     0     error (invalid witness file) 0 --- inspect .97 .63 48 0   0      error (invalid witness file) 0 --- inspect .0050 .0064 .53 0    0     - --- inspect - --- inspect
elevator_spec3_product03_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.5 8.5 440 120 0   0     false(unreach-call) 1 wit inspect 7.5  4.0  290 0   0     true -32 --- inspect 12     7.2   500   .66  0     false(unreach-call) 1 --- inspect 5.5  3.1  280 0   0      false(unreach-call) 1 --- inspect .85   .85   20    .34 0     - --- inspect - --- inspect
elevator_spec3_product11_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.7 8.7 440 99 0   0     false(unreach-call) 1 wit inspect 7.7  4.2  290 0   0     true -32 --- inspect 13     7.8   470   .62  0     false(unreach-call) 1 --- inspect 5.5  3.1  260 0   0      false(unreach-call) 1 --- inspect .90   .91   20    .34 0     - --- inspect - --- inspect
elevator_spec3_product19_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 7.9  4.2  290 0   0     true -32 --- inspect 15     8.7   520   .62  0     false(unreach-call) 1 --- inspect 5.5  3.1  260 0   0      false(unreach-call) 1 --- inspect .89   .89   20    .35 0     - --- inspect - --- inspect
elevator_spec3_product20_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.4  4.4  290 0   0     true -32 --- inspect 15     8.5   470   .62  0     false(unreach-call) 1 --- inspect 5.5  3.1  270 0   0      false(unreach-call) 1 --- inspect .85   .85   20    .35 0     - --- inspect - --- inspect
elevator_spec3_product23_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.6 8.6 440 97 0   0     false(unreach-call) 1 wit inspect 9.8  5.3  330 0   0     true -32 --- inspect 14     8.2   470   .62  0     false(unreach-call) 1 --- inspect 5.5  3.1  270 0   0      false(unreach-call) 1 --- inspect .88   .89   20    .36 0     - --- inspect - --- inspect
elevator_spec3_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.6 8.6 440 120 0   0     false(unreach-call) 1 wit inspect 8.2  4.4  320 0   0     true -32 --- inspect 15     8.9   540   .62  0     false(unreach-call) 1 --- inspect 5.8  3.2  270 0   0      false(unreach-call) 1 --- inspect .86   .86   20    .36 0     - --- inspect - --- inspect
elevator_spec3_product27_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.6 8.6 440 120 0   0     false(unreach-call) 1 wit inspect 8.2  4.4  290 0   0     true -32 --- inspect 17     9.8   470   .62  0     false(unreach-call) 1 --- inspect 5.4  3.0  270 0   0      false(unreach-call) 1 --- inspect .89   .88   20    .35 0     - --- inspect - --- inspect
elevator_spec3_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.6 8.6 440 110 0   0     false(unreach-call) 1 wit inspect 8.2  4.4  300 0   0     true -32 --- inspect 14     8.3   530   .62  0     false(unreach-call) 1 --- inspect 5.6  3.1  270 0   0      false(unreach-call) 1 --- inspect .90   .93   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.6  4.6  310 0   0     true -32 --- inspect 14     8.2   510   .62  0     false(unreach-call) 1 --- inspect 5.6  3.2  270 0   0      false(unreach-call) 1 --- inspect .89   .89   20    .36 .078 - --- inspect - --- inspect
elevator_spec3_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.6 8.6 440 93 0   0     false(unreach-call) 1 wit inspect 8.0  4.4  320 0   0     true -32 --- inspect 15     8.8   530   .62  0     false(unreach-call) 1 --- inspect 5.6  3.1  270 0   0      false(unreach-call) 1 --- inspect .88   .88   20    .36 0     - --- inspect - --- inspect
elevator_spec3_productSimulator_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 8.7 8.7 430 100 0   .090 error (invalid witness file) 0 --- inspect .68 .43 41 0   0     error (2) 0 --- inspect .020 .021 5.6 0     0     error (invalid witness file) 0 --- inspect .97 .65 47 0   0      error (invalid witness file) 0 --- inspect .0020 .0045 .48 0    0     - --- inspect - --- inspect
elevator_spec9_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.5 8.5 430 100 0   0     false(unreach-call) 1 wit inspect 6.9  3.7  290 0   0     true -32 --- inspect 15     8.7   470   .62  0     false(unreach-call) 1 --- inspect 5.1  2.9  260 0   0      false(unreach-call) 1 --- inspect .84   .84   20    .34 0     - --- inspect - --- inspect
elevator_spec9_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.5 8.5 430 110 0   0     false(unreach-call) 1 wit inspect 7.0  3.7  290 0   0     true -32 --- inspect 16     9.3   470   .086 0     false(unreach-call) 1 --- inspect 5.3  3.0  270 0   0      false(unreach-call) 1 --- inspect .85   .85   20    .36 0     - --- inspect - --- inspect
elevator_spec9_product30_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 7.3  3.9  290 0   0     true -32 --- inspect 15     8.6   460   .62  0     false(unreach-call) 1 --- inspect 5.2  2.9  260 0   0      false(unreach-call) 1 --- inspect .86   .87   20    .36 .074 - --- inspect - --- inspect
elevator_spec9_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.6 8.6 430 96 0   .078 false(unreach-call) 1 wit inspect 7.3  3.9  290 0   0     true -32 --- inspect 15     8.8   470   .62  0     false(unreach-call) 1 --- inspect 5.3  3.0  270 0   0      false(unreach-call) 1 --- inspect .89   .88   20    .36 0     - --- inspect - --- inspect
elevator_spec9_productSimulator_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 8.6 8.6 430 120 0   0     error (invalid witness file) 0 --- inspect .58 .36 40 0   0     error (2) 0 --- inspect .020 .020 5.6 0     0     error (invalid witness file) 0 --- inspect .93 .61 47 0   0      error (invalid witness file) 0 --- inspect .0066 .0085 .54 0    0     - --- inspect - --- inspect
elevator_spec13_product21_true-unreach-call_false-termination.cil.c true 1 wit inspect 8.5 8.5 370 100 0   .074 - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    3000 0   0     out of memory 0 --- inspect 200     130     7000   .63 0    
elevator_spec13_product22_true-unreach-call_false-termination.cil.c true 1 wit inspect 8.6 8.6 370 98 0   .074 - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    3600 0   0     out of memory 0 --- inspect 180     120     7000   .64 0    
elevator_spec13_product23_true-unreach-call_false-termination.cil.c true 1 wit inspect 8.6 8.6 370 110 0   0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    4300 0   0     out of memory 0 --- inspect 240     170     7000   .63 0    
elevator_spec13_product24_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    890    4700 0   0     out of memory 0 --- inspect 220     150     7000   .63 0    
elevator_spec13_product29_true-unreach-call_false-termination.cil.c true 1 wit inspect 8.5 8.5 370 110 0   .074 - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    3100 0   0     out of memory 0 --- inspect 220     150     7000   .64 0    
elevator_spec13_product30_true-unreach-call_false-termination.cil.c true 1 wit inspect 8.7 8.7 370 100 0   .074 - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    3700 0   0     out of memory 0 --- inspect 200     130     7000   .63 0    
elevator_spec13_product31_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    890    4100 0   0     out of memory 0 --- inspect 200     130     7000   .64 0    
elevator_spec13_product32_true-unreach-call_false-termination.cil.c true 1 wit inspect 8.5 8.5 370 130 0   0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    880    4700 0   0     out of memory 0 --- inspect 190     130     7000   .63 0    
elevator_spec13_productSimulator_true-unreach-call_false-termination.cil.c unknown 0 --- inspect 8.6 8.7 430 110 0   0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 41 0   0     error (2) 0 --- inspect .022 .023 5.7 0    0    
elevator_spec14_product03_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.7 8.7 370 140 0   0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 17    9.1  680 0   0     out of memory 0 --- inspect 260     190     7000   .63 0    
elevator_spec14_product11_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 18    9.7  700 0   0     out of memory 0 --- inspect 280     200     7000   .63 0    
elevator_spec14_product19_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.4 8.4 370 100 0   0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 18    10    700 0   0     out of memory 0 --- inspect 270     190     7000   .63 0    
elevator_spec14_product23_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 24    14    1100 0   0     out of memory 0 --- inspect 250     160     7000   .63 0    
elevator_spec14_product27_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 19    10    720 0   0     out of memory 0 --- inspect 320     230     7000   .65 0    
elevator_spec14_product31_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 24    14    1100 0   0     out of memory 0 --- inspect 200     130     7000   .64 0    
elevator_spec1_product01_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.5 8.5 370 120 0   0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 63    52    1600 0   0     out of memory 0 --- inspect 260     180     7000   .63 0    
elevator_spec1_product03_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 73    62    1700 0   0     out of memory 0 --- inspect 250     180     7000   .63 0    
elevator_spec1_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.5 8.6 370 89 0   0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 66    56    1700 0   0     out of memory 0 --- inspect 230     160     7000   .62 0    
elevator_spec1_product11_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 85    73    1800 0   0     out of memory 0 --- inspect 240     170     7000   .65 0    
elevator_spec1_product17_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.7 8.7 370 97 0   0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 76    66    1700 0   0     out of memory 0 --- inspect 230     160     7000   .65 0    
elevator_spec1_product19_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.4 8.5 370 98 0   0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 87    76    1900 0   0     out of memory 0 --- inspect 250     180     7000   .63 0    
elevator_spec1_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 140    130    2200 0   0     out of memory 0 --- inspect 250     170     7000   .63 0    
elevator_spec1_product23_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 140    120    2300 0   0     out of memory 0 --- inspect 300     210     7000   .62 .074
elevator_spec1_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.7 8.7 370 100 0   .074 - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 76    65    1900 0   0     out of memory 0 --- inspect 220     150     7000   .62 0    
elevator_spec1_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 96    85    1900 0   0     out of memory 0 --- inspect 270     190     7000   .64 0    
elevator_spec1_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.4 8.4 370 110 0   0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 270    260    2400 0   0     out of memory 0 --- inspect 190     130     7000   .65 0    
elevator_spec1_product31_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 160    150    2500 0   0     out of memory 0 --- inspect 290     200     7000   .63 0    
elevator_spec2_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 28    19    1000 0   0     out of memory 0 --- inspect 160     100     7000   .64 0    
elevator_spec2_product03_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 30    21    1100 0   0     out of memory 0 --- inspect 190     120     7000   .63 0    
elevator_spec2_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.4 8.4 370 100 0   0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 30    20    1100 0   0     out of memory 0 --- inspect 190     120     7000   .64 0    
elevator_spec2_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.3 8.4 370 96 0   0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 33    23    1200 0   0     out of memory 0 --- inspect 190     120     7000   .64 0    
elevator_spec2_product17_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.4 8.4 370 95 0   0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 32    22    1100 0   0     out of memory 0 --- inspect 160     100     7000   .63 0    
elevator_spec2_product19_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.6 8.7 370 110 0   0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 34    24    1200 0   0     out of memory 0 --- inspect 190     130     7000   .63 0    
elevator_spec2_product21_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 44    34    1300 0   0     out of memory 0 --- inspect 170     110     7000   .65 0    
elevator_spec2_product23_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 45    34    1500 0   0     out of memory 0 --- inspect 280     190     7000   .64 0    
elevator_spec2_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.5 8.5 370 130 0   0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 35    24    1200 0   0     out of memory 0 --- inspect 160     100     7000   .64 .033
elevator_spec2_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.5 8.5 370 120 0   0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 39    29    1300 0   0     out of memory 0 --- inspect 210     130     7000   .63 0    
elevator_spec2_product29_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 53    42    1500 0   0     out of memory 0 --- inspect 200     130     7000   .63 0    
elevator_spec2_product31_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 48    37    1600 0   0     out of memory 0 --- inspect 270     180     7000   .63 0    
elevator_spec3_product01_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 16    8.6  650 0   .074 out of memory 0 --- inspect 140     94     7000   .66 .074
elevator_spec3_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.5 8.5 370 99 0   0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 17    9.2  660 0   0     out of memory 0 --- inspect 150     96     7000   .66 0    
elevator_spec3_product17_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.5 8.5 370 120 0   0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 17    9.2  660 0   0     out of memory 0 --- inspect 150     98     7000   .63 .033
elevator_spec3_product18_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 21    12    840 0   0     out of memory 0 --- inspect 210     140     7000   .64 0    
elevator_spec3_product21_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 20    11    880 0   0     out of memory 0 --- inspect 220     150     7000   .66 0    
elevator_spec3_product22_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 30    17    1400 0   0     out of memory 0 --- inspect 210     150     7000   .64 0    
elevator_spec3_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.6 8.6 370 95 0   0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 17    9.4  680 0   0     out of memory 0 --- inspect 130     83     7000   .63 0    
elevator_spec3_product26_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 23    13    930 0   0     out of memory 0 --- inspect 190     130     7000   .64 0    
elevator_spec3_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.4 8.4 370 110 0   0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 21    11    880 0   0     out of memory 0 --- inspect 200     140     7000   .64 0    
elevator_spec3_product30_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.5 8.6 370 100 0   0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 28    15    1600 0   0     out of memory 0 --- inspect 200     140     7000   .64 .074
elevator_spec9_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 29    20    1100 0   0     out of memory 0 --- inspect 160     100     7000   .65 0    
elevator_spec9_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.6 8.7 370 110 0   0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 33    23    1100 0   0     out of memory 0 --- inspect 190     120     7000   .63 0    
elevator_spec9_product25_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 33    23    1200 0   0     out of memory 0 --- inspect 180     120     7000   .65 0    
elevator_spec9_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.5 8.4 370 110 0   0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 35    25    1200 0   0     out of memory 0 --- inspect 200     130     7000   .64 0    
elevator_spec9_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect 8.4 8.4 370 110 0   0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 60    49    1500 0   0     out of memory 0 --- inspect 190     130     7000   .65 0    
elevator_spec9_product31_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 53    41    1600 0   0     out of memory 0 --- inspect 170     120     7000   .46 0    
email_spec0_product16_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 8.8 8.7 430 110 0   0     error (invalid witness file) 0 --- inspect .58 .36 40 0   0     error (2) 0 --- inspect .020 .021 5.6 0     0     error (invalid witness file) 0 --- inspect .95 .61 47 0   0      error (invalid witness file) 0 --- inspect .0046 .0065 .53 0    0     - --- inspect - --- inspect
email_spec0_product21_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 8.7 8.7 430 110 0   0     error (invalid witness file) 0 --- inspect .60 .36 40 0   0     error (2) 0 --- inspect .021 .023 5.6 0     0     error (invalid witness file) 0 --- inspect .98 .62 49 0   0      error (invalid witness file) 0 --- inspect .0056 .0096 .57 0    0     - --- inspect - --- inspect
email_spec0_product22_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 8.6 8.5 430 100 0   0     error (invalid witness file) 0 --- inspect .71 .44 40 0   0     error (2) 0 --- inspect .040 .041 5.5 0     0     error (invalid witness file) 0 --- inspect .97 .66 47 0   0      error (invalid witness file) 0 --- inspect .0036 .0046 .53 0    0     - --- inspect - --- inspect
email_spec0_product26_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 8.7 8.7 430 130 0   .066 error (invalid witness file) 0 --- inspect .68 .44 41 0   0     error (2) 0 --- inspect .019 .020 5.6 0     0     error (invalid witness file) 0 --- inspect .92 .59 47 0   0      error (invalid witness file) 0 --- inspect .0056 .0069 .53 0    0     - --- inspect - --- inspect
email_spec0_product31_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 8.5 8.5 430 120 0   0     error (invalid witness file) 0 --- inspect .60 .40 40 0   0     error (2) 0 --- inspect .050 .051 5.5 0     0     error (invalid witness file) 0 --- inspect 1.0  .66 49 0   0      error (invalid witness file) 0 --- inspect .0059 .0093 .53 0    0     - --- inspect - --- inspect
email_spec0_product33_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 8.5 8.5 430 120 0   0     error (invalid witness file) 0 --- inspect .62 .40 40 0   0     error (2) 0 --- inspect .051 .052 5.5 0     0     error (invalid witness file) 0 --- inspect .99 .65 48 0   0      error (invalid witness file) 0 --- inspect .0054 .0064 .53 0    0     - --- inspect - --- inspect
email_spec0_product34_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 8.6 8.6 430 120 0   0     error (invalid witness file) 0 --- inspect .62 .39 42 0   0     error (2) 0 --- inspect .028 .029 5.6 0     0     error (invalid witness file) 0 --- inspect .92 .60 47 0   0      error (invalid witness file) 0 --- inspect .0056 .0069 .53 0    0     - --- inspect - --- inspect
email_spec0_product35_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 8.6 8.6 430 100 0   0     error (invalid witness file) 0 --- inspect .59 .37 40 0   0     error (2) 0 --- inspect .052 .053 5.5 0     0     error (invalid witness file) 0 --- inspect .94 .62 47 0   0      error (invalid witness file) 0 --- inspect .0047 .0059 .53 0    0     - --- inspect - --- inspect
email_spec0_productSimulator_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 8.7 8.7 430 130 0   0     error (invalid witness file) 0 --- inspect .66 .41 41 0   0     error (2) 0 --- inspect .024 .025 5.5 0     0     error (invalid witness file) 0 --- inspect .94 .60 47 0   0      error (invalid witness file) 0 --- inspect .0054 .0069 .53 0    0     - --- inspect - --- inspect
email_spec11_product15_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 8.7 8.7 430 120 0   0     error (invalid witness file) 0 --- inspect .65 .40 41 0   0     error (2) 0 --- inspect .024 .026 5.5 0     0     error (invalid witness file) 0 --- inspect .97 .64 47 0   0      error (invalid witness file) 0 --- inspect .0060 .0075 .54 0    0     - --- inspect - --- inspect
email_spec11_product20_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 8.5 8.5 430 100 0   0     error (invalid witness file) 0 --- inspect .60 .37 40 0   0     error (2) 0 --- inspect .048 .051 5.6 0     0     error (invalid witness file) 0 --- inspect .97 .63 48 0   0      error (invalid witness file) 0 --- inspect .0020 .0030 .52 0    0     - --- inspect - --- inspect
email_spec11_product22_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 8.7 8.7 430 93 0   0     error (invalid witness file) 0 --- inspect .59 .36 40 0   0     error (2) 0 --- inspect .048 .052 5.5 0     0     error (invalid witness file) 0 --- inspect .94 .61 47 0   0      error (invalid witness file) 0 --- inspect .0057 .0076 .54 0    0     - --- inspect - --- inspect
email_spec11_product26_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 8.7 8.7 430 97 0   0     error (invalid witness file) 0 --- inspect .60 .37 41 0   0     error (2) 0 --- inspect .020 .021 5.6 0     0     error (invalid witness file) 0 --- inspect .96 .62 48 0   0      error (invalid witness file) 0 --- inspect .0067 .0088 .53 0    0     - --- inspect - --- inspect
email_spec11_product30_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 8.7 8.6 430 96 0   0     error (invalid witness file) 0 --- inspect .63 .39 42 0   0     error (2) 0 --- inspect .023 .024 5.6 0     0     error (invalid witness file) 0 --- inspect .98 .63 48 0   0      error (invalid witness file) 0 --- inspect .0052 .0068 .41 0    0     - --- inspect - --- inspect
email_spec11_product32_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 8.5 8.5 430 110 0   0     error (invalid witness file) 0 --- inspect .60 .39 40 0   0     error (2) 0 --- inspect .038 .040 5.5 0     0     error (invalid witness file) 0 --- inspect .92 .59 47 0   0      error (invalid witness file) 0 --- inspect .0053 .0064 .53 0    0     - --- inspect - --- inspect
email_spec11_product33_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 8.7 8.7 430 120 0   0     error (invalid witness file) 0 --- inspect .59 .37 40 0   0     error (2) 0 --- inspect .043 .047 5.5 0     0     error (invalid witness file) 0 --- inspect .92 .62 47 0   0      error (invalid witness file) 0 --- inspect .0047 .0052 .40 0    0     - --- inspect - --- inspect
email_spec11_product35_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 8.8 8.7 430 100 0   0     error (invalid witness file) 0 --- inspect .61 .39 41 0   0     error (2) 0 --- inspect .053 .054 5.5 0     0     error (invalid witness file) 0 --- inspect .93 .61 46 0   0      error (invalid witness file) 0 --- inspect .0044 .0054 .54 0    0     - --- inspect - --- inspect
email_spec11_productSimulator_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 8.8 8.8 430 100 0   0     error (invalid witness file) 0 --- inspect .61 .40 41 0   0     error (2) 0 --- inspect .049 .050 5.5 0     0     error (invalid witness file) 0 --- inspect .94 .59 47 0   0      error (invalid witness file) 0 --- inspect .0056 .0071 .52 0    0     - --- inspect - --- inspect
email_spec1_product14_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 8.6 8.6 430 98 0   0     error (invalid witness file) 0 --- inspect .60 .38 41 0   0     error (2) 0 --- inspect .021 .023 5.7 0     0     error (invalid witness file) 0 --- inspect .93 .62 46 0   0      error (invalid witness file) 0 --- inspect .0057 .0069 .53 0    0     - --- inspect - --- inspect
email_spec1_product15_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 8.7 8.7 430 100 0   0     error (invalid witness file) 0 --- inspect .62 .38 41 0   0     error (2) 0 --- inspect .039 .040 5.5 0     0     error (invalid witness file) 0 --- inspect .98 .65 47 0   0      error (invalid witness file) 0 --- inspect .0018 .0022 .53 0    0     - --- inspect -