Tool ULTIMATE Taipan 0.1.23-3204b741 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*
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]
Date of execution 2017-12-02 17:23:13 CET 2017-12-03 07:22:17 CET 2017-12-03 07:45:29 CET 2017-12-03 07:47:53 CET 2017-12-03 07:50:34 CET 2017-12-03 06:47:45 CET 2017-12-03 07:25:40 CET
Run set utaipan.sv-comp18.ReachSafety-ControlFlow cpa-seq-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.ReachSafety-ControlFlow uautomizer-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.ReachSafety-ControlFlow cpa-witness2test-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.ReachSafety-ControlFlow fshell-witness2test-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.ReachSafety-ControlFlow cpa-seq-validate-correctness-witnesses-utaipan.sv-comp18-correctness-witness.ReachSafety-ControlFlow uautomizer-validate-correctness-witnesses-utaipan.sv-comp18-correctness-witness.ReachSafety-ControlFlow
Options --full-output -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/utaipan.2017-12-02_1723.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/utaipan.2017-12-02_1723.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/utaipan.2017-12-02_1723.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/utaipan.2017-12-02_1723.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/utaipan.2017-12-02_1723.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/utaipan.2017-12-02_1723.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
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c false(unreach-call) 1 wit inspect 58   1300 440 true -32 wit inspect 6.7  270 false(unreach-call) 1 wit inspect 9.9   470   unknown 0 wit inspect 4.5  270 true -32 wit inspect .80   20    - wit inspect - wit inspect
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c false(unreach-call) 1 wit inspect 33   950 270 true -32 wit inspect 4.9  270 false(unreach-call) 1 wit inspect 8.7   390   unknown 0 wit inspect 3.8  220 true -32 wit inspect .70   20    - wit inspect - wit inspect
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c false(unreach-call) 1 wit inspect 50   1300 430 true -32 wit inspect 5.6  260 false(unreach-call) 1 wit inspect 9.1   440   unknown 0 wit inspect 4.0  220 true -32 wit inspect .76   20    - wit inspect - wit inspect
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c false(unreach-call) 1 wit inspect 16   640 130 true -32 wit inspect 4.6  270 false(unreach-call) 1 wit inspect 8.1   370   unknown 0 wit inspect 3.8  220 true -32 wit inspect .71   19    - wit inspect - wit inspect
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c timeout 0 wit inspect 900   3900 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .018 5.0
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 600   4600 6800 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 340    7000 true 2 wit inspect 57     880  
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c timeout 0 wit inspect 900   4600 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .047 4.8
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c timeout 0 wit inspect 900   4600 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 41 error (2) 0 wit inspect .048 4.9
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 16   720 140 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.5  270 true 2 wit inspect 19     520  
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 17   620 130 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.1  270 true 2 wit inspect 19     530  
ssh-simplified/s3_clnt_1_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 10   570 83 true -32 wit inspect 5.2  260 false(unreach-call) 1 wit inspect 7.7   370   unknown 0 wit inspect 3.7  220 true -32 wit inspect .65   20    - wit inspect - wit inspect
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 10   550 73 true -32 wit inspect 5.2  270 false(unreach-call) 1 wit inspect 7.8   380   unknown 0 wit inspect 3.9  220 true -32 wit inspect .69   19    - wit inspect - wit inspect
ssh-simplified/s3_clnt_3_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 15   650 120 true -32 wit inspect 5.3  270 false(unreach-call) 1 wit inspect 7.6   370   unknown 0 wit inspect 3.6  210 true -32 wit inspect .66   20    - wit inspect - wit inspect
ssh-simplified/s3_clnt_4_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 14   610 120 true -32 wit inspect 5.3  270 false(unreach-call) 1 wit inspect 8.9   370   unknown 0 wit inspect 3.8  210 true -32 wit inspect .65   19    - wit inspect - wit inspect
ssh-simplified/s3_srvr_10_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 9.3 470 73 true -32 wit inspect 4.6  270 false(unreach-call) 1 wit inspect 7.6   360   unknown 0 wit inspect 3.7  220 true -32 wit inspect .68   19    - wit inspect - wit inspect
ssh-simplified/s3_srvr_11_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 39   4300 370 true -32 wit inspect 6.3  270 false(unreach-call) 1 wit inspect 9.6   460   unknown 0 wit inspect 4.3  220 true -32 wit inspect .67   20    - wit inspect - wit inspect
ssh-simplified/s3_srvr_12_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 710   4900 8400 true -32 wit inspect 6.6  280 false(unreach-call) 1 wit inspect 8.9   430   unknown 0 wit inspect 4.2  220 true -32 wit inspect .68   20    - wit inspect - wit inspect
ssh-simplified/s3_srvr_13_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 21   720 170 true -32 wit inspect 5.5  270 false(unreach-call) 1 wit inspect 8.2   380   unknown 0 wit inspect 3.9  220 true -32 wit inspect .65   20    - wit inspect - wit inspect
ssh-simplified/s3_srvr_14_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 16   640 130 true -32 wit inspect 5.8  270 false(unreach-call) 1 wit inspect 7.9   360   unknown 0 wit inspect 3.8  220 true -32 wit inspect .68   19    - wit inspect - wit inspect
ssh-simplified/s3_srvr_1_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 15   630 130 true -32 wit inspect 5.7  290 false(unreach-call) 1 wit inspect 7.8   390   unknown 0 wit inspect 3.8  210 true -32 wit inspect .68   20    - wit inspect - wit inspect
ssh-simplified/s3_srvr_2_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 16   660 130 true -32 wit inspect 5.4  270 false(unreach-call) 1 wit inspect 7.5   390   unknown 0 wit inspect 4.0  220 true -32 wit inspect .66   20    - wit inspect - wit inspect
ssh-simplified/s3_srvr_6_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 6.2 320 50 false(unreach-call) 1 wit inspect 3.8  260 false(unreach-call) 1 wit inspect 6.8   330   unknown 0 wit inspect 3.2  210 true -32 wit inspect .65   19    - wit inspect - wit inspect
ssh-simplified/s3_clnt_1_true-unreach-call_true-termination.cil.c true 2 wit inspect 440   5300 5300 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 12    400 true 2 wit inspect 29     1000  
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c true 2 wit inspect 500   5400 6500 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 13    410 true 2 wit inspect 34     1300  
ssh-simplified/s3_clnt_3_true-unreach-call_true-termination.cil.c true 2 wit inspect 550   5500 6500 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 13    430 true 2 wit inspect 32     1100  
ssh-simplified/s3_clnt_4_true-unreach-call_true-termination.cil.c true 2 wit inspect 440   5400 5700 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 13    400 true 2 wit inspect 35     1100  
ssh-simplified/s3_srvr_1_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900   5400 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .050 4.9
ssh-simplified/s3_srvr_1a_true-unreach-call_false-termination.cil.c true 2 wit inspect 7.5 370 56 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.5  310 true 2 wit inspect 19     500  
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c true 2 wit inspect 5.7 290 52 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.3  280 true 2 wit inspect 8.6   370  
ssh-simplified/s3_srvr_2_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900   5400 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .019 4.9
ssh-simplified/s3_srvr_3_true-unreach-call_false-termination.cil.c true 2 wit inspect 500   4700 5900 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5200 true 2 wit inspect 44     1100  
ssh-simplified/s3_srvr_4_true-unreach-call_false-termination.cil.c true 2 wit inspect 200   4900 2400 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4700 true 2 wit inspect 38     950  
ssh-simplified/s3_srvr_6_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900   5400 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 43 error (2) 0 wit inspect .022 4.9
ssh-simplified/s3_srvr_7_true-unreach-call_false-termination.cil.c true 2 wit inspect 240   4900 3300 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4600 true 2 wit inspect 45     1000  
ssh-simplified/s3_srvr_8_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900   5400 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .019 4.9
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c false(unreach-call) 1 wit inspect 6.3 280 49 true -32 wit inspect 3.5  260 false(unreach-call) 1 wit inspect 6.9   280   unknown 0 wit inspect 3.0  210 true -32 wit inspect .59   19    - wit inspect - wit inspect
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c false(unreach-call) 1 wit inspect 6.1 290 49 true -32 wit inspect 3.4  260 false(unreach-call) 1 wit inspect 6.3   280   unknown 0 wit inspect 3.0  210 true -32 wit inspect .60   19    - wit inspect - wit inspect
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 20   850 150 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.1  290 true 2 wit inspect 16     710  
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 26   1400 180 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.5  290 true 2 wit inspect 20     1200  
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 37   3000 320 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.2  290 true 2 wit inspect 24     2000  
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 51   4600 450 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.7  290 true 2 wit inspect 38     3500  
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 130   6100 1000 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.7  290 true 2 wit inspect 63     6000  
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 290   8800 2000 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.8  290 out of memory 0 wit inspect 110     7000  
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 9.1 390 81 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.6  280 true 2 wit inspect 7.2   280  
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 7.3 380 62 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.4  280 true 2 wit inspect 8.0   300  
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 9.2 520 69 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.0  280 true 2 wit inspect 9.5   380  
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 11   590 86 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0  280 true 2 wit inspect 12     510  
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 14   670 120 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.8  280 true 2 wit inspect 13     520  
ntdrivers/cdaudio_false-unreach-call.i.cil.c timeout 0 wit inspect 900   5300 12000 error (invalid witness file) 0 wit inspect .58 42 error (2) 0 wit inspect .051 4.8 error (invalid witness file) 0 wit inspect .84 51 error (invalid witness file) 0 wit inspect .0040 .33 - wit inspect - wit inspect
ntdrivers/diskperf_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 20   750 160 timeout 0 wit inspect 92    2100 false(unreach-call) 1 wit inspect 13     480   unknown 0 wit inspect 5.0  270 timeout 0 wit inspect 96      19    - wit inspect - wit inspect
ntdrivers/floppy_false-unreach-call.i.cil.c timeout 0 wit inspect 900   6300 11000 error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .87 49 error (invalid witness file) 0 wit inspect .0038 .31 - wit inspect - wit inspect
ntdrivers/kbfiltr_false-unreach-call.i.cil.c timeout 0 wit inspect 900   4700 10000 error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .030 4.9 error (invalid witness file) 0 wit inspect .84 49 error (invalid witness file) 0 wit inspect .0039 .26 - wit inspect - wit inspect
ntdrivers/parport_false-unreach-call.i.cil.c unknown 0 wit inspect 150   1400 1400 error (invalid witness file) 0 wit inspect .50 41 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .83 49 error (invalid witness file) 0 wit inspect .0046 .26 - wit inspect - wit inspect
ntdrivers/cdaudio_true-unreach-call.i.cil.c timeout 0 wit inspect 900   4800 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 41 error (2) 0 wit inspect .018 4.8
ntdrivers/diskperf_true-unreach-call.i.cil.c timeout 0 wit inspect 900   6300 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .020 4.8
ntdrivers/floppy2_true-unreach-call_true-termination.i.cil.c timeout 0 wit inspect 900   6100 9500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 44 error (2) 0 wit inspect .037 4.9
ntdrivers/floppy_true-unreach-call_true-valid-memsafety.i.cil.c timeout 0 wit inspect 900   6300 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .025 4.9
ntdrivers/parport_true-unreach-call.i.cil.c true 2 wit inspect 710   4800 8200 - wit inspect - wit inspect - wit inspect - wit inspect error 0 wit inspect 19    390 true 2 wit inspect 230     4700  
ssh/s3_clnt.blast.01_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 180   990 1800 true -32 wit inspect 5.1  270 false(unreach-call) 1 wit inspect 29     530   unknown 0 wit inspect 4.0  220 error (2) 0 wit inspect .77   20    - wit inspect - wit inspect
ssh/s3_clnt.blast.02_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 70   810 680 true -32 wit inspect 4.8  270 false(unreach-call) 1 wit inspect 28     530   unknown 0 wit inspect 3.8  220 error (2) 0 wit inspect .76   20    - wit inspect - wit inspect
ssh/s3_clnt.blast.03_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 70   840 650 true -32 wit inspect 5.5  280 false(unreach-call) 1 wit inspect 30     530   unknown 0 wit inspect 4.2  230 error (2) 0 wit inspect .76   20    - wit inspect - wit inspect
ssh/s3_clnt.blast.04_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 67   770 790 true -32 wit inspect 5.2  270 false(unreach-call) 1 wit inspect 28     530   unknown 0 wit inspect 3.8  220 error (2) 0 wit inspect .76   20    - wit inspect - wit inspect
ssh/s3_srvr.blast.01_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 45   630 460 true -32 wit inspect 5.0  260 false(unreach-call) 1 wit inspect 23     490   unknown 0 wit inspect 4.3  240 error (2) 0 wit inspect .81   20    - wit inspect - wit inspect
ssh/s3_srvr.blast.02_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 32   600 280 true -32 wit inspect 5.4  260 false(unreach-call) 1 wit inspect 24     480   unknown 0 wit inspect 4.4  220 error (2) 0 wit inspect .77   20    - wit inspect - wit inspect
ssh/s3_srvr.blast.03_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 31   580 270 true -32 wit inspect 5.2  260 false(unreach-call) 1 wit inspect 23     480   unknown 0 wit inspect 4.0  220 error (2) 0 wit inspect .80   20    - wit inspect - wit inspect
ssh/s3_srvr.blast.04_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 32   580 280 true -32 wit inspect 5.2  260 false(unreach-call) 1 wit inspect 24     480   unknown 0 wit inspect 3.8  220 error (2) 0 wit inspect .77   20    - wit inspect - wit inspect
ssh/s3_srvr.blast.06_false-unreach-call.i.cil.c timeout 0 wit inspect 900   4800 10000 error (invalid witness file) 0 wit inspect .52 42 error (2) 0 wit inspect .051 4.9 error (invalid witness file) 0 wit inspect .87 51 error (invalid witness file) 0 wit inspect .0035 .34 - wit inspect - wit inspect
ssh/s3_srvr.blast.07_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 560   4900 6300 true -32 wit inspect 6.0  270 false(unreach-call) 1 wit inspect 31     590   unknown 0 wit inspect 4.6  220 error (2) 0 wit inspect .81   20    - wit inspect - wit inspect
ssh/s3_srvr.blast.08_false-unreach-call.i.cil.c timeout 0 wit inspect 900   5500 11000 error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .048 4.9 error (invalid witness file) 0 wit inspect .90 49 error (invalid witness file) 0 wit inspect .0038 .34 - wit inspect - wit inspect
ssh/s3_srvr.blast.09_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 890   4800 11000 true -32 wit inspect 5.8  270 false(unreach-call) 1 wit inspect 30     580   unknown 0 wit inspect 4.6  230 error (2) 0 wit inspect .78   20    - wit inspect - wit inspect
ssh/s3_srvr.blast.10_false-unreach-call.i.cil.c timeout 0 wit inspect 900   5200 10000 error (invalid witness file) 0 wit inspect .51 42 error (2) 0 wit inspect .049 4.8 error (invalid witness file) 0 wit inspect .86 47 error (invalid witness file) 0 wit inspect .0037 .34 - wit inspect - wit inspect
ssh/s3_srvr.blast.11_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 120   4600 1500 true -32 wit inspect 5.6  260 false(unreach-call) 1 wit inspect 49     630   unknown 0 wit inspect 4.3  260 error (2) 0 wit inspect .81   20    - wit inspect - wit inspect
ssh/s3_srvr.blast.12_false-unreach-call.i.cil.c timeout 0 wit inspect 900   4800 11000 error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .046 4.8 error (invalid witness file) 0 wit inspect .86 47 error (invalid witness file) 0 wit inspect .0035 .30 - wit inspect - wit inspect
ssh/s3_srvr.blast.13_false-unreach-call.i.cil.c timeout 0 wit inspect 900   5100 9600 error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .84 50 error (invalid witness file) 0 wit inspect .0039 .29 - wit inspect - wit inspect
ssh/s3_srvr.blast.14_false-unreach-call.i.cil.c timeout 0 wit inspect 900   4800 11000 error (invalid witness file) 0 wit inspect .52 44 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .81 47 error (invalid witness file) 0 wit inspect .0045 .26 - wit inspect - wit inspect
ssh/s3_srvr.blast.15_false-unreach-call.i.cil.c timeout 0 wit inspect 900   5400 11000 error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .021 4.9 error (invalid witness file) 0 wit inspect .80 47 error (invalid witness file) 0 wit inspect .0041 .34 - wit inspect - wit inspect
ssh/s3_srvr.blast.16_false-unreach-call.i.cil.c timeout 0 wit inspect 900   4800 11000 error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .93 49 error (invalid witness file) 0 wit inspect .0035 .33 - wit inspect - wit inspect
ssh/s3_clnt.blast.01_true-unreach-call.i.cil.c false(unreach-call) -16 wit inspect 400   4700 3900 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.5  270 false(unreach-call) -16 wit inspect 160     870  
ssh/s3_clnt.blast.02_true-unreach-call.i.cil.c timeout 0 wit inspect 900   5300 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .72 43 error (2) 0 wit inspect .052 4.8
ssh/s3_clnt.blast.03_true-unreach-call.i.cil.c timeout 0 wit inspect 900   5200 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .018 4.9
ssh/s3_clnt.blast.04_true-unreach-call.i.cil.c false(unreach-call) -16 wit inspect 500   4800 5600 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.0  270 false(unreach-call) -16 wit inspect 400     1400  
ssh/s3_srvr.blast.01_true-unreach-call.i.cil.c timeout 0 wit inspect 900   6300 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .018 4.9
ssh/s3_srvr.blast.02_true-unreach-call.i.cil.c timeout 0 wit inspect 900   5900 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .024 4.8
ssh/s3_srvr.blast.06_true-unreach-call.i.cil.c timeout 0 wit inspect 900   6100 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .018 4.9
ssh/s3_srvr.blast.07_true-unreach-call.i.cil.c timeout 0 wit inspect 900   5800 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 47 error (2) 0 wit inspect .018 5.0
ssh/s3_srvr.blast.08_true-unreach-call.i.cil.c timeout 0 wit inspect 900   6500 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 42 error (2) 0 wit inspect .018 4.9
ssh/s3_srvr.blast.09_true-unreach-call.i.cil.c timeout 0 wit inspect 900   6000 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .021 4.9
ssh/s3_srvr.blast.10_true-unreach-call.i.cil.c timeout 0 wit inspect 900   6300 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .018 4.9
ssh/s3_srvr.blast.11_true-unreach-call.i.cil.c timeout 0 wit inspect 900   6100 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .018 4.9
ssh/s3_srvr.blast.12_true-unreach-call.i.cil.c timeout 0 wit inspect 900   6200 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .047 5.0
ssh/s3_srvr.blast.13_true-unreach-call.i.cil.c timeout 0 wit inspect 900   6000 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .018 4.8
ssh/s3_srvr.blast.14_true-unreach-call.i.cil.c timeout 0 wit inspect 900   6500 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .020 4.8
ssh/s3_srvr.blast.15_true-unreach-call.i.cil.c timeout 0 wit inspect 900   6300 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 43 error (2) 0 wit inspect .024 4.9
ssh/s3_srvr.blast.16_true-unreach-call.i.cil.c timeout 0 wit inspect 900   6300 8400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .018 4.9
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 94 46 42000 330000 510000 42 -895 250   10000 42 30 480 13000 42 0 130 7300 42 -576 120 590 52 42 3200 29000 52 14 1500 40000
    correct results 54 78 8000 120000 91000 1 1 3.8 260 30 30 480 13000 0 0 21 42 150 6400 23 46 820 30000
        correct true 24 48 4800 75000 56000 0 0 0 0 21 42 150 6400 23 46 820 30000
        correct false 30 30 3200 41000 35000 1 1 3.8 260 30 30 480 13000 0 0 0 0
    incorrect results 2 -32 900 9500 9500 28 -896 150   7500 0 0 18 -576 12 350 0 2 -32 570 2300
        incorrect true 0 28 -896 150   7500 0 0 18 -576 12 350 0 0
        incorrect false 2 -32 900 9500 9500 0 0 0 0 0 2 -32 570 2300
score (94 tasks, max score: 146) 46 -895 30 0 -576 42 14
Run set utaipan.sv-comp18.ReachSafety-ControlFlow cpa-seq-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.ReachSafety-ControlFlow uautomizer-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.ReachSafety-ControlFlow cpa-witness2test-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.ReachSafety-ControlFlow fshell-witness2test-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.ReachSafety-ControlFlow cpa-seq-validate-correctness-witnesses-utaipan.sv-comp18-correctness-witness.ReachSafety-ControlFlow uautomizer-validate-correctness-witnesses-utaipan.sv-comp18-correctness-witness.ReachSafety-ControlFlow