Witness Inspection

A description of this web service can be found in the CAV paper "Verification-Aided Debugging: An Interactive Web-Service for Exploring Error Witnesses" (more material).

View and Validate the Witness

Input Given to this Service about the Witness (URL Query)

Key Value
programName sv-benchmarks/c/forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i
programSHA 85bd663c92282d4dfdefb34d4d1bb2e7b23df33069d11197ed5810f4ac1a16c6
witnessName results-verified/map2check.2017-12-01_1946.logfiles/sv-comp18.dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i.files/witness.graphml
witnessSHA 8476adc4c70ef8fffc507869ee462588f5eb8891348589c574336eab9e09238f

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/8476adc4c70ef8fffc507869ee462588f5eb8891348589c574336eab9e09238f.json

Key Value
architecture 32bit
creationtime 2017-12-01T21:30 CET (sv-comp)
producer Map2Check
program-sha256 85bd663c92282d4dfdefb34d4d1bb2e7b23df33069d11197ed5810f4ac1a16c6
programfile ../../sv-benchmarks/c/forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i
programhash b9633ec6dc7e01a7231c1be5ed310faef61ba6b0
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/8476adc4c70ef8fffc507869ee462588f5eb8891348589c574336eab9e09238f.graphml
witness-sha256 8476adc4c70ef8fffc507869ee462588f5eb8891348589c574336eab9e09238f
witness-size 2920
witness-type violation_witness

Available Results for the Program from Witness Store SV-COMP '24

Trying to find witnesses for program (85bd663c92282d4dfdefb34d4d1bb2e7b23df33069d11197ed5810f4ac1a16c6, sv-benchmarks/c/forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i).

Found 0 witnesses for program sv-benchmarks/c/forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i, 85bd663c92282d4dfdefb34d4d1bb2e7b23df33069d11197ed5810f4ac1a16c6
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/85bd663c92282d4dfdefb34d4d1bb2e7b23df33069d11197ed5810f4ac1a16c6.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness

Available Results for the Program from Witness Store SV-COMP '23

Trying to find witnesses for program (85bd663c92282d4dfdefb34d4d1bb2e7b23df33069d11197ed5810f4ac1a16c6, sv-benchmarks/c/forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i).

Found 0 witnesses for program sv-benchmarks/c/forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i, 85bd663c92282d4dfdefb34d4d1bb2e7b23df33069d11197ed5810f4ac1a16c6
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/85bd663c92282d4dfdefb34d4d1bb2e7b23df33069d11197ed5810f4ac1a16c6.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness

Available Results for the Program from Witness Store SV-COMP '22

Trying to find witnesses for program (85bd663c92282d4dfdefb34d4d1bb2e7b23df33069d11197ed5810f4ac1a16c6, sv-benchmarks/c/forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i).

Found 0 witnesses for program sv-benchmarks/c/forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i, 85bd663c92282d4dfdefb34d4d1bb2e7b23df33069d11197ed5810f4ac1a16c6
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/85bd663c92282d4dfdefb34d4d1bb2e7b23df33069d11197ed5810f4ac1a16c6.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness

Available Results for the Program from Witness Store SV-COMP '21

Trying to find witnesses for program (85bd663c92282d4dfdefb34d4d1bb2e7b23df33069d11197ed5810f4ac1a16c6, sv-benchmarks/c/forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i).

Found 0 witnesses for program sv-benchmarks/c/forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i, 85bd663c92282d4dfdefb34d4d1bb2e7b23df33069d11197ed5810f4ac1a16c6
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/85bd663c92282d4dfdefb34d4d1bb2e7b23df33069d11197ed5810f4ac1a16c6.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness

Available Results for the Program from Witness Store SV-COMP '20

Trying to find witnesses for program (85bd663c92282d4dfdefb34d4d1bb2e7b23df33069d11197ed5810f4ac1a16c6, sv-benchmarks/c/forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i).

