Tool SMACK 1.9.3 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-07 19:13:55 CET 2018-12-08 22:05:35 CET 2018-12-08 23:40:49 CET 2018-12-08 23:45:33 CET 2018-12-12 21:01:56 CET 2018-12-08 20:48:05 CET 2018-12-08 22:13:47 CET
Run set smack.sv-comp19_prop-reachsafety.ReachSafety-ProductLines cpa-seq-validate-violation-witnesses-smack.sv-comp19_prop-reachsafety.ReachSafety-ProductLines uautomizer-validate-violation-witnesses-smack.sv-comp19_prop-reachsafety.ReachSafety-ProductLines cpa-witness2test-validate-violation-witnesses-smack.sv-comp19_prop-reachsafety.ReachSafety-ProductLines fshell-witness2test-validate-violation-witnesses-smack.sv-comp19_prop-reachsafety.ReachSafety-ProductLines cpa-seq-validate-correctness-witnesses-smack.sv-comp19_prop-reachsafety.ReachSafety-ProductLines uautomizer-validate-correctness-witnesses-smack.sv-comp19_prop-reachsafety.ReachSafety-ProductLines
Options -w error-witness.graphml -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/smack.2018-12-07_1913.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/smack.2018-12-07_1913.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/smack.2018-12-07_1913.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/smack.2018-12-07_1913.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/smack.2018-12-07_1913.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/smack.2018-12-07_1913.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 9.7 9.1 250 130 2.2  0     false(unreach-call) 1 wit inspect 8.5  4.5  320 0   0     true -32 --- inspect 18     10     510   .62 0      false(unreach-call) 1 --- inspect 12    6.2  480 0   0      false(unreach-call) 1 --- inspect .99   .98   21    .42 0     - --- inspect - --- inspect
elevator_spec14_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 11   10   250 140 2.2  0     false(unreach-call) 1 wit inspect 8.0  4.3  310 0   .074 true -32 --- inspect 14     8.1   520   .66 0      false(unreach-call) 1 --- inspect 13    7.1  600 0   0      false(unreach-call) 1 --- inspect 1.0    1.0    21    .45 0     - --- inspect - --- inspect
elevator_spec14_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.3 7.6 230 100 2.2  0     false(unreach-call) 1 wit inspect 7.3  3.9  300 0   0     true -32 --- inspect 21     11     510   .66 0      false(unreach-call) 1 --- inspect 14    7.2  490 0   0      false(unreach-call) 1 --- inspect 1.0    1.0    21    .43 0     - --- inspect - --- inspect
elevator_spec14_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 11   10   250 120 2.3  0     false(unreach-call) 1 wit inspect 9.2  4.9  310 0   0     true -32 --- inspect 19     11     470   .66 0      false(unreach-call) 1 --- inspect 14    7.4  580 0   0      false(unreach-call) 1 --- inspect 1.0    1.0    21    .45 0     - --- inspect - --- inspect
elevator_spec14_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 16   15   300 230 2.5  0     false(unreach-call) 1 wit inspect 8.3  4.4  310 0   0     true -32 --- inspect 18     10     530   .66 0      false(unreach-call) 1 --- inspect 14    7.4  620 0   1.2    false(unreach-call) 1 --- inspect 1.1    1.1    21    .48 0     - --- inspect - --- inspect
elevator_spec1_product18_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 8.1 7.6 240 98 2.2  0     false(unreach-call) 1 wit inspect 7.5  4.0  300 0   0     true -32 --- inspect 19     11     460   .66 0      false(unreach-call) 1 --- inspect 14    7.6  620 0   0      false(unreach-call) 1 --- inspect 1.0    1.0    21    .43 0     - --- inspect - --- inspect
elevator_spec1_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 9.2 8.6 230 130 2.3  0     false(unreach-call) 1 wit inspect 8.7  4.6  280 0   0     true -32 --- inspect 17     10     520   .66 0      false(unreach-call) 1 --- inspect 22    11    690 0   .086  false(unreach-call) 1 --- inspect 1.1    1.0    21    .45 0     - --- inspect - --- inspect
elevator_spec1_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 9.4 9.1 240 110 2.3  0     false(unreach-call) 1 wit inspect 7.1  3.8  320 0   0     true -32 --- inspect 21     12     520   .66 0      false(unreach-call) 1 --- inspect 17    9.1  610 0   0      false(unreach-call) 1 --- inspect 1.1    1.1    21    .45 0     - --- inspect - --- inspect
elevator_spec1_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 10   9.7 250 120 2.4  0     false(unreach-call) 1 wit inspect 8.4  4.5  300 0   0     true -32 --- inspect 15     8.8   530   .62 0      false(unreach-call) 1 --- inspect 17    9.1  630 0   0      false(unreach-call) 1 --- inspect 1.1    1.1    21    .48 0     - --- inspect - --- inspect
elevator_spec1_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 7.7 7.1 230 94 2.3  0     false(unreach-call) 1 wit inspect 7.5  4.0  280 0   .057 true -32 --- inspect 17     9.4   460   .62 0      false(unreach-call) 1 --- inspect 18    9.3  620 0   4.9    false(unreach-call) 1 --- inspect 1.0    1.0    21    .43 0     - --- inspect - --- inspect
elevator_spec1_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 10   9.6 250 140 2.3  0     false(unreach-call) 1 wit inspect 7.0  3.8  280 0   0     true -32 --- inspect 17     9.3   470   .62 0      false(unreach-call) 1 --- inspect 20    11    670 0   0      false(unreach-call) 1 --- inspect 1.1    1.0    21    .45 0     - --- inspect - --- inspect
elevator_spec1_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 10   9.7 240 130 2.3  0     false(unreach-call) 1 wit inspect 7.2  3.9  310 0   0     true -32 --- inspect 15     8.9   530   .62 0      false(unreach-call) 1 --- inspect 16    8.4  620 0   0      false(unreach-call) 1 --- inspect 1.1    1.1    21    .46 0     - --- inspect - --- inspect
elevator_spec1_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 9.9 9.2 250 130 2.4  0     false(unreach-call) 1 wit inspect 8.3  4.5  340 0   0     true -32 --- inspect 23     13     480   .62 0      false(unreach-call) 1 --- inspect 19    10    680 0   0      false(unreach-call) 1 --- inspect 1.1    1.1    21    .48 0     - --- inspect - --- inspect
elevator_spec1_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 19   18   320 200 2.6  0     false(unreach-call) 1 wit inspect 8.2  4.4  330 0   0     true -32 --- inspect 21     12     520   .62 0      false(unreach-call) 1 --- inspect 22    12    810 0   0      false(unreach-call) 1 --- inspect 1.1    1.1    21    .52 0     - --- inspect - --- inspect
elevator_spec2_product18_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 10   9.6 250 150 2.2  0     false(unreach-call) 1 wit inspect 7.6  4.0  300 0   0     true -32 --- inspect 17     9.6   470   .62 0      false(unreach-call) 1 --- inspect 14    7.3  580 0   0      false(unreach-call) 1 --- inspect 1.0    1.1    21    .43 0     - --- inspect - --- inspect
elevator_spec2_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 9.9 9.6 240 140 2.3  0     false(unreach-call) 1 wit inspect 7.7  4.1  310 0   0     true -32 --- inspect 17     10     470   .62 .074  false(unreach-call) 1 --- inspect 15    8.1  640 0   0      false(unreach-call) 1 --- inspect 1.1    1.1    21    .45 0     - --- inspect - --- inspect
elevator_spec2_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 9.8 9.1 240 140 2.3  0     false(unreach-call) 1 wit inspect 7.6  4.1  290 0   0     true -32 --- inspect 15     8.9   470   .62 0      false(unreach-call) 1 --- inspect 15    7.6  600 0   .086  false(unreach-call) 1 --- inspect 1.0    1.0    21    .45 0     - --- inspect - --- inspect
elevator_spec2_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 10   9.6 250 130 2.4  0     false(unreach-call) 1 wit inspect 7.9  4.3  290 0   0     true -32 --- inspect 21     12     460   .62 0      false(unreach-call) 1 --- inspect 16    8.4  670 0   .078  false(unreach-call) 1 --- inspect 1.1    1.1    21    .47 0     - --- inspect - --- inspect
elevator_spec2_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 9.1 8.6 230 110 2.3  0     false(unreach-call) 1 wit inspect 8.8  4.7  290 0   0     true -32 --- inspect 15     8.7   470   .62 0      false(unreach-call) 1 --- inspect 14    7.1  580 0   .086  false(unreach-call) 1 --- inspect 1.0    1.0    21    .43 0     - --- inspect - --- inspect
elevator_spec2_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 9.4 8.6 240 110 2.3  0     false(unreach-call) 1 wit inspect 7.3  3.9  280 0   0     true -32 --- inspect 14     8.2   470   .62 0      false(unreach-call) 1 --- inspect 14    7.6  650 0   0      false(unreach-call) 1 --- inspect 1.0    1.0    21    .45 0     - --- inspect - --- inspect
elevator_spec2_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 9.3 8.7 230 130 2.3  0     false(unreach-call) 1 wit inspect 8.9  4.7  310 0   0     true -32 --- inspect 16     8.9   470   .62 .074  false(unreach-call) 1 --- inspect 15    7.9  590 0   0      false(unreach-call) 1 --- inspect 1.1    1.1    21    .45 .074 - --- inspect - --- inspect
elevator_spec2_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 11   11   260 130 2.4  0     false(unreach-call) 1 wit inspect 7.6  4.1  290 0   0     true -32 --- inspect 19     10     460   .62 0      false(unreach-call) 1 --- inspect 21    11    680 0   0      false(unreach-call) 1 --- inspect 1.1    1.1    21    .48 0     - --- inspect - --- inspect
elevator_spec2_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 14   13   270 180 2.6  0     false(unreach-call) 1 wit inspect 10    5.4  310 0   0     true -32 --- inspect 17     10     470   .66 0      false(unreach-call) 1 --- inspect 21    11    720 0   .16   false(unreach-call) 1 --- inspect 1.1    1.1    21    .50 .082 - --- inspect - --- inspect
elevator_spec3_product03_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 10   9.7 240 120 2.3  0     false(unreach-call) 1 wit inspect 7.2  3.9  290 0   0     true -32 --- inspect 15     8.8   510   .66 0      false(unreach-call) 1 --- inspect 17    8.8  580 0   0      false(unreach-call) 1 --- inspect 1.1    1.1    21    .44 0     - --- inspect - --- inspect
elevator_spec3_product11_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 11   10   240 140 2.3  0     false(unreach-call) 1 wit inspect 9.2  5.0  300 0   0     true -32 --- inspect 16     9.2   470   .62 0      false(unreach-call) 1 --- inspect 18    9.7  580 0   0      false(unreach-call) 1 --- inspect 1.1    1.1    21    .44 0     - --- inspect - --- inspect
elevator_spec3_product19_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 14   14   290 180 2.3  0     false(unreach-call) 1 wit inspect 7.8  4.2  300 0   0     true -32 --- inspect 15     8.9   470   .66 0      false(unreach-call) 1 --- inspect 20    10    630 0   0      false(unreach-call) 1 --- inspect 1.1    1.1    21    .45 0     - --- inspect - --- inspect
elevator_spec3_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 17   16   320 200 2.3  0     false(unreach-call) 1 wit inspect 8.4  4.5  330 0   0     true -32 --- inspect 15     9.0   460   .62 0      false(unreach-call) 1 --- inspect 14    7.5  580 0   0      false(unreach-call) 1 --- inspect 1.1    1.1    21    .45 0     - --- inspect - --- inspect
elevator_spec3_product23_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 15   14   290 180 2.4  0     false(unreach-call) 1 wit inspect 7.8  4.2  310 0   0     true -32 --- inspect 18     9.9   530   .66 0      false(unreach-call) 1 --- inspect 16    8.7  640 0   0      false(unreach-call) 1 --- inspect 1.1    1.1    21    .47 0     - --- inspect - --- inspect
elevator_spec3_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 13   12   260 180 2.4  0     false(unreach-call) 1 wit inspect 8.7  4.6  350 0   0     true -32 --- inspect 17     9.6   520   .62 0      false(unreach-call) 1 --- inspect 16    8.8  680 0   0      false(unreach-call) 1 --- inspect 1.1    1.1    21    .48 0     - --- inspect - --- inspect
elevator_spec3_product27_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 14   13   290 180 2.3  0     false(unreach-call) 1 wit inspect 10    5.4  320 0   0     true -32 --- inspect 17     9.6   470   .66 .0041 false(unreach-call) 1 --- inspect 15    8.2  580 0   0      false(unreach-call) 1 --- inspect 1.1    1.1    21    .45 .074 - --- inspect - --- inspect
elevator_spec3_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 15   14   300 170 2.4  0     false(unreach-call) 1 wit inspect 8.5  4.5  330 0   0     true -32 --- inspect 14     8.2   530   .66 .074  false(unreach-call) 1 --- inspect 15    8.1  620 0   0      false(unreach-call) 1 --- inspect 1.1    1.1    21    .45 0     - --- inspect - --- inspect
elevator_spec3_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 15   14   300 180 2.4  0     false(unreach-call) 1 wit inspect 8.5  4.6  350 0   0     true -32 --- inspect 15     8.3   470   .62 0      false(unreach-call) 1 --- inspect 17    9.0  630 0   0      false(unreach-call) 1 --- inspect 1.1    1.1    21    .47 0     - --- inspect - --- inspect
elevator_spec3_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 19   18   300 220 2.4  0     false(unreach-call) 1 wit inspect 9.4  5.1  360 0   0     true -32 --- inspect 17     9.5   470   .66 .078  false(unreach-call) 1 --- inspect 17    8.9  620 0   0      false(unreach-call) 1 --- inspect 1.1    1.1    21    .48 0     - --- inspect - --- inspect
elevator_spec3_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 79   77   450 730 2.6  0     false(unreach-call) 1 wit inspect 11    5.9  390 0   .082 true -32 --- inspect 18     10     530   .62 0      false(unreach-call) 1 --- inspect 19    10    760 0   .082  false(unreach-call) 1 --- inspect 1.2    1.2    22    .52 0     - --- inspect - --- inspect
elevator_spec9_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 9.8 9.2 240 120 2.3  0     false(unreach-call) 1 wit inspect 7.2  3.9  280 0   0     true -32 --- inspect 18     10     470   .62 0      false(unreach-call) 1 --- inspect 14    7.6  590 0   0      false(unreach-call) 1 --- inspect 1.0    1.0    21    .43 0     - --- inspect - --- inspect
elevator_spec9_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 11   10   250 130 2.3  0     false(unreach-call) 1 wit inspect 7.4  3.9  290 0   0     true -32 --- inspect 15     8.7   520   .66 0      false(unreach-call) 1 --- inspect 22    11    680 0   0      false(unreach-call) 1 --- inspect 1.0    1.0    21    .45 0     - --- inspect - --- inspect
elevator_spec9_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 9.4 8.7 240 130 2.3  0     false(unreach-call) 1 wit inspect 9.3  5.0  310 0   0     true -32 --- inspect 15     8.6   520   .62 0      false(unreach-call) 1 --- inspect 18    9.2  580 0   0      false(unreach-call) 1 --- inspect 1.1    1.1    21    .46 0     - --- inspect - --- inspect
elevator_spec9_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 12   11   260 150 2.4  0     false(unreach-call) 1 wit inspect 7.1  3.8  320 0   0     true -32 --- inspect 22     12     470   .66 0      false(unreach-call) 1 --- inspect 18    9.9  810 0   0      false(unreach-call) 1 --- inspect 1.1    1.1    21    .48 .078 - --- inspect - --- inspect
elevator_spec9_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 16   15   270 210 2.6  0     false(unreach-call) 1 wit inspect 8.2  4.4  300 0   .082 true -32 --- inspect 17     10     510   .62 0      false(unreach-call) 1 --- inspect 21    12    960 0   0      false(unreach-call) 1 --- inspect 1.1    1.1    21    .52 0     - --- inspect - --- inspect
elevator_spec13_product21_true-unreach-call_false-termination.cil.c true 1 wit inspect 890   880   880 6200 2.4  0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    880    2700 0   0      out of memory 0 --- inspect 200     130     7000   .66 0    
elevator_spec13_product22_true-unreach-call_false-termination.cil.c true 1 wit inspect 890   880   810 6000 2.3  0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    880    3400 0   0      out of memory 0 --- inspect 230     150     7000   .44 0    
elevator_spec13_product23_true-unreach-call_false-termination.cil.c true 1 wit inspect 890   880   850 8400 2.4  0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    3800 0   0      out of memory 0 --- inspect 250     170     7000   1.3  .020
elevator_spec13_product24_true-unreach-call_false-termination.cil.c true 1 wit inspect 890   880   810 5800 2.4  0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    880    4600 0   0      out of memory 0 --- inspect 230     160     7000   .67 .074
elevator_spec13_product29_true-unreach-call_false-termination.cil.c true 1 wit inspect 890   880   870 7600 2.4  0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    2800 0   .074  out of memory 0 --- inspect 200     130     7000   .69 0    
elevator_spec13_product30_true-unreach-call_false-termination.cil.c true 1 wit inspect 890   880   820 6800 2.4  0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    880    3400 0   0      out of memory 0 --- inspect 260     170     7000   .62 0    
elevator_spec13_product31_true-unreach-call_false-termination.cil.c true 1 wit inspect 890   880   840 5500 2.4  0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    3700 0   0      out of memory 0 --- inspect 230     150     7000   .64 0    
elevator_spec13_product32_true-unreach-call_false-termination.cil.c true 1 wit inspect 890   880   830 5900 2.4  0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    880    4300 0   0      out of memory 0 --- inspect 210     150     7000   .69 0    
elevator_spec13_productSimulator_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 890   930   790 6600 2.7  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .46 40 0   0      error (2) 0 --- inspect .022 .022 5.6 0    0    
elevator_spec14_product03_true-unreach-call_true-termination.cil.c true 2 wit inspect 190   190   710 1500 2.1  0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 17    9.5  690 0   0      out of memory 0 --- inspect 310     220     7000   .66 0    
elevator_spec14_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect 130   130   630 1100 2.2  0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 21    12    680 0   0      out of memory 0 --- inspect 290     210     7000   .65 0    
elevator_spec14_product19_true-unreach-call_true-termination.cil.c true 2 wit inspect 180   170   680 1500 2.1  0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 21    12    700 0   0      out of memory 0 --- inspect 340     250     7000   .63 0    
elevator_spec14_product23_true-unreach-call_true-termination.cil.c true 2 wit inspect 160   160   620 1300 2.2  0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 28    17    1100 0   0      out of memory 0 --- inspect 230     150     7000   .65 0    
elevator_spec14_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect 240   240   750 2200 2.2  0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 27    15    720 0   0      out of memory 0 --- inspect 280     190     7000   .66 0    
elevator_spec14_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect 170   170   720 1200 2.2  0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 32    19    1100 0   0      out of memory 0 --- inspect 240     160     7000   .65 0    
elevator_spec1_product01_true-unreach-call_true-termination.cil.c true 2 wit inspect 48   46   470 610 2.2  0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 74    61    1600 0   0      out of memory 0 --- inspect 280     200     7000   .61 0    
elevator_spec1_product03_true-unreach-call_true-termination.cil.c true 2 wit inspect 94   92   590 730 2.2  0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 92    76    1700 0   0      out of memory 0 --- inspect 300     210     7000   .65 0    
elevator_spec1_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect 50   48   490 540 2.2  0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 70    58    1700 0   0      out of memory 0 --- inspect 270     190     7000   .65 0    
elevator_spec1_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect 110   110   620 970 2.3  0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 99    86    1800 0   0      out of memory 0 --- inspect 260     180     7000   .65 0    
elevator_spec1_product17_true-unreach-call_true-termination.cil.c true 2 wit inspect 69   67   540 670 2.2  0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 91    77    1700 0   0      out of memory 0 --- inspect 270     190     7000   .69 0    
elevator_spec1_product19_true-unreach-call_true-termination.cil.c true 2 wit inspect 96   94   580 990 2.3  0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 100    89    1900 0   0      out of memory 0 --- inspect 320     230     7000   .64 0    
elevator_spec1_product21_true-unreach-call_true-termination.cil.c true 2 wit inspect 130   130   580 1100 2.3  0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 170    160    2300 0   0      out of memory 0 --- inspect 240     160     7000   .64 0    
elevator_spec1_product23_true-unreach-call_true-termination.cil.c true 2 wit inspect 220   210   670 1800 2.3  0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 170    150    2300 0   0      out of memory 0 --- inspect 310     220     7000   .64 0    
elevator_spec1_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect 64   62   520 660 2.2  0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 100    85    1800 0   0      out of memory 0 --- inspect 320     220     7000   .65 0    
elevator_spec1_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect 72   70   540 710 2.3  0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 130    110    2000 0   0      out of memory 0 --- inspect 260     180     7000   .66 0    
elevator_spec1_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect 130   130   600 1200 2.3  0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 340    330    2300 0   0      out of memory 0 --- inspect 290     200     7000   .66 0    
elevator_spec1_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect 210   210   710 2200 2.4  0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 200    180    2400 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 27   26   430 320 2.2  0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 35    23    1000 0   0      out of memory 0 --- inspect 180     120     7000   .64 0    
elevator_spec2_product03_true-unreach-call_true-termination.cil.c true 2 wit inspect 33   32   430 310 2.2  0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 41    27    1100 0   0      out of memory 0 --- inspect 220     140     7000   .66 0    
elevator_spec2_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect 33   32   430 320 2.2  0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 37    24    1100 0   0      out of memory 0 --- inspect 180     120     7000   .66 0    
elevator_spec2_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect 36   34   440 350 2.2  0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 39    27    1100 0   0      out of memory 0 --- inspect 220     140     7000   1.5  0    
elevator_spec2_product17_true-unreach-call_true-termination.cil.c true 2 wit inspect 29   28   420 290 2.2  2.3   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 39    27    1100 0   0      out of memory 0 --- inspect 190     120     7000   .63 0    
elevator_spec2_product19_true-unreach-call_true-termination.cil.c true 2 wit inspect 39   38   450 350 2.3  0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 41    29    1200 0   0      out of memory 0 --- inspect 240     160     7000   .63 0    
elevator_spec2_product21_true-unreach-call_true-termination.cil.c true 2 wit inspect 33   32   440 330 2.3  0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 68    51    1300 0   0      out of memory 0 --- inspect 210     140     7000   .63 0    
elevator_spec2_product23_true-unreach-call_true-termination.cil.c true 2 wit inspect 32   31   430 330 2.3  0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 54    41    1500 0   0      out of memory 0 --- inspect 300     210     7000   .63 0    
elevator_spec2_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect 30   29   420 320 2.2  0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 44    30    1200 0   0      out of memory 0 --- inspect 170     110     7000   .70 0    
elevator_spec2_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect 43   42   480 390 2.3  0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 46    34    1200 0   0      out of memory 0 --- inspect 190     130     7000   .65 0    
elevator_spec2_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect 25   24   370 250 2.3  0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 62    51    1400 0   0      out of memory 0 --- inspect 190     130     7000   .66 .033
elevator_spec2_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect 40   39   450 390 2.4  0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 65    50    1500 0   0      out of memory 0 --- inspect 280     190     7000   .65 0    
elevator_spec3_product01_true-unreach-call_true-termination.cil.c true 2 wit inspect 99   96   540 780 2.2  0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 21    12    650 0   0      out of memory 0 --- inspect 190     120     7000   .64 0    
elevator_spec3_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect 120   120   590 950 2.3  0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 19    10    660 0   0      out of memory 0 --- inspect 160     100     7000   .64 0    
elevator_spec3_product17_true-unreach-call_true-termination.cil.c true 2 wit inspect 100   100   600 980 2.3  0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 21    11    660 0   0      out of memory 0 --- inspect 210     140     7000   .63 .074
elevator_spec3_product18_true-unreach-call_true-termination.cil.c true 2 wit inspect 120   120   580 1100 2.3  0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 25    14    880 0   0      out of memory 0 --- inspect 230     150     7000   .64 0    
elevator_spec3_product21_true-unreach-call_true-termination.cil.c true 2 wit inspect 220   220   730 1700 2.3  0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 27    15    900 0   0      out of memory 0 --- inspect 230     160     7000   .63 0    
elevator_spec3_product22_true-unreach-call_true-termination.cil.c true 2 wit inspect 130   130   550 1100 2.4  0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 38    21    1400 0   0      out of memory 0 --- inspect 260     180     7000   .63 0    
elevator_spec3_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect 95   93   580 670 2.3  0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 18    10    680 0   0      out of memory 0 --- inspect 190     120     7000   .64 0    
elevator_spec3_product26_true-unreach-call_true-termination.cil.c true 2 wit inspect 98   96   530 820 2.3  0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 28    15    950 0   .025  out of memory 0 --- inspect 240     160     7000   .64 0    
elevator_spec3_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect 200   200   650 1600 2.4  0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 24    13    890 0   0      out of memory 0 --- inspect 240     170     7000   .64 0    
elevator_spec3_product30_true-unreach-call_true-termination.cil.c true 2 wit inspect 190   180   570 1500 2.4  0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 40    22    1600 0   0      out of memory 0 --- inspect 240     160     7000   .66 0    
elevator_spec9_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect 32   31   440 340 2.2  0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 36    24    1100 0   .074  out of memory 0 --- inspect 200     130     7000   .66 0    
elevator_spec9_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect 30   29   420 280 2.2  0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 42    29    1200 0   0      out of memory 0 --- inspect 170     110     7000   .63 0    
elevator_spec9_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect 31   30   440 370 2.2  0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 41    29    1200 0   0      out of memory 0 --- inspect 220     150     7000   .65 0    
elevator_spec9_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect 38   37   420 340 2.3  0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 47    33    1200 0   0      out of memory 0 --- inspect 180     120     7000   .66 0    
elevator_spec9_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect 37   36   450 370 2.3  0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 71    58    1400 0   .074  out of memory 0 --- inspect 190     130     7000   .70 0    
elevator_spec9_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect 26   25   440 340 2.3  0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 76    60    1500 0   0      out of memory 0 --- inspect 210     140     7000   .63 0    
email_spec0_product16_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 39   38   300 470 1.8  0     false(unreach-call) 1 wit inspect 6.5  3.5  280 0   .13  true -32 --- inspect 14     8.0   460   .66 0      false(unreach-call) 1 --- inspect 7.7  4.2  300 0   0      false(unreach-call) 1 --- inspect .94   .94   21    .43 0     - --- inspect - --- inspect
email_spec0_product21_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 59   57   370 640 2.0  0     false(unreach-call) 1 wit inspect 6.7  3.6  280 0   0     true -32 --- inspect 16     9.3   470   .66 0      false(unreach-call) 1 --- inspect 7.4  4.0  300 0   0      false(unreach-call) 1 --- inspect .96   .96   21    .44 0     - --- inspect - --- inspect
email_spec0_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 55   54   320 660 1.8  0     false(unreach-call) 1 wit inspect 7.1  3.8  300 0   0     true -32 --- inspect 16     9.0   460   .62 0      false(unreach-call) 1 --- inspect 7.0  3.9  280 0   .066  false(unreach-call) 1 --- inspect .96   .95   21    .44 0     - --- inspect - --- inspect
email_spec0_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 150   150   400 1400 2.0  0     false(unreach-call) 1 wit inspect 7.6  4.1  290 0   .066 true -32 --- inspect 20     11     490   .62 0      false(unreach-call) 1 --- inspect 7.3  4.0  320 0   0      false(unreach-call) 1 --- inspect .99   .99   21    .45 0     - --- inspect - --- inspect
email_spec0_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 27   26   310 390 1.9  0     false(unreach-call) 1 wit inspect 7.1  3.8  300 0   0     true -32 --- inspect 17     9.4   490   .62 .066  false(unreach-call) 1 --- inspect 7.7  4.1  290 0   0      false(unreach-call) 1 --- inspect .99   .98   21    .45 0     - --- inspect - --- inspect
email_spec0_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 40   39   330 460 2.0  0     false(unreach-call) 1 wit inspect 6.6  3.5  280 0   0     true -32 --- inspect 15     8.4   470   .62 0      false(unreach-call) 1 --- inspect 7.6  4.1  310 0   0      false(unreach-call) 1 --- inspect 1.0    .99   21    .46 0     - --- inspect - --- inspect
email_spec0_product34_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 72   70   400 750 2.1  0     false(unreach-call) 1 wit inspect 8.8  4.7  300 0   0     true -32 --- inspect 18     9.9   510   .62 0      false(unreach-call) 1 --- inspect 8.4  4.5  320 0   0      false(unreach-call) 1 --- inspect 1.0    1.1    21    .39 .066 - --- inspect - --- inspect
email_spec0_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 58   56   390 590 2.2  0     false(unreach-call) 1 wit inspect 8.1  4.3  280 0   0     true -32 --- inspect 16     9.1   460   .62 0      false(unreach-call) 1 --- inspect 8.3  4.5  340 0   0      false(unreach-call) 1 --- inspect .98   .98   21    .47 0     - --- inspect - --- inspect
email_spec0_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 540   540   900 4200 2.5  0     false(unreach-call) 1 wit inspect 10    5.5  290 0   0     true -32 --- inspect 18     9.8   530   .62 0      false(unreach-call) 1 --- inspect 8.7  4.8  380 0   0      false(unreach-call) 1 --- inspect 1.0    1.0    21    .51 0     - --- inspect - --- inspect
email_spec11_product15_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 50   49   300 670 1.7  0     false(unreach-call) 1 wit inspect 8.9  4.7  300 0   0     true -32 --- inspect 15     8.5   460   .62 0      false(unreach-call) 1 --- inspect 7.2  3.9  290 0   0      false(unreach-call) 1 --- inspect 1.0    1.0    21    .44 0     - --- inspect - --- inspect
email_spec11_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 96   94   370 1100 2.0  0     false(unreach-call) 1 wit inspect 7.6  4.0  300 0   0     true -32 --- inspect 15     8.5   490   .66 0      false(unreach-call) 1 --- inspect 8.7  4.7  320 0   0      false(unreach-call) 1 --- inspect 1.0    1.0    21    .46 0     - --- inspect - --- inspect
email_spec11_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 40   39   310 470 1.8  0     false(unreach-call) 1 wit inspect 8.1  4.3  300 0   0     true -32 --- inspect 15     8.3   470   .62 0      false(unreach-call) 1 --- inspect 7.0  3.8  280 0   0      false(unreach-call) 1 --- inspect .95   .95   21    .43 0     - --- inspect - --- inspect
email_spec11_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 120   120   390 1200 2.0  0     false(unreach-call) 1 wit inspect 7.9  4.2  280 0   0     true -32 --- inspect 17     9.8   460   .66 0      false(unreach-call) 1 --- inspect 7.6  4.1  320 0   0      false(unreach-call) 1 --- inspect .99   .99   21    .46 0     - --- inspect - --- inspect
email_spec11_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 34   33   310 410 1.9  0     false(unreach-call) 1 wit inspect 8.2  4.4  300 0   0     true -32 --- inspect 16     9.0   490   .62 0      false(unreach-call) 1 --- inspect 7.2  3.9  290 0   0      false(unreach-call) 1 --- inspect 1.0    1.0    21    .46 0     - --- inspect - --- inspect
email_spec11_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 47   45   370 490 2.1  0     false(unreach-call) 1 wit inspect 7.0  3.7  300 0   0     true -32 --- inspect 15     8.5   470   .66 0      false(unreach-call) 1 --- inspect 7.9  4.3  300 0   0      false(unreach-call) 1 --- inspect 1.0    1.0    21    .46 0     - --- inspect - --- inspect
email_spec11_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 48   46   330 590 2.0  0     false(unreach-call) 1 wit inspect 6.9  3.7  300 0   0     true -32 --- inspect 19     10     500   .66 0      false(unreach-call) 1 --- inspect 8.4  4.5  300 0   0      false(unreach-call) 1 --- inspect .99   .98   21    .46 0     - --- inspect - --- inspect
email_spec11_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 160   160   440 1300 2.2  0     false(unreach-call) 1 wit inspect 8.1  4.3  280 0   0     true -32 --- inspect 14     8.0   520   .62 0      false(unreach-call) 1 --- inspect 7.8  4.2  300 0   0      false(unreach-call) 1 --- inspect .99   .98   21    .46 0     - --- inspect - --- inspect
email_spec11_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 550   550   900 4600 2.5  0     false(unreach-call) 1 wit inspect 11    5.7  320 0   0     true -32 --- inspect 20     11     470   .62 0      false(unreach-call) 1 --- inspect 7.5  4.1  300 0   0      false(unreach-call) 1 --- inspect 1.0    1.0    21    .51 0     - --- inspect - --- inspect
email_spec1_product14_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 17   17   260 230 1.9  0     false(unreach-call) 1 wit inspect 7.4  3.9  300 0   0     true -32 --- inspect 15     8.6   480   .62 0      false(unreach-call) 1 --- inspect 8.0  4.3  340 0   .16   false(unreach-call) 1 --- inspect 1.0    .99   21    .44 0     - --- inspect - --- inspect
email_spec1_product15_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 13   12   220 160 1.7  0