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/Collatz_unknown-termination_false-no-overflow.c
programSHA 24b7e10190698e4022be968650337df07e87192188ebba57e38dae7824c717c2
witnessName results-verified/pinaka.2018-12-06_2014.logfiles/sv-comp19_prop-nooverflow.Collatz_unknown-termination_false-no-overflow.c.files/witness.graphml
witnessSHA 35dc3e992373d6959df31ee6b3cacf80d8771e06cd8373fc74c19133ec1fd45f

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/35dc3e992373d6959df31ee6b3cacf80d8771e06cd8373fc74c19133ec1fd45f.json

Key Value
architecture 64bit
creationtime 2018-12-07T05:21 CET (sv-comp)
producer Pinaka
program-sha256 24b7e10190698e4022be968650337df07e87192188ebba57e38dae7824c717c2
programfile ../../sv-benchmarks/c/termination-crafted/Collatz_unknown-termination_false-no-overflow.c
programhash 24b7e10190698e4022be968650337df07e87192188ebba57e38dae7824c717c2
sourcecodelang C
specification CHECK( init(main()), LTL(G ! overflow) )
witness-file witnessFileByHash/35dc3e992373d6959df31ee6b3cacf80d8771e06cd8373fc74c19133ec1fd45f.graphml
witness-sha256 35dc3e992373d6959df31ee6b3cacf80d8771e06cd8373fc74c19133ec1fd45f
witness-size 4066
witness-type violation_witness

This witness was created for this program (cf. table above, 24b7e10190698e4022be968650337df07e87192188ebba57e38dae7824c717c2).

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

Trying to find witnesses for program (24b7e10190698e4022be968650337df07e87192188ebba57e38dae7824c717c2, sv-benchmarks/c/termination-crafted/Collatz_unknown-termination_false-no-overflow.c).

Found 0 witnesses for program sv-benchmarks/c/termination-crafted/Collatz_unknown-termination_false-no-overflow.c, 24b7e10190698e4022be968650337df07e87192188ebba57e38dae7824c717c2
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/24b7e10190698e4022be968650337df07e87192188ebba57e38dae7824c717c2.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 (24b7e10190698e4022be968650337df07e87192188ebba57e38dae7824c717c2, sv-benchmarks/c/termination-crafted/Collatz_unknown-termination_false-no-overflow.c).

Found 0 witnesses for program sv-benchmarks/c/termination-crafted/Collatz_unknown-termination_false-no-overflow.c, 24b7e10190698e4022be968650337df07e87192188ebba57e38dae7824c717c2
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/24b7e10190698e4022be968650337df07e87192188ebba57e38dae7824c717c2.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 (24b7e10190698e4022be968650337df07e87192188ebba57e38dae7824c717c2, sv-benchmarks/c/termination-crafted/Collatz_unknown-termination_false-no-overflow.c).

Found 0 witnesses for program sv-benchmarks/c/termination-crafted/Collatz_unknown-termination_false-no-overflow.c, 24b7e10190698e4022be968650337df07e87192188ebba57e38dae7824c717c2
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/24b7e10190698e4022be968650337df07e87192188ebba57e38dae7824c717c2.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 (24b7e10190698e4022be968650337df07e87192188ebba57e38dae7824c717c2, sv-benchmarks/c/termination-crafted/Collatz_unknown-termination_false-no-overflow.c).

