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/recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c
programSHA 47f2e219cca1845e93995805a47abde03d96fdb8abce7bb0dc45093de4fb0653
witnessName results-verified/symbiotic.2017-12-01_2241.logfiles/sv-comp18.BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c.files/witness.graphml
witnessSHA e8b49e21894c0568120bff51f2e0271f872d62a116a2ae686eb2aa1aa2b300b4

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2017-12-02T17:14 CET (sv-comp)
producer Symbiotic
program-sha256 47f2e219cca1845e93995805a47abde03d96fdb8abce7bb0dc45093de4fb0653
programfile /tmp/vcloud-vcloud-master/worker/working_dir_68647ab9-5223-4d3d-bc46-a22c00438f65/sv-benchmarks/c/recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c
programhash ccae6f392e1d87c0b193f39dee91a5c51306cb93
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/e8b49e21894c0568120bff51f2e0271f872d62a116a2ae686eb2aa1aa2b300b4.graphml
witness-sha256 e8b49e21894c0568120bff51f2e0271f872d62a116a2ae686eb2aa1aa2b300b4
witness-size 1318
witness-type violation_witness

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

Trying to find witnesses for program (47f2e219cca1845e93995805a47abde03d96fdb8abce7bb0dc45093de4fb0653, sv-benchmarks/c/recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c, 47f2e219cca1845e93995805a47abde03d96fdb8abce7bb0dc45093de4fb0653
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/47f2e219cca1845e93995805a47abde03d96fdb8abce7bb0dc45093de4fb0653.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 (47f2e219cca1845e93995805a47abde03d96fdb8abce7bb0dc45093de4fb0653, sv-benchmarks/c/recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c, 47f2e219cca1845e93995805a47abde03d96fdb8abce7bb0dc45093de4fb0653
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/47f2e219cca1845e93995805a47abde03d96fdb8abce7bb0dc45093de4fb0653.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 (47f2e219cca1845e93995805a47abde03d96fdb8abce7bb0dc45093de4fb0653, sv-benchmarks/c/recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c, 47f2e219cca1845e93995805a47abde03d96fdb8abce7bb0dc45093de4fb0653
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/47f2e219cca1845e93995805a47abde03d96fdb8abce7bb0dc45093de4fb0653.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 (47f2e219cca1845e93995805a47abde03d96fdb8abce7bb0dc45093de4fb0653, sv-benchmarks/c/recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c, 47f2e219cca1845e93995805a47abde03d96fdb8abce7bb0dc45093de4fb0653
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/47f2e219cca1845e93995805a47abde03d96fdb8abce7bb0dc45093de4fb0653.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 (47f2e219cca1845e93995805a47abde03d96fdb8abce7bb0dc45093de4fb0653, sv-benchmarks/c/recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c).

Found 20 witnesses for program sv-benchmarks/c/recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c, 47f2e219cca1845e93995805a47abde03d96fdb8abce7bb0dc45093de4fb0653
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/47f2e219cca1845e93995805a47abde03d96fdb8abce7bb0dc45093de4fb0653.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download bb4703f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Pinaka 3 2019-12-03T22:56 CET (comp)
Download e1b257e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.9 5 2019-11-30T10:04:21+01:00
Download d09bb82 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ 5 2019-12-01T00:14:07+01:00
Download 416ed5e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2019-12-01 04:34:02
Download ddb28ec Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 7 2019-12-03T23:16 CET (comp)
Download 5efe0a0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 7 2019-12-11T21:43:42+01:00 Download 4dc56fe
Download 3ff84e3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 7 2019-12-11T21:09:26+01:00 Download 416ed5e
Download d0df5c3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 7 2019-12-11T20:44:46+01:00 Download 492b4db
Download d15aba3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 7 2019-12-06T02:41:15+01:00 Download 9bd49b9
Download c9945df Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 7 2019-12-03T08:56:50+01:00 Download f3c8863
Download ed938ab Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 7 2019-12-03T08:18:56+01:00 Download c4f232b
Download c4f232b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 7 2019-11-30T12:10:34+01:00
Download 4dc56fe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 7 2019-12-01T04:40:16+01:00
Download 842b622 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-11T21:41:19+01:00 Download 6ebabd0
Download 2586c4a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-11T20:54:26+01:00 Download e26aa2b
Download bf2e1b4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-08T00:26:01+01:00 Download 1b08fe4
Download 5845ad0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-07T21:17:45+01:00 Download 8ac6bb6
Download 0e83771 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-05T20:21:28+01:00 Download 9464f29
Download 8c00ab1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-04T02:58:25+01:00 Download ddb28ec
Download f6c3596 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-04T01:04 CET (comp)

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

Trying to find witnesses for program (47f2e219cca1845e93995805a47abde03d96fdb8abce7bb0dc45093de4fb0653, sv-benchmarks/c/recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c).

Found 29 witnesses for program sv-benchmarks/c/recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c, 47f2e219cca1845e93995805a47abde03d96fdb8abce7bb0dc45093de4fb0653
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/47f2e219cca1845e93995805a47abde03d96fdb8abce7bb0dc45093de4fb0653.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 4552ef1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 1 2018-12-08T14:01 CET (sv-comp)
Download 42c6648 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness SMACK 1.9.3 3 2018-12-08T10:05:21
Download 514b5cb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Pinaka 3 2018-12-07T12:11 CET (sv-comp)
Download df512bc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 5 2018-12-06T20:07:17+01:00
Download c265c10 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-05T22:40:24+01:00
Download c4d1d99 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T03:19 CET (sv-comp)
Download 396f883 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 4 2018-12-08T10:44:53
Download 48e1f05 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 8 2018-12-07T01:23 CET (sv-comp)
Download c4f2034 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 9 2018-12-07T13:29:11+01:00
Download af1881d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-09T18:20:40+01:00 Download 9ecfa51
Download 632fc45 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-08T23:44:07+01:00 Download c4d1d99
Download ea4cfe5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-08T03:55:13+01:00 Download 0c762cf
Download 09422ce Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-07T18:47:52+01:00 Download 6f30640
Download 75eccca Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-07T01:19:19+01:00 Download bf8c8d8
Download c47d0b4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-06T09:47:59+01:00 Download 37c28c2
Download 37c28c2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-06T01:07:03+01:00
Download 313482a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-09T21:23:32+01:00 Download 516bae5
Download 5d05cae Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-09T20:53:11+01:00 Download 77792d5
Download 9d4f423 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-09T20:35:48+01:00 Download 43c0953
Download 3b4231e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-09T20:19:45+01:00 Download 1c65e3f
Download 34ad9de Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-08T22:11:18+01:00 Download 396f883
Download 15f4fea Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-08T07:59:57+01:00 Download c4f2034
Download ccb5cae Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-08T05:05:26+01:00 Download 0c7e497
Download 1048504 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-07T17:45:05+01:00 Download 48e1f05
Download 6323725 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T10:17:52+01:00 Download 8ccd368
Download 96bff51 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:19:59+01:00 Download 39ad82f
Download 7c52966 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:07:05+01:00 Download fac5db6
Download 54e3497 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T20:40 CET (sv-comp)
Download ab0e769 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T13:20 CET (sv-comp)

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

Trying to find witnesses for program (47f2e219cca1845e93995805a47abde03d96fdb8abce7bb0dc45093de4fb0653, sv-benchmarks/c/recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c).

Found 29 witnesses for program sv-benchmarks/c/recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c, 47f2e219cca1845e93995805a47abde03d96fdb8abce7bb0dc45093de4fb0653
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/47f2e219cca1845e93995805a47abde03d96fdb8abce7bb0dc45093de4fb0653.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download a3b7e08 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 7 2017-12-03T07:43Z
Download 4de12aa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 1 2017-12-03T04:34 CET (sv-comp)
Download 500fcee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Map2Check 4 2017-12-02T01:28 CET (sv-comp)
Download 52bbcc5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Kojak 7 2017-12-03T10:24Z
Download 5de3440 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-02T18:17:20.729337
Download 8816e4a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-02T06:18:30.345898
Download 39bdbf2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness ESBMC 3.1 7 2017-12-01T13:45 CET (sv-comp)
Download 541b907 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T11:16:27+01:00
Download 4919cc3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CBMC 9 2017-12-01T12:10 CET (sv-comp)
Download 7d8603b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 7 2017-12-03T10:24Z
Download 968fb45 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness skink 4 2017-12-01T22:33 CET (sv-comp)
Download 54abb17 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VeriAbs 1.3 9 Sun Dec 3 01:52:42 2017
Download 69acf71 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Taipan 11 2017-12-03T04:12Z
Download e8b49e2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T17:14 CET (sv-comp)
Download 90f2707 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Map2Check 2 2017-12-01T21:27 CET (sv-comp)
Download 713763d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Kojak 10 2017-12-02T13:54Z
Download 535ff46 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-01T18:09:34.940608
Download 6408900 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 4 2017-12-01T11:11:21.347032
Download 535d423 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 6 2017-12-01T17:44 CET (sv-comp)
Download e60ff59 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 6 2017-11-30T18:14 CET (sv-comp)
Download c61cdf4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 7 2017-11-30T22:09:44+01:00
Download 2107d4a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 7 2017-11-30T15:11:18+01:00
Download be77c1c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 5 2017-11-30T22:39:23+01:00
Download 9bcf574 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 7 2017-12-02T10:42:12+01:00
Download 657722d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 8 2017-12-01T01:40 CET (sv-comp)
Download 1c3482a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 11 2017-12-02T10:09Z
Download e2473be Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T19:48:37.484109
Download aa968be Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T15:34:19.357053
Download d36ea44 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 9 2017-12-01T15:36 CET (sv-comp)

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

Trying to find witnesses for program (47f2e219cca1845e93995805a47abde03d96fdb8abce7bb0dc45093de4fb0653, sv-benchmarks/c/recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c, 47f2e219cca1845e93995805a47abde03d96fdb8abce7bb0dc45093de4fb0653
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/47f2e219cca1845e93995805a47abde03d96fdb8abce7bb0dc45093de4fb0653.json

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