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).

This link does not point to a witness, but below is a list of witnesses for the same program.

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

Trying to find witnesses for program (efd89e7b390064d688e1eebb599a77ec99587f4751caf8bf660f2bf53e476dd2, sv-benchmarks/c/ldv-memsafety/memsetNonZero_true-valid-memsafety_true-termination.c).

Found 27 witnesses for program sv-benchmarks/c/ldv-memsafety/memsetNonZero_true-valid-memsafety_true-termination.c, efd89e7b390064d688e1eebb599a77ec99587f4751caf8bf660f2bf53e476dd2
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/efd89e7b390064d688e1eebb599a77ec99587f4751caf8bf660f2bf53e476dd2.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download c8ddd42 Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2023-12-18T08:50:39+01:00
Download 2d28818 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 3 2023-11-29T22:19:49Z
Download 072575b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.3 3 2023-12-18T12:07:03+01:00 Download c8ddd42
Download 76758d0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.3 3 2023-11-30T04:42:52+01:00
Download 037adb1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2.1-svn-e677b7cd46+ 3 2023-12-03T22:56:46+01:00
Download 747e408 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 3 2023-12-18T18:39:56+01:00
Download 9a6c32f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-38892M 3 2023-12-18T02:06:07+01:00
Download 1b3372d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Bubaak 3 2023-12-05T08:14:10Z
Download cd75c32 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Bubaak 3 2023-12-04T09:09:00Z
Download 82fc488 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Bubaak 3 2023-12-01T19:40:25Z
Download 5049c26 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) correctness_witness ESBMC 7.4.0 incr 3 2023-12-01T10:52:13Z
Download e29cffe Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 2.0 3 2023-12-19T14:03:00+01:00
Download 64c95b0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Taipan 5 2023-12-02T11:36:25Z
Download 41bb3ed Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness PredatorHP 4 2023-11-30T08:25:22Z
Download 5b36bfa Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Mopsa (v1.0~pre2) 3 2023-11-29T12:06:55Z
Download 63f8c18 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Kojak 5 2023-12-02T22:08:33Z
Download 95d748e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Goblint (tags/svcomp24-0-gc2e9465a7) 4 2023-12-01T01:18:52Z
Download 715d2b2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CBMC 4 2023-12-17T21:05:28+01:00
Download db3a6da Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Automizer 5 2023-11-29T00:51:02Z
Download 9ea7a10 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 7.4.0 3 2023-12-01T16:16:05Z
Download 8c44450 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 3 2023-12-17T00:46:49Z
Download c68967c Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 3 2023-11-30T00:31:04Z
Download 049edf3 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Goblint (tags/svcomp24-0-gc2e9465a7) 3 2023-12-01T01:43:45Z
Download aad0d5d Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 4 2023-12-17T18:43:26+01:00
Download 1ae3a45 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Bubaak 3 2023-12-05T09:34:09Z
Download c4ae03c Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Bubaak 3 2023-12-04T14:30:21Z
Download 0cb1379 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Bubaak 3 2023-12-01T21:11:27Z

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

Trying to find witnesses for program (efd89e7b390064d688e1eebb599a77ec99587f4751caf8bf660f2bf53e476dd2, sv-benchmarks/c/ldv-memsafety/memsetNonZero_true-valid-memsafety_true-termination.c).

