Tool symbiotic 5.0.0-KLEE:1faddfe0-dg:12c34aac-symbiotic:5e14b94d-minisat:3db58943-llvm-instrumentation:cd767593-stp:17249213 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741 CPA-witness2test 1.6.1-svn 26773 CProver witness2test 0.1 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741
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* [apollon005; apollon043; apollon077; apollon078; apollon087; apollon118] [apollon061; apollon077; apollon078; apollon086; apollon134] [apollon038; apollon077; apollon078; apollon083] [apollon077; apollon078; apollon161] apollon*
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [4; 8], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33554 MB; 33553 MB] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB]
Date of execution 2017-12-01 22:41:19 CET 2017-12-02 21:10:50 CET 2017-12-02 22:39:24 CET 2017-12-02 22:51:52 CET 2017-12-02 23:01:21 CET 2017-12-02 19:44:15 CET 2017-12-02 21:36:25 CET
Run set symbiotic.sv-comp18.ReachSafety-Loops cpa-seq-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.ReachSafety-Loops uautomizer-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.ReachSafety-Loops cpa-witness2test-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.ReachSafety-Loops fshell-witness2test-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.ReachSafety-Loops cpa-seq-validate-correctness-witnesses-symbiotic.sv-comp18-correctness-witness.ReachSafety-Loops uautomizer-validate-correctness-witnesses-symbiotic.sv-comp18-correctness-witness.ReachSafety-Loops
Options --witness witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/symbiotic.2017-12-01_2241.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -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 --full-output --validate ../../results-verified/symbiotic.2017-12-01_2241.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/symbiotic.2017-12-01_2241.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true --graphml-witness ../../results-verified/symbiotic.2017-12-01_2241.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/symbiotic.2017-12-01_2241.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/symbiotic.2017-12-01_2241.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
loops/array_false-unreach-call_true-termination.i 1 .19 12 1.8 1 3.2  270 -32 4.9   250   0 2.0  210 1 .57   18    - -
loops/bubble_sort_false-unreach-call.i 1 .26 12 2.7 0 4.7  270 0 5.5   210   0 3.7  220 1 .69   18    - -
loops/count_up_down_false-unreach-call_true-termination.i 1 .16 11 1.9 1 4.2  260 1 3.6   250   0 2.8  190 1 .58   18    - -
loops/eureka_01_false-unreach-call_true-termination.i 0 .97 15 13   0 92    1000 -32 4.9   230   0 2.0  210 -32 .57   18    - -
loops/for_bounded_loop1_false-unreach-call_true-termination.i 1 .16 11 1.6 1 4.2  260 -32 4.0   250   0 2.0  210 -32 .58   18    - -
loops/insertion_sort_false-unreach-call_true-termination.i 0 .19 11 1.9 0 .41 43 0 .026 4.8 0 .64 49 0 .0012 .30 - -
loops/invert_string_false-unreach-call_true-termination.i 0 .22 12 2.2 0 .56 43 0 .019 4.9 0 .65 49 0 .0013 .26 - -
loops/linear_search_false-unreach-call.i 0 .19 12 2.3 0 .52 41 0 .019 4.9 0 .88 50 0 .0011 .26 - -
loops/ludcmp_false-unreach-call.i 1 .16 11 1.7 1 7.0  520 0 97     4500   0 2.1  210 1 .60   18    - -
loops/matrix_false-unreach-call_true-termination.i 0 900    1700 9700   0 .39 43 0 .020 4.8 0 .90 49 0 .0010 .29 - -
loops/n.c24_false-unreach-call.i 0 900    1800 11000   0 .40 43 0 .018 4.9 0 .65 51 0 .0035 .26 - -
loops/nec11_false-unreach-call_false-termination.i 0 .12 11 1.0 0 .72 44 0 .018 4.9 0 .66 51 0 .0037 .26 - -
loops/nec20_false-unreach-call_true-termination.i 1 .17 11 2.4 1 4.4  260 -32 4.5   230   0 2.8  210 0 .60   18    - -
loops/s3_false-unreach-call.i 0 .47 12 4.6 0 .55 43 0 .019 4.9 0 .89 49 0 .0036 .29 - -
loops/string_false-unreach-call_true-termination.i 1 .20 12 2.4 1 4.2  270 -32 3.3   220   0 2.9  210 -32 .63   18    - -
loops/sum01_bug02_false-unreach-call_true-termination.i 1 .20 11 1.9 1 5.6  270 -32 3.9   270   0 2.8  210 -32 .60   18    - -
loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i 1 .17 11 2.3 1 3.9  260 -32 3.4   270   0 2.0  210 -32 .57   18    - -
loops/sum01_false-unreach-call_true-termination.i 1 .19 11 2.0 1 6.8  290 -32 5.4   260   0 1.9  210 -32 .57   18    - -
loops/sum03_false-unreach-call_true-termination.i 1 .17 11 1.8 1 4.6  270 -32 4.6   230   0 2.0  210 1 .58   18    - -
loops/sum04_false-unreach-call_true-termination.i 1 .16 11 1.7 1 3.1  260 -32 3.4   250   0 1.9  210 1 .56   18    - -
loops/sum_array_false-unreach-call.i 0 .21 12 2.0 0 .40 41 0 .018 4.8 0 .87 49 0 .0012 .34 - -
loops/terminator_01_false-unreach-call_true-termination.i 1 .16 11 1.4 1 3.3  260 -32 4.5   230   0 1.9  180 1 .57   18    - -
loops/terminator_02_false-unreach-call_true-termination.i 1 .17 11 1.5 1 3.4  260 1 3.5   260   0 2.0  210 1 .60   18    - -
loops/terminator_03_false-unreach-call_true-termination.i 1 .15 11 1.5 1 3.6  260 1 3.5   250   0 2.7  210 -32 .57   18    - -
loops/trex01_false-unreach-call_true-termination.i 1 .19 11 1.8 1 3.3  260 -32 4.5   220   0 2.0  210 -32 .59   18    - -
loops/trex02_false-unreach-call_true-termination.i 1 .16 11 1.7 1 3.0  260 1 4.9   260   0 2.8  210 -32 .60   18    - -
loops/trex03_false-unreach-call_true-termination.i 1 .19 12 2.2 1 3.4  260 1 5.1   260   0 2.9  210 1 .61   18    - -
loops/verisec_NetBSD-libc__loop_false-unreach-call_true-termination.i 1 .16 11 1.7 1 3.3  250 -32 3.0   230   0 2.8  210 1 .56   18    - -
loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call_true-termination.i 1 .20 12 2.3 1 2.7  260 -32 3.7   250   0 3.0  210 0 .57   18    - -
loops/vogal_false-unreach-call.i 1 .18 12 2.2 1 5.0  300 -32 5.3   240   0 2.0  210 -32 .57   18    - -
loops/while_infinite_loop_4_false-unreach-call_true-termination.i 1 .16 11 1.8 1 2.0  260 -32 5.1   250   0 2.0  190 1 .56   18    - -
loops/array_true-unreach-call_true-termination.i 2 .18 12 2.3 - - - - 2 4.6  270 2 7.2   280  
loops/bubble_sort_true-unreach-call_true-termination.i 2 .15 11 1.6 - - - - 2 4.2  260 2 5.0   230  
loops/count_up_down_true-unreach-call_true-termination.i 2 .17 11 1.5 - - - - 0 910    4900 2 27     330  
loops/eureka_01_true-unreach-call.i 1 .17 11 1.9 - - - - 0 900    6000 0 960     1400  
loops/eureka_05_true-unreach-call_true-termination.i 2 .17 11 2.0 - - - - 0 900    6100 2 56     830  
loops/for_infinite_loop_1_true-unreach-call_false-termination.i 0 900    15000 14000   - - - - 0 .58 41 0 .022 4.9
loops/for_infinite_loop_2_true-unreach-call_false-termination.i 0 900    15000 14000   - - - - 0 .54 43 0 .019 4.9
loops/insertion_sort_true-unreach-call_true-termination.i 0 .20 12 2.1 - - - - 0 .53 44 0 .018 4.8
loops/invert_string_true-unreach-call_true-termination.i 2 .18 11 2.0 - - - - 2 21    520 2 160     720  
loops/linear_sea.ch_true-unreach-call.i 0 .18 12 1.9 - - - - 0 .71 44 0 .018 4.8
loops/lu.cmp_true-unreach-call.i 1 .16 11 1.8 - - - - 0 900    6100 0 960     4100  
loops/matrix_true-unreach-call_true-termination.i 2 .20 12 2.4 - - - - 2 4.1  270 2 10     370  
loops/n.c11_true-unreach-call_false-termination.i 0 900    77 12000   - - - - 0 .59 43 0 .023 4.8
loops/n.c40_true-unreach-call_true-termination.i 2 .17 11 1.7 - - - - 2 4.0  270 2 6.9   350  
loops/nec40_true-unreach-call_true-termination.i 2 .18 11 1.6 - - - - 2 3.6  260 2 9.9   350  
loops/string_true-unreach-call_true-termination.i 2 .17 11 2.4 - - - - 2 3.6  280 2 10     370  
loops/sum01_true-unreach-call_true-termination.i 2 .15 11 2.1 - - - - 0 400    7000 2 9.1   380  
loops/sum03_true-unreach-call_false-termination.i 0 900    15000 13000   - - - - 0 .71 43 0 .022 4.8
loops/sum04_true-unreach-call_true-termination.i 2 .14 11 1.8 - - - - 2 5.6  280 2 12     420  
loops/sum_array_true-unreach-call.i 0 .20 12 2.0 - - - - 0 .70 41 0 .019 4.9
loops/terminator_02_true-unreach-call_true-termination.i 0 900    3100 9100   - - - - 0 .55 43 0 .021 4.8
loops/terminator_03_true-unreach-call_true-termination.i 0 900    69 11000   - - - - 0 .53 41 0 .020 5.0
loops/trex01_true-unreach-call_true-termination.i 2 .26 12 3.3 - - - - 2 34    1100 2 5.4   260  
loops/trex02_true-unreach-call_true-termination.i 2 .14 11 1.6 - - - - 2 3.8  260 2 5.0   250  
loops/trex03_true-unreach-call_true-termination.i 0 900    2400 9000   - - - - 0 .55 43 0 .020 4.9
loops/trex04_true-unreach-call_false-termination.i 2 .18 11 1.7 - - - - 2 4.1  270 2 5.4   250  
loops/veris.c_NetBSD-libc__loop_true-unreach-call_true-termination.i 2 .14 11 1.6 - - - - 0 410    7000 2 11     310  
loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i 2 .65 12 6.6 - - - - 2 8.6  300 2 7.3   270  
loops/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call_true-termination.i 2 .14 11 1.7 - - - - 2 4.1  270 2 5.4   260  
loops/vogal_true-unreach-call.i 2 .19 11 2.1 - - - - 2 35    960 2 230     1100  
loops/while_infinite_loop_1_true-unreach-call_false-termination.i 0 900    15000 13000   - - - - 0 .63 46 0 .018 4.9
loops/while_infinite_loop_2_true-unreach-call_false-termination.i 0 900    15000 12000   - - - - 0 .68 43 0 .020 4.8
loops/while_infinite_loop_3_true-unreach-call_false-termination.i 0 900    15000 12000   - - - - 0 .68 43 0 .020 4.9
loop-acceleration/array_false-unreach-call1_true-termination.i 1 .18 11 1.7 0 97    930 -32 5.0   240   0 1.9  180 1 .57   18    - -
loop-acceleration/array_false-unreach-call2_true-termination.i 1 .17 12 1.9 0 97    1200 -32 3.8   280   0 2.7  210 1 .56   18    - -
loop-acceleration/array_false-unreach-call3_true-termination.i 0 2.2  13 31   0 94    1000 -32 4.8   250   0 2.6  210 -32 .61   18    - -
loop-acceleration/const_false-unreach-call1.i 1 .16 11 1.5 1 7.7  630 -32 4.9   260   0 2.6  180 1 .58   18    - -
loop-acceleration/diamond_false-unreach-call1.i 1 .15 11 1.8 1 5.9  290 -32 3.2   220   0 2.8  210 1 .60   18    - -
loop-acceleration/functions_false-unreach-call1_true-termination.i 1 .14 11 1.6 0 92    1900 -32 4.9   260   0 2.6  180 1 .94   18    - -
loop-acceleration/multivar_false-unreach-call1_true-termination.i 1 .15 11 1.7 1 2.3  270 1 4.8   250   0 1.9  180 1 .60   18    - -
loop-acceleration/nested_false-unreach-call1.i 1 .14 11 1.6 0 91    1900 -32 3.5   270   0 1.9  180 1 3.3    18    - -
loop-acceleration/phases_false-unreach-call1.i 0 220    15000 3300   0 .56 41 0 .019 5.0 0 .66 49 0 .0011 .28 - -
loop-acceleration/phases_false-unreach-call2_false-termination.i 1 .18 11 1.7 1 3.1  260 -32 3.1   240   0 2.8  210 1 .60   18    - -
loop-acceleration/simple_false-unreach-call1.i 1 .14 11 1.7 0 92    1900 -32 3.4   260   0 1.9  180 1 .77   18    - -
loop-acceleration/simple_false-unreach-call2_true-termination.i 1 .17 11 1.8 1 3.1  260 1 3.4   260   0 2.9  190 1 .76   18    - -
loop-acceleration/simple_false-unreach-call3_true-termination.i 1 .16 11 1.5 1 3.3  260 1 3.3   250   0 2.6  180 1 .59   18    - -
loop-acceleration/simple_false-unreach-call4.i 1 .14 11 1.5 0 91    1700 -32 5.2   250   0 2.7  180 1 .77   18    - -
loop-acceleration/underapprox_false-unreach-call1_true-termination.i 1 .15 11 1.6 1 2.8  260 -32 3.3   260   0 1.9  190 1 .57   18    - -
loop-acceleration/underapprox_false-unreach-call2_true-termination.i 1 .15 11 1.6 1 3.7  260 -32 5.0   250   0 2.7  180 1 .58   18    - -
loop-acceleration/array_true-unreach-call1_true-termination.i 2 .17 11 1.6 - - - - 2 2.8  270 2 10     280  
loop-acceleration/array_true-unreach-call2_true-termination.i 1 .17 11 1.8 - - - - 0 900    2700 0 960     3600  
loop-acceleration/array_true-unreach-call3_true-termination.i 2 7.9  15 93   - - - - 2 3.7  260 2 9.5   310  
loop-acceleration/array_true-unreach-call4_true-termination.i 1 7.1  15 84   - - - - 0 900    3800 0 86     7000  
loop-acceleration/const_true-unreach-call1.i 2 .17 11 1.5 - - - - 2 3.5  260 2 7.9   270  
loop-acceleration/diamond_true-unreach-call1_true-termination.i 2 .15 11 1.6 - - - - 2 15    480 0 960     560  
loop-acceleration/diamond_true-unreach-call2.i 2 .19 11 1.8 - - - - 2 6.3  310 2 62     690  
loop-acceleration/functions_true-unreach-call1_true-termination.i 1 .17 11 1.7 - - - - 0 500    7000 0 960     690  
loop-acceleration/multivar_true-unreach-call1_true-termination.i 2 .16 11 1.8 - - - - 2 770    5600 2 5.4   250  
loop-acceleration/nested_true-unreach-call1.i 2 .17 11 1.4 - - - - 2 4.8  270 2 23     380  
loop-acceleration/overflow_true-unreach-call1.i 1 .16 11 1.7 - - - - 0 610    7000 0 960     630  
loop-acceleration/phases_true-unreach-call1.i 1 200    7800 3400   - - - - 0 900    2700 0 960     640  
loop-acceleration/phases_true-unreach-call2_false-termination.i 0 900    11000 9100   - - - - 0 .68 41 0 .018 5.0
loop-acceleration/simple_true-unreach-call1.i 1 .15 11 1.6 - - - - 0 350    7000 0 960     570  
loop-acceleration/simple_true-unreach-call2_true-termination.i 2 .14 11 1.8 - - - - 2 3.6  260 2 3.8   260  
loop-acceleration/simple_true-unreach-call3_true-termination.i 1 .16 11 1.8 - - - - 0 700    7000 0 960     530  
loop-acceleration/simple_true-unreach-call4.i 2 .14 11 1.5 - - - - 2 4.3  260 2 7.0   260  
loop-acceleration/underapprox_true-unreach-call1_true-termination.i 2 .16 11 1.5 - - - - 2 5.5  270 2 61     440  
loop-acceleration/underapprox_true-unreach-call2_true-termination.i 2 .17 11 1.6 - - - - 2 3.9  260 2 7.2   280  
loop-crafted/simple_array_index_value_false-unreach-call1_false-termination.i 1 .24 24 3.0 1 2.4  270 1 3.3   250   0 2.8  210 -32 .57   18    - -
loop-crafted/simple_array_index_value_true-unreach-call1_true-termination.i 1 .19 11 1.6 - - - - 0 900    4200 0 960     700  
loop-crafted/simple_array_index_value_true-unreach-call2_true-termination.i 1 280    58 4000   - - - - 0 900    810 0 960     740  
loop-crafted/simple_array_index_value_true-unreach-call3_true-termination.i 1 .24 13 3.1 - - - - 0 810    7000 0 960     750  
loop-crafted/simple_array_index_value_true-unreach-call4_true-termination.i 0 900    260 10000   - - - - 0 .69 41 0 .024 4.8
loop-crafted/simple_vardep_true-unreach-call1_true-termination.i 2 240    15000 2900   - - - - 2 4.2  270 2 5.4   260  
loop-crafted/simple_vardep_true-unreach-call2_true-termination.i 2 240    15000 3700   - - - - 2 3.9  270 2 5.1   260  
loop-invgen/id_trans_false-unreach-call_true-termination.i 1 .19 12 1.9 1 2.9  260 -32 5.1   260   0 2.9  210 -32 .57   18    - -
loop-invgen/MADWiFi-encode_ie_ok_true-unreach-call_true-termination.i 0 900    1400 14000   - - - - 0 .71 44 0 .025 5.0
loop-invgen/NetBSD_loop_true-unreach-call_true-termination.i 0 900    1100 11000   - - - - 0 .67 45 0 .018 4.8
loop-invgen/SpamAssassin-loop_true-unreach-call_false-termination.i 0 900    1500 7300   - - - - 0 .55 43 0 .022 5.0
loop-invgen/apache-escape-absolute_true-unreach-call_true-termination.i 0 900    3300 13000   - - - - 0 .53 43 0 .019 5.0
loop-invgen/apache-get-tag_true-unreach-call_true-termination.i 0 900    3600 9000   - - - - 0 .54 41 0 .023 5.0
loop-invgen/down_true-unreach-call_true-termination.i 0 900    420 11000   - - - - 0 .67 41 0 .026 4.8
loop-invgen/fragtest_simple_true-unreach-call_true-termination.i 0 900    1400 8600   - - - - 0 .61 44 0 .018 4.9
loop-invgen/half_2_true-unreach-call_true-termination.i 0 900    1700 11000   - - - - 0 .58 43 0 .023 5.0
loop-invgen/heapsort_true-unreach-call_true-termination.i 0 900    1200 12000   - - - - 0 .55 43 0 .019 5.0
loop-invgen/id_build_true-unreach-call_true-termination.i 0 900    1700 12000   - - - - 0 .55 45 0 .021 4.8
loop-invgen/large_const_true-unreach-call_true-termination.i 2 .16 12 1.9 - - - - 2 4.1  280 2 9.1   350  
loop-invgen/nest-if3_true-unreach-call_true-termination.i 0 900    38 12000   - - - - 0 .40 44 0 .023 5.0
loop-invgen/nested6_true-unreach-call_true-termination.i 0 900    3500 9100   - - - - 0 .63 44 0 .019 4.9
loop-invgen/nested9_true-unreach-call_true-termination.i 0 900    520 14000   - - - - 0 .69 42 0 .026 4.9
loop-invgen/sendmail-close-angle_true-unreach-call_true-termination.i 0 900    900 13000   - - - - 0 .56 45 0 .019 4.8
loop-invgen/seq_true-unreach-call_true-termination.i 0 900    1500 13000   - - - - 0 .57 43 0 .020 4.8
loop-invgen/string_concat-noarr_true-unreach-call_true-termination.i 0 900    300 10000   - - - - 0 .69 44 0 .020 4.8
loop-invgen/up_true-unreach-call_true-termination.i 0 900    1800 11000   - - - - 0 .59 46 0 .020 4.9
loop-lit/afnp2014_true-unreach-call_true-termination.c.i 2 6.4  14 91   - - - - 0 330    7000 2 7.2   280  
loop-lit/bhmr2007_true-unreach-call_true-termination.c.i 0 900    21 11000   - - - - 0 .69 44 0 .020 4.9
loop-lit/cggmp2005_true-unreach-call_true-termination.c.i 2 .16 11 1.6 - - - - 2 3.7  270 2 8.4   300  
loop-lit/cggmp2005_variant_true-unreach-call_true-termination.c.i 2 .15 11 1.7 - - - - 0 380    7000 2 8.2   320  
loop-lit/cggmp2005b_true-unreach-call_true-termination.c.i 2 .16 11 1.7 - - - - 2 5.0  260 2 8.2   270  
loop-lit/css2003_true-unreach-call_true-termination.c.i 2 7.5  160 100   - - - - 2 4.0  270 2 5.4   260  
loop-lit/ddlm2013_true-unreach-call.i 0 900    76 14000   - - - - 0 .57 43 0 .022 4.9
loop-lit/gj2007_true-unreach-call_true-termination.c.i 2 .15 11 1.9 - - - - 2 41    490 2 120     1300  
loop-lit/gj2007b_true-unreach-call_true-termination.c.i 0 900    1600 9700   - - - - 0 .66 46 0 .019 4.9
loop-lit/gr2006_true-unreach-call_true-termination.c.i 2 .16 11 1.8 - - - - 2 49    910 2 94     1600  
loop-lit/gsv2008_true-unreach-call_true-termination.c.i 0 900    39 12000   - - - - 0 .70 43 0 .018 4.9
loop-lit/hhk2008_true-unreach-call_true-termination.c.i 2 .17 11 1.5 - - - - 0 380    7000 2 8.8   280  
loop-lit/jm2006_true-unreach-call_true-termination.c.i 2 .15 11 1.8 - - - - 0 900    4900 2 9.8   280  
loop-lit/jm2006_variant_true-unreach-call_true-termination.c.i 2 .18 12 1.7 - - - - 0 900    4700 2 8.4   300  
loop-lit/mcmillan2006_true-unreach-call_true-termination.c.i 0 140    270 1700   - - - - 0 .59 43 0 .019 4.8
loop-lit/gcnr2008_false-unreach-call_false-termination.i 1 .19 11 1.8 0 92    2200 1 3.4   260   0 2.8  210 1 .58   18    - -
loop-new/count_by_1_true-unreach-call_true-termination.i 2 .16 11 1.5 - - - - 2 3.4  270 2 6.6   260  
loop-new/count_by_1_variant_true-unreach-call_true-termination.i 2 2.9  180 46   - - - - 2 3.5  270 2 7.9   300  
loop-new/count_by_2_true-unreach-call_true-termination.i 1 .14 11 1.8 - - - - 0 440    7000 0 960     4700  
loop-new/count_by_k_true-unreach-call_true-termination.i 0 900    12 12000   - - - - 0 .66 43 0 .019 4.9
loop-new/count_by_nondet_true-unreach-call_true-termination.i 0 900    56 12000   - - - - 0 .62 43 0 .018 4.8
loop-new/gauss_sum_true-unreach-call_true-termination.i 1 .66 12 8.3 - - - - 0 910    6500 0 960     930  
loop-new/half_true-unreach-call_true-termination.i 0 900    1900 12000   - - - - 0 .63 43 0 .019 5.0
loop-new/nested_true-unreach-call_true-termination.i 2 .26 12 3.3 - - - - 0 900    3300 2 36     910  
loop-industry-pattern/aiob_1_true-unreach-call.c 2 .20 11 2.1 - - - - 2 43    600 0 960     1900  
loop-industry-pattern/aiob_2_true-unreach-call.c 2 .19 11 1.9 - - - - 2 46    510 0 960     2100  
loop-industry-pattern/aiob_3_true-unreach-call.c 2 .18 11 2.2 - - - - 2 49    590 0 960     1900  
loop-industry-pattern/aiob_4_true-unreach-call.c 2 .20 11 1.5 - - - - 2 37    530 0 960     1700  
loop-industry-pattern/mod3_true-unreach-call.c 0 900    22 12000   - - - - 0 .55 43 0 .018 4.9
loop-industry-pattern/nested_true-unreach-call.c 0 900    11000 13000   - - - - 0 .62 41 0 .020 4.9
loop-industry-pattern/ofuf_1_true-unreach-call.c 0 900    58 14000   - - - - 0 .57 44 0 .028 4.8
loop-industry-pattern/ofuf_2_true-unreach-call.c 0 900    60 14000   - - - - 0 .67 44 0 .023 5.0
loop-industry-pattern/ofuf_3_true-unreach-call.c 0 900    59 12000   - - - - 0 .58 45 0 .024 4.9
loop-industry-pattern/ofuf_4_true-unreach-call.c 0 900    62 14000   - - - - 0 .56 41 0 .020 4.9
loop-industry-pattern/ofuf_5_true-unreach-call.c 0 900    59 12000   - - - - 0 .58 42 0 .019 4.9
loops/heavy_true-unreach-call.c 1 .41 30 5.8 - - - - 0 900    7000 0 290     7000  
loops/compact_false-unreach-call.c 0 900    1100 8700   0 .61 41 0 .018 4.8 0 .65 50 0 .0015 .26 - -
loops/heavy_false-unreach-call.c 0 .41 30 4.3 0 91    2500 0 97     6900   0 2.0  210 0 96      18    - -
sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
total 163 152 43000   210000 550000 52 31 1100 26000 52 -918 360 21000 52 0 110 8900 52 -390 120   770 111 78 19000 160000 111 88 19000 61000
    correct results 88 137 520   31000 7100 31 31 120 8800 10 10 39 2500 0 26 26 19   480 39 78 1300 20000 44 88 1100 18000
        correct true 49 98 510   30000 7000 0 0 0 0 39 78 1300 20000 44 88 1100 18000
        correct false 39 39 6.7 450 72 31 31 120 8800 10 10 39 2500 0 26 26 19   480 0 0
    correct-unconfimed results 18 15 490   8100 7600 0 0 0 0 0 0
        correct-unconfirmed true 15 15 490   8000 7600 0 0 0 0 0 0
        correct-unconfirmed false 3 0 3.6 58 49 0 0 0 0 0 0
    incorrect results 0 0 29 -928 120 7200 0 13 -416 7.6 240 0 0
        incorrect true 0 0 29 -928 120 7200 0 13 -416 7.6 240 0 0
        incorrect false 0 0 0 0 0 0 0
score (163 tasks, max score: 274) 152 31 -918 0 -390 78 88
Run set symbiotic.sv-comp18.ReachSafety-Loops cpa-seq-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.ReachSafety-Loops uautomizer-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.ReachSafety-Loops cpa-witness2test-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.ReachSafety-Loops fshell-witness2test-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.ReachSafety-Loops cpa-seq-validate-correctness-witnesses-symbiotic.sv-comp18-correctness-witness.ReachSafety-Loops uautomizer-validate-correctness-witnesses-symbiotic.sv-comp18-correctness-witness.ReachSafety-Loops