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/termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow_true-termination_true-valid-memsafety.c
programSHA cad2c6f6e8ebe2adcd550e4a56b83be37e52f812ae33bfb645236c6925734dbf
witnessName results-verified/2ls.2017-12-01_1141.logfiles/sv-comp18.Arrays01-EquivalentConstantIndices_true-no-overflow_true-termination_true-valid-memsafety.c.files/witness.graphml
witnessSHA 61309e82d048ca12b25b7ce9ae627d0660e4a703800f2b36c413c65184418d57

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/61309e82d048ca12b25b7ce9ae627d0660e4a703800f2b36c413c65184418d57.json

Key Value
architecture 64bit
creationtime 2017-12-01T12:48 CET (sv-comp)
producer 2LS
program-sha256 cad2c6f6e8ebe2adcd550e4a56b83be37e52f812ae33bfb645236c6925734dbf
programfile ../../sv-benchmarks/c/termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow_true-termination_true-valid-memsafety.c
programhash cf39454d83b4ec00341bd0b620b0fa6b2321ce21
sourcecodelang C
specification CHECK( init(main()), LTL(F end) )
witness-file witnessFileByHash/61309e82d048ca12b25b7ce9ae627d0660e4a703800f2b36c413c65184418d57.graphml
witness-sha256 61309e82d048ca12b25b7ce9ae627d0660e4a703800f2b36c413c65184418d57
witness-size 8630
witness-type correctness_witness

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

Trying to find witnesses for program (cad2c6f6e8ebe2adcd550e4a56b83be37e52f812ae33bfb645236c6925734dbf, sv-benchmarks/c/termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow_true-termination_true-valid-memsafety.c).