Found 21 witnesses for program sv-benchmarks/c/ldv-memsafety/memsetNonZero_true-valid-memsafety_true-termination.c, efd89e7b390064d688e1eebb599a77ec99587f4751caf8bf660f2bf53e476dd2
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/efd89e7b390064d688e1eebb599a77ec99587f4751caf8bf660f2bf53e476dd2.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download faf0bc3 Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2022-12-09T06:44:25+01:00
Download 6575f69 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 3 2023-01-28T14:17:52+01:00 Download faf0bc3
Download e1a2496 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 3 2022-12-10T21:12:45+01:00
Download 3cd4709 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2.1-svn-1715bd67dc+ 3 2022-12-12T00:39:54+01:00
Download 1e070e4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0 3 2022-12-11T04:04:26+01:00
Download 12ad3e2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-38892M 3 2022-12-09T02:34:26+01:00
Download a4e08b2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Bubaak 3 2022-12-08T16:06:25Z
Download d1c82ab Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) correctness_witness ESBMC 7.0.0 incr 3 2022-12-18T22:19:23Z
Download c517c55 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) correctness_witness ESBMC 6.8.0 incr 3 2022-12-25T10:08:05Z
Download bd08312 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Taipan 4 2022-12-14T04:34:31Z
Download 63cf041 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Mopsa (v1.0~pre2) 3 2022-12-11T11:07:58Z
Download 055ef87 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Kojak 4 2022-12-15T01:29:01Z
Download 728b8e7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CBMC 4 2022-12-08T10:27:26+01:00
Download 83196bf Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Automizer 4 2022-12-13T21:30:49Z
Download f949d9a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 3 2022-12-10T04:36:21+01:00
Download fea142c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(reach_error())) ) correctness_witness ESBMC 6.8.0 3 2022-12-25T09:46:01Z
Download 926a2af Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 7.0.0 3 2022-12-18T22:03:12Z
Download 6052541 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 3 2022-12-25T09:46:01Z
Download 3b6e69a Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 3 2022-12-12T17:43:18Z
Download 2898130 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 4 2022-12-08T04:36:44+01:00
Download f90dd46 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Bubaak 2 2022-12-08T14:25:54Z

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

Trying to find witnesses for program (efd89e7b390064d688e1eebb599a77ec99587f4751caf8bf660f2bf53e476dd2, sv-benchmarks/c/ldv-memsafety/memsetNonZero_true-valid-memsafety_true-termination.c).

Found 14 witnesses for program sv-benchmarks/c/ldv-memsafety/memsetNonZero_true-valid-memsafety_true-termination.c, efd89e7b390064d688e1eebb599a77ec99587f4751caf8bf660f2bf53e476dd2
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/efd89e7b390064d688e1eebb599a77ec99587f4751caf8bf660f2bf53e476dd2.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 3f03b7b Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2021-12-07T09:26:54+01:00
Download 09f2ca3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.1 3 2021-12-05T15:19:04+01:00
Download 08a21bd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-eda176372c+ 3 2021-12-09T14:52:26+01:00
Download 304a1f4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-38892M 3 2021-12-07T02:27:19+01:00
Download ed499d1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) correctness_witness ESBMC 6.8.0 incr 3 2021-12-08T11:24:21Z
Download 85df973 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 2.0.1-svn-fe6f522dd3+ 3 2021-12-08T18:27:37+01:00
Download a7695e4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Taipan 4 2021-12-10T02:26:56Z
Download ac77a6a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Kojak 4 2021-12-10T07:27:23Z
Download 1454ac0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CBMC 4 2021-12-06T07:23:23+01:00
Download 7ca846a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Automizer 4 2021-12-06T18:30:45Z
Download 586d20c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(reach_error())) ) correctness_witness ESBMC 6.8.0 3 2021-12-08T11:16:44Z
Download 4f995d0 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 2 2021-12-10T18:19:40
Download 4bc69fa Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 3 2021-12-07T14:26:21Z
Download 29e8e88 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 4 2021-12-06T03:25:55+01:00

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

Trying to find witnesses for program (efd89e7b390064d688e1eebb599a77ec99587f4751caf8bf660f2bf53e476dd2, sv-benchmarks/c/ldv-memsafety/memsetNonZero_true-valid-memsafety_true-termination.c).

Found 5 witnesses for program sv-benchmarks/c/ldv-memsafety/memsetNonZero_true-valid-memsafety_true-termination.c, efd89e7b390064d688e1eebb599a77ec99587f4751caf8bf660f2bf53e476dd2
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/efd89e7b390064d688e1eebb599a77ec99587f4751caf8bf660f2bf53e476dd2.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 8c6a0bd Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2020-12-06T18:24:05+01:00
Download 709a594 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-eda176372c+ 3 2020-12-08T04:41:33+01:00
Download c356d89 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 2.0 3 2020-12-05T12:51:24+01:00
Download 18bede1 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 2 2020-12-11T14:38:21
Download 82f4110 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 2 2020-12-08T16:29:36

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

