Tool 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-11-30 11:20:26 CET 2017-12-01 07:29:20 CET 2017-12-01 08:07:14 CET 2017-12-01 08:15:38 CET 2017-12-01 08:19:10 CET 2017-12-01 04:11:27 CET 2017-12-01 07:35:08 CET
Run set cpa-seq.sv-comp18.ReachSafety-ControlFlow cpa-seq-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.ReachSafety-ControlFlow uautomizer-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.ReachSafety-ControlFlow cpa-witness2test-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.ReachSafety-ControlFlow fshell-witness2test-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.ReachSafety-ControlFlow cpa-seq-validate-correctness-witnesses-cpa-seq.sv-comp18-correctness-witness.ReachSafety-ControlFlow uautomizer-validate-correctness-witnesses-cpa-seq.sv-comp18-correctness-witness.ReachSafety-ControlFlow
Options -svcomp18 -heap 10000M -benchmark -timelimit 900s -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-seq.2017-11-30_1120.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/cpa-seq.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-seq.2017-11-30_1120.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/cpa-seq.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-seq.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/cpa-seq.2017-11-30_1120.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 8.8 340 77 false(unreach-call) 1 wit inspect 6.0 270 false(unreach-call) 1 wit inspect 13   470 unknown 0 wit inspect 4.5 260 true -32 wit inspect 1.0  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 6.9 300 53 false(unreach-call) 1 wit inspect 4.7 270 false(unreach-call) 1 wit inspect 10   370 unknown 0 wit inspect 4.1 220 true -32 wit inspect .76 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 8.1 330 65 false(unreach-call) 1 wit inspect 5.2 290 false(unreach-call) 1 wit inspect 11   410 unknown 0 wit inspect 5.3 260 true -32 wit inspect .79 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 5.8 300 47 false(unreach-call) 1 wit inspect 4.7 290 false(unreach-call) 1 wit inspect 8.8 340 unknown 0 wit inspect 4.7 210 true -32 wit inspect .76 19 - wit inspect - wit inspect
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 8.3 330 62 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 14   420 true 2 wit inspect 110   1100
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 100   1300 1300 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 430   7000 true 2 wit inspect 67   860
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 7.4 310 70 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.8 330 true 2 wit inspect 67   890
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 8.0 330 66 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 11   360 true 2 wit inspect 89   1100
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 4.9 280 40 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.9 260 true 2 wit inspect 18   510
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 6.3 290 49 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9 280 true 2 wit inspect 19   520
ssh-simplified/s3_clnt_1_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 6.4 300 47 false(unreach-call) 1 wit inspect 4.5 280 false(unreach-call) 1 wit inspect 7.6 350 unknown 0 wit inspect 4.7 220 true -32 wit inspect .71 20 - wit inspect - wit inspect
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 6.7 300 52 false(unreach-call) 1 wit inspect 3.2 270 false(unreach-call) 1 wit inspect 8.9 350 unknown 0 wit inspect 4.0 240 true -32 wit inspect .75 20 - wit inspect - wit inspect
ssh-simplified/s3_clnt_3_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 6.1 300 46 false(unreach-call) 1 wit inspect 5.6 280 false(unreach-call) 1 wit inspect 9.6 360 unknown 0 wit inspect 3.8 220 true -32 wit inspect .74 20 - wit inspect - wit inspect
ssh-simplified/s3_clnt_4_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 6.3 300 49 false(unreach-call) 1 wit inspect 4.9 280 false(unreach-call) 1 wit inspect 8.4 350 unknown 0 wit inspect 4.5 210 true -32 wit inspect .84 20 - wit inspect - wit inspect
ssh-simplified/s3_srvr_10_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 3.8 280 35 false(unreach-call) 1 wit inspect 4.2 270 false(unreach-call) 1 wit inspect 7.7 320 unknown 0 wit inspect 3.5 210 true -32 wit inspect .89 19 - wit inspect - wit inspect
ssh-simplified/s3_srvr_11_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 100   800 1400 false(unreach-call) 1 wit inspect 5.8 290 false(unreach-call) 1 wit inspect 12   540 unknown 0 wit inspect 4.8 220 true -32 wit inspect .74 21 - wit inspect - wit inspect
ssh-simplified/s3_srvr_12_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 160   860 1800 false(unreach-call) 1 wit inspect 6.9 290 false(unreach-call) 1 wit inspect 12   430 unknown 0 wit inspect 5.6 230 true -32 wit inspect .79 21 - wit inspect - wit inspect
ssh-simplified/s3_srvr_13_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 5.4 290 44 false(unreach-call) 1 wit inspect 4.6 280 false(unreach-call) 1 wit inspect 11   370 unknown 0 wit inspect 3.8 210 true -32 wit inspect .71 20 - wit inspect - wit inspect
ssh-simplified/s3_srvr_14_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 8.8 380 70 false(unreach-call) 1 wit inspect 4.9 290 false(unreach-call) 1 wit inspect 8.4 340 unknown 0 wit inspect 4.5 220 true -32 wit inspect .72 19 - wit inspect - wit inspect
ssh-simplified/s3_srvr_1_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 5.9 290 45 false(unreach-call) 1 wit inspect 5.7 280 false(unreach-call) 1 wit inspect 9.7 380 unknown 0 wit inspect 4.3 230 true -32 wit inspect .88 20 - wit inspect - wit inspect
ssh-simplified/s3_srvr_2_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 5.5 290 45 false(unreach-call) 1 wit inspect 5.1 280 false(unreach-call) 1 wit inspect 8.1 380 unknown 0 wit inspect 5.2 230 true -32 wit inspect .78 20 - wit inspect - wit inspect
ssh-simplified/s3_srvr_6_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 3.3 260 29 false(unreach-call) 1 wit inspect 3.9 270 false(unreach-call) 1 wit inspect 7.3 300 unknown 0 wit inspect 3.5 210 true -32 wit inspect .68 19 - wit inspect - wit inspect
ssh-simplified/s3_clnt_1_true-unreach-call_true-termination.cil.c true 2 wit inspect 13   710 120 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 12   540 true 2 wit inspect 36   1100
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c true 2 wit inspect 13   720 120 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 14   430 true 2 wit inspect 38   1100
ssh-simplified/s3_clnt_3_true-unreach-call_true-termination.cil.c true 2 wit inspect 14   730 140 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 15   460 true 2 wit inspect 34   1100
ssh-simplified/s3_clnt_4_true-unreach-call_true-termination.cil.c true 2 wit inspect 13   720 120 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 14   420 true 2 wit inspect 39   990
ssh-simplified/s3_srvr_1_true-unreach-call_false-termination.cil.c true 1 wit inspect 14   730 140 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910   5100 false(unreach-call) -16 wit inspect 13   450
ssh-simplified/s3_srvr_1a_true-unreach-call_false-termination.cil.c true 2 wit inspect 3.1 250 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 10   310 false(unreach-call) -16 wit inspect 6.3 260
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c true 2 wit inspect 2.6 250 24 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.9 280 false(unreach-call) -16 wit inspect 7.5 320
ssh-simplified/s3_srvr_2_true-unreach-call_false-termination.cil.c true 1 wit inspect 14   730 120 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910   4900 false(unreach-call) -16 wit inspect 23   590
ssh-simplified/s3_srvr_3_true-unreach-call_false-termination.cil.c true 1 wit inspect 14   730 140 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910   4900 false(unreach-call) -16 wit inspect 23   580
ssh-simplified/s3_srvr_4_true-unreach-call_false-termination.cil.c true 1 wit inspect 14   730 150 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910   4800 false(unreach-call) -16 wit inspect 21   560
ssh-simplified/s3_srvr_6_true-unreach-call_false-termination.cil.c true 1 wit inspect 81   2300 1100 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900   5000 false(unreach-call) -16 wit inspect 23   560
ssh-simplified/s3_srvr_7_true-unreach-call_false-termination.cil.c true 1 wit inspect 46   1300 460 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910   4700 false(unreach-call) -16 wit inspect 29   590
ssh-simplified/s3_srvr_8_true-unreach-call_false-termination.cil.c true 1 wit inspect 14   740 140 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910   4600 false(unreach-call) -16 wit inspect 22   580
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c false(unreach-call) 1 wit inspect 3.3 270 32 false(unreach-call) 1 wit inspect 3.7 260 false(unreach-call) 1 wit inspect 6.3 270 unknown 0 wit inspect 3.2 210 true -32 wit inspect .64 19 - wit inspect - wit inspect
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c false(unreach-call) 1 wit inspect 3.8 270 34 false(unreach-call) 1 wit inspect 4.0 270 false(unreach-call) 1 wit inspect 8.3 310 unknown 0 wit inspect 3.5 220 true -32 wit inspect .68 19 - wit inspect - wit inspect
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 15   740 120 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.1 290 false(unreach-call) -16 wit inspect 6.1 270
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 44   1200 470 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.5 290 false(unreach-call) -16 wit inspect 5.8 260
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 150   1300 1900 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.3 280 true 2 wit inspect 28   2100
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 150   1200 1800 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.4 280 true 2 wit inspect 42   3500
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 150   1200 1900 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.5 290 true 2 wit inspect 69   6000
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 150   1200 1700 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.6 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 3.1 250 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.7 280 false(unreach-call) -16 wit inspect 6.5 230
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 3.5 260 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8 280 true 2 wit inspect 8.4 310
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 4.3 270 35 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.9 280 false(unreach-call) -16 wit inspect 5.4 260
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 6.0 290 47 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.3 280 false(unreach-call) -16 wit inspect 5.3 260
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 8.4 430 68 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.1 280 false(unreach-call) -16 wit inspect 6.0 260
ntdrivers/cdaudio_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 54   1800 580 false(unreach-call) 1 wit inspect 29   730 true -32 wit inspect 27   570 unknown 0 wit inspect 12   390 error (2) 0 wit inspect 2.0  42 - wit inspect - wit inspect
ntdrivers/diskperf_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 15   510 150 false(unreach-call) 1 wit inspect 14   560 false(unreach-call) 1 wit inspect 13   470 unknown 0 wit inspect 5.2 270 timeout 0 wit inspect 96    19 - wit inspect - wit inspect
ntdrivers/floppy_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 11   470 100 false(unreach-call) 1 wit inspect 9.6 450 true -32 wit inspect 26   590 unknown 0 wit inspect 6.5 280 timeout 0 wit inspect 96    19 - wit inspect - wit inspect
ntdrivers/kbfiltr_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 12   460 110 false(unreach-call) 1 wit inspect 7.6 300 true -32 wit inspect 13   450 unknown 0 wit inspect 5.0 270 error (2) 0 wit inspect .98 20 - wit inspect - wit inspect
ntdrivers/parport_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 11   470 96 false(unreach-call) 1 wit inspect 7.9 310 unknown 0 wit inspect 83   870 unknown 0 wit inspect 6.1 290 error (2) 0 wit inspect 1.8  22 - wit inspect - wit inspect
ntdrivers/cdaudio_true-unreach-call.i.cil.c true 2 wit inspect 12   480 110 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 28   660 timeout 0 wit inspect 960   2800
ntdrivers/diskperf_true-unreach-call.i.cil.c true 2 wit inspect 99   1900 1300 - wit inspect - wit inspect - wit inspect - wit inspect error 0 wit inspect 14   480 true 2 wit inspect 200   4700
ntdrivers/floppy2_true-unreach-call_true-termination.i.cil.c true 2 wit inspect 81   2000 780 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910   7000 true 2 wit inspect 570   7000
ntdrivers/floppy_true-unreach-call_true-valid-memsafety.i.cil.c true 2 wit inspect 39   920 360 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900   3200 true 2 wit inspect 740   6900
ntdrivers/parport_true-unreach-call.i.cil.c true 2 wit inspect 120   2700 1200 - wit inspect - wit inspect - wit inspect - wit inspect error 0 wit inspect 16   430 true 2 wit inspect 270   4700
ssh/s3_clnt.blast.01_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 61   2500 580 true -32 wit inspect 6.4 280 false(unreach-call) 1 wit inspect 52   670 unknown 0 wit inspect 5.2 270 error (2) 0 wit inspect .82 21 - wit inspect - wit inspect
ssh/s3_clnt.blast.02_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 63   3300 600 true -32 wit inspect 5.8 280 false(unreach-call) 1 wit inspect 40   560 unknown 0 wit inspect 5.0 270 error (2) 0 wit inspect .81 20 - wit inspect - wit inspect
ssh/s3_clnt.blast.03_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 25   1400 230 true -32 wit inspect 5.7 280 false(unreach-call) 1 wit inspect 45   610 unknown 0 wit inspect 5.2 270 error (2) 0 wit inspect .86 20 - wit inspect - wit inspect
ssh/s3_clnt.blast.04_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 61   2500 580 true -32 wit inspect 6.4 280 false(unreach-call) 1 wit inspect 40   590 unknown 0 wit inspect 5.1 270 error (2) 0 wit inspect .86 20 - wit inspect - wit inspect
ssh/s3_srvr.blast.01_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 34   1600 370 true -32 wit inspect 5.4 280 true -32 wit inspect 9.1 330 unknown 0 wit inspect 4.7 270 error (2) 0 wit inspect .97 20 - wit inspect - wit inspect
ssh/s3_srvr.blast.02_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 22   1000 210 true -32 wit inspect 6.3 280 true -32 wit inspect 9.4 330 unknown 0 wit inspect 5.9 270 error (2) 0 wit inspect .99 20 - wit inspect - wit inspect
ssh/s3_srvr.blast.03_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 26   1400 220 true -32 wit inspect 5.4 280 true -32 wit inspect 8.9 330 unknown 0 wit inspect 5.0 270 error (2) 0 wit inspect 1.0  20 - wit inspect - wit inspect
ssh/s3_srvr.blast.04_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 22   980 190 true -32 wit inspect 6.6 280 true -32 wit inspect 8.5 330 unknown 0 wit inspect 4.6 270 error (2) 0 wit inspect 1.2  20 - wit inspect - wit inspect
ssh/s3_srvr.blast.06_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 43   1300 340 true -32 wit inspect 6.8 280 true -32 wit inspect 8.5 330 unknown 0 wit inspect 4.8 270 error (2) 0 wit inspect .83 21 - wit inspect - wit inspect
ssh/s3_srvr.blast.07_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 81   3700 860 true -32 wit inspect 5.7 290 true -32 wit inspect 8.8 320 unknown 0 wit inspect 5.0 270 error (2) 0 wit inspect .83 21 - wit inspect - wit inspect
ssh/s3_srvr.blast.08_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 110   2700 870 true -32 wit inspect 8.4 290 true -32 wit inspect 7.8 330 unknown 0 wit inspect 5.2 270 error (2) 0 wit inspect .87 22 - wit inspect - wit inspect
ssh/s3_srvr.blast.09_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 79   3700 790 true -32 wit inspect 5.8 280 true -32 wit inspect 8.0 320 unknown 0 wit inspect 5.6 270 error (2) 0 wit inspect .84 22 - wit inspect - wit inspect
ssh/s3_srvr.blast.10_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 97   2700 890 true -32 wit inspect 7.0 280 true -32 wit inspect 8.2 320 unknown 0 wit inspect 6.4 270 error (2) 0 wit inspect .86 22 - wit inspect - wit inspect
ssh/s3_srvr.blast.11_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 30   1500 260 true -32 wit inspect 5.8 280 false(unreach-call) 1 wit inspect 60   630 unknown 0 wit inspect 5.9 270 error (2) 0 wit inspect .82 20 - wit inspect - wit inspect
ssh/s3_srvr.blast.12_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 44   1400 350 true -32 wit inspect 6.3 280 true -32 wit inspect 8.5 340 unknown 0 wit inspect 4.9 270 error (2) 0 wit inspect .84 21 - wit inspect - wit inspect
ssh/s3_srvr.blast.13_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 91   3700 850 true -32 wit inspect 5.8 280 true -32 wit inspect 8.3 330 unknown 0 wit inspect 4.9 270 error (2) 0 wit inspect 1.1  21 - wit inspect - wit inspect
ssh/s3_srvr.blast.14_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 39   1200 320 true -32 wit inspect 6.3 290 true -32 wit inspect 8.2 330 unknown 0 wit inspect 5.1 270 error (2) 0 wit inspect 1.0  22 - wit inspect - wit inspect
ssh/s3_srvr.blast.15_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 110   2900 1100 true -32 wit inspect 6.0 280 true -32 wit inspect 8.6 330 unknown 0 wit inspect 6.3 260 error (2) 0 wit inspect .87 22 - wit inspect - wit inspect
ssh/s3_srvr.blast.16_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 42   1100 310 true -32 wit inspect 6.8 280 true -32 wit inspect 9.7 330 unknown 0 wit inspect 5.9 270 error (2) 0 wit inspect .94 21 - wit inspect - wit inspect
ssh/s3_clnt.blast.01_true-unreach-call.i.cil.c true 1 wit inspect 170   2800 1800 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900   2200 false(unreach-call) -16 wit inspect 84   700
ssh/s3_clnt.blast.02_true-unreach-call.i.cil.c true 1 wit inspect 220   2800 2300 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900   1900 false(unreach-call) -16 wit inspect 84   720
ssh/s3_clnt.blast.03_true-unreach-call.i.cil.c true 1 wit inspect 130   2800 1400 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900   1800 false(unreach-call) -16 wit inspect 92   720
ssh/s3_clnt.blast.04_true-unreach-call.i.cil.c true 1 wit inspect 160   2800 1700 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900   1600 false(unreach-call) -16 wit inspect 91   700
ssh/s3_srvr.blast.01_true-unreach-call.i.cil.c true 1 wit inspect 150   4100 1400 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900   2000 timeout 0 wit inspect 960   5100
ssh/s3_srvr.blast.02_true-unreach-call.i.cil.c true 1 wit inspect 50   2600 500 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900   1900 timeout 0 wit inspect 960   6400
ssh/s3_srvr.blast.06_true-unreach-call.i.cil.c true 1 wit inspect 290   4400 2800 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900   2000 out of memory 0 wit inspect 710   7000
ssh/s3_srvr.blast.07_true-unreach-call.i.cil.c true 1 wit inspect 130   4100 1100 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900   2000 out of memory 0 wit inspect 530   7000
ssh/s3_srvr.blast.08_true-unreach-call.i.cil.c true 1 wit inspect 140   3900 1300 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900   1900 out of memory 0 wit inspect 650   7000
ssh/s3_srvr.blast.09_true-unreach-call.i.cil.c true 1 wit inspect 120   4100 1100 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900   2000 timeout 0 wit inspect 960   6800
ssh/s3_srvr.blast.10_true-unreach-call.i.cil.c true 1 wit inspect 130   2800 1400 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900   2100 timeout 0 wit inspect 960   5000
ssh/s3_srvr.blast.11_true-unreach-call.i.cil.c true 1 wit inspect 110   4000 1100 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900   1900 out of memory 0 wit inspect 830   7000
ssh/s3_srvr.blast.12_true-unreach-call.i.cil.c true 1 wit inspect 250   4300 2400 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900   2000 out of memory 0 wit inspect 550   7000
ssh/s3_srvr.blast.13_true-unreach-call.i.cil.c true 1 wit inspect 110   3900 1100 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900   1800 out of memory 0 wit inspect 570   7000
ssh/s3_srvr.blast.14_true-unreach-call.i.cil.c true 1 wit inspect 200   4200 1700 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900   2000 out of memory 0 wit inspect 480   7000
ssh/s3_srvr.blast.15_true-unreach-call.i.cil.c true 1 wit inspect 150   3900 1400 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900   1900 out of memory 0 wit inspect 560   7000
ssh/s3_srvr.blast.16_true-unreach-call.i.cil.c true 1 wit inspect 230   4300 2200 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900   2100 timeout 0 wit inspect 960   6600
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 108 5700 140000 58000 42 -585 270 13000 42 -520 690 17000 42 0 210 11000 42 -576 230 870 52 46 24000 93000 52 -268 14000 150000
    correct results 56 84 1900 44000 21000 23 23 160 7300 24 24 420 10000 0 0 23 46 210 7900 18 36 2400 45000
        correct true 28 56 1200 23000 14000 0 0 0 0 23 46 210 7900 18 36 2400 45000
        correct false 28 28 700 21000 7200 23 23 160 7300 24 24 420 10000 0 0 0 0
    correct-unconfimed results 38 24 3800 98000 37000 0 0 0 0 0 0
        correct-unconfirmed true 24 24 2900 69000 29000 0 0 0 0 0 0
        correct-unconfirmed false 14 0 840 29000 7700 0 0 0 0 0 0
    incorrect results 0 19 -608 120 5300 17 -544 190 6200 0 18 -576 14 350 0 19 -304 560 8900
        incorrect true 0 19 -608 120 5300 17 -544 190 6200 0 18 -576 14 350 0 0
        incorrect false 0 0 0 0 0 0 19 -304 560 8900
score (94 tasks, max score: 146) 108 -585 -520 0 -576 46 -268
Run set cpa-seq.sv-comp18.ReachSafety-ControlFlow cpa-seq-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.ReachSafety-ControlFlow uautomizer-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.ReachSafety-ControlFlow cpa-witness2test-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.ReachSafety-ControlFlow fshell-witness2test-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.ReachSafety-ControlFlow cpa-seq-validate-correctness-witnesses-cpa-seq.sv-comp18-correctness-witness.ReachSafety-ControlFlow uautomizer-validate-correctness-witnesses-cpa-seq.sv-comp18-correctness-witness.ReachSafety-ControlFlow