Found 33 witnesses for program sv-benchmarks/c/termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow_true-termination_true-valid-memsafety.c, cad2c6f6e8ebe2adcd550e4a56b83be37e52f812ae33bfb645236c6925734dbf
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/cad2c6f6e8ebe2adcd550e4a56b83be37e52f812ae33bfb645236c6925734dbf.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download c1fe10e Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2023-12-18T09:58:01+01:00
Download 7ef2006 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 3 2023-12-17T02:18:34Z
Download 3d70d0e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 3 2023-11-29T21:14:07Z
Download 8dd2036 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.3 35 2023-12-18T12:06:02+01:00 Download c1fe10e
Download 23ee0e9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.3 5 2023-11-30T05:56:54+01:00
Download a1b91ac Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2.1-svn-e677b7cd46+ 5 2023-12-04T00:15:12+01:00
Download 9d83651 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 8 2023-12-02T12:35:29Z
Download 425f820 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-29T14:05:15Z
Download 398419b 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) 30 2023-12-01T00:58:48Z
Download 293ee63 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 8 2023-11-28T23:37:00Z
Download 7dd27a9 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 2LS 13 2023-11-30T23:06:59+01:00
Download ac3db25 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 5 2023-12-18T18:35:52+01:00
Download ff2c3a1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness frama-c-sv version 0.4.0 3 2023-12-03T06:22:10Z
Download 7cd6470 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness VeriOover 1 2023-12-20T03:37 CET (comp)
Download fc522a5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Mopsa (v1.0~pre2) 3 2023-11-29T08:53:41Z
Download 8a91786 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Goblint (tags/svcomp24-0-gc2e9465a7) 30 2023-12-01T01:00:01Z
Download 9169bd5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-20T03:41:15+01:00 Download 7cd6470
Download 2909dbb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-19T15:12:20+01:00 Download 5cc5889
Download c901722 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-19T03:42:38+01:00 Download 840a425
Download b4f9bcf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-17T06:10:16+01:00 Download 7a1686a
Download f97bd71 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-04T01:45:32+01:00 Download 434edfa
Download 889d74b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-03T09:54:16+01:00 Download ff2c3a1
Download d0e9420 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-01T03:51:18+01:00 Download 8a91786
Download af444b2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-01T00:00:30+01:00 Download 2233046
Download 6c69fd8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-11-30T12:43:43+01:00 Download e7b06a6
Download e7b06a6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-11-30T07:02:12+01:00
Download 2f96e20 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-11-29T18:26:12+01:00 Download fc522a5
Download 434edfa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-e677b7cd46+ 5 2023-12-03T18:08:00+01:00
Download 7a1686a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2023-12-17T02:05:43+01:00
Download 840a425 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 5 2023-12-18T17:09:34+01:00
Download 2233046 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness 2LS 11 2023-11-30T20:42:05+01:00
Download 8c30400 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 9 2023-11-30T21:06:54+01:00
Download 9b7d5fc Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: "2.0" uuid: fc0490c4-d0a5-48ab-affe-b0cc011b44f3 creation_time: 2023-12-01T01:00:01Z producer: name: Goblint version: tags/svcomp24-0-gc2e9465a7 command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--sets'' ''ana.specification'' ''../../sv-benchmarks/c/properties/no-overflow.prp'' ''--sets'' ''exp.architecture'' ''64bit'' ''../../sv-benchmarks/c/termination-crafted/Arrays01-EquivalentConstantIndices-1.c''' task: input_files: - ../../sv-benchmarks/c/termination-crafted/Arrays01-EquivalentConstantIndices-1.c input_file_hashes: ../../sv-benchmarks/c/termination-crafted/Arrays01-EquivalentConstantIndices-1.c: cad2c6f6e8ebe2adcd550e4a56b83be37e52f812ae33bfb645236c6925734dbf data_model: LP64 language: C specification: CHECK( init(main()), LTL(G ! overflow) ) content: - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-crafted/Arrays01-EquivalentConstantIndices-1.c file_hash: cad2c6f6e8ebe2adcd550e4a56b83be37e52f812ae33bfb645236c6925734dbf line: 13 column: 6 function: main value: ((((((((8 <= i && i <= 1048) || i == 7) || i == 6) || i == 5) || i == 4) || i == 3) || i == 2) || i == 1) || (0 == i && i == 0) format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-crafted/Arrays01-EquivalentConstantIndices-1.c file_hash: cad2c6f6e8ebe2adcd550e4a56b83be37e52f812ae33bfb645236c6925734dbf line: 17 column: 8 function: main value: i == 1048 format: c_expression correctness_witness CPAchecker 2.3 7 2023-12-01T05:37:14+01:00

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

Trying to find witnesses for program (cad2c6f6e8ebe2adcd550e4a56b83be37e52f812ae33bfb645236c6925734dbf, sv-benchmarks/c/termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow_true-termination_true-valid-memsafety.c).

Found 31 witnesses for program sv-benchmarks/c/termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow_true-termination_true-valid-memsafety.c, cad2c6f6e8ebe2adcd550e4a56b83be37e52f812ae33bfb645236c6925734dbf
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/cad2c6f6e8ebe2adcd550e4a56b83be37e52f812ae33bfb645236c6925734dbf.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 1731f89 Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2022-12-09T06:23:22+01:00
Download f150d8c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 3 2022-12-25T11:08:50Z
Download cd53e59 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 3 2022-12-12T12:27:46Z
Download 2d26b51 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 35 2023-01-28T14:20:54+01:00 Download 1731f89
Download b9e59af Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 5 2022-12-10T20:14:34+01:00
Download b9c19cb Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2.1-svn-1715bd67dc+ 5 2022-12-12T00:24:50+01:00
Download e3747f4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 5 2022-12-10T04:36:51+01:00
Download 7153c14 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 8 2022-12-14T07:44:43Z
Download eaed2c5 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-11T12:31:19Z
Download 598caed 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 7 2022-12-13T10:13:34Z
Download 94bf827 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 2LS 13 2022-12-08T00:24:54+01:00
Download 3163648 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 2 2023-01-28T22:25:56+01:00 Download 536019e
Download 2667f88 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness frama-c-sv version 0.4.0 3 2022-12-09T10:32:28Z
Download 7cd6470 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness VeriOover 1 2022-12-12T11:01 CET (comp)
Download 19ce9d3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Mopsa (v1.0~pre2) 3 2022-12-11T09:39:45Z
Download 536019e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Goblint (tags/svcomp23-0-g4f5dcf38f) 39 2022-12-10T06:57:10Z
Download 1abfc70 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T11:32:10+01:00 Download 7cd6470
Download c26d9c1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T03:45:55+01:00 Download 19ce9d3
Download 65b6a17 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T02:33:09+01:00 Download a5cbe97
Download 90accd2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T00:12:54+01:00 Download c9209b3
Download 1ee7c46 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T18:01:17+01:00 Download 35cb181
Download 7182058 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T17:38:33+01:00 Download 2667f88
Download 0561ca3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T11:23:31+01:00 Download 59f7595
Download 898a403 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T00:31:08+01:00 Download 8fc4ff7
Download 31b528d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-27T23:00:49+01:00 Download 06907d8
Download 59f7595 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2022-12-10T21:53:39+01:00
Download a5cbe97 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-1715bd67dc+ 5 2022-12-11T20:44:41+01:00
Download 8fc4ff7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2022-12-25T12:50:31+01:00
Download 35cb181 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 5 2022-12-10T01:36:39+01:00
Download 06907d8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness 2LS 11 2022-12-08T00:51:42+01:00
Download 834ec52 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 9 2022-12-07T22:13:08+01:00

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

Trying to find witnesses for program (cad2c6f6e8ebe2adcd550e4a56b83be37e52f812ae33bfb645236c6925734dbf, sv-benchmarks/c/termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow_true-termination_true-valid-memsafety.c).

Found 22 witnesses for program sv-benchmarks/c/termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow_true-termination_true-valid-memsafety.c, cad2c6f6e8ebe2adcd550e4a56b83be37e52f812ae33bfb645236c6925734dbf
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/cad2c6f6e8ebe2adcd550e4a56b83be37e52f812ae33bfb645236c6925734dbf.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 7cfaefb Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2021-12-07T10:14:49+01:00
Download 5af532d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 3 2021-12-07T14:49:59Z
Download 1c4bba1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.1 5 2021-12-05T17:46:49+01:00
Download f3b0d17 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-fe6f522dd3+ 5 2021-12-08T18:20:27+01:00
Download 9921a3e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-eda176372c+ 5 2021-12-09T15:05:09+01:00
Download 716b705 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 8 2021-12-09T23:09:04Z
Download 65a0c67 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 7 2021-12-06T23:11:24Z
Download 4eb2d60 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 2LS 13 2021-12-05T19:48:49+01:00
Download 18b83e7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness SESL 2 2021-12-06T11:15:46+01:00
Download ed4b7a1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness frama-c-sv version 0.2.8 3 2021-12-13T19:58:07Z
Download 3791e9a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2021-12-14T00:15:29+01:00 Download ed4b7a1
Download 0fbb538 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2021-12-10T20:56:10+01:00 Download b456437
Download fc603ef Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2021-12-09T15:37:46+01:00 Download e1bd19b
Download 38af62a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2021-12-08T21:28:35+01:00 Download e86fca1
Download a3f463d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2021-12-06T01:17:57+01:00 Download f748a45
Download bcc0437 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2021-12-05T20:10:14+01:00 Download 892ebe4
Download 892ebe4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2021-12-05T18:06:05+01:00
Download b456437 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 5 2021-12-10T17:09:58+01:00
Download e86fca1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-fe6f522dd3+ 5 2021-12-08T20:16:32+01:00
Download e1bd19b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-eda176372c+ 5 2021-12-09T09:47:17+01:00
Download f748a45 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness 2LS 11 2021-12-06T00:32:54+01:00
Download 968d295 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 8 2021-12-05T23:51:12+01:00

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

Trying to find witnesses for program (cad2c6f6e8ebe2adcd550e4a56b83be37e52f812ae33bfb645236c6925734dbf, sv-benchmarks/c/termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow_true-termination_true-valid-memsafety.c).

Found 11 witnesses for program sv-benchmarks/c/termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow_true-termination_true-valid-memsafety.c, cad2c6f6e8ebe2adcd550e4a56b83be37e52f812ae33bfb645236c6925734dbf
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/cad2c6f6e8ebe2adcd550e4a56b83be37e52f812ae33bfb645236c6925734dbf.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 383bdab Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2020-12-06T18:33:18+01:00
Download abbc4fb Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0 5 2020-12-05T15:11:51+01:00
Download 1ea008c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-eda176372c+ 5 2020-12-08T05:20:49+01:00
Download 9a4b4f1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.2.1 3 2020-12-06T23:34:45
Download 13652a0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) unknown_witness Goblint (svcomp21-0-g82e03b87) 3 2020-12-07T15:10:24
Download e8b2d75 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 5 2020-12-09T02:00:34+01:00 Download f771411
Download 6dd22f7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 5 2020-12-08T06:20:12+01:00 Download a74ec41
Download 7dbdd79 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 5 2020-12-06T16:51:29+01:00 Download 22468cd
Download 9c348d6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 5 2020-12-06T13:12:48+01:00 Download b56f0c3
Download b56f0c3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 5 2020-12-05T14:51:30+01:00
Download a74ec41 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-eda176372c+ 5 2020-12-07T22:27:34+01:00

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

Trying to find witnesses for program (cad2c6f6e8ebe2adcd550e4a56b83be37e52f812ae33bfb645236c6925734dbf, sv-benchmarks/c/termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow_true-termination_true-valid-memsafety.c).

Found 4 witnesses for program sv-benchmarks/c/termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow_true-termination_true-valid-memsafety.c, cad2c6f6e8ebe2adcd550e4a56b83be37e52f812ae33bfb645236c6925734dbf
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/cad2c6f6e8ebe2adcd550e4a56b83be37e52f812ae33bfb645236c6925734dbf.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download e628268 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 1.9 5 2019-11-30T14:46:10+01:00
Download 1de3328 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ 5 2019-12-01T00:23:32+01:00
Download 4c1cece Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.9 5 2019-11-29T14:49:46+01:00
Download 7478511 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ 5 2019-12-01T01:40:51+01:00

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

Trying to find witnesses for program (cad2c6f6e8ebe2adcd550e4a56b83be37e52f812ae33bfb645236c6925734dbf, sv-benchmarks/c/termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow_true-termination_true-valid-memsafety.c).

Found 3 witnesses for program sv-benchmarks/c/termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow_true-termination_true-valid-memsafety.c, cad2c6f6e8ebe2adcd550e4a56b83be37e52f812ae33bfb645236c6925734dbf
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/cad2c6f6e8ebe2adcd550e4a56b83be37e52f812ae33bfb645236c6925734dbf.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 1a7f6bf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 5 2018-12-07T15:44:55+01:00
Download c781436 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-05T09:32:38+01:00
Download c7cfd95 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T16:46 CET (sv-comp)

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

Trying to find witnesses for program (cad2c6f6e8ebe2adcd550e4a56b83be37e52f812ae33bfb645236c6925734dbf, sv-benchmarks/c/termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow_true-termination_true-valid-memsafety.c).

Found 6 witnesses for program sv-benchmarks/c/termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow_true-termination_true-valid-memsafety.c, cad2c6f6e8ebe2adcd550e4a56b83be37e52f812ae33bfb645236c6925734dbf
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/cad2c6f6e8ebe2adcd550e4a56b83be37e52f812ae33bfb645236c6925734dbf.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 1bf4d73 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-02T18:38:14.329247
Download 0afe287 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T11:08:45+01:00
Download 8d8ce2c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 6 2017-12-03T10:36Z
Download b7894f8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness 2LS 9 2017-12-01T10:22 CET (sv-comp)
Download 1a4dfe7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 5 2017-12-01T18:10 CET (sv-comp)
Download 61309e8 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 9 2017-12-01T12:48 CET (sv-comp)

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

Trying to find witnesses for program (cad2c6f6e8ebe2adcd550e4a56b83be37e52f812ae33bfb645236c6925734dbf, sv-benchmarks/c/termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow_true-termination_true-valid-memsafety.c).

Found 0 witnesses for program sv-benchmarks/c/termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow_true-termination_true-valid-memsafety.c, cad2c6f6e8ebe2adcd550e4a56b83be37e52f812ae33bfb645236c6925734dbf
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/cad2c6f6e8ebe2adcd550e4a56b83be37e52f812ae33bfb645236c6925734dbf.json

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