Found 22 witnesses for program sv-benchmarks/c/termination-crafted/Collatz_unknown-termination_false-no-overflow.c, 24b7e10190698e4022be968650337df07e87192188ebba57e38dae7824c717c2
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/24b7e10190698e4022be968650337df07e87192188ebba57e38dae7824c717c2.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 09481f1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.2.1 3 2020-12-06T23:30:39
Download daa6e56 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Symbiotic 2 2020-12-11T20:52:42
Download 9473cde Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Symbiotic 2 2020-12-08T17:15:27
Download 65b8173 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Pinaka 4 2020-12-08T09:47:14
Download a0b34ae Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0 5 2020-12-12T01:24:56+01:00 Download daa6e56
Download 458cd3e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0 5 2020-12-09T22:12:37+01:00 Download 10eb093
Download 4db6730 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0 5 2020-12-09T21:28:16+01:00 Download cf66a1c
Download 30cc386 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0 5 2020-12-09T03:58:13+01:00 Download 9473cde
Download 05427cc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0 5 2020-12-09T02:33:29+01:00 Download 8af8082
Download 8d35bd5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0 5 2020-12-08T13:36:27+01:00 Download 65b8173
Download 5db509c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0 5 2020-12-08T07:34:42+01:00 Download d82e4d1
Download d0e99c7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0 5 2020-12-07T16:43:30+01:00 Download 718c057
Download 53224b7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0 5 2020-12-07T00:15:56+01:00 Download 09481f1
Download 209ee61 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0 5 2020-12-06T19:02:02+01:00 Download 29c670e
Download c3a1ea8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0 5 2020-12-06T18:27:34+01:00 Download a05bbc8
Download f34fc00 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0 5 2020-12-06T18:01:46+01:00 Download 42a481c
Download 08f1ee3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0 5 2020-12-06T10:33:14+01:00 Download 29c670e
Download 3720bb6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0 5 2020-12-06T07:28:24+01:00 Download a05bbc8
Download fa47024 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0 5 2020-12-05T18:36:17+01:00 Download 42a481c
Download 42a481c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0 5 2020-12-05T12:23:51+01:00
Download d82e4d1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0.1-svn-eda176372c+ 5 2020-12-08T05:36:25+01:00
Download d4a36dc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) unknown_witness Goblint (svcomp21-0-g82e03b87) 3 2020-12-07T12:05:42

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

Trying to find witnesses for program (24b7e10190698e4022be968650337df07e87192188ebba57e38dae7824c717c2, sv-benchmarks/c/termination-crafted/Collatz_unknown-termination_false-no-overflow.c).

Found 15 witnesses for program sv-benchmarks/c/termination-crafted/Collatz_unknown-termination_false-no-overflow.c, 24b7e10190698e4022be968650337df07e87192188ebba57e38dae7824c717c2
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/24b7e10190698e4022be968650337df07e87192188ebba57e38dae7824c717c2.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download d8e3294 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Symbiotic 1 2019-12-01 19:03:31
Download 11c0e67 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Pinaka 4 2019-12-03T23:13 CET (comp)
Download 327fdd3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 5 2019-12-11T21:56:18+01:00 Download 4735e13
Download 8b35adf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 5 2019-12-11T21:54:43+01:00 Download c5b6966
Download 774ec6c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 5 2019-12-11T21:09:43+01:00 Download d8e3294
Download 9eca9b1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 5 2019-12-11T20:44:26+01:00 Download 7dbeaa6
Download 52c1184 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 5 2019-12-08T00:26:31+01:00 Download 8cd6142
Download a0c92b7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 5 2019-12-07T21:14:49+01:00 Download ae4a18e
Download 8671bd8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 5 2019-12-05T20:20:14+01:00 Download abcb88b
Download faaa88c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 5 2019-12-05T19:34:31+01:00 Download b5616f6
Download f565af6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 5 2019-12-04T02:58:16+01:00 Download 11c0e67
Download cdc5ab7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 5 2019-12-03T08:09:51+01:00 Download e64bcbd
Download e64bcbd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 5 2019-11-29T20:06:33+01:00
Download c5b6966 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ 5 2019-11-30T22:59:12+01:00
Download dbcec30 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.9 5 2019-12-11T20:54:28+01:00 Download c54b378

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

Trying to find witnesses for program (24b7e10190698e4022be968650337df07e87192188ebba57e38dae7824c717c2, sv-benchmarks/c/termination-crafted/Collatz_unknown-termination_false-no-overflow.c).