Found 25 witnesses for program sv-benchmarks/c/forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i, 85bd663c92282d4dfdefb34d4d1bb2e7b23df33069d11197ed5810f4ac1a16c6
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/85bd663c92282d4dfdefb34d4d1bb2e7b23df33069d11197ed5810f4ac1a16c6.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 90b018c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2019-12-01 22:04:24
Download 2e2d86c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 10 2019-12-11T21:09:16+01:00 Download 90b018c
Download d97ab2b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 9 2019-12-08T00:06:16+01:00 Download 3a8430a
Download d7c1103 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.9 9 2019-12-06T02:38:43+01:00 Download be2d70c
Download 52303d5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.9 13 2019-12-11T21:59:42+01:00 Download c8100dc
Download 2adf800 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.9 13 2019-12-05T20:21:08+01:00 Download 02f3248
Download 06c5040 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.9 13 2019-12-03T08:10:32+01:00 Download cf8d0eb
Download c8100dc Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ 13 2019-12-01T09:51:38+01:00
Download cf8d0eb Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 1.9 13 2019-11-30T11:22:15+01:00
Download 139a4b8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.9 13 2019-12-11T20:56:02+01:00 Download f9fdd9a
Download cabe433 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2019-12-01 15:31:15
Download 02059e8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 21 2019-12-11T21:43:24+01:00 Download 37ff597
Download a5361df Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 21 2019-12-11T21:41:05+01:00 Download 73d7f94
Download d83d7ae Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 29 2019-12-11T20:54:23+01:00 Download b93996c
Download 7b13d43 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 21 2019-12-08T00:07:40+01:00 Download d6e7f22
Download 6b12ce3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 21 2019-12-07T21:17:31+01:00 Download 5601f78
Download 1be42dc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 21 2019-12-03T08:09:04+01:00 Download cf038ac
Download cf038ac Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 18 2019-11-30T13:53:56+01:00
Download 2160057 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8 8 2019-12-07T10:31:31+01:00
Download 73d7f94 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 18 2019-11-30T22:54:49+01:00
Download 9d4ba55 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 13 2019-12-11T21:09:30+01:00 Download cabe433
Download 90546ba Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 13 2019-12-11T20:45:49+01:00 Download 7b4d187
Download 8155bbf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 13 2019-12-08T01:51:18+01:00 Download 2160057
Download f58adb6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 13 2019-12-05T20:21:44+01:00 Download ed86d1d
Download f883f65 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 13 2019-12-03T08:56:48+01:00 Download cb1e80f

Available Results for the Program from Witness Store SV-COMP '19

Trying to find witnesses for program (85bd663c92282d4dfdefb34d4d1bb2e7b23df33069d11197ed5810f4ac1a16c6, sv-benchmarks/c/forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i).

Found 28 witnesses for program sv-benchmarks/c/forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i, 85bd663c92282d4dfdefb34d4d1bb2e7b23df33069d11197ed5810f4ac1a16c6
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/85bd663c92282d4dfdefb34d4d1bb2e7b23df33069d11197ed5810f4ac1a16c6.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 629c89a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2018-12-08T08:03 CET (sv-comp)
Download 82eb977 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-08T23:44:42+01:00 Download 629c89a
Download 97d28b5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 13 2018-12-08T04:24:31+01:00
Download 2f577f0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.7-svn 29852 13 2018-12-08T05:04:39+01:00 Download f2d3710
Download 0ded626 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.7-svn 29852 13 2018-12-06T09:20:57+01:00 Download 6eb00da
Download 86a767f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) violation_witness CPAchecker 1.7-svn 29852 14 2018-12-07T09:18:23+01:00 Download ae84a1b
Download 1d96055 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-07T01:23:20+01:00 Download d897e66
Download 8bafc0f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.7-svn 29852 13 2018-12-06T10:19:22+01:00 Download ff91600
Download efa487e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T13:35 CET (sv-comp)
Download e5381a6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 3 2018-12-08T02:06:59
Download e73a503 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7 8 2018-12-10T18:57:09+01:00
Download d0fdba2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 17 2018-12-07T13:48:58+01:00
Download cf27cd5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 20 2018-12-09T20:39:26+01:00 Download 7adfa9a
Download 440787a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 20 2018-12-09T20:21:18+01:00 Download 6fc70f4
Download 8ed62ce Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 20 2018-12-08T08:39:43+01:00 Download d0fdba2
Download 37bc56e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 20 2018-12-08T05:00:42+01:00 Download 9aab333
Download 58d9995 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 20 2018-12-07T09:15:22+01:00 Download e495841
Download 4286ad4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 20 2018-12-06T10:13:58+01:00 Download 02f8b43
Download 7e78e0b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 20 2018-12-06T09:48:00+01:00 Download 3e16c87
Download 48f8e44 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 20 2018-12-06T09:20:29+01:00 Download 6261554
Download 3e16c87 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 17 2018-12-06T07:03:48+01:00
Download f9e1a81 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 13 2018-12-10T20:38:15+01:00 Download e73a503
Download 5ba71ce Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 13 2018-12-10T10:48:46+01:00 Download 9b29995
Download c54cb8e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 13 2018-12-09T18:22:11+01:00 Download f0b2711
Download 205784f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 13 2018-12-08T23:42:47+01:00 Download efa487e
Download 79d5dd6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 13 2018-12-08T22:10:14+01:00 Download e5381a6
Download 594160b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 13 2018-12-08T04:18:53+01:00 Download 9b29995
Download a03b48c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 13 2018-12-07T01:15:18+01:00 Download 89214ee