Trying to find witnesses for program (efd89e7b390064d688e1eebb599a77ec99587f4751caf8bf660f2bf53e476dd2, sv-benchmarks/c/ldv-memsafety/memsetNonZero_true-valid-memsafety_true-termination.c).

Found 2 witnesses for program sv-benchmarks/c/ldv-memsafety/memsetNonZero_true-valid-memsafety_true-termination.c, efd89e7b390064d688e1eebb599a77ec99587f4751caf8bf660f2bf53e476dd2
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/efd89e7b390064d688e1eebb599a77ec99587f4751caf8bf660f2bf53e476dd2.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download a0c6a64 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.9 3 2019-11-30T06:31:23+01:00
Download adf15fb Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ 3 2019-12-01T07:32:26+01:00

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

Trying to find witnesses for program (efd89e7b390064d688e1eebb599a77ec99587f4751caf8bf660f2bf53e476dd2, sv-benchmarks/c/ldv-memsafety/memsetNonZero_true-valid-memsafety_true-termination.c).

Found 4 witnesses for program sv-benchmarks/c/ldv-memsafety/memsetNonZero_true-valid-memsafety_true-termination.c, efd89e7b390064d688e1eebb599a77ec99587f4751caf8bf660f2bf53e476dd2
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/efd89e7b390064d688e1eebb599a77ec99587f4751caf8bf660f2bf53e476dd2.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download cefd13d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 1 2018-12-08T01:11 CET (sv-comp)
Download f1c407e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 3 2018-12-07T05:45:28+01:00
Download 569d410 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.7-svn 29852 3 2018-12-05T18:58:22+01:00
Download 78ff63e Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T10:09 CET (sv-comp)

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

Trying to find witnesses for program (efd89e7b390064d688e1eebb599a77ec99587f4751caf8bf660f2bf53e476dd2, sv-benchmarks/c/ldv-memsafety/memsetNonZero_true-valid-memsafety_true-termination.c).

Found 14 witnesses for program sv-benchmarks/c/ldv-memsafety/memsetNonZero_true-valid-memsafety_true-termination.c, efd89e7b390064d688e1eebb599a77ec99587f4751caf8bf660f2bf53e476dd2
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/efd89e7b390064d688e1eebb599a77ec99587f4751caf8bf660f2bf53e476dd2.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download b3a555a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 1 2017-12-02T23:53 CET (sv-comp)
Download 8e237e5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.6.1-svn 4 2017-12-01T09:23:48+01:00
Download e593c6a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.6.1-svn 26773 3 2017-12-01T08:28:15+01:00
Download 1c4587b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-02T10:49:15.983281
Download 6a75300 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-01T23:02:57.994638
Download d41c666 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Taipan 4 2017-12-03T06:53Z
Download 2aab8cc Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Map2Check 2 2017-12-01T23:46 CET (sv-comp)
Download 5a05052 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Kojak 3 2017-12-03T04:24Z
Download 503a12c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CBMC 4 2017-12-01T08:26 CET (sv-comp)
Download 73568d5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Automizer 4 2017-12-03T04:18Z
Download edcac80 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T22:00:13.369984
Download c823622 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T09:13:10.539481
Download 740cd98 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 5 2017-12-01T15:43 CET (sv-comp)
Download 7183ebe Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 3 2017-12-01T15:22 CET (sv-comp)

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

Trying to find witnesses for program (efd89e7b390064d688e1eebb599a77ec99587f4751caf8bf660f2bf53e476dd2, sv-benchmarks/c/ldv-memsafety/memsetNonZero_true-valid-memsafety_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/ldv-memsafety/memsetNonZero_true-valid-memsafety_true-termination.c, efd89e7b390064d688e1eebb599a77ec99587f4751caf8bf660f2bf53e476dd2
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/efd89e7b390064d688e1eebb599a77ec99587f4751caf8bf660f2bf53e476dd2.json

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