Tool DIVINE CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a CPA-witness2test 1.7-svn 29852 CProver witness2test 0.1 CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon*
OS Linux 4.15.0-42-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33546 MB
Date of execution 2018-12-06 11:06:04 CET 2018-12-08 03:24:14 CET 2018-12-08 05:17:35 CET 2018-12-08 06:43:53 CET 2018-12-12 20:24:22 CET 2018-12-08 01:45:35 CET 2018-12-08 04:38:54 CET
Run set divine-smt.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-seq-validate-violation-witnesses-divine-smt.sv-comp19_prop-reachsafety.ReachSafety-Recursive uautomizer-validate-violation-witnesses-divine-smt.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-witness2test-validate-violation-witnesses-divine-smt.sv-comp19_prop-reachsafety.ReachSafety-Recursive fshell-witness2test-validate-violation-witnesses-divine-smt.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-seq-validate-correctness-witnesses-divine-smt.sv-comp19_prop-reachsafety.ReachSafety-Recursive uautomizer-validate-correctness-witnesses-divine-smt.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/divine-smt.2018-12-06_1106.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/divine-smt.2018-12-06_1106.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true -witness ../../results-verified/divine-smt.2018-12-06_1106.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/divine-smt.2018-12-06_1106.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/divine-smt.2018-12-06_1106.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/divine-smt.2018-12-06_1106.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ 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 12   9.5 440 130 0      0     false(unreach-call) 1 wit inspect 7.2  4.0  270 0   0      true -32 --- inspect 8.1   4.9   300   .66 0    unknown 0 --- inspect 4.5 2.6  250 0   0    true -32 --- inspect .57   .57   20    .049 0      - --- inspect - --- inspect
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 9.9 9.0 430 120 0      0     false(unreach-call) 1 wit inspect 4.7  2.6  270 0   .0041 true -32 --- inspect 7.5   4.2   300   .66 0    unknown 0 --- inspect 4.7 2.8  240 0   .37 error (2) 0 --- inspect .60   .60   20    .049 0      - --- inspect - --- inspect
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 9.1 8.7 430 110 0      0     false(unreach-call) 1 wit inspect 4.7  2.6  250 0   0      true -32 --- inspect 8.8   5.1   300   .66 0    unknown 0 --- inspect 3.9 2.3  250 0   0    true -32 --- inspect .57   .57   20    .049 0      - --- inspect - --- inspect
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 9.1 8.6 430 110 0      0     false(unreach-call) 1 wit inspect 4.9  2.8  260 0   0      true -32 --- inspect 6.9   4.0   300   .62 0    unknown 0 --- inspect 3.7 2.2  250 0   0    false(unreach-call) 1 --- inspect .58   .59   20    .049 0      - --- inspect - --- inspect
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 24   13   450 290 0      0     false(unreach-call) 1 wit inspect 12    6.8  340 0   0      true -32 --- inspect 7.5   4.7   310   .66 0    unknown 0 --- inspect 4.2 2.4  240 0   0    true -32 --- inspect .60   .59   20    .049 0      - --- inspect - --- inspect
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 360   100   680 3500 0      0     false(unreach-call) 1 wit inspect 32    26    480 0   0      true -32 --- inspect 7.5   4.3   310   .62 0    unknown 0 --- inspect 4.7 2.7  250 0   0    true -32 --- inspect .57   .57   20    .049 0      - --- inspect - --- inspect
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 9.1 8.8 430 120 0      0     false(unreach-call) 1 wit inspect 3.9  2.2  250 0   .0041 false(unreach-call) 1 --- inspect 7.5   4.6   300   .66 0    unknown 0 --- inspect 3.8 2.2  240 0   0    true -32 --- inspect .57   .57   20    .049 0      - --- inspect - --- inspect
recursive/Ackermann01_true-unreach-call_true-no-overflow.c timeout 0 --- inspect 900   230   1300 9000 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .46 40 0   0   error (2) 0 --- inspect .025 .025 5.6 0    0  
recursive/Ackermann03_true-unreach-call_true-no-overflow.c timeout 0 --- inspect 900   230   1900 8700 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .45 40 0   0   error (2) 0 --- inspect .025 .026 5.7 0    0  
recursive/Ackermann04_true-unreach-call_true-no-overflow.c timeout 0 --- inspect 900   230   1300 9300 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .47 41 0   0   error (2) 0 --- inspect .025 .026 5.6 0    0  
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900   230   680 8400 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .42 40 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0  
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900   230   430 9300 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .38 40 0   0   error (2) 0 --- inspect .028 .029 5.6 0    0  
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900   230   420 9200 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .47 41 0   0   error (2) 0 --- inspect .022 .024 5.6 0    0  
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c timeout 0 --- inspect 900   230   990 9700 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .45 40 0   0   error (2) 0 --- inspect .027 .027 5.6 0    0  
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 8.1 8.2 370 100 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.5  2.0  250 0   0   true 2 --- inspect 37     22     1500   .62 0  
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900   230   1000 9000 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .67 .41 40 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0  
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900   230   660 8000 .0041 .086 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .40 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0  
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900   230   420 8100 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .81 .48 42 0   0   error (2) 0 --- inspect .026 .026 5.6 0    0  
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c timeout 0 --- inspect 900   230   450 9600 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .36 42 0   0   error (2) 0 --- inspect .022 .023 5.6 0    0  
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900   230   540 9000 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .57 .36 40 0   0   error (2) 0 --- inspect .024 .025 5.7 0    0  
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900   230   550 8900 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .36 40 0   0   error (2) 0 --- inspect .021 .022 5.7 0    0  
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900   230   1400 8800 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .41 40 0   0   error (2) 0 --- inspect .027 .027 5.6 0    0  
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 28   13   380 300 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.5  2.5  250 0   0   true 2 --- inspect 8.3   4.7   310   .66 0  
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 31   14   380 350 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.4  1.9  250 0   0   true 2 --- inspect 14     8.7   460   .66 0  
recursive-simple/afterrec_2calls_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 8.1 8.1 430 110 0      0     true -32 wit inspect 4.3  2.4  250 0   0      false(unreach-call) 1 --- inspect 8.1   4.5   300   .66 0    unknown 0 --- inspect 3.6 2.1  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 8.0 8.0 430 110 0      0     true -32 wit inspect 4.4  2.4  250 0   0      false(unreach-call) 1 --- inspect 8.0   4.5   310   .66 0    unknown 0 --- inspect 3.5 2.0  240 0   0    false(unreach-call) 1 --- inspect .56   .58   20    .045 0      - --- inspect - --- inspect
recursive-simple/fibo_10_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 8.4 8.4 430 100 0      0     false(unreach-call) 1 wit inspect 8.3  4.7  330 0   0      true -32 --- inspect 7.3   4.6   310   .66 0    false(unreach-call) 1 --- inspect 3.7 2.2  250 0   0    false(unreach-call) 1 --- inspect .60   .60   20    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_15_false-unreach-call.c false(unreach-call) 1 wit inspect 8.4 8.4 430 130 0      0     false(unreach-call) 1 wit inspect 22    15    1200 0   0      true -32 --- inspect 8.6   5.2   310   .66 0    false(unreach-call) 1 --- inspect 4.5 2.7  250 0   0    false(unreach-call) 1 --- inspect .60   .62   20    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_20_false-unreach-call.c false(unreach-call) 1 wit inspect 9.1 8.8 440 120 0      0     out of memory 0 --- inspect 49    39    7000 0   0      true -32 --- inspect 7.3   4.5   310   .66 0    false(unreach-call) 1 --- inspect 4.6 2.6  250 0   0    false(unreach-call) 1 --- inspect .58   .58   20    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_25_false-unreach-call.c false(unreach-call) 1 wit inspect 18   14   640 240 0      0     timeout 0 --- inspect 98    64    3900 0   0      true -32 --- inspect 8.4   4.7   310   .66 0    false(unreach-call) 1 --- inspect 3.5 2.1  250 0   0    false(unreach-call) 1 --- inspect .61   .60   20    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_10_false-unreach-call.c false(unreach-call) 1 wit inspect 8.3 8.3 430 97 0      0     false(unreach-call) 1 wit inspect 7.0  3.9  340 0   0      true -32 --- inspect 8.6   4.8   310   .66 0    false(unreach-call) 1 --- inspect 4.6 2.6  250 0   0    false(unreach-call) 1 --- inspect .59   .59   20    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_15_false-unreach-call.c false(unreach-call) 1 wit inspect 8.4 8.4 430 110 0      0     false(unreach-call) 1 wit inspect 26    17    1200 0   0      true -32 --- inspect 9.2   5.0   310   .66 0    false(unreach-call) 1 --- inspect 4.5 2.6  250 0   0    false(unreach-call) 1 --- inspect .60   .59   20    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_20_false-unreach-call.c false(unreach-call) 1 wit inspect 9.1 8.7 440 140 0      0     out of memory 0 --- inspect 58    42    7000 0   0      true -32 --- inspect 8.7   4.9   310   .66 0    false(unreach-call) 1 --- inspect 4.5 2.6  240 0   0    false(unreach-call) 1 --- inspect .57   .60   20    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_25_false-unreach-call.c false(unreach-call) 1 wit inspect 18   14   640 210 0      0     timeout 0 --- inspect 98    58    3800 0   0      true -32 --- inspect 8.7   4.9   310   .66 0    false(unreach-call) 1 --- inspect 4.0 2.3  250 0   0    false(unreach-call) 1 --- inspect .57   .58   20    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_2_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 8.4 8.4 430 110 0      0     false(unreach-call) 1 wit inspect 3.8  2.1  250 0   0      true -32 --- inspect 7.7   4.8   300   .66 0    false(unreach-call) 1 --- inspect 4.8 2.8  250 0   0    false(unreach-call) 1 --- inspect .58   .59   20    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_4_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 8.3 8.3 430 110 0      0     false(unreach-call) 1 wit inspect 4.2  2.3  260 0   0      true -32 --- inspect 7.8   4.4   310   .66 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_5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 8.2 8.3 430 100 0      0     false(unreach-call) 1 wit inspect 6.0  3.3  260 0   0      true -32 --- inspect 7.9   4.7   310   .66 0    false(unreach-call) 1 --- inspect 4.6 2.6  250 0   0    false(unreach-call) 1 --- inspect .61   .62   20    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_6_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 8.5 8.5 430 120 0      0     false(unreach-call) 1 wit inspect 6.2  3.3  270 0   0      true -32 --- inspect 8.5   4.7   310   .66 0    false(unreach-call) 1 --- inspect 3.5 2.1  240 0   0    false(unreach-call) 1 --- inspect .61   .62   20    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_8_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 8.4 8.4 430 110 0      0     false(unreach-call) 1 wit inspect 5.6  3.1  280 0   0      true -32 --- inspect 8.7   4.9   310   .66 0    false(unreach-call) 1 --- inspect 4.7 2.7  240 0   0    false(unreach-call) 1 --- inspect .57   .57   20    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 8.2 8.2 430 110 0      0     false(unreach-call) 1 wit inspect 6.0  3.4  260 0   0      true -32 --- inspect 8.4   4.7   310   .66 0    false(unreach-call) 1 --- inspect 4.4 2.5  250 0   0    false(unreach-call) 1 --- inspect .59   .60   20    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_7_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 8.2 8.2 430 130 0      0     false(unreach-call) 1 wit inspect 4.8  2.7  280 0   0      true -32 --- 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_b3_o2_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 8.6 8.5 430 100 0      0     false(unreach-call) 1 wit inspect 5.3  2.9  260 0   .094  true -32 --- inspect 9.2   5.4   310   .66 0    unknown 0 --- inspect 4.7 2.7  250 0   0    true -32 --- inspect .59   .59   20    .049 0      - --- inspect - --- inspect
recursive-simple/id2_i5_o5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 8.4 8.4 430 120 0      0     false(unreach-call) 1 wit inspect 5.3  2.9  260 0   0      true -32 --- inspect 7.6   4.3   320   .62 0    false(unreach-call) 1 --- inspect 3.9 2.3  250 0   0    false(unreach-call) 1 --- inspect .58   .58   20    .049 0      - --- inspect - --- inspect
recursive-simple/id_b3_o2_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 8.7 8.5 430 100 0      0     false(unreach-call) 1 wit inspect 4.9  2.7  260 0   0      true -32 --- inspect 9.3   5.5   310   .66 0    unknown 0 --- inspect 4.0 2.4  250 0   0    true -32 --- inspect .60   .61   20    .049 0      - --- inspect - --- inspect
recursive-simple/id_i10_o10_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 8.3 8.3 430 110 0      0     false(unreach-call) 1 wit inspect 4.5  2.5  270 0   0      true -32 --- inspect 7.6   4.3   310   .62 0    false(unreach-call) 1 --- inspect 4.1 2.4  250 0   0    false(unreach-call) 1 --- inspect .59   .60   20    .045 0      - --- inspect - --- inspect
recursive-simple/id_i15_o15_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 8.1 8.1 430 110 0      0     false(unreach-call) 1 wit inspect 4.7  2.6  260 0   0      true -32 --- inspect 8.4   4.7   310   .66 0    false(unreach-call) 1 --- inspect 4.0 2.3  240 0   0    false(unreach-call) 1 --- inspect .57   .57   20    .045 0      - --- inspect - --- inspect
recursive-simple/id_i20_o20_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 8.3 8.3 430 120 0      0     false(unreach-call) 1 wit inspect 5.2  2.9  270 0   0      true -32 --- inspect 7.6   4.8   310   .66 0    false(unreach-call) 1 --- inspect 4.3 2.5  240 0   0    false(unreach-call) 1 --- inspect .59   .59   20    .045 0      - --- inspect - --- inspect
recursive-simple/id_i25_o25_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 8.3 8.3 430 96 0      0     false(unreach-call) 1 wit inspect 5.7  3.2  270 0   0      true -32 --- inspect 7.6   4.3   300   .66 0    false(unreach-call) 1 --- inspect 4.7 2.7  250 0   0    false(unreach-call) 1 --- inspect .59   .61   20    .045 .0041 - --- inspect - --- inspect
recursive-simple/id_i5_o5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 8.2 8.2 430 100 0      0     false(unreach-call) 1 wit inspect 5.9  3.3  260 0   0      true -32 --- inspect 9.4   5.5   310   .66 0    false(unreach-call) 1 --- inspect 4.3 2.5  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 timeout 0 --- inspect 900   230   400 8100 .0041 0     error (invalid witness file) 0 --- inspect .69 .42 42 0   0      error (2) 0 --- inspect .032 .033 5.6 0    0    error (invalid witness file) 0 --- inspect 1.1 .68 48 0   0    error (invalid witness file) 0 --- inspect .0055 .0070 .52 0     0      - --- inspect - --- inspect
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 290   120   450 3000 0      0     false(unreach-call) 1 wit inspect 11    5.9  450 0   0      true -32 --- inspect 8.8   5.0   320   .66 0    unknown 0 --- inspect 3.5 2.1  250 0   0    true -32 --- inspect .60   .61   20    .049 0      - --- inspect - --- inspect
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 12   10   430 160 0      0     false(unreach-call) 1 wit inspect 4.8  2.6  270 0   0      true -32 --- inspect 9.1   5.4   310   .66 0    unknown 0 --- inspect 3.4 2.0  240 0   0    true -32 --- inspect .59   .59   20    .049 0      - --- inspect - --- inspect
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c timeout 0 --- inspect 900   230   400 9000 .0041 0     error (invalid witness file) 0 --- inspect .73 .45 40 0   0      error (2) 0 --- inspect .028 .029 5.6 0    0    error (invalid witness file) 0 --- inspect 1.1 .71 47 0   0    error (invalid witness file) 0 --- inspect .0054 .0065 .53 0     0      - --- inspect - --- inspect
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 20   13   440 230 0      0     false(unreach-call) 1 wit inspect 6.1  3.4  270 0   0      true -32 --- inspect 8.8   4.9   320   .66 0    unknown 0 --- inspect 4.6 2.7  240 0   0    true -32 --- inspect .57   .57   20    .049 0      - --- inspect - --- inspect
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 9.0 8.7 430 100 0      0     false(unreach-call) 1 wit inspect 5.4  3.0  260 0   0      true -32 --- inspect 8.1   5.0   320   .66 0    unknown 0 --- inspect 3.8 2.2  250 0   0    true -32 --- inspect .58   .58   20    .049 0      - --- inspect - --- inspect
recursive-simple/sum_10x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 8.2 8.2 430 89 0      0     false(unreach-call) 1 wit inspect 5.1  2.8  270 0   0      true -32 --- inspect 7.8   4.4   310   .62 .14 false(unreach-call) 1 --- inspect 3.7 2.2  250 0   0    false(unreach-call) 1 --- inspect .57   .58   20    .045 0      - --- inspect - --- inspect
recursive-simple/sum_15x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 8.3 8.4 430 110 0      0     false(unreach-call) 1 wit inspect 6.1  3.4  270 0   0      true -32 --- inspect 8.1   5.0   310   .66 0    false(unreach-call) 1 --- inspect 3.5 2.0  240 0   0    false(unreach-call) 1 --- inspect .61   .61   20    .045 0      - --- inspect - --- inspect
recursive-simple/sum_20x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 8.2 8.2 430 97 0      0     false(unreach-call) 1 wit inspect 4.7  2.6  270 0   0      true -32 --- inspect 7.9   4.9   310   .66 0    false(unreach-call) 1 --- inspect 4.1 2.4  250 0   0    false(unreach-call) 1 --- inspect .56   .56   20    .045 0      - --- inspect - --- inspect
recursive-simple/sum_25x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 7.9 8.0 430 120 0      0     false(unreach-call) 1 wit inspect 5.1  2.8  280 0   0      true -32 --- inspect 8.2   5.0   300   .66 0    false(unreach-call) 1 --- inspect 3.5 2.1  250 0   0    false(unreach-call) 1 --- inspect .57   .57   20    .045 .0041 - --- inspect - --- inspect
recursive-simple/sum_2x3_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 8.2 8.2 430 100 0      0     false(unreach-call) 1 wit inspect 4.4  2.4  260 0   0      true -32 --- inspect 7.4   4.2   310   .66 0    false(unreach-call) 1 --- inspect 4.5 2.7  250 0   0    false(unreach-call) 1 --- inspect .57   .57   20    .045 .0041 - --- inspect - --- inspect
recursive-simple/sum_non_eq_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 8.6 8.5 430 110 0      0     false(unreach-call) 1 wit inspect 4.8  2.7  260 0   0      false(unreach-call) 1 --- inspect 7.0   3.9   310   .66 0    unknown 0 --- inspect 4.2 2.5  250 0   0    false(unreach-call) 1 --- inspect .57   .59   20    .049 0      - --- inspect - --- inspect
recursive-simple/afterrec_2calls_true-unreach-call_true-termination.c true 2 wit inspect 8.0 8.0 370 92 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.4  2.0  250 0   0   true 2 --- inspect 8.0   4.8   320   .66 0  
recursive-simple/afterrec_true-unreach-call_true-termination.c true 2 wit inspect 8.2 8.2 370 120 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.4  2.4  250 0   0   true 2 --- inspect 8.1   4.9   310   .62 0  
recursive-simple/fibo_10_true-unreach-call_true-termination.c true 2 wit inspect 8.3 8.3 370 110 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.4  1.9  250 0   0   true 2 --- inspect 55     34     2300   .62 0  
recursive-simple/fibo_15_true-unreach-call.c true 2 wit inspect 8.3 8.3 370 80 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.1  2.3  250 0   0   true 2 --- inspect 800     730     6400   .62 0  
recursive-simple/fibo_20_true-unreach-call.c true 1 wit inspect 8.5 8.3 370 110 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.5  2.5  250 0   0   timeout 0 --- inspect 960     910     5400   .63 0  
recursive-simple/fibo_25_true-unreach-call.c true 1 wit inspect 14   9.7 400 160 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.5  1.9  250 0   0   timeout 0 --- inspect 960     910     5800   .65 0  
recursive-simple/fibo_2calls_10_true-unreach-call.c true 2 wit inspect 8.2 8.2 370 100 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.8  2.1  250 0   0   true 2 --- inspect 110     71     4500   .62 0  
recursive-simple/fibo_2calls_15_true-unreach-call.c true 1 wit inspect 8.3 8.3 370 100 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.3  2.4  250 0   0   timeout 0 --- inspect 960     900     5100   .71 0  
recursive-simple/fibo_2calls_20_true-unreach-call.c true 1 wit inspect 8.6 8.4 370 95 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.6  2.6  250 0   0   timeout 0 --- inspect 960     900     5200   1.4  0  
recursive-simple/fibo_2calls_25_true-unreach-call.c true 1 wit inspect 14   9.6 400 160 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.5  2.0  250 0   0   out of memory 0 --- inspect 660     600     7000   .64 0  
recursive-simple/fibo_2calls_2_true-unreach-call_true-termination.c true 2 wit inspect 8.1 8.1 370 130 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.5  2.5  250 0   0   true 2 --- inspect 13     7.9   390   .66 0  
recursive-simple/fibo_2calls_4_true-unreach-call_true-termination.c true 2 wit inspect 8.3 8.3 370 100 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.6  2.6  250 0   0   true 2 --- inspect 18     11     540   .66 0  
recursive-simple/fibo_2calls_5_true-unreach-call_true-termination.c true 2 wit inspect 8.2 8.2 370 130 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.6  2.6  250 0   0   true 2 --- inspect 26     16     510   .66 0  
recursive-simple/fibo_2calls_6_true-unreach-call_true-termination.c true 2 wit inspect 8.4 8.5 370 96 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.8  2.7  250 0   0   true 2 --- inspect 29     18     750   .66 0  
recursive-simple/fibo_2calls_8_true-unreach-call_true-termination.c true 2 wit inspect 8.2 8.2 370 96 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.5  2.0  250 0   0   true 2 --- inspect 53     33     1000   .62 0  
recursive-simple/fibo_5_true-unreach-call_true-termination.c true 2 wit inspect 8.3 8.3 370 100 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.6  2.5  250 0   0   true 2 --- inspect 18     11     560   .62 0  
recursive-simple/fibo_7_true-unreach-call_true-termination.c true 2 wit inspect 8.1 8.2 370 99 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.6  2.0  250 0   0   true 2 --- inspect 22     14     650   .66 0  
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c timeout 0 --- inspect 900   230   400 9400 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .43 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0  
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c timeout 0 --- inspect 900   230   400 9700 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .38 41 0   0   error (2) 0 --- inspect .027 .028 5.7 0    0  
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c timeout 0 --- inspect 900   230   400 8800 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .43 40 0   0   error (2) 0 --- inspect .020 .022 5.6 0    0  
recursive-simple/id2_i5_o5_true-unreach-call_true-termination.c true 2 wit inspect 8.1 8.1 370 93 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.3  2.4  250 0   0   true 2 --- inspect 15     9.3   500   .66 0  
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c timeout 0 --- inspect 900   230   400 7800 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .38 40 0   0   error (2) 0 --- inspect .023 .024 5.6 0    0  
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c timeout 0 --- inspect 900   230   400 9000 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .37 41 0   0   error (2) 0 --- inspect .023 .024 5.6 0    0  
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c timeout 0 --- inspect 900   230   400 8700 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .46 41 0   0   error (2) 0 --- inspect .022 .022 5.6 0    0  
recursive-simple/id_i10_o10_true-unreach-call_true-termination.c true 2 wit inspect 8.2 8.2 370 120 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.2  2.4  250 0   0   true 2 --- inspect 16     9.8   520   .62 0  
recursive-simple/id_i15_o15_true-unreach-call_true-termination.c true 2 wit inspect 8.1 8.1 370 120 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.3  2.4  250 0   0   true 2 --- inspect 22     14     610   .62 0  
recursive-simple/id_i20_o20_true-unreach-call_true-termination.c true 2 wit inspect 8.1 8.1 370 93 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.3  2.4  250 0   0   true 2 --- inspect 34     21     560   .62 0  
recursive-simple/id_i25_o25_true-unreach-call_true-termination.c true 2 wit inspect 8.3 8.3 370 120 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.0  2.3  250 0   0   true 2 --- inspect 36     23     760   .66 0  
recursive-simple/id_i5_o5_true-unreach-call_true-termination.c true 2 wit inspect 8.1 8.2 370 93 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.6  2.0  250 0   0   true 2 --- inspect 15     8.8   440   .66 0  
recursive-simple/sum_10x0_true-unreach-call_true-termination.c true 2 wit inspect 8.1 8.2 370 100 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.8  2.1  250 0   0   true 2 --- inspect 21     13     590   .66 0  
recursive-simple/sum_15x0_true-unreach-call_true-termination.c true 2 wit inspect 8.1 8.2 370 98 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.6  2.0  250 0   0   true 2 --- inspect 32     19     530   .66 0  
recursive-simple/sum_20x0_true-unreach-call_true-termination.c true 2 wit inspect 8.2 8.2 370 99 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.3  2.4  250 0   0   true 2 --- inspect 37     23     590   .62 0  
recursive-simple/sum_25x0_true-unreach-call_true-termination.c true 2 wit inspect 8.0 8.0 370 110 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.5  1.9  250 0   0   true 2 --- inspect 53     35     720   .62 0  
recursive-simple/sum_2x3_true-unreach-call_true-termination.c true 2 wit inspect 8.1 8.1 370 100 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.2  2.3  250 0   0   true 2 --- inspect 14     8.1   380   .66 0  
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c timeout 0 --- inspect 900   230   410 9200 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .39 41 0   0   error (2) 0 --- inspect .021 .022 5.7 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 99 22000 6200 46000 220000 .094 .086 44 -28 580   370   34000 0   .10 44 -1212 340 200 13000 27   .14 44 26 180 100 10000 0   .37 44 -322 25   25   850 2.0  .012 52 6 140 79   8600 0   0   52 52 6000 5400 55000 21 0  
    correct results 68 94 1300 810 28000 15000 0     0     36 36 270   160   12000 0   .10 4 4 31 18 1200 2.6 0    26 26 110 63 6400 0   0    30 30 18   18   610 1.4  .012 3 6 12 6.9 750 0   0   26 52 1500 1200 27000 17 0  
        correct true 26 52 260 220 9600 3200 0     0     0 0 0 0 3 6 12 6.9 750 0   0   26 52 1500 1200 27000 17 0  
        correct false 42 42 1000 580 19000 12000 0     0     36 36 270   160   12000 0   .10 4 4 31 18 1200 2.6 0    26 26 110 63 6400 0   0    30 30 18   18   610 1.4  .012 0 0
    correct-unconfimed results 5 5 54 44 1900 620 0     0     0 0 0 0 0 0
        correct-unconfirmed true 5 5 54 44 1900 620 0     0     0 0 0 0 0 0
        correct-unconfirmed false 0 0 0 0 0 0 0
    incorrect results 0 2 -64 8.7 4.8 500 0   0    38 -1216 310 180 12000 25   .14 0 11 -352 6.4 6.4 220 .54 0     0 0
        incorrect true 0 2 -64 8.7 4.8 500 0   0    38 -1216 310 180 12000 25   .14 0 11 -352 6.4 6.4 220 .54 0     0 0
        incorrect false 0 0 0 0 0 0 0
score (96 tasks, max score: 148) 99 -28 -1212 26 -322 6 52
Run set divine-smt.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-seq-validate-violation-witnesses-divine-smt.sv-comp19_prop-reachsafety.ReachSafety-Recursive uautomizer-validate-violation-witnesses-divine-smt.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-witness2test-validate-violation-witnesses-divine-smt.sv-comp19_prop-reachsafety.ReachSafety-Recursive fshell-witness2test-validate-violation-witnesses-divine-smt.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-seq-validate-correctness-witnesses-divine-smt.sv-comp19_prop-reachsafety.ReachSafety-Recursive uautomizer-validate-correctness-witnesses-divine-smt.sv-comp19_prop-reachsafety.ReachSafety-Recursive