Tool VeriAbs 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* [apollon020; apollon077; apollon078; apollon084; apollon149; apollon164] apollon* [apollon037; apollon065; apollon077; apollon078; apollon155; apollon159] 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 18:04:04 CET 2017-12-03 04:46:33 CET 2017-12-03 06:08:30 CET 2017-12-03 06:21:09 CET 2017-12-03 06:27:12 CET 2017-12-03 03:55:53 CET 2017-12-03 04:55:47 CET
Run set veriabs.sv-comp18.ReachSafety-ControlFlow cpa-seq-validate-violation-witnesses-veriabs.sv-comp18-violation-witness.ReachSafety-ControlFlow uautomizer-validate-violation-witnesses-veriabs.sv-comp18-violation-witness.ReachSafety-ControlFlow cpa-witness2test-validate-violation-witnesses-veriabs.sv-comp18-violation-witness.ReachSafety-ControlFlow fshell-witness2test-validate-violation-witnesses-veriabs.sv-comp18-violation-witness.ReachSafety-ControlFlow cpa-seq-validate-correctness-witnesses-veriabs.sv-comp18-correctness-witness.ReachSafety-ControlFlow uautomizer-validate-correctness-witnesses-veriabs.sv-comp18-correctness-witness.ReachSafety-ControlFlow
Options -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/veriabs.2017-12-02_1804.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/veriabs.2017-12-02_1804.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/veriabs.2017-12-02_1804.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/veriabs.2017-12-02_1804.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/veriabs.2017-12-02_1804.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/veriabs.2017-12-02_1804.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 error 0 wit inspect 200 830 2100 error (invalid witness file) 0 wit inspect .57 42 error (2) 0 wit inspect .023 4.9 error (invalid witness file) 0 wit inspect .64 49 error (invalid witness file) 0 wit inspect .0012 .32 - wit inspect - wit inspect
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c false(unreach-call) 1 wit inspect 270 370 3400 false(unreach-call) 1 wit inspect 5.3  280 false(unreach-call) 1 wit inspect 9.7   380   unknown 0 wit inspect 2.8  220 false(unreach-call) 1 wit inspect .75   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 270 390 2900 false(unreach-call) 1 wit inspect 8.1  270 false(unreach-call) 1 wit inspect 11     430   unknown 0 wit inspect 4.5  260 false(unreach-call) 1 wit inspect .82   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 260 340 3000 false(unreach-call) 1 wit inspect 5.0  280 false(unreach-call) 1 wit inspect 7.9   350   unknown 0 wit inspect 2.7  220 false(unreach-call) 1 wit inspect .76   19    - wit inspect - wit inspect
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c error 0 wit inspect 200 840 1400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .018 4.9
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c unknown 0 wit inspect 890 670 8500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 42 error (2) 0 wit inspect .018 4.9
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 280 510 2700 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 10    330 true 2 wit inspect 190     1700  
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 280 610 2900 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.9  360 true 2 wit inspect 190     2200  
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 260 350 2500 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.7  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 270 450 3700 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.5  270 true 2 wit inspect 18     520  
ssh-simplified/s3_clnt_1_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 58 440 670 false(unreach-call) 1 wit inspect 3.8  280 false(unreach-call) 1 wit inspect 8.6   370   unknown 0 wit inspect 4.2  220 false(unreach-call) 1 wit inspect .75   20    - wit inspect - wit inspect
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 61 450 610 false(unreach-call) 1 wit inspect 5.4  280 false(unreach-call) 1 wit inspect 7.8   370   unknown 0 wit inspect 4.4  230 false(unreach-call) 1 wit inspect .73   20    - wit inspect - wit inspect
ssh-simplified/s3_clnt_3_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 62 490 650 false(unreach-call) 1 wit inspect 5.8  290 false(unreach-call) 1 wit inspect 9.0   370   unknown 0 wit inspect 4.3  220 true -32 wit inspect .75   20    - wit inspect - wit inspect
ssh-simplified/s3_clnt_4_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 60 450 630 false(unreach-call) 1 wit inspect 5.7  290 false(unreach-call) 1 wit inspect 8.2   370   unknown 0 wit inspect 2.9  230 true -32 wit inspect .76   20    - wit inspect - wit inspect
ssh-simplified/s3_srvr_10_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 92 720 1100 false(unreach-call) 1 wit inspect 4.7  270 false(unreach-call) 1 wit inspect 7.7   340   unknown 0 wit inspect 2.5  220 false(unreach-call) 1 wit inspect .72   19    - wit inspect - wit inspect
ssh-simplified/s3_srvr_11_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 360 910 4300 true -32 wit inspect 4.0  290 false(unreach-call) 1 wit inspect 11     600   unknown 0 wit inspect 3.3  280 false(unreach-call) 1 wit inspect .76   20    - wit inspect - wit inspect
ssh-simplified/s3_srvr_12_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 240 1000 3500 false(unreach-call) 1 wit inspect 5.9  290 false(unreach-call) 1 wit inspect 10     430   unknown 0 wit inspect 3.2  230 true -32 wit inspect .76   21    - wit inspect - wit inspect
ssh-simplified/s3_srvr_13_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 120 920 1300 false(unreach-call) 1 wit inspect 3.2  280 false(unreach-call) 1 wit inspect 9.6   390   unknown 0 wit inspect 4.3  220 true -32 wit inspect .76   20    - wit inspect - wit inspect
ssh-simplified/s3_srvr_14_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 120 900 1200 false(unreach-call) 1 wit inspect 4.4  270 false(unreach-call) 1 wit inspect 8.3   350   unknown 0 wit inspect 3.7  220 false(unreach-call) 1 wit inspect .73   20    - wit inspect - wit inspect
ssh-simplified/s3_srvr_1_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 110 840 1300 false(unreach-call) 1 wit inspect 5.5  280 false(unreach-call) 1 wit inspect 9.4   390   unknown 0 wit inspect 4.0  220 false(unreach-call) 1 wit inspect .74   20    - wit inspect - wit inspect
ssh-simplified/s3_srvr_2_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 110 830 1400 false(unreach-call) 1 wit inspect 3.4  280 false(unreach-call) 1 wit inspect 9.1   400   unknown 0 wit inspect 4.3  220 false(unreach-call) 1 wit inspect .74   20    - wit inspect - wit inspect
ssh-simplified/s3_srvr_6_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 120 940 1300 false(unreach-call) 1 wit inspect 2.8  270 false(unreach-call) 1 wit inspect 8.3   320   unknown 0 wit inspect 3.8  210 false(unreach-call) 1 wit inspect .74   19    - wit inspect - wit inspect
ssh-simplified/s3_clnt_1_true-unreach-call_true-termination.cil.c true 1 wit inspect 95 640 1000 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 10    290 false(unreach-call) -16 wit inspect 4.7   310  
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c true 1 wit inspect 94 660 950 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 8.7  290 false(unreach-call) -16 wit inspect 6.8   300  
ssh-simplified/s3_clnt_3_true-unreach-call_true-termination.cil.c true 1 wit inspect 100 700 1100 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 11    290 false(unreach-call) -16 wit inspect 7.4   310  
ssh-simplified/s3_clnt_4_true-unreach-call_true-termination.cil.c true 1 wit inspect 96 640 1200 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 9.0  290 false(unreach-call) -16 wit inspect 6.9   300  
ssh-simplified/s3_srvr_1_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900 1400 5100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 41 error (2) 0 wit inspect .019 5.0
ssh-simplified/s3_srvr_1a_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900 2800 5400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 41 error (2) 0 wit inspect .018 4.9
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 860 1800 4500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 44 error (2) 0 wit inspect .019 4.8
ssh-simplified/s3_srvr_2_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900 1500 5400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 42 error (2) 0 wit inspect .022 5.0
ssh-simplified/s3_srvr_3_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900 1500 5300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 44 error (2) 0 wit inspect .019 4.9
ssh-simplified/s3_srvr_4_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900 1500 5600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .018 4.8
ssh-simplified/s3_srvr_6_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900 1700 7200 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 41 error (2) 0 wit inspect .023 4.9
ssh-simplified/s3_srvr_7_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900 1600 5200 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .49 43 error (2) 0 wit inspect .018 4.9
ssh-simplified/s3_srvr_8_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900 1600 5600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .019 4.8
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c false(unreach-call) 1 wit inspect 27 290 230 false(unreach-call) 1 wit inspect 4.3  290 false(unreach-call) 1 wit inspect 6.3   280   unknown 0 wit inspect 2.3  220 false(unreach-call) 1 wit inspect .67   19    - wit inspect - wit inspect
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c false(unreach-call) 1 wit inspect 29 280 270 false(unreach-call) 1 wit inspect 4.3  270 false(unreach-call) 1 wit inspect 7.5   300   unknown 0 wit inspect 3.6  220 false(unreach-call) 1 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 18 310 170 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.4  290 false(unreach-call) -16 wit inspect 5.6   270  
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 19 320 150 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.0  300 false(unreach-call) -16 wit inspect 5.5   260  
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 20 310 170 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.5  300 false(unreach-call) -16 wit inspect 5.8   270  
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 21 340 180 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.9  300 false(unreach-call) -16 wit inspect 5.9   280  
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 21 300 200 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0  310 false(unreach-call) -16 wit inspect 5.8   270  
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 24 370 220 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.7  310 false(unreach-call) -16 wit inspect 5.4   270  
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 14 290 120 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.0  280 false(unreach-call) -16 wit inspect 5.2   250  
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 15 320 120 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.9  280 false(unreach-call) -16 wit inspect 5.2   250  
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 15 300 120 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.5  300 false(unreach-call) -16 wit inspect 3.7   260  
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 17 320 160 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.8  290 false(unreach-call) -16 wit inspect 5.6   260  
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 17 290 130 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.7  290 false(unreach-call) -16 wit inspect 5.2   260  
ntdrivers/cdaudio_false-unreach-call.i.cil.c unknown 0 wit inspect 74 360 570 error (invalid witness file) 0 wit inspect .39 41 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .65 49 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect - wit inspect
ntdrivers/diskperf_false-unreach-call.i.cil.c unknown 0 wit inspect 55 320 430 error (invalid witness file) 0 wit inspect .58 41 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .67 49 error (invalid witness file) 0 wit inspect .0012 .27 - wit inspect - wit inspect
ntdrivers/floppy_false-unreach-call.i.cil.c unknown 0 wit inspect 80 360 640 error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .67 49 error (invalid witness file) 0 wit inspect .0016 .29 - wit inspect - wit inspect
ntdrivers/kbfiltr_false-unreach-call.i.cil.c unknown 0 wit inspect 37 280 290 error (invalid witness file) 0 wit inspect .60 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .84 47 error (invalid witness file) 0 wit inspect .0010 .26 - wit inspect - wit inspect
ntdrivers/parport_false-unreach-call.i.cil.c unknown 0 wit inspect 520 2500 5000 error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .021 4.9 error (invalid witness file) 0 wit inspect .65 49 error (invalid witness file) 0 wit inspect .0018 .30 - wit inspect - wit inspect
ntdrivers/cdaudio_true-unreach-call.i.cil.c unknown 0 wit inspect 78 370 610 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .018 4.9
ntdrivers/diskperf_true-unreach-call.i.cil.c unknown 0 wit inspect 740 2300 6400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .019 4.9
ntdrivers/floppy2_true-unreach-call_true-termination.i.cil.c unknown 0 wit inspect 150 1300 1300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 41 error (2) 0 wit inspect .018 4.8
ntdrivers/floppy_true-unreach-call_true-valid-memsafety.i.cil.c unknown 0 wit inspect 79 390 670 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .018 4.8
ntdrivers/parport_true-unreach-call.i.cil.c unknown 0 wit inspect 530 2500 3800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .019 4.9
ssh/s3_clnt.blast.01_false-unreach-call.i.cil.c unknown 0 wit inspect 720 1600 6000 error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .023 4.9 error (invalid witness file) 0 wit inspect .86 51 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
ssh/s3_clnt.blast.02_false-unreach-call.i.cil.c timeout 0 wit inspect 900 9700 9300 error (invalid witness file) 0 wit inspect .61 42 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .65 50 error (invalid witness file) 0 wit inspect .0017 .27 - wit inspect - wit inspect
ssh/s3_clnt.blast.03_false-unreach-call.i.cil.c timeout 0 wit inspect 900 9700 9200 error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .017 4.9 error (invalid witness file) 0 wit inspect .82 47 error (invalid witness file) 0 wit inspect .0011 .34 - wit inspect - wit inspect
ssh/s3_clnt.blast.04_false-unreach-call.i.cil.c timeout 0 wit inspect 900 9700 9900 error (invalid witness file) 0 wit inspect .41 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .65 49 error (invalid witness file) 0 wit inspect .0012 .34 - wit inspect - wit inspect
ssh/s3_srvr.blast.01_false-unreach-call.i.cil.c timeout 0 wit inspect 900 2100 9300 error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .69 53 error (invalid witness file) 0 wit inspect .0013 .29 - wit inspect - wit inspect
ssh/s3_srvr.blast.02_false-unreach-call.i.cil.c timeout 0 wit inspect 900 2000 9300 error (invalid witness file) 0 wit inspect .83 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .66 49 error (invalid witness file) 0 wit inspect .0025 .29 - wit inspect - wit inspect
ssh/s3_srvr.blast.03_false-unreach-call.i.cil.c timeout 0 wit inspect 900 2100 8400 error (invalid witness file) 0 wit inspect .41 41 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .68 49 error (invalid witness file) 0 wit inspect .0013 .29 - wit inspect - wit inspect
ssh/s3_srvr.blast.04_false-unreach-call.i.cil.c timeout 0 wit inspect 900 2000 8400 error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .67 51 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect - wit inspect
ssh/s3_srvr.blast.06_false-unreach-call.i.cil.c timeout 0 wit inspect 900 2100 9800 error (invalid witness file) 0 wit inspect .41 43 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .67 49 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect - wit inspect
ssh/s3_srvr.blast.07_false-unreach-call.i.cil.c timeout 0 wit inspect 900 1800 7800 error (invalid witness file) 0 wit inspect .40 44 error (2) 0 wit inspect .020 5.0 error (invalid witness file) 0 wit inspect .85 50 error (invalid witness file) 0 wit inspect .0012 .29 - wit inspect - wit inspect
ssh/s3_srvr.blast.08_false-unreach-call.i.cil.c timeout 0 wit inspect 900 1900 8000 error (invalid witness file) 0 wit inspect .41 41 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .84 47 error (invalid witness file) 0 wit inspect .0018 .29 - wit inspect - wit inspect
ssh/s3_srvr.blast.09_false-unreach-call.i.cil.c timeout 0 wit inspect 900 2100 8700 error (invalid witness file) 0 wit inspect .40 43 error (2) 0 wit inspect .024 4.9 error (invalid witness file) 0 wit inspect .67 50 error (invalid witness file) 0 wit inspect .0018 .32 - wit inspect - wit inspect
ssh/s3_srvr.blast.10_false-unreach-call.i.cil.c timeout 0 wit inspect 900 2000 7300 error (invalid witness file) 0 wit inspect .71 44 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect .79 47 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect - wit inspect
ssh/s3_srvr.blast.11_false-unreach-call.i.cil.c timeout 0 wit inspect 900 2100 9300 error (invalid witness file) 0 wit inspect .43 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .65 49 error (invalid witness file) 0 wit inspect .0017 .29 - wit inspect - wit inspect
ssh/s3_srvr.blast.12_false-unreach-call.i.cil.c timeout 0 wit inspect 900 2100 7200 error (invalid witness file) 0 wit inspect .65 44 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .80 47 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
ssh/s3_srvr.blast.13_false-unreach-call.i.cil.c timeout 0 wit inspect 900 1800 11000 error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .82 47 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect - wit inspect
ssh/s3_srvr.blast.14_false-unreach-call.i.cil.c timeout 0 wit inspect 900 2100 7300 error (invalid witness file) 0 wit inspect .40 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .83 49 error (invalid witness file) 0 wit inspect .0018 .26 - wit inspect - wit inspect
ssh/s3_srvr.blast.15_false-unreach-call.i.cil.c timeout 0 wit inspect 900 2400 8200 error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .84 47 error (invalid witness file) 0 wit inspect .0014 .27 - wit inspect - wit inspect
ssh/s3_srvr.blast.16_false-unreach-call.i.cil.c timeout 0 wit inspect 900 1900 7300 error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .85 49 error (invalid witness file) 0 wit inspect .0012 .34 - wit inspect - wit inspect
ssh/s3_clnt.blast.01_true-unreach-call.i.cil.c unknown 0 wit inspect 650 1700 5900 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .020 4.9
ssh/s3_clnt.blast.02_true-unreach-call.i.cil.c timeout 0 wit inspect 900 9800 8700 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 44 error (2) 0 wit inspect .019 4.8
ssh/s3_clnt.blast.03_true-unreach-call.i.cil.c timeout 0 wit inspect 900 9700 8400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .41 43 error (2) 0 wit inspect .023 4.8
ssh/s3_clnt.blast.04_true-unreach-call.i.cil.c timeout 0 wit inspect 900 9800 9000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 42 error (2) 0 wit inspect .019 4.8
ssh/s3_srvr.blast.01_true-unreach-call.i.cil.c timeout 0 wit inspect 900 2000 8000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 44 error (2) 0 wit inspect .021 4.8
ssh/s3_srvr.blast.02_true-unreach-call.i.cil.c timeout 0 wit inspect 900 2100 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .021 5.0
ssh/s3_srvr.blast.06_true-unreach-call.i.cil.c timeout 0 wit inspect 900 1800 9000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 45 error (2) 0 wit inspect .018 4.9
ssh/s3_srvr.blast.07_true-unreach-call.i.cil.c timeout 0 wit inspect 900 2000 8800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 42 error (2) 0 wit inspect .022 4.8
ssh/s3_srvr.blast.08_true-unreach-call.i.cil.c timeout 0 wit inspect 900 2100 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 41 error (2) 0 wit inspect .018 4.9
ssh/s3_srvr.blast.09_true-unreach-call.i.cil.c timeout 0 wit inspect 900 1900 7700 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .018 4.9
ssh/s3_srvr.blast.10_true-unreach-call.i.cil.c timeout 0 wit inspect 900 1800 8200 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .019 4.9
ssh/s3_srvr.blast.11_true-unreach-call.i.cil.c timeout 0 wit inspect 900 2000 9600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .73 45 error (2) 0 wit inspect .019 4.8
ssh/s3_srvr.blast.12_true-unreach-call.i.cil.c timeout 0 wit inspect 900 2000 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .019 4.9
ssh/s3_srvr.blast.13_true-unreach-call.i.cil.c timeout 0 wit inspect 900 2100 8600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .019 4.9
ssh/s3_srvr.blast.14_true-unreach-call.i.cil.c timeout 0 wit inspect 900 1700 9800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .018 4.9
ssh/s3_srvr.blast.15_true-unreach-call.i.cil.c timeout 0 wit inspect 900 2000 8200 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .019 4.9
ssh/s3_srvr.blast.16_true-unreach-call.i.cil.c timeout 0 wit inspect 900 2600 8400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 44 error (2) 0 wit inspect .021 4.8
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 51 48000 170000 440000 42 -16 95   5800 42 17 150 6600 42 0 79 5100 42 -115 13   340 52 30 160 7100 52 -232 510 9200
    correct results 32 47 3700 16000 41000 16 16 78   4500 17 17 150 6400 0 13 13 9.6 260 15 30 100 4500 4 8 420 5000
        correct true 15 30 1300 5400 14000 0 0 0 0 15 30 100 4500 4 8 420 5000
        correct false 17 17 2400 11000 28000 16 16 78   4500 17 17 150 6400 0 13 13 9.6 260 0 0
    correct-unconfimed results 4 4 380 2600 4200 0 0 0 0 0 0
        correct-unconfirmed true 4 4 380 2600 4200 0 0 0 0 0 0
        correct-unconfirmed false 0 0 0 0 0 0 0
    incorrect results 0 1 -32 4.0 290 0 0 4 -128 3.0 81 0 15 -240 85 4100
        incorrect true 0 1 -32 4.0 290 0 0 4 -128 3.0 81 0 0
        incorrect false 0 0 0 0 0 0 15 -240 85 4100
score (94 tasks, max score: 146) 51 -16 17 0 -115 30 -232
Run set veriabs.sv-comp18.ReachSafety-ControlFlow cpa-seq-validate-violation-witnesses-veriabs.sv-comp18-violation-witness.ReachSafety-ControlFlow uautomizer-validate-violation-witnesses-veriabs.sv-comp18-violation-witness.ReachSafety-ControlFlow cpa-witness2test-validate-violation-witnesses-veriabs.sv-comp18-violation-witness.ReachSafety-ControlFlow fshell-witness2test-validate-violation-witnesses-veriabs.sv-comp18-violation-witness.ReachSafety-ControlFlow cpa-seq-validate-correctness-witnesses-veriabs.sv-comp18-correctness-witness.ReachSafety-ControlFlow uautomizer-validate-correctness-witnesses-veriabs.sv-comp18-correctness-witness.ReachSafety-ControlFlow