Tool Map2Check v7.2-Flock : Tue Nov 27 22:00:00 -04 2018 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* [apollon053; apollon130] 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 12:20:21 CET 2018-12-07 01:02:57 CET 2018-12-07 02:56:49 CET 2018-12-07 03:56:35 CET 2018-12-12 20:36:04 CET 2018-12-07 00:06:42 CET 2018-12-07 01:25:40 CET
Run set map2check.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-seq-validate-violation-witnesses-map2check.sv-comp19_prop-reachsafety.ReachSafety-Recursive uautomizer-validate-violation-witnesses-map2check.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-witness2test-validate-violation-witnesses-map2check.sv-comp19_prop-reachsafety.ReachSafety-Recursive fshell-witness2test-validate-violation-witnesses-map2check.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-seq-validate-correctness-witnesses-map2check.sv-comp19_prop-reachsafety.ReachSafety-Recursive uautomizer-validate-correctness-witnesses-map2check.sv-comp19_prop-reachsafety.ReachSafety-Recursive
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/map2check.2018-12-06_1220.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/map2check.2018-12-06_1220.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/map2check.2018-12-06_1220.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/map2check.2018-12-06_1220.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/map2check.2018-12-06_1220.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/map2check.2018-12-06_1220.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ 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)
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 31    30    95 440   42      0      false(unreach-call) 1 wit inspect 5.7  3.2  270 0   0   true -32 --- inspect 7.5   4.7   310   .62 0   false(unreach-call) 1 --- inspect 4.0  2.3  250 0   0   false(unreach-call) 1 --- inspect .61   .61   20    .049 0      - --- inspect - --- inspect
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900    900    130 9000   .029  0      error (invalid witness file) 0 --- inspect .58 .36 41 0   0   error (2) 0 --- inspect .032 .033 5.5 0    0   error (invalid witness file) 0 --- inspect 1.1  .76 47 0   0   error (invalid witness file) 0 --- inspect .0058 .0076 .54 0     0      - --- inspect - --- inspect
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect .49 .47 83 4.4 .016  0      false(unreach-call) 1 wit inspect 3.7  2.1  250 0   0   true -32 --- inspect 6.9   3.9   300   .62 0   false(unreach-call) 1 --- inspect 3.5  2.0  250 0   0   false(unreach-call) 1 --- inspect .57   .56   20    .049 0      - --- inspect - --- inspect
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect .45 .43 83 5.1 .0082 0      false(unreach-call) 1 wit inspect 4.2  2.3  260 0   0   false(unreach-call) 1 --- inspect 7.9   4.4   300   .66 0   false(unreach-call) 1 --- inspect 3.6  2.0  250 0   0   false(unreach-call) 1 --- inspect .58   .58   20    .049 0      - --- inspect - --- inspect
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c unknown 0 --- inspect 21    21    95 290   .045  0      error (invalid witness file) 0 --- inspect .59 .36 41 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0   error (invalid witness file) 0 --- inspect .94 .60 46 0   0   error (invalid witness file) 0 --- inspect .0056 .0072 .53 0     0      - --- inspect - --- inspect
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c unknown 0 --- inspect 23    23    110 310   .074  0      error (invalid witness file) 0 --- inspect .59 .37 41 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0   error (invalid witness file) 0 --- inspect .98 .65 47 0   0   error (invalid witness file) 0 --- inspect .0022 .0028 .53 0     0      - --- inspect - --- inspect
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 260    260    140 3700   .18   0      false(unreach-call) 1 wit inspect 3.9  2.2  260 0   0   false(unreach-call) 1 --- inspect 6.8   4.3   310   .66 0   false(unreach-call) 1 --- inspect 3.8  2.2  250 0   0   false(unreach-call) 1 --- inspect .59   .59   20    .049 0      - --- inspect - --- inspect
recursive/Ackermann01_true-unreach-call_true-no-overflow.c timeout 0 --- inspect 900    620    180 11000   1000      .0082 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .39 40 0   0   error (2) 0 --- inspect .021 .023 5.6 0   0  
recursive/Ackermann03_true-unreach-call_true-no-overflow.c timeout 0 --- inspect 900    630    120 11000   410      .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .39 41 0   0   error (2) 0 --- inspect .021 .021 5.6 0   0  
recursive/Ackermann04_true-unreach-call_true-no-overflow.c timeout 0 --- inspect 900    620    140 11000   570      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .45 41 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0  
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900    460    3100 11000   27000      .0082 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .70 .43 41 0   0   error (2) 0 --- inspect .020 .022 5.6 0   0  
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900    450    75 11000   1.5    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .46 41 0   0   error (2) 0 --- inspect .028 .028 5.7 0   0  
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900    450    75 9700   4.3    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 40 0   0   error (2) 0 --- inspect .020 .021 5.8 0   0  
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c timeout 0 --- inspect 900    450    91 8800   130      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .39 40 0   0   error (2) 0 --- inspect .022 .024 5.7 0   0  
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900    470    84 9600   28000      .0082 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .47 40 0   0   error (2) 0 --- inspect .021 .022 5.6 0   0  
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900    900    83 12000   .29   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .39 40 0   0   error (2) 0 --- inspect .023 .024 5.6 0   0  
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900    900    260 12000   .31   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .42 40 0   0   error (2) 0 --- inspect .021 .022 5.8 0   0  
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900    460    2700 10000   29000      .0082 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .45 41 0   0   error (2) 0 --- inspect .019 .020 5.6 0   0  
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c timeout 0 --- inspect 900    450    76 9400   .41   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .38 44 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0  
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900    450    81 10000   84      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .47 41 0   0   error (2) 0 --- inspect .026 .027 5.6 0   0  
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900    450    75 9000   7.2    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .81 .51 41 0   0   error (2) 0 --- inspect .020 .021 5.8 0   0  
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900    450    97 9700   260      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .38 42 0   0   error (2) 0 --- inspect .023 .024 5.7 0   0  
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900    470    2200 12000   29000      .0082 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .80 .48 40 0   0   error (2) 0 --- inspect .021 .021 5.6 0   0  
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900    470    2300 11000   29000      .0082 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 40 0   0   error (2) 0 --- inspect .021 .022 5.6 0   0  
recursive-simple/afterrec_2calls_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .43 .41 83 4.8 .0082 0      false(unreach-call) 1 wit inspect 3.9  2.1  250 0   0   true -32 --- inspect 6.5   3.7   290   .66 0   false(unreach-call) 1 --- inspect 3.4  2.0  250 0   0   false(unreach-call) 1 --- inspect .57   .57   20    .045 0      - --- inspect - --- inspect
recursive-simple/afterrec_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .43 .41 83 5.6 .0082 0      false(unreach-call) 1 wit inspect 3.5  2.0  250 0   0   true -32 --- inspect 7.3   4.2   310   .66 0   false(unreach-call) 1 --- inspect 3.4  2.0  240 0   0   false(unreach-call) 1 --- inspect .56   .56   20    .045 0      - --- inspect - --- inspect
recursive-simple/fibo_10_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .44 .42 83 5.4 .0082 0      false(unreach-call) 1 wit inspect 6.7  3.7  330 0   0   true -32 --- inspect 7.1   4.1   310   .66 0   false(unreach-call) 1 --- inspect 4.4  2.6  250 0   0   false(unreach-call) 1 --- inspect .60   .62   20    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_15_false-unreach-call.c false(unreach-call) 1 wit inspect .43 .41 83 5.2 .0082 0      false(unreach-call) 1 wit inspect 20    14    1200 0   0   true -32 --- inspect 6.7   4.2   310   .66 0   false(unreach-call) 1 --- inspect 3.5  2.0  250 0   0   false(unreach-call) 1 --- inspect .57   .57   20    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_20_false-unreach-call.c false(unreach-call) 1 wit inspect .44 .42 83 5.3 .0082 0      out of memory 0 --- inspect 44    33    7000 0   0   true -32 --- inspect 8.5   5.2   310   .62 0   false(unreach-call) 1 --- inspect 3.4  2.0  250 0   0   false(unreach-call) 1 --- inspect .62   .64   20    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_25_false-unreach-call.c false(unreach-call) 1 wit inspect .42 .40 83 5.1 .0082 0      timeout 0 --- inspect 96    65    3600 0   0   true -32 --- inspect 7.2   4.1   310   .62 0   false(unreach-call) 1 --- inspect 3.4  2.0  240 0   0   false(unreach-call) 1 --- inspect .60   .60   20    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_10_false-unreach-call.c false(unreach-call) 1 wit inspect .43 .41 83 5.5 .0082 0      false(unreach-call) 1 wit inspect 6.9  3.8  340 0   0   true -32 --- inspect 7.5   4.2   310   .66 0   false(unreach-call) 1 --- inspect 3.4  2.0  250 0   0   false(unreach-call) 1 --- inspect .60   .60   20    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_15_false-unreach-call.c false(unreach-call) 1 wit inspect .44 .42 83 5.2 .0082 0      false(unreach-call) 1 wit inspect 23    16    1200 0   0   true -32 --- inspect 7.5   4.3   310   .66 0   false(unreach-call) 1 --- inspect 3.5  2.0  250 0   0   false(unreach-call) 1 --- inspect .64   .64   20    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_20_false-unreach-call.c false(unreach-call) 1 wit inspect .43 .41 83 5.2 .0082 0      out of memory 0 --- inspect 45    34    7000 0   0   true -32 --- inspect 7.3   4.2   310   .66 0   false(unreach-call) 1 --- inspect 3.4  2.0  240 0   0   false(unreach-call) 1 --- inspect .58   .57   20    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_25_false-unreach-call.c false(unreach-call) 1 wit inspect .45 .43 82 5.5 .0082 0      timeout 0 --- inspect 97    63    4000 0   0   true -32 --- inspect 7.8   4.8   300   .62 0   false(unreach-call) 1 --- inspect 3.5  2.1  240 0   0   false(unreach-call) 1 --- inspect .60   .60   20    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_2_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .45 .43 83 5.7 .0082 0      false(unreach-call) 1 wit inspect 3.8  2.1  250 0   0   true -32 --- inspect 6.7   4.2   310   .66 0   false(unreach-call) 1 --- inspect 3.4  2.0  250 0   0   false(unreach-call) 1 --- inspect .57   .57   20    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_4_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .42 .40 83 5.0 .0082 0      false(unreach-call) 1 wit inspect 4.3  2.4  260 0   0   true -32 --- inspect 7.7   4.3   310   .66 0   false(unreach-call) 1 --- inspect 3.4  2.0  250 0   0   false(unreach-call) 1 --- inspect .59   .62   20    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .46 .44 83 5.5 .0082 0      false(unreach-call) 1 wit inspect 4.4  2.4  270 0   0   true -32 --- inspect 7.5   4.7   310   .66 0   false(unreach-call) 1 --- inspect 3.4  2.0  250 0   0   false(unreach-call) 1 --- inspect .57   .57   20    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_6_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .44 .42 83 5.5 .0082 0      false(unreach-call) 1 wit inspect 4.7  2.6  270 0   0   true -32 --- inspect 7.5   4.2   310   .66 0   false(unreach-call) 1 --- inspect 3.7  2.1  250 0   0   false(unreach-call) 1 --- inspect .57   .57   20    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_8_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .43 .41 83 4.7 .0082 0      false(unreach-call) 1 wit inspect 5.4  3.0  280 0   0   true -32 --- inspect 7.3   4.1   310   .66 0   false(unreach-call) 1 --- inspect 4.0  2.3  250 0   0   false(unreach-call) 1 --- inspect .60   .63   20    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .45 .43 83 5.0 .0082 0      false(unreach-call) 1 wit inspect 4.4  2.4  270 0   0   true -32 --- inspect 6.8   3.9   310   .66 0   false(unreach-call) 1 --- inspect 3.5  2.0  250 0   0   false(unreach-call) 1 --- inspect .60   .61   20    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_7_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .45 .44 82 5.1 .0082 0      false(unreach-call) 1 wit inspect 4.8  2.7  280 0   0   true -32 --- inspect 7.2   4.1   310   .66 0   false(unreach-call) 1 --- inspect 3.6  2.1  250 0   0   false(unreach-call) 1 --- inspect .57   .57   20    .049 .0041 - --- inspect - --- inspect
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect 5.5  5.5  91 67   .037  0      true -32 wit inspect 3.9  2.2  260 0   0   true -32 --- inspect 7.3   4.2   310   .66 0   unknown 0 --- inspect 3.4  1.9  250 0   0   false(unreach-call) 1 --- inspect .57   .58   20    .049 0      - --- inspect - --- inspect
recursive-simple/id2_i5_o5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .43 .41 83 4.9 .0082 0      false(unreach-call) 1 wit inspect 4.0  2.2  260 0   0   true -32 --- inspect 7.2   4.1   310   .66 0   false(unreach-call) 1 --- inspect 3.5  2.1  250 0   0   false(unreach-call) 1 --- inspect .57   .58   20    .049 0      - --- inspect - --- inspect
recursive-simple/id_b3_o2_false-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect 5.3  5.3  92 71   .033  0      false(unreach-call) 1 wit inspect 4.3  2.4  260 0   0   true -32 --- inspect 8.0   4.5   310   .66 0   false(unreach-call) 1 --- inspect 3.6  2.1  250 0   0   false(unreach-call) 1 --- inspect .58   .58   20    .049 .0041 - --- inspect - --- inspect
recursive-simple/id_i10_o10_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .45 .43 83 5.1 .0082 0      false(unreach-call) 1 wit inspect 4.1  2.3  260 0   0   true -32 --- inspect 7.0   4.0   320   .66 0   false(unreach-call) 1 --- inspect 3.4  2.0  240 0   0   false(unreach-call) 1 --- inspect .57   .57   20    .045 0      - --- inspect - --- inspect
recursive-simple/id_i15_o15_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .42 .40 83 4.8 .0082 0      false(unreach-call) 1 wit inspect 4.3  2.4  270 0   0   true -32 --- inspect 7.1   4.0   310   .66 0   false(unreach-call) 1 --- inspect 3.8  2.2  250 0   0   false(unreach-call) 1 --- inspect .57   .57   20    .045 .0041 - --- inspect - --- inspect
recursive-simple/id_i20_o20_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .42 .40 82 5.3 .0082 0      false(unreach-call) 1 wit inspect 4.3  2.4  270 0   0   true -32 --- inspect 6.9   4.4   310   .66 0   false(unreach-call) 1 --- inspect 3.4  2.0  240 0   0   false(unreach-call) 1 --- inspect .57   .57   20    .045 0      - --- inspect - --- inspect
recursive-simple/id_i25_o25_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .43 .41 82 5.8 .0082 0      false(unreach-call) 1 wit inspect 4.5  2.5  270 0   0   true -32 --- inspect 6.9   4.3   310   .66 0   false(unreach-call) 1 --- inspect 3.4  2.0  250 0   0   false(unreach-call) 1 --- inspect .60   .60   20    .045 0      - --- inspect - --- inspect
recursive-simple/id_i5_o5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .42 .40 83 5.1 .0082 0      false(unreach-call) 1 wit inspect 4.2  2.3  260 0   0   true -32 --- inspect 7.5   4.7   320   .66 0   false(unreach-call) 1 --- inspect 3.3  1.9  250 0   0   false(unreach-call) 1 --- inspect .58   .58   20    .045 0      - --- inspect - --- inspect
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 7.2  6.9  85 93   92      0      true -32 wit inspect 3.7  2.1  250 0   0   true -32 --- inspect 7.6   4.3   310   .66 0   unknown 0 --- inspect 3.4  2.0  240 0   0   false(unreach-call) 1 --- inspect .60   .60   20    .049 0      - --- inspect - --- inspect
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 6.6  6.4  84 90   88      0      true -32 wit inspect 3.9  2.2  260 0   0   true -32 --- inspect 7.0   4.0   310   .66 0   unknown 0 --- inspect 3.4  2.0  250 0   0   false(unreach-call) 1 --- inspect .60   .60   20    .049 .0041 - --- inspect - --- inspect
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 5.8  5.7  79 87   19      0      true -32 wit inspect 3.9  2.2  260 0   0   true -32 --- inspect 7.1   4.0   310   .66 0   unknown 0 --- inspect 3.5  2.0  250 0   0   false(unreach-call) 1 --- inspect .58   .59   20    .049 0      - --- inspect - --- inspect
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect .89 .80 82 10   27      0      true -32 wit inspect 3.9  2.1  260 0   0   true -32 --- inspect 7.1   4.5   310   .66 0   unknown 0 --- inspect 3.5  2.0  240 0   0   false(unreach-call) 1 --- inspect .58   .57   20    .049 0      - --- inspect - --- inspect
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 6.7  6.1  87 87   52      0      true -32 wit inspect 3.8  2.1  260 0   0   true -32 --- inspect 7.1   4.5   310   .66 0   unknown 0 --- inspect 3.6  2.0  250 0   0   false(unreach-call) 1 --- inspect .60   .60   20    .049 0      - --- inspect - --- inspect
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 6.9  6.4  87 90   72      0      true -32 wit inspect 4.0  2.2  260 0   0   true -32 --- inspect 7.1   4.5   320   .66 0   unknown 0 --- inspect 3.5  2.0  240 0   0   false(unreach-call) 1 --- inspect .57   .57   20    .049 0      - --- inspect - --- inspect
recursive-simple/sum_10x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .44 .42 83 5.6 .0082 0      false(unreach-call) 1 wit inspect 4.1  2.3  260 0   0   true -32 --- inspect 7.5   4.6   310   .66 0   false(unreach-call) 1 --- inspect 3.5  2.0  240 0   0   false(unreach-call) 1 --- inspect .58   .58   20    .045 0      - --- inspect - --- inspect
recursive-simple/sum_15x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .45 .43 83 5.2 .0082 0      false(unreach-call) 1 wit inspect 4.4  2.4  270 0   0   true -32 --- inspect 7.2   4.2   310   .62 0   false(unreach-call) 1 --- inspect 3.5  2.1  250 0   0   false(unreach-call) 1 --- inspect .56   .56   20    .045 0      - --- inspect - --- inspect
recursive-simple/sum_20x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .45 .43 83 5.9 .0082 0      false(unreach-call) 1 wit inspect 4.5  2.5  270 0   0   true -32 --- inspect 7.1   4.5   310   .66 0   false(unreach-call) 1 --- inspect 4.5  2.6  250 0   0   false(unreach-call) 1 --- inspect .57   .57   20    .045 0      - --- inspect - --- inspect
recursive-simple/sum_25x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .42 .40 83 4.8 .0082 0      false(unreach-call) 1 wit inspect 4.8  2.7  270 0   0   true -32 --- inspect 7.1   4.5   310   .66 0   false(unreach-call) 1 --- inspect 3.4  2.0  250 0   0   false(unreach-call) 1 --- inspect .58   .57   20    .045 0      - --- inspect - --- inspect
recursive-simple/sum_2x3_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .42 .40 83 5.0 .0082 0      false(unreach-call) 1 wit inspect 4.0  2.2  260 0   0   true -32 --- inspect 7.0   4.5   310   .66 0   false(unreach-call) 1 --- inspect 3.6  2.1  250 0   0   false(unreach-call) 1 --- inspect .59   .59   20    .045 0      - --- inspect - --- inspect
recursive-simple/sum_non_eq_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect .43 .41 83 5.6 .0082 0      true -32 wit inspect 3.8  2.2  250 0   0   false(unreach-call) 1 --- inspect 7.0   3.9   310   .66 0   unknown 0 --- inspect 3.5  2.0  250 0   0   false(unreach-call) 1 --- inspect .61   .60   20    .049 .0041 - --- inspect - --- inspect
recursive-simple/afterrec_2calls_true-unreach-call_true-termination.c timeout 0 --- inspect 900    480    85 9700   30000      .0082 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .36 41 0   0   error (2) 0 --- inspect .021 .022 5.7 0   0  
recursive-simple/afterrec_true-unreach-call_true-termination.c timeout 0 --- inspect 900    480    84 11000   30000      .0082 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .82 .50 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0   0  
recursive-simple/fibo_10_true-unreach-call_true-termination.c timeout 0 --- inspect 900    470    84 11000   29000      .074  - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .41 40 0   0   error (2) 0 --- inspect .021 .022 5.7 0   0  
recursive-simple/fibo_15_true-unreach-call.c timeout 0 --- inspect 900    460    83 10000   24000      .0082 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .37 42 0   0   error (2) 0 --- inspect .020 .022 5.6 0   0  
recursive-simple/fibo_20_true-unreach-call.c timeout 0 --- inspect 900    450    77 8300   13000      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .45 41 0   0   error (2) 0 --- inspect .022 .023 5.8 0   0  
recursive-simple/fibo_25_true-unreach-call.c timeout 0 --- inspect 900    450    75 9700   2100      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .38 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0   0  
recursive-simple/fibo_2calls_10_true-unreach-call.c timeout 0 --- inspect 900    460    85 12000   28000      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .46 40 0   0   error (2) 0 --- inspect .021 .021 5.6 0   0  
recursive-simple/fibo_2calls_15_true-unreach-call.c timeout 0 --- inspect 900    450    83 9000   22000      .0082 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .38 40 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0  
recursive-simple/fibo_2calls_20_true-unreach-call.c timeout 0 --- inspect 900    450    77 8500   13000      .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .40 40 0   0   error (2) 0 --- inspect .021 .035 5.6 0   0  
recursive-simple/fibo_2calls_25_true-unreach-call.c timeout 0 --- inspect 900    450    75 9300   2000      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .57 .34 40 0   0   error (2) 0 --- inspect .024 .025 5.6 0   0  
recursive-simple/fibo_2calls_2_true-unreach-call_true-termination.c timeout 0 --- inspect 900    470    85 11000   29000      .0082 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 43 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0  
recursive-simple/fibo_2calls_4_true-unreach-call_true-termination.c timeout 0 --- inspect 900    470    85 9400   28000      .0082 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .83 .51 42 0   0   error (2) 0 --- inspect .022 .023 5.6 0   0  
recursive-simple/fibo_2calls_5_true-unreach-call_true-termination.c timeout 0 --- inspect 900    470    85 12000   29000      .0082 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .36 41 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0  
recursive-simple/fibo_2calls_6_true-unreach-call_true-termination.c timeout 0 --- inspect 900    470    85 10000   28000      .0082 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .38 42 0   0   error (2) 0 --- inspect .022 .023 5.6 0   0  
recursive-simple/fibo_2calls_8_true-unreach-call_true-termination.c timeout 0 --- inspect 900    460    84 11000   29000      .0082 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .80 .48 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0   0  
recursive-simple/fibo_5_true-unreach-call_true-termination.c timeout 0 --- inspect 900    470    84 9700   29000      .0082 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .34 40 0   0   error (2) 0 --- inspect .021 .022 5.6 0   0  
recursive-simple/fibo_7_true-unreach-call_true-termination.c timeout 0 --- inspect 900    470    85 10000   29000      .0082 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .40 40 0   0   error (2) 0 --- inspect .021 .021 5.6 0   0  
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c timeout 0 --- inspect 900    900    340 10000   11      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .35 40 0   0   error (2) 0 --- inspect .022 .023 5.6 0   0  
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c timeout 0 --- inspect 900    900    340 8600   11      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .39 40 0   0   error (2) 0 --- inspect .021 .021 5.6 0   0  
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c timeout 0 --- inspect 900    900    350 7800   11      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .45 42 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0  
recursive-simple/id2_i5_o5_true-unreach-call_true-termination.c timeout 0 --- inspect 900    470    85 9700   29000      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .69 .42 40 0   0   error (2) 0 --- inspect .023 .023 5.6 0   0  
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c timeout 0 --- inspect 900    900    340 9600   10      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .70 .44 41 0   0   error (2) 0 --- inspect .021 .021 5.6 0   0  
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c unknown 0 --- inspect .75 .75 39 8.7 0      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .38 40 0   0   error (2) 0 --- inspect .021 .022 5.6 0   0  
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c unknown 0 --- inspect .76 .75 39 9.1 0      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .38 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0   0  
recursive-simple/id_i10_o10_true-unreach-call_true-termination.c timeout 0 --- inspect 900    470    85 10000   29000      .0082 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .42 40 0   0   error (2) 0 --- inspect .024 .025 5.7 0   0  
recursive-simple/id_i15_o15_true-unreach-call_true-termination.c timeout 0 --- inspect 900    480    84 10000   29000      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 41 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0  
recursive-simple/id_i20_o20_true-unreach-call_true-termination.c timeout 0 --- inspect 900    480    85 10000   29000      .0082 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .82 .51 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0   0  
recursive-simple/id_i25_o25_true-unreach-call_true-termination.c timeout 0 --- inspect 900    480    85 10000   29000      .0082 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .39 40 0   0   error (2) 0 --- inspect .031 .031 5.6 0   0  
recursive-simple/id_i5_o5_true-unreach-call_true-termination.c timeout 0 --- inspect 900    480    85 11000   30000      .0082 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .40 41 0   0   error (2) 0 --- inspect .024 .025 5.7 0   0  
recursive-simple/sum_10x0_true-unreach-call_true-termination.c timeout 0 --- inspect 900    470    85 11000   30000      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .38 41 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0  
recursive-simple/sum_15x0_true-unreach-call_true-termination.c timeout 0 --- inspect 900    470    84 10000   29000      .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .70 .43 40 0   0   error (2) 0 --- inspect .021 .021 5.6 0   0  
recursive-simple/sum_20x0_true-unreach-call_true-termination.c timeout 0 --- inspect 900    480    84 12000   29000      .0082 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .47 42 0   0   error (2) 0 --- inspect .021 .022 5.6 0   0  
recursive-simple/sum_25x0_true-unreach-call_true-termination.c timeout 0 --- inspect 900    480    84 11000   29000      .0082 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .34 41 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0  
recursive-simple/sum_2x3_true-unreach-call_true-termination.c timeout 0 --- inspect 900    480    85 9400   29000      .0082 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .79 .48 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0   0  
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c timeout 0 --- inspect 900    460    4300 9400   28000      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .35 40 0   0   error (2) 0 --- inspect .022 .022 5.5 0   0  
sv-benchmarks/c/ 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)
total 96 37 46000 28000 24000 520000 890000 .28 44 -227 480 310 33000 0   0   44 -1213 300 180 13000 27   0   44 33 150 87 10000 0   0   44 41 24 24 830 2.0 .020 52 0 35 21 2100 0   0   52 0 1.1 1.2 290 0   0  
    correct results 37 37 48 45 3100 620 350 0    29 29 170 97 9700 0   0   3 3 22 13 920 2.0 0   33 33 120 69 8100 0   0   41 41 24 24 830 2.0 .020 0 0
        correct true 0 0 0 0 0 0 0
        correct false 37 37 48 45 3100 620 350 0    29 29 170 97 9700 0   0   3 3 22 13 920 2.0 0   33 33 120 69 8100 0   0   41 41 24 24 830 2.0 .020 0 0
    incorrect results 0 8 -256 31 17 2000 0   0   38 -1216 280 160 12000 25   0   0 0 0 0
        incorrect true 0 8 -256 31 17 2000 0   0   38 -1216 280 160 12000 25   0   0 0 0 0
        incorrect false 0 0 0 0 0 0 0
score (96 tasks, max score: 148) 37 -227 -1213 33 41 0 0
Run set map2check.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-seq-validate-violation-witnesses-map2check.sv-comp19_prop-reachsafety.ReachSafety-Recursive uautomizer-validate-violation-witnesses-map2check.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-witness2test-validate-violation-witnesses-map2check.sv-comp19_prop-reachsafety.ReachSafety-Recursive fshell-witness2test-validate-violation-witnesses-map2check.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-seq-validate-correctness-witnesses-map2check.sv-comp19_prop-reachsafety.ReachSafety-Recursive uautomizer-validate-correctness-witnesses-map2check.sv-comp19_prop-reachsafety.ReachSafety-Recursive