Tool PeSCo 1.7-svn b8d6131600+ CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a CPA-witness2test 1.7-svn 29852 CProver witness2test 0.1 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* [apollon004; apollon069; apollon137; apollon154] [apollon004; apollon006; apollon021; apollon061; apollon109; apollon155] apollon*
OS Linux 4.15.0-42-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33546 MB
Date of execution 2018-12-06 12:44:04 CET 2018-12-08 07:39:30 CET 2018-12-08 12:16:42 CET 2018-12-08 13:32:07 CET 2018-12-12 20:37:42 CET 2018-12-08 09:11:31 CET
Run set pesco.sv-comp19_prop-memsafety.MemSafety-LinkedLists cpa-seq-validate-violation-witnesses-pesco.sv-comp19_prop-memsafety.MemSafety-LinkedLists uautomizer-validate-violation-witnesses-pesco.sv-comp19_prop-memsafety.MemSafety-LinkedLists cpa-witness2test-validate-violation-witnesses-pesco.sv-comp19_prop-memsafety.MemSafety-LinkedLists fshell-witness2test-validate-violation-witnesses-pesco.sv-comp19_prop-memsafety.MemSafety-LinkedLists uautomizer-validate-correctness-witnesses-pesco.sv-comp19_prop-memsafety.MemSafety-LinkedLists
Options -svcomp19-pesco -heap 10000M -stack 2048k -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/pesco.2018-12-06_1244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/pesco.2018-12-06_1244.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/pesco.2018-12-06_1244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/pesco.2018-12-06_1244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/pesco.2018-12-06_1244.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)
heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   750   4600 10000 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   910   1100 .70 0    
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i error (recursion) 0 wit inspect 4.3 1.5 290 40 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   920   930 .77 .029
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 910   260   11000 6300 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   860   2800 .69 0    
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   580   5000 7600 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   930   1800 .64 0    
heap-manipulation/tree_false-unreach-call_false-valid-deref.i timeout 0 wit inspect 970   270   11000 6000 0   0   error (invalid witness file) 0 --- inspect .65 .41 43 0   0   error (invalid witness file) 0 --- inspect 5.6 3.1 270 .61 0   error (invalid witness file) 0 --- inspect .99 .66 49 0   0      error (invalid witness file) 0 --- inspect .0018 .0022 .53 0     0     - --- inspect
heap-manipulation/tree_false-valid-deref.i timeout 0 wit inspect 910   340   11000 7000 0   0   error (1) 0 --- inspect .72 .43 47 0   0   false(valid-deref) 1 --- inspect 10   5.6 320 .66 0   unknown 0 --- inspect 1.1  .66 50 0   0      error (1) 0 --- inspect .071  .072  11    0     0     - --- inspect
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i timeout (exception) 0 wit inspect 920   240   11000 5900 0   0   error (1) 0 --- inspect .72 .44 46 0   0   timeout 0 --- inspect 97   78   680 1.4  0   unknown 0 --- inspect 1.0  .66 52 0   0      error (1) 0 --- inspect .074  .075  12    0     0     - --- inspect
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 930   280   11000 5600 0   0   error (1) 0 --- inspect .72 .46 46 0   0   unknown 0 --- inspect 83   57   750 .68 0   unknown 0 --- inspect 1.3  .81 49 0   0      error (1) 0 --- inspect .076  .076  11    0     0     - --- inspect
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 930   330   11000 6300 0   0   error (1) 0 --- inspect .70 .44 44 0   0   timeout 0 --- inspect 97   66   860 .87 0   unknown 0 --- inspect .99 .64 49 0   0      error (1) 0 --- inspect .078  .077  11    0     0     - --- inspect
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 920   350   11000 7100 0   0   error (1) 0 --- inspect .83 .50 44 0   0   timeout 0 --- inspect 97   70   980 1.7  0   unknown 0 --- inspect 1.0  .68 51 0   0      error (1) 0 --- inspect .071  .070  11    0     0     - --- inspect
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   280   11000 6600 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   870   1300 .63 0    
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i timeout (exception) 0 wit inspect 910   290   11000 5600 0   0   error (1) 0 --- inspect .79 .49 44 0   0   unknown 0 --- inspect 22   13   350 .68 0   unknown 0 --- inspect 1.2  .79 51 0   0      error (1) 0 --- inspect .067  .067  11    0     0     - --- inspect
list-properties/list_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 910   320   11000 7100 0   0   error (1) 0 --- inspect .88 .54 45 0   0   unknown 0 --- inspect 33   20   520 .71 0   unknown 0 --- inspect 1.0  .66 50 0   0      error (1) 0 --- inspect .081  .080  11    0     0     - --- inspect
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 910   320   11000 6100 0   0   error (1) 0 --- inspect .71 .44 45 0   0   unknown 0 --- inspect 22   12   390 .71 0   unknown 0 --- inspect 1.0  .63 49 0   0      error (1) 0 --- inspect .072  .072  11    0     0     - --- inspect
list-properties/simple_true-unreach-call_false-valid-memtrack.i timeout (exception) 0 wit inspect 920   330   11000 6400 0   0   error (1) 0 --- inspect .84 .52 44 0   0   unknown 0 --- inspect 26   15   490 .71 0   unknown 0 --- inspect 1.1  .72 50 0   0      error (1) 0 --- inspect .073  .073  11    0     0     - --- inspect
list-properties/splice_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 910   280   11000 7000 0   0   error (1) 0 --- inspect .78 .48 45 0   0   unknown 0 --- inspect 23   14   350 .68 0   unknown 0 --- inspect 1.1  .67 52 0   0      error (1) 0 --- inspect .068  .068  11    0     0     - --- inspect
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i true 2 wit inspect 6.8 2.0 310 60 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (7) 0 --- inspect 40   21   540 .75 0    
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i true 2 wit inspect 6.7 2.0 300 58 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (7) 0 --- inspect 32   18   520 .75 0    
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i true 2 wit inspect 6.4 2.0 290 56 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (7) 0 --- inspect 32   18   520 .75 0    
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 6.5 2.1 290 57 0   0   false(valid-memtrack) 1 wit inspect 9.3  4.9  310 0   0   error (7) 0 --- inspect 39   21   520 .71 0   unknown 0 --- inspect 7.5  4.2  280 0   0      error (2) 0 --- inspect 1.0    1.0    21    .13  0     - --- inspect
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 7.0 2.1 300 57 0   0   false(valid-memtrack) 1 wit inspect 9.8  5.1  310 0   0   error (7) 0 --- inspect 31   18   530 .71 0   unknown 0 --- inspect 7.6  4.3  290 0   .053  error (2) 0 --- inspect 1.0    1.0    21    .13  .086 - --- inspect
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 6.8 2.1 300 65 0   0   false(valid-memtrack) 1 wit inspect 7.8  4.1  310 0   0   error (7) 0 --- inspect 31   18   530 .68 0   unknown 0 --- inspect 7.9  4.5  290 0   0      error (2) 0 --- inspect 1.0    1.0    21    .13  0     - --- inspect
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 7.3 2.2 310 57 0   0   false(valid-memtrack) 1 wit inspect 8.0  4.2  310 0   0   error (7) 0 --- inspect 32   18   530 .71 0   unknown 0 --- inspect 7.5  4.2  280 0   0      error (2) 0 --- inspect 1.1    1.0    21    .13  0     - --- inspect
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 6.7 2.0 300 54 0   0   false(valid-memtrack) 1 wit inspect 8.4  4.5  310 0   0   error (7) 0 --- inspect 31   18   540 .68 0   unknown 0 --- inspect 7.6  4.3  280 0   0      error (2) 0 --- inspect 1.0    1.0    21    .13  0     - --- inspect
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 6.8 2.1 300 57 0   0   false(valid-memtrack) 1 wit inspect 8.9  4.7  310 0   0   error (7) 0 --- inspect 33   18   520 .68 0   unknown 0 --- inspect 7.7  4.3  290 0   .0041 error (2) 0 --- inspect 1.0    1.0    21    .13  0     - --- inspect
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 7.0 2.1 300 56 0   0   false(valid-memtrack) 1 wit inspect 8.4  4.4  310 0   0   error (7) 0 --- inspect 31   18   530 .75 0   unknown 0 --- inspect 7.2  4.0  280 0   0      error (2) 0 --- inspect 1.0    1.0    21    .13  0     - --- inspect
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 6.7 2.1 300 60 0   0   false(valid-memtrack) 1 wit inspect 8.1  4.3  310 0   0   error (7) 0 --- inspect 32   18   520 .68 0   unknown 0 --- inspect 7.8  4.4  290 0   0      error (2) 0 --- inspect 1.0    1.0    21    .13  0     - --- inspect
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 6.7 2.1 300 59 0   0   false(valid-memtrack) 1 wit inspect 8.4  4.4  310 0   0   error (7) 0 --- inspect 34   19   530 .68 0   unknown 0 --- inspect 7.6  4.3  280 0   0      error (2) 0 --- inspect 1.0    1.0    21    .13  0     - --- inspect
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 7.1 2.1 310 64 0   0   false(valid-memtrack) 1 wit inspect 8.6  4.5  310 0   0   error (7) 0 --- inspect 33   19   530 .68 0   unknown 0 --- inspect 7.9  4.4  300 0   0      error (2) 0 --- inspect 1.0    1.0    21    .13  0     - --- inspect
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 970   270   11000 7000 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect 5.4 3.3 270 .65 0    
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 920   360   9300 4700 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   920   890 .63 0    
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 930   350   11000 6900 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   880   2300 1.6  0    
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 960   230   11000 5700 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect 5.1 2.8 260 .65 0    
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i timeout (exception) 0 wit inspect 970   280   11000 5500 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect 5.5 3.0 270 .65 0    
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 970   280   11000 6300 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect 5.5 3.5 270 .66 0    
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 910   330   11000 6200 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   900   1400 .65 0    
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   340   11000 6200 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   870   1900 1.6  0    
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 960   290   11000 6200 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect 5.4 2.9 260 .65 0    
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i timeout (exception) 0 wit inspect 900   270   11000 6300 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   900   1600 .65 0    
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 920   360   11000 4900 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   870   2300 .70 0    
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   360   9300 5000 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   840   1200 .63 0    
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i timeout (exception) 0 wit inspect 900   360   11000 7500 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   870   2300 .69 0    
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 960   230   11000 5500 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect 5.4 3.3 270 .65 0    
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i timeout (exception) 0 wit inspect 910   400   11000 7500 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   860   1200 .65 0    
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 910   400   12000 6900 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   870   2100 .70 0    
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 940   360   11000 6400 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   860   2300 .71 0    
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i timeout (exception) 0 wit inspect 920   350   11000 6400 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   820   2200 .71 0    
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 920   300   11000 5700 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   900   2400 1.4  0    
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i timeout (exception) 0 wit inspect 910   380   11000 6600 0   0   error (1) 0 --- inspect .75 .46 44 0   0   false(valid-deref) 1 --- inspect 87   60   910 .62 0   unknown 0 --- inspect 1.0  .66 49 0   0      error (1) 0 --- inspect .067  .066  11    0     0     - --- inspect
forester-heap/sll-01_false-unreach-call_false-valid-deref.i timeout 0 wit inspect 970   280   11000 6500 0   0   error (invalid witness file) 0 --- inspect .65 .39 42 0   0   error (invalid witness file) 0 --- inspect 5.8 3.5 270 .61 0   error (invalid witness file) 0 --- inspect 1.2  .76 50 0   0      error (invalid witness file) 0 --- inspect .0049 .0064 .53 0     0     - --- inspect
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i timeout 0 wit inspect 910   390   11000 8100 0   0   error (1) 0 --- inspect .70 .44 45 0   0   false(valid-deref) 1 --- inspect 61   42   750 .62 0   unknown 0 --- inspect .99 .63 49 0   0      error (1) 0 --- inspect .078  .078  11    0     0     - --- inspect
list-simple/dll2c_append_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.4 1.5 290 38 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   920   950 .66 0    
list-simple/dll2c_append_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.2 1.5 280 36 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   930   970 .64 0    
list-simple/dll2c_insert_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.4 1.6 290 39 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   930   920 .65 0    
list-simple/dll2c_insert_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.3 1.5 280 38 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   930   950 .65 0    
list-simple/dll2c_prepend_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.4 1.6 280 38 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   910   1100 .69 0    
list-simple/dll2c_prepend_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.3 1.5 280 44 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   930   1100 .64 0    
list-simple/dll2c_remove_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.1 1.5 280 36 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   920   1400 .65 0    
list-simple/dll2c_remove_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.1 1.5 280 41 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   900   1100 .71 0    
list-simple/dll2c_update_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.2 1.5 280 37 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 310   280   1200 .62 0    
list-simple/dll2c_update_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.3 1.6 280 32 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 340   310   1100 .62 0    
list-simple/dll2n_append_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.3 1.5 290 37 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   920   1700 .70 0    
list-simple/dll2n_append_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.2 1.5 280 37 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   930   1800 1.6  0    
list-simple/dll2n_insert_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.3 1.5 290 34 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   940   1100 .67 0    
list-simple/dll2n_insert_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.3 1.5 280 34 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   930   1500 .64 0    
list-simple/dll2n_prepend_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.1 1.4 260 35 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   930   870 .82 0    
list-simple/dll2n_prepend_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.2 1.5 280 35 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   930   910 1.8  0    
list-simple/dll2n_remove_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.1 1.5 280 33 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   920   1200 1.5  0    
list-simple/dll2n_remove_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.1 1.4 280 35 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 160   140   1000 .62 0    
list-simple/dll2n_update_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.2 1.5 280 41 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   910   1400 1.6  0    
list-simple/dll2n_update_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.4 1.5 280 40 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   920   1400 .68 0    
list-simple/sll2c_append_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.3 1.5 280 35 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   920   1100 .63 0    
list-simple/sll2c_append_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.3 1.6 280 41 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   930   1400 .79 0    
list-simple/sll2c_insert_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.3 1.5 280 35 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   930   1300 .62 0    
list-simple/sll2c_insert_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.4 1.5 280 40 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   930   1100 .64 0    
list-simple/sll2c_prepend_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.3 1.5 280 40 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   930   1000 .75 0    
list-simple/sll2c_prepend_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.3 1.5 290 38 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   930   1400 .74 0    
list-simple/sll2c_remove_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.1 1.5 280 39 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   890   720 .71 0    
list-simple/sll2c_remove_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.0 1.4 280 37 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 390   350   700 .62 0    
list-simple/sll2c_update_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.1 1.5 290 41 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   910   960 .71 0    
list-simple/sll2c_update_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.2 1.5 280 30 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   910   930 .71 0    
list-simple/sll2n_append_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.1 1.5 280 38 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (7) 0 --- inspect 660   640   2300 .71 .39 
list-simple/sll2n_append_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.2 1.4 290 35 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   940   1700 .75 0    
list-simple/sll2n_insert_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.4 1.5 290 38 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   940   980 .73 0    
list-simple/sll2n_insert_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.3 1.5 290 41 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   930   990 1.7  0    
list-simple/sll2n_prepend_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.2 1.5 280 37 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   940   810 1.6  0    
list-simple/sll2n_prepend_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.3 1.5 280 41 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   940   840 .78 0    
list-simple/sll2n_remove_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.1 1.4 280 33 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   910   1100 .72 0    
list-simple/sll2n_remove_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.2 1.5 270 37 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 360   330   740 .62 0    
list-simple/sll2n_update_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.3 1.5 280 34 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 500   470   960 .62 0    
list-simple/sll2n_update_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.2 1.5 260 40 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 610   580   790 .62 0    
list-ext3-properties/dll_circular_traversal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.2 1.5 280 39 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   920   2500 .63 0    
list-ext3-properties/dll_nondet_free_order_true-valid-memsafety.i true 2 wit inspect 4.2 1.4 290 36 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   940   1800 1.4  0    
list-ext3-properties/dll_nullified_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.0 1.5 270 36 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   880   2100 .69 0    
list-ext3-properties/sll_circular_traversal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.5 1.5 280 34 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   930   1300 .75 0    
list-ext3-properties/sll_length_check_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 18   4.8 980 130 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   890   2400 1.4  0    
list-ext3-properties/sll_nondet_insert_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 270   140   5800 2400 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   920   1100 1.6  0    
list-ext3-properties/sll_of_sll_nondet_append_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 920   430   7200 5100 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   940   630 .70 0    
list-ext3-properties/sll_shallow_copy_true-valid-memsafety.i true 2 wit inspect 3.8 1.4 280 33 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 17   11   470 .66 0    
list-ext3-properties/dll_circular_traversal_false-valid-deref.i false(valid-deref) 1 wit inspect 4.8 1.6 280 40 0   0   false(valid-deref) 1 wit inspect 6.5  3.5  280 0   0   timeout 0 --- inspect 97   86   2600 1.6  0   unknown 0 --- inspect 5.9  3.3  270 0   0      false(valid-deref) 1 --- inspect .71   .71   21    .082 0     - --- inspect
list-ext3-properties/sll_circular_traversal_false-valid-deref.i false(valid-deref) 1 wit inspect 4.6 1.6 270 38 0   0   false(valid-deref) 1 wit inspect 7.6  4.1  260 0   0   out of memory 0 --- inspect 80   54   7000 .71 0   unknown 0 --- inspect 5.9  3.3  270 0   0      false(valid-deref) 1 --- inspect .70   .70   21    .082 0     - --- inspect
list-ext3-properties/dll_nondet_free_order_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 4.4 1.6 280 40 0   0   false(valid-memtrack) 1 wit inspect 4.9  2.7  260 0   0   unknown 0 --- inspect 20   12   360 .68 0   unknown 0 --- inspect 5.0  2.9  260 0   0      false(valid-deref) -16 --- inspect .67   .67   21    .086 0     - --- inspect
list-ext3-properties/sll_shallow_copy_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 3.8 1.4 280 34 0   0   false(valid-memtrack) 1 wit inspect 4.7  2.6  250 0   0   true -32 --- inspect 13   8.0 460 .66 0   unknown 0 --- inspect 4.6  2.6  270 0   0      true -32 --- inspect .64   .64   20    .070 0     - --- inspect
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)
total 103 114 36000 13000 430000 250000 0   0   28 14 120 64 4800 0   0   28 -29 1200 800   24000 22    0   28 0 110 65 4600 0   .057 28 -46 14    14    430 1.6   .086 75 16 58000 55000 93000 62   .42
    correct results 64 114 580 240 24000 5100 0   0   14 14 110 58 4200 0   0   3 3 160 110   2000 1.9  0   0 2 2 1.4  1.4  42 .16  0     8 16 2700 2500 7000 5.0 0   
        correct true 50 100 490 210 20000 4300 0   0   0 0 0 0 8 16 2700 2500 7000 5.0 0   
        correct false 14 14 86 27 4100 740 0   0   14 14 110 58 4200 0   0   3 3 160 110   2000 1.9  0   0 2 2 1.4  1.4  42 .16  0     0
    incorrect results 0 0 1 -32 13 8.0 460 .66 0   0 2 -48 1.3  1.3  41 .16  0     0
        incorrect true 0 0 1 -32 13 8.0 460 .66 0   0 1 -32 .64 .64 20 .070 0     0
        incorrect false 0 0 0 0 1 -16 .67 .67 21 .086 0     0
score (103 tasks, max score: 178) 114 14 -29 0 -46 16
Run set pesco.sv-comp19_prop-memsafety.MemSafety-LinkedLists cpa-seq-validate-violation-witnesses-pesco.sv-comp19_prop-memsafety.MemSafety-LinkedLists uautomizer-validate-violation-witnesses-pesco.sv-comp19_prop-memsafety.MemSafety-LinkedLists cpa-witness2test-validate-violation-witnesses-pesco.sv-comp19_prop-memsafety.MemSafety-LinkedLists fshell-witness2test-validate-violation-witnesses-pesco.sv-comp19_prop-memsafety.MemSafety-LinkedLists uautomizer-validate-correctness-witnesses-pesco.sv-comp19_prop-memsafety.MemSafety-LinkedLists