Tool VeriFuzz 1.0.0 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-09 02:47:33 CET 2018-12-09 17:43:44 CET 2018-12-09 18:26:53 CET 2018-12-09 18:31:36 CET 2018-12-12 22:04:17 CET 2018-12-09 17:35:51 CET 2018-12-09 18:23:50 CET
Run set verifuzz.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-seq-validate-violation-witnesses-verifuzz.sv-comp19_prop-reachsafety.ReachSafety-Recursive uautomizer-validate-violation-witnesses-verifuzz.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-witness2test-validate-violation-witnesses-verifuzz.sv-comp19_prop-reachsafety.ReachSafety-Recursive fshell-witness2test-validate-violation-witnesses-verifuzz.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-seq-validate-correctness-witnesses-verifuzz.sv-comp19_prop-reachsafety.ReachSafety-Recursive uautomizer-validate-correctness-witnesses-verifuzz.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/verifuzz.2018-12-09_0247.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/verifuzz.2018-12-09_0247.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/verifuzz.2018-12-09_0247.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/verifuzz.2018-12-09_0247.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/verifuzz.2018-12-09_0247.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/verifuzz.2018-12-09_0247.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.0 2.6 150 46 .66 0      false(unreach-call) 1 wit inspect 6.1  3.4  270 0   .029  true -32 --- inspect 7.2   4.6   310   .62 0      false(unreach-call) 1 --- inspect 3.6  2.1  250 0   .0041 false(unreach-call) 1 --- inspect .59   .59   20    .049 0      - --- inspect - --- inspect
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 3.5 2.0 150 34 .59 .0041 false(unreach-call) 1 wit inspect 4.6  2.5  270 0   .033  true -32 --- inspect 7.9   4.9   310   .66 0      false(unreach-call) 1 --- inspect 3.5  2.1  250 0   0      false(unreach-call) 1 --- inspect .58   .58   20    .049 .0041 - --- inspect - --- inspect
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 3.3 2.0 150 38 .59 0      false(unreach-call) 1 wit inspect 3.7  2.1  250 0   0      true -32 --- inspect 6.6   3.7   290   .66 0      false(unreach-call) 1 --- inspect 3.6  2.1  250 0   0      false(unreach-call) 1 --- inspect .58   .58   20    .049 0      - --- inspect - --- inspect
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 3.6 2.2 150 40 .61 0      false(unreach-call) 1 wit inspect 4.0  2.3  260 0   0      false(unreach-call) 1 --- 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 .58   .58   20    .049 0      - --- inspect - --- inspect
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 46   44   150 530 .68 .070  false(unreach-call) 1 wit inspect 11    6.5  390 0   .11   true -32 --- inspect 7.3   4.1   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/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 16   14   150 180 .68 .041  false(unreach-call) 1 wit inspect 28    21    480 0   0      true -32 --- inspect 7.3   4.1   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/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 13   12   150 160 .66 0      false(unreach-call) 1 wit inspect 4.0  2.2  260 0   0      false(unreach-call) 1 --- inspect 6.5   3.7   300   .66 0      false(unreach-call) 1 --- inspect 3.4  2.0  250 0   0      false(unreach-call) 1 --- inspect .59   .60   20    .049 0      - --- inspect - --- inspect
recursive/Ackermann01_true-unreach-call_true-no-overflow.c timeout 0 --- inspect 900   910   150 12000 .59 .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .40 40 0   0   error (2) 0 --- inspect .019 .020 5.6 0   0  
recursive/Ackermann03_true-unreach-call_true-no-overflow.c timeout 0 --- inspect 900   910   150 11000 .74 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .46 41 0   0   error (2) 0 --- inspect .020 .020 5.6 0   0  
recursive/Ackermann04_true-unreach-call_true-no-overflow.c timeout 0 --- inspect 900   910   150 12000 .71 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .70 .43 42 0   0   error (2) 0 --- inspect .020 .020 5.6 0   0  
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900   900   150 11000 .63 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .45 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 --- inspect 900   900   150 13000 .77 .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .79 .47 42 0   0   error (2) 0 --- inspect .020 .020 5.6 0   0  
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900   900   200 11000 .71 46      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .47 40 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0  
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c timeout 0 --- inspect 900   900   150 9000 .63 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .35 40 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0  
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900   920   150 12000 .61 .012  - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .68 .43 41 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   150 11000 .61 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .38 41 0   0   error (2) 0 --- inspect .020 .020 5.6 0   0  
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900   900   150 10000 .82 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .69 .42 40 0   0   error (2) 0 --- inspect .020 .020 5.6 0   0  
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900   920   150 11000 .91 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .79 .49 40 0   0   error (2) 0 --- inspect .020 .020 5.6 0   0  
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c timeout 0 --- inspect 900   900   150 11000 .83 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .46 41 0   0   error (2) 0 --- inspect .021 .021 5.6 0   0  
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900   900   150 11000 .62 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .45 41 0   0   error (2) 0 --- inspect .020 .020 5.6 0   0  
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900   900   150 11000 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .44 40 0   0   error (2) 0 --- inspect .021 .021 5.6 0   0  
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900   900   200 12000 .61 46      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .45 42 0   0   error (2) 0 --- inspect .020 .020 5.6 0   0  
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900   920   150 12000 .84 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .70 .43 42 0   0   error (2) 0 --- inspect .024 .025 5.6 0   0  
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900   920   150 12000 .74 .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .44 42 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0  
recursive-simple/afterrec_2calls_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.6 2.4 200 36 .59 45      false(unreach-call) 1 wit inspect 3.7  2.0  250 0   0      true -32 --- inspect 7.1   4.5   310   .66 0      false(unreach-call) 1 --- inspect 3.5  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 3.3 2.2 160 36 .58 0      false(unreach-call) 1 wit inspect 3.5  2.0  250 0   0      true -32 --- inspect 7.3   4.7   310   .66 0      false(unreach-call) 1 --- inspect 3.4  2.0  250 0   0      false(unreach-call) 1 --- inspect .56   .57   20    .045 0      - --- inspect - --- inspect
recursive-simple/fibo_10_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.6 2.1 150 37 .60 0      false(unreach-call) 1 wit inspect 7.1  4.0  350 0   0      true -32 --- inspect 7.3   4.5   310   .62 0      false(unreach-call) 1 --- inspect 3.4  2.0  250 0   .094  false(unreach-call) 1 --- inspect .57   .57   20    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_15_false-unreach-call.c false(unreach-call) 1 wit inspect 3.6 2.3 150 35 .60 0      false(unreach-call) 1 wit inspect 21    14    1200 0   0      true -32 --- inspect 7.4   4.2   310   .62 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_20_false-unreach-call.c false(unreach-call) 1 wit inspect 3.5 2.1 150 34 .60 .0041 out of memory 0 --- inspect 44    33    7000 0   .029  true -32 --- inspect 7.0   4.5   310   .66 0      false(unreach-call) 1 --- inspect 3.4  2.0  240 0   0      false(unreach-call) 1 --- inspect .57   .57   20    .049 .0041 - --- inspect - --- inspect
recursive-simple/fibo_25_false-unreach-call.c false(unreach-call) 1 wit inspect 3.5 2.2 150 38 .60 0      timeout 0 --- inspect 97    63    3500 0   .016  true -32 --- inspect 6.9   4.4   310   .62 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_10_false-unreach-call.c false(unreach-call) 1 wit inspect 3.5 2.0 150 32 .62 0      false(unreach-call) 1 wit inspect 8.4  4.6  420 0   0      true -32 --- inspect 7.4   4.7   310   .66 0      false(unreach-call) 1 --- inspect 3.6  2.1  250 0   0      false(unreach-call) 1 --- inspect .58   .58   20    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_15_false-unreach-call.c false(unreach-call) 1 wit inspect 3.5 2.1 150 34 .62 0      false(unreach-call) 1 wit inspect 25    17    1200 0   0      true -32 --- inspect 7.8   4.9   310   .66 0      false(unreach-call) 1 --- inspect 3.5  2.1  250 0   0      false(unreach-call) 1 --- inspect .58   .58   20    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_20_false-unreach-call.c false(unreach-call) 1 wit inspect 3.5 2.0 150 35 .62 1.5    out of memory 0 --- inspect 48    36    7000 0   0      true -32 --- inspect 7.3   4.6   310   .66 0      false(unreach-call) 1 --- inspect 4.5  2.6  250 0   0      false(unreach-call) 1 --- inspect .57   .57   20    .049 .0041 - --- inspect - --- inspect
recursive-simple/fibo_2calls_25_false-unreach-call.c false(unreach-call) 1 wit inspect 3.6 2.1 150 35 .62 0      timeout 0 --- inspect 97    61    3600 0   0      true -32 --- inspect 7.7   4.4   310   .66 0      false(unreach-call) 1 --- inspect 3.5  2.0  250 0   0      false(unreach-call) 1 --- inspect .58   .58   20    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_2_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.4 2.1 150 39 .62 0      false(unreach-call) 1 wit inspect 3.7  2.0  250 0   0      true -32 --- inspect 7.1   4.5   310   .66 0      false(unreach-call) 1 --- inspect 3.6  2.1  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.7 2.1 150 36 .62 0      false(unreach-call) 1 wit inspect 4.8  2.6  270 0   .0082 true -32 --- inspect 7.3   4.6   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_5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.6 2.2 150 33 .62 0      false(unreach-call) 1 wit inspect 5.0  2.7  270 0   0      true -32 --- inspect 7.2   4.5   310   .66 0      false(unreach-call) 1 --- inspect 3.5  2.0  250 0   0      false(unreach-call) 1 --- inspect .68   .68   20    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_6_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.5 2.0 150 37 .62 .041  false(unreach-call) 1 wit inspect 5.5  3.0  270 0   0      true -32 --- inspect 7.7   4.3   310   .62 0      false(unreach-call) 1 --- inspect 3.6  2.1  250 0   0      false(unreach-call) 1 --- inspect .56   .57   20    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_8_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.4 2.3 200 36 .62 46      false(unreach-call) 1 wit inspect 6.5  3.5  300 0   0      true -32 --- inspect 7.6   4.3   310   .62 0      false(unreach-call) 1 --- inspect 3.6  2.1  250 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 3.4 2.0 150 33 .60 0      false(unreach-call) 1 wit inspect 4.7  2.6  270 0   0      true -32 --- inspect 8.5   4.8   320   .66 0      false(unreach-call) 1 --- inspect 3.5  2.1  250 0   0      false(unreach-call) 1 --- inspect .57   .57   20    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_7_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.4 2.2 150 35 .60 0      false(unreach-call) 1 wit inspect 4.9  2.7  280 0   .016  true -32 --- inspect 7.2   4.1   310   .66 0      false(unreach-call) 1 --- inspect 3.6  2.1  250 0   .0041 false(unreach-call) 1 --- inspect .59   .59   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 3.8 2.4 150 40 .68 0      false(unreach-call) 1 wit inspect 4.4  2.5  260 0   0      true -32 --- inspect 7.1   4.5   310   .66 0      false(unreach-call) 1 --- inspect 3.6  2.1  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.6 2.2 150 36 .59 0      false(unreach-call) 1 wit inspect 4.5  2.5  260 0   0      true -32 --- inspect 6.7   4.3   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/id_b3_o2_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 3.6 2.4 150 41 .68 0      false(unreach-call) 1 wit inspect 4.3  2.3  260 0   .029  true -32 --- inspect 6.8   3.9   300   .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/id_i10_o10_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.5 2.1 150 34 .58 0      false(unreach-call) 1 wit inspect 4.7  2.6  270 0   0      true -32 --- inspect 6.9   4.4   310   .66 0      false(unreach-call) 1 --- inspect 3.7  2.1  250 0   0      false(unreach-call) 1 --- inspect .56   .56   20    .045 0      - --- inspect - --- inspect
recursive-simple/id_i15_o15_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.5 2.0 150 35 .58 0      false(unreach-call) 1 wit inspect 4.9  2.7  270 0   0      true -32 --- inspect 7.5   4.3   310   .66 0      false(unreach-call) 1 --- inspect 3.4  2.0  240 0   0      false(unreach-call) 1 --- inspect .59   .59   20    .045 0      - --- inspect - --- inspect
recursive-simple/id_i20_o20_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.5 2.2 150 32 .58 0      false(unreach-call) 1 wit inspect 5.1  2.8  270 0   .45   true -32 --- inspect 7.0   4.0   320   .66 0      false(unreach-call) 1 --- inspect 3.5  2.0  250 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 3.5 2.2 150 34 .58 0      false(unreach-call) 1 wit inspect 5.7  3.1  270 0   0      true -32 --- inspect 7.2   4.5   310   .66 0      false(unreach-call) 1 --- inspect 3.3  1.9  240 0   0      false(unreach-call) 1 --- inspect .59   .59   20    .045 0      - --- inspect - --- inspect
recursive-simple/id_i5_o5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.3 2.0 150 38 .58 0      false(unreach-call) 1 wit inspect 4.5  2.5  260 0   0      true -32 --- inspect 7.2   4.5   310   .62 0      false(unreach-call) 1 --- inspect 3.3  2.0  250 0   0      false(unreach-call) 1 --- inspect .56   .57   20    .045 .0041 - --- inspect - --- inspect
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 600   600   150 7900 .69 0      timeout 0 --- inspect 93    72    2400 0   0      true -32 --- inspect 7.3   4.6   310   .62 0      false(unreach-call) 1 --- inspect 3.5  2.1  240 0   .0041 false(unreach-call) 1 --- inspect .58   .58   20    .049 0      - --- inspect - --- inspect
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 590   590   150 6800 .69 0      false(unreach-call) 1 wit inspect 8.6  4.5  450 0   0      true -32 --- inspect 7.5   4.3   320   .62 0      false(unreach-call) 1 --- inspect 3.3  2.0  250 0   0      false(unreach-call) 1 --- inspect .58   .58   20    .049 0      - --- inspect - --- inspect
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 54   52   150 610 .66 0      false(unreach-call) 1 wit inspect 4.6  2.5  270 0   0      true -32 --- inspect 6.9   4.4   300   .66 0      false(unreach-call) 1 --- inspect 3.4  2.0  250 0   0      false(unreach-call) 1 --- 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   900   150 9300 .60 0      error (invalid witness file) 0 --- inspect .60 .36 42 0   0      error (2) 0 --- inspect .020 .021 5.6 0    0      error (invalid witness file) 0 --- inspect .97 .62 49 0   0      error (invalid witness file) 0 --- inspect .0046 .0060 .54 0     0      - --- inspect - --- inspect
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 53   52   150 740 .66 0      false(unreach-call) 1 wit inspect 5.4  3.0  270 0   .12   true -32 --- inspect 7.4   4.1   310   .66 .0041 false(unreach-call) 1 --- inspect 3.5  2.0  250 0   .0041 false(unreach-call) 1 --- 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 18   17   150 190 .66 0      false(unreach-call) 1 wit inspect 4.1  2.2  260 0   0      true -32 --- inspect 7.6   4.7   310   .62 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/sum_10x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.5 2.2 150 35 .58 0      false(unreach-call) 1 wit inspect 5.9  3.2  270 0   0      true -32 --- inspect 7.6   4.3   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_15x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.3 2.1 150 38 .58 0      false(unreach-call) 1 wit inspect 5.8  3.2  270 0   0      true -32 --- inspect 6.8   4.3   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_20x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.4 2.0 150 35 .58 .029  false(unreach-call) 1 wit inspect 5.0  2.8  280 0   .016  true -32 --- inspect 7.3   4.6   310   .66 0      false(unreach-call) 1 --- inspect 3.4  2.0  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 3.4 2.2 150 34 .58 0      false(unreach-call) 1 wit inspect 5.6  3.0  280 0   .029  true -32 --- inspect 7.4   4.2   310   .66 0      false(unreach-call) 1 --- inspect 3.4  2.0  250 0   0      false(unreach-call) 1 --- inspect .56   .56   20    .045 0      - --- inspect - --- inspect
recursive-simple/sum_2x3_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.6 2.0 150 35 .58 0      false(unreach-call) 1 wit inspect 4.2  2.3  260 0   0      true -32 --- inspect 7.4   4.6   310   .62 0      false(unreach-call) 1 --- inspect 3.6  2.1  250 0   0      false(unreach-call) 1 --- inspect .57   .57   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.4 2.1 150 36 .59 .12   false(unreach-call) 1 wit inspect 3.9  2.1  260 0   0      false(unreach-call) 1 --- inspect 6.4   4.1   310   .66 0      false(unreach-call) 1 --- inspect 3.6  2.1  250 0   .13   false(unreach-call) 1 --- inspect .59   .60   20    .049 .0041 - --- inspect - --- inspect
recursive-simple/afterrec_2calls_true-unreach-call_true-termination.c timeout 0 --- inspect 900   920   150 8900 .76 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 40 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0  
recursive-simple/afterrec_true-unreach-call_true-termination.c timeout 0 --- inspect 900   920   150 12000 .80 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .45 41 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0  
recursive-simple/fibo_10_true-unreach-call_true-termination.c timeout 0 --- inspect 900   920   150 13000 .82 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .47 41 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0  
recursive-simple/fibo_15_true-unreach-call.c timeout 0 --- inspect 900   920   150 12000 .71 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .44 41 0   0   error (2) 0 --- inspect .020 .020 5.6 0   0  
recursive-simple/fibo_20_true-unreach-call.c timeout 0 --- inspect 900   910   150 14000 .55 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .45 40 0   0   error (2) 0 --- inspect .019 .020 5.6 0   0  
recursive-simple/fibo_25_true-unreach-call.c timeout 0 --- inspect 900   900   150 12000 .53 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .67 .39 42 0   0   error (2) 0 --- inspect .020 .020 5.6 0   0  
recursive-simple/fibo_2calls_10_true-unreach-call.c timeout 0 --- inspect 900   920   150 11000 .83 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .69 .44 40 0   0   error (2) 0 --- inspect .020 .021 5.7 0   0  
recursive-simple/fibo_2calls_15_true-unreach-call.c timeout 0 --- inspect 900   920   150 11000 .82 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .45 43 0   0   error (2) 0 --- inspect .020 .020 5.6 0   0  
recursive-simple/fibo_2calls_20_true-unreach-call.c timeout 0 --- inspect 900   910   150 12000 .54 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .82 .51 41 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0  
recursive-simple/fibo_2calls_25_true-unreach-call.c timeout 0 --- inspect 900   900   150 12000 .59 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .47 40 0   0   error (2) 0 --- inspect .019 .020 5.6 0   0  
recursive-simple/fibo_2calls_2_true-unreach-call_true-termination.c timeout 0 --- inspect 900   920   150 12000 .65 .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .44 43 0   0   error (2) 0 --- inspect .020 .020 5.6 0   0  
recursive-simple/fibo_2calls_4_true-unreach-call_true-termination.c timeout 0 --- inspect 900   920   150 13000 .62 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .43 41 0   0   error (2) 0 --- inspect .020 .020 5.6 0   0  
recursive-simple/fibo_2calls_5_true-unreach-call_true-termination.c timeout 0 --- inspect 900   920   150 12000 .61 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .46 40 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   920   150 11000 .79 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 41 0   0   error (2) 0 --- inspect .020 .020 5.6 0   0  
recursive-simple/fibo_2calls_8_true-unreach-call_true-termination.c timeout 0 --- inspect 900   920   150 13000 .61 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .46 40 0   0   error (2) 0 --- inspect .019 .020 5.6 0   0  
recursive-simple/fibo_5_true-unreach-call_true-termination.c timeout 0 --- inspect 900   920   150 12000 .86 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .44 40 0   0   error (2) 0 --- inspect .020 .020 5.6 0   0  
recursive-simple/fibo_7_true-unreach-call_true-termination.c timeout 0 --- inspect 900   920   150 13000 .79 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .36 40 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0  
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c timeout 0 --- inspect 900   900   150 12000 .74 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .46 41 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0  
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c timeout 0 --- inspect 900   900   200 12000 .93 44      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .70 .43 41 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0  
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c timeout 0 --- inspect 900   900   150 11000 1.0  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .45 43 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   920   150 12000 .82 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .45 40 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0  
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c timeout 0 --- inspect 900   900   150 11000 1.7  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .70 .42 42 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0  
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c timeout 0 --- inspect 900   900   150 11000 1.0  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .46 42 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0  
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c timeout 0 --- inspect 900   900   150 12000 .80 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .44 42 0   0   error (2) 0 --- inspect .020 .020 5.6 0   0  
recursive-simple/id_i10_o10_true-unreach-call_true-termination.c timeout 0 --- inspect 900   920   150 11000 .76 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .43 41 0   0   error (2) 0 --- inspect .019 .020 5.6 0   0  
recursive-simple/id_i15_o15_true-unreach-call_true-termination.c timeout 0 --- inspect 900   920   150 11000 .73 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .69 .42 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   920   150 13000 .82 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .68 .41 41 0   0   error (2) 0 --- inspect .020 .021 5.7 0   0  
recursive-simple/id_i25_o25_true-unreach-call_true-termination.c timeout 0 --- inspect 900   920   150 11000 .83 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .45 40 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0  
recursive-simple/id_i5_o5_true-unreach-call_true-termination.c timeout 0 --- inspect 900   920   150 12000 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .70 .43 41 0   0   error (2) 0 --- inspect .020 .020 5.6 0   0  
recursive-simple/sum_10x0_true-unreach-call_true-termination.c timeout 0 --- inspect 900   920   150 11000 .82 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .36 41 0   0   error (2) 0 --- inspect .020 .020 5.6 0   0  
recursive-simple/sum_15x0_true-unreach-call_true-termination.c timeout 0 --- inspect 900   920   150 11000 .79 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .36 41 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   920   150 11000 .71 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .44 42 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0  
recursive-simple/sum_25x0_true-unreach-call_true-termination.c timeout 0 --- inspect 900   920   150 12000 .83 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .47 42 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   920   150 11000 .88 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .47 41 0   0   error (2) 0 --- inspect .020 .020 5.6 0   0  
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c timeout 0 --- inspect 900   900   150 9400 .60 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .81 .49 40 0   0   error (2) 0 --- inspect .020 .021 5.6 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 43 49000 50000 15000 630000 67 230 44 38 640 420 36000 0   .89 44 -1277 310 190 13000 28   .0041 44 43 150 89 11000 0   .24 44 43 25 25 870 2.1 .025 52 0 37 23 2100 0   0   52 0 1.0 1.1 290 0   0  
    correct results 43 43 1500 1500 6600 18000 27 93 38 38 260 150 13000 0   .84 3 3 20 12 910 2.0 0      43 43 150 88 11000 0   .24 43 43 25 25 870 2.1 .025 0 0
        correct true 0 0 0 0 0 0 0
        correct false 43 43 1500 1500 6600 18000 27 93 38 38 260 150 13000 0   .84 3 3 20 12 910 2.0 0      43 43 150 88 11000 0   .24 43 43 25 25 870 2.1 .025 0 0
    incorrect results 0 0 40 -1280 290 180 12000 26   .0041 0 0 0 0
        incorrect true 0 0 40 -1280 290 180 12000 26   .0041 0 0 0 0
        incorrect false 0 0 0 0 0 0 0
score (96 tasks, max score: 148) 43 38 -1277 43 43 0 0
Run set verifuzz.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-seq-validate-violation-witnesses-verifuzz.sv-comp19_prop-reachsafety.ReachSafety-Recursive uautomizer-validate-violation-witnesses-verifuzz.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-witness2test-validate-violation-witnesses-verifuzz.sv-comp19_prop-reachsafety.ReachSafety-Recursive fshell-witness2test-validate-violation-witnesses-verifuzz.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-seq-validate-correctness-witnesses-verifuzz.sv-comp19_prop-reachsafety.ReachSafety-Recursive uautomizer-validate-correctness-witnesses-verifuzz.sv-comp19_prop-reachsafety.ReachSafety-Recursive