Found 18 witnesses for program sv-benchmarks/c/termination-crafted/Collatz_unknown-termination_false-no-overflow.c, 24b7e10190698e4022be968650337df07e87192188ebba57e38dae7824c717c2
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/24b7e10190698e4022be968650337df07e87192188ebba57e38dae7824c717c2.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 70ba256 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Symbiotic 1 2018-12-08T12:19 CET (sv-comp)
Download 28e428d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness SMACK 1.9.3 4 2018-12-08T10:31:59
Download 35dc3e9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Pinaka 4 2018-12-07T05:21 CET (sv-comp)
Download e01c4e1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 5 2018-12-07T22:06:12+01:00
Download e76a457 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-09T20:53:25+01:00 Download ec4a792
Download 015d877 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-09T20:34:34+01:00 Download 7c6f49f
Download 18366ce Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-09T20:27:59+01:00 Download 8b62663
Download a00c6e9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-09T18:10:34+01:00 Download 638369d
Download 6cb51d4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-08T23:43:44+01:00 Download 70ba256
Download ff2ff81 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-08T22:10:20+01:00 Download 28e428d
Download 5bffa0c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-08T09:00:50+01:00 Download e01c4e1
Download fdbb49d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-08T05:04:03+01:00 Download a238485
Download 25262aa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-07T17:45:04+01:00 Download 35dc3e9
Download 33245ee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:48:03+01:00 Download c1e9e16
Download 2c3dd23 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:40:29+01:00 Download 666d772
Download bcf5a6c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:19:44+01:00 Download ffcce33
Download 2cb44f8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:19:02+01:00 Download cc06db6
Download c1e9e16 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-05T16:38:21+01:00

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

Trying to find witnesses for program (24b7e10190698e4022be968650337df07e87192188ebba57e38dae7824c717c2, sv-benchmarks/c/termination-crafted/Collatz_unknown-termination_false-no-overflow.c).

Found 19 witnesses for program sv-benchmarks/c/termination-crafted/Collatz_unknown-termination_false-no-overflow.c, 24b7e10190698e4022be968650337df07e87192188ebba57e38dae7824c717c2
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/24b7e10190698e4022be968650337df07e87192188ebba57e38dae7824c717c2.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 4808eff Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Taipan 4 2017-12-03T07:43Z
Download 103df6f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Symbiotic 1 2017-12-03T04:33 CET (sv-comp)
Download ea623ea Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Map2Check 2 2017-12-02T01:42 CET (sv-comp)
Download 64f5ccd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Kojak 4 2017-12-03T10:34Z
Download cd83077 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-02T18:44:52.122476
Download 4b6e517 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness ESBMC 4.6.0 incr 4 2017-12-02T06:54:17.160923
Download 154a4d8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T11:53:00+01:00 aca57a7
Download 8dd1ce4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T11:52:11+01:00 b716c9d
Download 347d5a7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T08:58:56+01:00 b2084a8
Download 2ba57fb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T05:14:26+01:00 51b9c82
Download cf82f88 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 6 2017-12-02T20:09:36+01:00 931375b
Download 8d3549f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 5 2017-12-02T08:12:25+01:00 4d1b332
Download 0389384 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T12:33:27+01:00 87d7ca7
Download 6fda113 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T12:02:40+01:00 287b19a
Download 0e35aac Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T11:19:12+01:00 c6e44c0
Download edfd1b7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T10:56:47+01:00
Download 626da7b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CBMC 4 2017-12-01T11:39 CET (sv-comp)
Download 4ab067e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Automizer 4 2017-12-03T10:26Z
Download 666d772 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness 2LS 4 2017-12-01T10:57 CET (sv-comp)

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

Trying to find witnesses for program (24b7e10190698e4022be968650337df07e87192188ebba57e38dae7824c717c2, sv-benchmarks/c/termination-crafted/Collatz_unknown-termination_false-no-overflow.c).

Found 0 witnesses for program sv-benchmarks/c/termination-crafted/Collatz_unknown-termination_false-no-overflow.c, 24b7e10190698e4022be968650337df07e87192188ebba57e38dae7824c717c2
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/24b7e10190698e4022be968650337df07e87192188ebba57e38dae7824c717c2.json

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