Available Results for the Program from Witness Store SV-COMP '18

Trying to find witnesses for program (85bd663c92282d4dfdefb34d4d1bb2e7b23df33069d11197ed5810f4ac1a16c6, sv-benchmarks/c/forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i).

Found 21 witnesses for program sv-benchmarks/c/forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i, 85bd663c92282d4dfdefb34d4d1bb2e7b23df33069d11197ed5810f4ac1a16c6
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/85bd663c92282d4dfdefb34d4d1bb2e7b23df33069d11197ed5810f4ac1a16c6.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 47f82d5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Symbiotic 1 2017-12-02T23:58 CET (sv-comp)
Download ae84a1b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness PredatorHP 5 2017-12-01T22:01 CET (sv-comp)
Download b2dbc3c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Map2Check 2 2017-12-01T23:20 CET (sv-comp)
Download 33c4eaf Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 4.6.0 kind 5 2017-12-02T10:34:29.192989
Download 332b311 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 4.6.0 incr 5 2017-12-01T23:14:57.149614
Download 909804e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) violation_witness ESBMC 3.1 4 2017-12-01T09:09 CET (sv-comp)
Download 4c84ed8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness Forester 10 2017-12-01T19:33 CET (sv-comp)
Download acd2cdd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) violation_witness CBMC 14 2017-12-01T08:28 CET (sv-comp)
Download 0e6dbd6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T10:16 CET (sv-comp)
Download e495841 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness PredatorHP 5 2017-12-01T20:26 CET (sv-comp)
Download 8476adc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Map2Check 3 2017-12-01T21:30 CET (sv-comp)
Download 07072af Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Kojak 17 2017-12-02T08:56Z
Download 6e99233 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Forester 10 2017-12-01T18:13 CET (sv-comp)
Download 997de13 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 7 2017-12-01T12:13:58.295261
Download de5b0d6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 7 2017-12-01T09:02:39.967676
Download a3aed1c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 4 2017-11-30T22:35 CET (sv-comp)
Download b3e991d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 16 2017-11-30T20:15:09+01:00
Download 402059e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 4 2017-11-30T17:38:01+01:00
Download aab3594 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 2 2017-12-01T02:32:23+01:00
Download 9b3c35d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 14 2017-11-30T20:07 CET (sv-comp)
Download a18cbf8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 17 2017-12-02T03:59Z

Available Results for the Program from Witness Store SV-COMP '17

Trying to find witnesses for program (85bd663c92282d4dfdefb34d4d1bb2e7b23df33069d11197ed5810f4ac1a16c6, sv-benchmarks/c/forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i).

Found 0 witnesses for program sv-benchmarks/c/forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i, 85bd663c92282d4dfdefb34d4d1bb2e7b23df33069d11197ed5810f4ac1a16c6
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/85bd663c92282d4dfdefb34d4d1bb2e7b23df33069d11197ed5810f4ac1a16c6.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness