Tool 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-05 05:46:16 CET 2018-12-06 09:44:44 CET 2018-12-06 10:50:29 CET 2018-12-06 10:57:45 CET 2018-12-12 19:32:16 CET 2018-12-06 08:37:23 CET 2018-12-06 09:52:34 CET
Run set cpa-seq.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-seq-validate-violation-witnesses-cpa-seq.sv-comp19_prop-reachsafety.ReachSafety-Recursive uautomizer-validate-violation-witnesses-cpa-seq.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-witness2test-validate-violation-witnesses-cpa-seq.sv-comp19_prop-reachsafety.ReachSafety-Recursive fshell-witness2test-validate-violation-witnesses-cpa-seq.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-seq-validate-correctness-witnesses-cpa-seq.sv-comp19_prop-reachsafety.ReachSafety-Recursive uautomizer-validate-correctness-witnesses-cpa-seq.sv-comp19_prop-reachsafety.ReachSafety-Recursive
Options -svcomp19 -heap 10000M -benchmark -timelimit 900s -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/cpa-seq.2018-12-05_0546.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cpa-seq.2018-12-05_0546.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/cpa-seq.2018-12-05_0546.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/cpa-seq.2018-12-05_0546.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/cpa-seq.2018-12-05_0546.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cpa-seq.2018-12-05_0546.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 false(unreach-call) 1 wit inspect 4.5 2.0 280 43 0   0     false(unreach-call) 1 wit inspect 5.2  2.8  270 0   0   false(unreach-call) 1 --- inspect 8.8   4.8   310   .66 0   false(unreach-call) 1 --- inspect 3.9  2.3  250 0      0   false(unreach-call) 1 --- inspect .60   .60   21    .049 0      - --- inspect - --- inspect
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 3.7 1.7 270 33 0   0     false(unreach-call) 1 wit inspect 4.3  2.4  260 0   0   false(unreach-call) 1 --- inspect 7.1   4.1   310   .66 0   false(unreach-call) 1 --- inspect 3.8  2.2  250 0      0   false(unreach-call) 1 --- inspect .57   .57   20    .049 .0041 - --- inspect - --- inspect
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 2.8 1.3 260 28 0   0     false(unreach-call) 1 wit inspect 3.8  2.2  250 0   0   true -32 --- inspect 6.7   3.8   300   .62 0   false(unreach-call) 1 --- inspect 3.7  2.1  250 0      0   false(unreach-call) 1 --- inspect .57   .58   20    .049 0      - --- inspect - --- inspect
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 3.4 1.5 270 31 0   0     false(unreach-call) 1 wit inspect 4.1  2.3  250 0   0   false(unreach-call) 1 --- inspect 7.2   4.5   310   .62 0   false(unreach-call) 1 --- inspect 3.7  2.2  250 0      0   false(unreach-call) 1 --- inspect .57   .57   20    .049 0      - --- inspect - --- inspect
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 7.4 3.7 320 74 0   0     false(unreach-call) 1 wit inspect 5.2  2.9  270 0   0   false(unreach-call) 1 --- inspect 27     15     830   .66 0   false(unreach-call) 1 --- inspect 4.2  2.4  250 0      0   false(unreach-call) 1 --- inspect .59   .59   21    .049 0      - --- inspect - --- inspect
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 22   17   500 290 0   0     false(unreach-call) 1 wit inspect 9.4  5.0  330 0   0   timeout 0 --- inspect 97     74     4000   1.1  0   false(unreach-call) 1 --- inspect 5.4  3.0  280 0      0   false(unreach-call) 1 --- inspect .62   .62   23    .049 .0041 - --- inspect - --- inspect
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 3.3 1.4 270 30 0   0     false(unreach-call) 1 wit inspect 4.8  2.6  250 0   0   false(unreach-call) 1 --- inspect 6.7   4.2   300   .66 0   false(unreach-call) 1 --- inspect 3.7  2.2  250 0      0   false(unreach-call) 1 --- inspect .58   .58   20    .049 0      - --- inspect - --- inspect
recursive/Ackermann01_true-unreach-call_true-no-overflow.c true 2 wit inspect 5.0 2.1 290 50 0   0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.1  2.3  250 0   0   true 2 --- inspect 15     8.9   460   .66  0  
recursive/Ackermann03_true-unreach-call_true-no-overflow.c timeout 0 --- inspect 900   880   3000 12000 0   0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .40 40 0   0   error (2) 0 --- inspect .022 .023 5.7 0     0  
recursive/Ackermann04_true-unreach-call_true-no-overflow.c timeout 0 --- inspect 900   810   10000 11000 0   0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .41 40 0   0   error (2) 0 --- inspect .027 .028 5.5 0     0  
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900   890   840 14000 0   0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .56 .34 40 0   0   error (2) 0 --- inspect .021 .021 5.6 0     0  
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   880   3000 10000 0   0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.8  2.1  250 0   0   true 2 --- inspect 440     350     2400   .62  0  
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   870   14000 11000 0   0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.6  2.0  250 0   0   timeout 0 --- inspect 960     810     1300   .66  0  
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c timeout 0 wit inspect 910   900   1100 9700 0   0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.6  2.0  250 0   0   true 2 --- inspect 18     11     500   .66  0  
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 5.6 2.0 350 51 0   0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.5  2.0  250 0   0   true 2 --- inspect 33     20     1300   .62  0  
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900   860   4200 12000 0   0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 41 0   0   error (2) 0 --- inspect .030 .032 5.5 0     0  
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 3.7 1.7 280 36 0   0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.4  1.9  250 0   0   true 2 --- inspect 9.7   5.7   320   .62  0  
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900   890   810 12000 0   0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .46 42 0   0   error (2) 0 --- inspect .022 .023 5.7 0     0  
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c timeout 0 --- inspect 900   890   1100 13000 0   0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .39 40 0   0   error (2) 0 --- inspect .024 .025 5.6 0     0  
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 4.4 1.9 280 40 0   0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.2  2.4  250 0   0   true 2 --- inspect 13     7.8   350   .62  0  
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   900   770 12000 0   0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.2  2.3  250 0   0   timeout 0 --- inspect 960     820     1000   1.6   0  
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c true 1 wit inspect 3.7 1.7 280 37 0   0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.8  2.7  250 0   0   timeout 0 --- inspect 960     900     6300   1.4   0  
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   870   4000 13000 0   0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.6  2.0  250 0   0   true 2 --- inspect 7.6   4.4   310   .078 0  
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 910   870   7200 13000 0   0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 5.1  2.8  250 0   0   true 2 --- inspect 38     24     800   .62  0  
recursive-simple/afterrec_2calls_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.9 1.3 260 26 0   0     false(unreach-call) 1 wit inspect 3.8  2.1  250 0   0   false(unreach-call) 1 --- inspect 7.7   4.3   310   .66 0   false(unreach-call) 1 --- inspect 3.6  2.1  250 0      0   false(unreach-call) 1 --- inspect .56   .56   20    .045 0      - --- inspect - --- inspect
recursive-simple/afterrec_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.9 1.3 250 30 0   0     false(unreach-call) 1 wit inspect 3.6  2.1  250 0   0   false(unreach-call) 1 --- inspect 7.4   4.5   300   .62 0   false(unreach-call) 1 --- inspect 3.7  2.1  250 0      0   false(unreach-call) 1 --- inspect .57   .57   20    .045 0      - --- inspect - --- inspect
recursive-simple/fibo_10_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 6.1 2.5 340 61 0   0     false(unreach-call) 1 wit inspect 12    6.6  470 0   0   timeout 0 --- inspect 98     65     5500   .79 0   false(unreach-call) 1 --- inspect 7.2  3.9  310 0      0   false(unreach-call) 1 --- inspect .71   .71   27    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_15_false-unreach-call.c false(unreach-call) 1 wit inspect 21   9.4 1200 180 0   0     false(unreach-call) 1 wit inspect 65    37    2300 0   0   timeout 0 --- inspect 96     65     6800   1.6  0   false(unreach-call) 1 --- inspect 28    14    1200 0      0   false(unreach-call) 1 --- inspect 2.1    2.1    99    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_20_false-unreach-call.c false(unreach-call) 1 wit inspect 680   650   9900 3800 0   0     timeout 0 --- inspect 98    52    4200 0   0   timeout 0 --- inspect 93     60     7000   .74 0   timeout 0 --- inspect 98    52    4500 .012  0   false(unreach-call) 1 --- inspect 19      19      940    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_25_false-unreach-call.c out of memory 0 --- inspect 190   110   15000 1600 0   0     error (invalid witness file) 0 --- inspect .77 .47 41 0   0   error (2) 0 --- inspect .027 .027 5.6 0    0   error (invalid witness file) 0 --- inspect .97 .66 47 0      0   error (invalid witness file) 0 --- inspect .0048 .0062 .40 0     0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_10_false-unreach-call.c false(unreach-call) 1 wit inspect 6.1 2.4 350 45 0   0     false(unreach-call) 1 wit inspect 11    6.1  440 0   0   timeout 0 --- inspect 96     60     5400   .66 0   false(unreach-call) 1 --- inspect 6.4  3.6  290 0      0   false(unreach-call) 1 --- inspect .70   .70   27    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_15_false-unreach-call.c false(unreach-call) 1 wit inspect 19   10   1200 170 0   0     false(unreach-call) 1 wit inspect 47    30    2000 0   0   out of memory 0 --- inspect 89     56     7000   .68 0   false(unreach-call) 1 --- inspect 22    12    1100 0      0   false(unreach-call) 1 --- inspect 2.1    2.1    99    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_20_false-unreach-call.c timeout 0 --- inspect 910   890   9900 5000 0   0     error (invalid witness file) 0 --- inspect .59 .37 40 0   0   error (2) 0 --- inspect .021 .024 5.7 0    0   error (invalid witness file) 0 --- inspect .98 .64 48 0      0   error (invalid witness file) 0 --- inspect .0041 .0049 .53 0     0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_25_false-unreach-call.c out of memory 0 --- inspect 190   110   15000 1800 0   0     error (invalid witness file) 0 --- inspect .59 .37 40 0   0   error (2) 0 --- inspect .019 .020 5.6 0    0   error (invalid witness file) 0 --- inspect .98 .65 48 0      0   error (invalid witness file) 0 --- inspect .0050 .0060 .52 0     0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_2_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.1 1.4 250 29 0   0     false(unreach-call) 1 wit inspect 4.1  2.3  250 0   0   false(unreach-call) 1 --- inspect 7.8   4.4   310   .62 0   false(unreach-call) 1 --- inspect 3.7  2.2  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 3.6 1.6 270 36 0   0     false(unreach-call) 1 wit inspect 4.6  2.5  270 0   0   false(unreach-call) 1 --- inspect 8.5   4.7   320   .62 0   false(unreach-call) 1 --- inspect 3.9  2.3  250 0      0   false(unreach-call) 1 --- inspect .59   .58   21    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.7 1.6 280 31 0   0     false(unreach-call) 1 wit inspect 4.8  2.7  270 0   0   false(unreach-call) 1 --- inspect 32     18     750   .62 0   false(unreach-call) 1 --- inspect 4.1  2.4  250 0      0   false(unreach-call) 1 --- inspect .60   .60   21    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_6_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.9 1.6 280 33 0   0     false(unreach-call) 1 wit inspect 5.3  2.9  270 0   0   false(unreach-call) 1 --- inspect 66     41     2900   .62 0   false(unreach-call) 1 --- inspect 4.5  2.5  260 0      0   false(unreach-call) 1 --- inspect .59   .58   21    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_8_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 4.8 2.0 300 45 0   0     false(unreach-call) 1 wit inspect 7.8  4.2  320 0   0   timeout 0 --- inspect 96     70     4400   1.5  0   false(unreach-call) 1 --- inspect 5.3  2.9  290 0      0   false(unreach-call) 1 --- inspect .61   .61   23    .049 .0041 - --- inspect - --- inspect
recursive-simple/fibo_5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.7 1.6 280 34 0   0     false(unreach-call) 1 wit inspect 4.9  2.7  270 0   0   false(unreach-call) 1 --- inspect 26     14     920   .62 0   false(unreach-call) 1 --- inspect 4.3  2.5  270 0      0   false(unreach-call) 1 --- inspect .58   .58   21    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_7_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 4.0 1.7 290 36 0   0     false(unreach-call) 1 wit inspect 8.4  4.5  310 0   0   timeout 0 --- inspect 96     70     3300   1.1  0   false(unreach-call) 1 --- inspect 5.2  2.9  280 0      0   false(unreach-call) 1 --- inspect .61   .61   22    .049 .074  - --- inspect - --- inspect
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 3.4 1.5 270 37 0   0     false(unreach-call) 1 wit inspect 4.6  2.5  260 0   0   false(unreach-call) 1 --- inspect 7.6   4.3   310   .66 0   false(unreach-call) 1 --- inspect 3.8  2.2  250 0      0   false(unreach-call) 1 --- inspect .57   .57   20    .049 0      - --- inspect - --- inspect
recursive-simple/id2_i5_o5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.4 1.5 270 34 0   0     false(unreach-call) 1 wit inspect 4.4  2.5  260 0   0   false(unreach-call) 1 --- inspect 7.1   4.2   300   .62 0   false(unreach-call) 1 --- inspect 3.8  2.2  250 0      0   false(unreach-call) 1 --- inspect .60   .60   21    .049 0      - --- inspect - --- inspect
recursive-simple/id_b3_o2_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 3.4 1.5 270 33 0   0     false(unreach-call) 1 wit inspect 4.5  2.6  260 0   0   false(unreach-call) 1 --- inspect 7.4   4.6   310   .66 0   false(unreach-call) 1 --- inspect 3.7  2.2  250 0      0   false(unreach-call) 1 --- inspect .58   .59   20    .041 0      - --- inspect - --- inspect
recursive-simple/id_i10_o10_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.5 1.5 270 33 0   0     false(unreach-call) 1 wit inspect 6.0  3.3  270 0   0   false(unreach-call) 1 --- inspect 10     5.4   370   .66 0   false(unreach-call) 1 --- inspect 4.1  2.4  250 0      0   false(unreach-call) 1 --- inspect .57   .57   21    .045 0      - --- inspect - --- inspect
recursive-simple/id_i15_o15_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.7 1.6 280 35 0   0     false(unreach-call) 1 wit inspect 6.3  3.4  270 0   0   false(unreach-call) 1 --- inspect 12     6.5   520   .62 0   false(unreach-call) 1 --- inspect 4.3  2.4  250 0      0   false(unreach-call) 1 --- inspect .57   .57   21    .045 0      - --- inspect - --- inspect
recursive-simple/id_i20_o20_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.7 1.6 280 36 0   0     false(unreach-call) 1 wit inspect 6.6  3.6  270 0   0   false(unreach-call) 1 --- inspect 15     8.6   630   .62 0   false(unreach-call) 1 --- inspect 4.6  2.6  260 0      0   false(unreach-call) 1 --- inspect .58   .58   21    .045 .0041 - --- inspect - --- inspect
recursive-simple/id_i25_o25_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.8 1.7 280 35 0   0     false(unreach-call) 1 wit inspect 7.5  4.0  300 0   0   false(unreach-call) 1 --- inspect 20     12     860   .66 0   false(unreach-call) 1 --- inspect 4.7  2.7  260 0      0   false(unreach-call) 1 --- inspect .62   .61   21    .045 0      - --- inspect - --- inspect
recursive-simple/id_i5_o5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.4 1.5 270 33 0   0     false(unreach-call) 1 wit inspect 5.2  2.8  260 0   0   false(unreach-call) 1 --- inspect 7.5   4.3   310   .66 0   false(unreach-call) 1 --- inspect 3.9  2.2  250 0      0   false(unreach-call) 1 --- inspect .59   .59   20    .045 0      - --- inspect - --- inspect
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 120   89   4500 1200 0   0     exception 0 --- inspect 12    6.5  410 0   0   timeout 0 --- inspect 97     71     6400   .71 0   timeout 0 --- inspect 8.9  130    400 .0041 0   false(unreach-call) 1 --- inspect 1.1    1.1    47    .049 0      - --- inspect - --- inspect
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 7.6 2.6 470 61 0   0     false(unreach-call) 1 wit inspect 17    9.1  540 0   0   timeout 0 --- inspect 97     65     6600   1.1  0   false(unreach-call) 1 --- inspect 9.9  5.2  410 0      0   false(unreach-call) 1 --- inspect .62   .62   23    .049 0      - --- inspect - --- inspect
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 3.5 1.6 270 29 0   0     false(unreach-call) 1 wit inspect 5.0  2.8  270 0   0   false(unreach-call) 1 --- inspect 9.2   5.1   370   .62 0   false(unreach-call) 1 --- inspect 4.1  2.3  250 0      0   false(unreach-call) 1 --- inspect .57   .57   21    .049 0      - --- inspect - --- inspect
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 12   4.1 660 110 0   0     false(unreach-call) 1 wit inspect 44    27    1400 0   0   timeout 0 --- inspect 97     70     6500   .64 0   false(unreach-call) 1 --- inspect 20    11    600 0      0   false(unreach-call) 1 --- inspect .65   .65   26    .049 0      - --- inspect - --- inspect
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 4.0 1.7 280 40 0   0     false(unreach-call) 1 wit inspect 6.3  3.4  280 0   0   false(unreach-call) 1 --- inspect 17     9.0   730   .62 0   false(unreach-call) 1 --- inspect 4.5  2.6  260 0      0   false(unreach-call) 1 --- inspect .59   .60   21    .049 0      - --- inspect - --- inspect
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 3.5 1.5 270 31 0   0     false(unreach-call) 1 wit inspect 4.5  2.5  260 0   0   false(unreach-call) 1 --- inspect 7.9   4.5   310   .66 0   false(unreach-call) 1 --- inspect 4.9  2.8  250 0      0   false(unreach-call) 1 --- inspect .59   .59   20    .049 .0041 - --- inspect - --- inspect
recursive-simple/sum_10x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.5 1.6 270 32 0   0     false(unreach-call) 1 wit inspect 5.7  3.2  270 0   0   false(unreach-call) 1 --- inspect 8.7   5.3   330   .66 0   false(unreach-call) 1 --- inspect 4.2  2.4  250 0      0   false(unreach-call) 1 --- inspect .60   .59   21    .045 0      - --- inspect - --- inspect
recursive-simple/sum_15x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.6 1.6 280 34 0   0     false(unreach-call) 1 wit inspect 6.8  3.7  280 0   0   false(unreach-call) 1 --- inspect 12     6.6   520   .62 0   false(unreach-call) 1 --- inspect 4.2  2.4  250 0      0   false(unreach-call) 1 --- inspect .57   .57   21    .045 0      - --- inspect - --- inspect
recursive-simple/sum_20x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.7 1.7 280 36 0   0     false(unreach-call) 1 wit inspect 6.1  3.4  280 0   0   false(unreach-call) 1 --- inspect 15     8.2   630   .62 0   false(unreach-call) 1 --- inspect 4.5  2.6  260 0      0   false(unreach-call) 1 --- inspect .60   .60   21    .045 0      - --- inspect - --- inspect
recursive-simple/sum_25x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 4.0 1.7 280 33 0   .029 false(unreach-call) 1 wit inspect 7.5  4.0  280 0   0   false(unreach-call) 1 --- inspect 15     8.7   770   .62 0   false(unreach-call) 1 --- inspect 4.9  2.8  270 0      0   false(unreach-call) 1 --- inspect .58   .58   21    .045 0      - --- inspect - --- inspect
recursive-simple/sum_2x3_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.3 1.5 270 32 0   0     false(unreach-call) 1 wit inspect 4.5  2.5  260 0   0   false(unreach-call) 1 --- inspect 7.0   4.4   300   .66 0   false(unreach-call) 1 --- inspect 3.8  2.2  250 0      0   false(unreach-call) 1 --- inspect .57   .58   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 3.1 1.4 270 31 0   0     false(unreach-call) 1 wit inspect 4.5  2.5  250 0   0   false(unreach-call) 1 --- inspect 6.8   3.9   320   .66 0   false(unreach-call) 1 --- inspect 3.6  2.2  250 0      0   false(unreach-call) 1 --- inspect .58   .58   20    .049 0      - --- inspect - --- inspect
recursive-simple/afterrec_2calls_true-unreach-call_true-termination.c true 2 wit inspect 2.9 1.3 250 28 0   0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.4  2.5  250 0   0   true 2 --- inspect 9.0   5.3   320   .66  0  
recursive-simple/afterrec_true-unreach-call_true-termination.c true 2 wit inspect 2.9 1.3 250 31 0   0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.3  1.9  260 0   0   true 2 --- inspect 8.0   4.4   310   .66  0  
recursive-simple/fibo_10_true-unreach-call_true-termination.c true 2 wit inspect 6.9 2.3 450 57 0   0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.5  2.0  250 0   0   true 2 --- inspect 56     35     3100   .62  0  
recursive-simple/fibo_15_true-unreach-call.c true 2 wit inspect 36   28   1600 480 0   0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.9  2.2  250 0   0   true 2 --- inspect 590     540     6300   .62  0  
recursive-simple/fibo_20_true-unreach-call.c timeout 0 wit inspect 920   900   3900 12000 0   0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.5  2.0  250 0   0   out of memory 0 --- inspect 690     640     7000   .64  0  
recursive-simple/fibo_25_true-unreach-call.c timeout 0 wit inspect 960   870   4900 11000 0   0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .36 42 0   0   error (invalid witness file) 0 --- inspect 5.7   3.4   260   .65  0  
recursive-simple/fibo_2calls_10_true-unreach-call.c true 2 wit inspect 6.4 2.4 420 52 0   0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.5  2.5  250 0   0   true 2 --- inspect 86     56     3600   .62  0  
recursive-simple/fibo_2calls_15_true-unreach-call.c true 1 wit inspect 50   41   1900 590 0   0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.6  2.0  250 0   0   timeout 0 --- inspect 960     900     5200   .62  0  
recursive-simple/fibo_2calls_20_true-unreach-call.c timeout 0 wit inspect 920   890   3900 12000 0   0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.5  1.9  250 0   0   timeout 0 --- inspect 960     900     5500   .64  0  
recursive-simple/fibo_2calls_25_true-unreach-call.c timeout 0 wit inspect 960   880   5600 12000 0   0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .67 .41 42 0   0   error (invalid witness file) 0 --- inspect 5.2   2.9   260   .65  0  
recursive-simple/fibo_2calls_2_true-unreach-call_true-termination.c true 2 wit inspect 2.9 1.3 250 24 0   0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.6  2.1  250 0   0   true 2 --- inspect 12     6.7   390   .62  0  
recursive-simple/fibo_2calls_4_true-unreach-call_true-termination.c true 2 wit inspect 3.4 1.5 270 32 0   0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.9  2.2  250 0   0   true 2 --- inspect 17     10     530   .62  0  
recursive-simple/fibo_2calls_5_true-unreach-call_true-termination.c true 2 wit inspect 3.8 1.6 270 39 0   0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.3  2.4  250 0   0   true 2 --- inspect 23     14     670   .62  0  
recursive-simple/fibo_2calls_6_true-unreach-call_true-termination.c true 2 wit inspect 3.9 1.6 270 41 0   0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.7  2.1  250 0   0   true 2 --- inspect 32     19     700   .66  0  
recursive-simple/fibo_2calls_8_true-unreach-call_true-termination.c true 2 wit inspect 5.2 1.9 290 42 0   0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.7  2.1  250 0   0   true 2 --- inspect 46     29     1100   .62  0  
recursive-simple/fibo_5_true-unreach-call_true-termination.c true 2 wit inspect 3.5 1.5 270 34 0   0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.5  2.0  250 0   0   true 2 --- inspect 16     9.9   530   .66  0  
recursive-simple/fibo_7_true-unreach-call_true-termination.c true 2 wit inspect 4.3 1.7 270 42 0   0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.5  2.0  250 0   0   true 2 --- inspect 26     16     690   .66  0  
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 3.4 1.5 270 31 0   0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.0  2.3  250 0   0   true 2 --- inspect 14     8.3   460   .66  0  
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 3.6 1.6 270 29 0   0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.4  1.9  250 0   0   true 2 --- inspect 16     9.8   460   .66  0  
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 3.4 1.5 270 34 0   0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.2  2.4  250 0   0   true 2 --- inspect 15     8.7   470   .66  0  
recursive-simple/id2_i5_o5_true-unreach-call_true-termination.c true 2 wit inspect 3.5 1.5 270 34 0   0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.4  1.9  250 0   0   true 2 --- inspect 15     9.3   520   .66  0  
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 3.2 1.5 270 30 0   0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.6  2.5  250 0   0   true 2 --- inspect 13     8.0   390   .66  0  
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 3.1 1.4 260 29 0   0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.4  2.5  250 0   0   true 2 --- inspect 9.6   5.4   320   .66  0  
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 3.3 1.5 260 31 0   0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.5  1.9  250 0   0   true 2 --- inspect 9.2   5.3   320   .66  0  
recursive-simple/id_i10_o10_true-unreach-call_true-termination.c true 2 wit inspect 3.4 1.5 260 32 0   0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.4  1.9  250 0   0   true 2 --- inspect 18     11     510   .62  0  
recursive-simple/id_i15_o15_true-unreach-call_true-termination.c true 2 wit inspect 3.5 1.5 270 36 0   0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.6  2.0  250 0   0   true 2 --- inspect 28     17     500   .62  0  
recursive-simple/id_i20_o20_true-unreach-call_true-termination.c true 2 wit inspect 3.6 1.6 270 33 0   0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.9  2.8  250 0   0   true 2 --- inspect 32     20     720   .66  0  
recursive-simple/id_i25_o25_true-unreach-call_true-termination.c true 2 wit inspect 3.8 1.6 270 36 0   0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.4  2.4  250 0   0   true 2 --- inspect 41     26     770   .62  0  
recursive-simple/id_i5_o5_true-unreach-call_true-termination.c true 2 wit inspect 3.3 1.5 270 30 0   0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.4  1.9  250 0   0   true 2 --- inspect 13     7.4   440   .66  0  
recursive-simple/sum_10x0_true-unreach-call_true-termination.c true 2 wit inspect 3.6 1.6 260 36 0   0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.5  2.0  250 0   0   true 2 --- inspect 22     13     620   .66  0  
recursive-simple/sum_15x0_true-unreach-call_true-termination.c true 2 wit inspect 3.7 1.6 270 37 0   0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.6  2.0  250 0   0   true 2 --- inspect 30     19     690   .62  0  
recursive-simple/sum_20x0_true-unreach-call_true-termination.c true 2 wit inspect 4.2 1.7 300 34 0   0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.8  2.6  250 0   0   true 2 --- inspect 35     22     590   .62  0  
recursive-simple/sum_25x0_true-unreach-call_true-termination.c true 2 wit inspect 4.7 1.7 310 41 0   0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.4  1.9  250 0   0   true 2 --- inspect 49     32     820   .62  0  
recursive-simple/sum_2x3_true-unreach-call_true-termination.c true 2 wit inspect 3.3 1.5 260 31 0   0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.0  2.2  250 0   0   true 2 --- inspect 13     7.7   390   .62  0  
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 3.6 1.7 270 30 0   0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.1  2.3  250 0   0   true 2 --- inspect 10     5.8   330   .62  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 111 17000 16000 150000 210000 0   .029 44 39 490 270 21000 0   0   44 -3 1500   960   79000 30    0   44 39 340 310 17000 .016 0   44 41 46 46 2000 2.0 .094 52 6 180 99   11000 0   0   52 76 7400 6400 61000 31 0  
    correct results 75 109 1200 920 39000 8700 0   .029 39 39 380 210 16000 0   0   29 29 400   230   16000 19    0   39 39 230 130 12000 0     0   41 41 46 46 2000 2.0 .094 3 6 11 6.4 760 0   0   38 76 1900 1400 34000 24 0  
        correct true 34 68 160 82 11000 1700 0   0     0 0 0 0 3 6 11 6.4 760 0   0   38 76 1900 1400 34000 24 0  
        correct false 41 41 1000 830 28000 7000 0   .029 39 39 380 210 16000 0   0   29 29 400   230   16000 19    0   39 39 230 130 12000 0     0   41 41 46 46 2000 2.0 .094 0 0
    correct-unconfimed results 2 2 53 43 2200 630 0   0     0 0 0 0 0 0
        correct-unconfirmed true 2 2 53 43 2200 630 0   0     0 0 0 0 0 0
        correct-unconfirmed false 0 0 0 0 0 0 0
    incorrect results 0 0 1 -32 6.7 3.8 300 .62 0   0 0 0 0
        incorrect true 0 0 1 -32 6.7 3.8 300 .62 0   0 0 0 0
        incorrect false 0 0 0 0 0 0 0
score (96 tasks, max score: 148) 111 39 -3 39 41 6 76
Run set cpa-seq.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-seq-validate-violation-witnesses-cpa-seq.sv-comp19_prop-reachsafety.ReachSafety-Recursive uautomizer-validate-violation-witnesses-cpa-seq.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-witness2test-validate-violation-witnesses-cpa-seq.sv-comp19_prop-reachsafety.ReachSafety-Recursive fshell-witness2test-validate-violation-witnesses-cpa-seq.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-seq-validate-correctness-witnesses-cpa-seq.sv-comp19_prop-reachsafety.ReachSafety-Recursive uautomizer-validate-correctness-witnesses-cpa-seq.sv-comp19_prop-reachsafety.ReachSafety-Recursive