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 ../../../comp/sv-benchmarks/c/ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call_1.i
programSHA cfbaa098b91d7d6e2fb23fb20bbccd7906bcc05119f8ccd4cb636ae3ab0c71c1
witnessName results-verified/predatorhp.2017-12-01_2024.logfiles/sv-comp18.alias_of_return_2_true-termination.c_true-unreach-call_1.i.files/witness.graphml
witnessSHA 1164367800f070800b667cba6410a6c78486882e1711d7752cdf367b47e88be7

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2017-12-01T20:34 CET (sv-comp)
memorymodel precise
producer PredatorHP
program-sha256 cfbaa098b91d7d6e2fb23fb20bbccd7906bcc05119f8ccd4cb636ae3ab0c71c1
programfile ../../sv-benchmarks/c/ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call_1.i
programhash 62fac85ee26c8658f396c1a4c5337152e82c18ea
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/1164367800f070800b667cba6410a6c78486882e1711d7752cdf367b47e88be7.graphml
witness-sha256 1164367800f070800b667cba6410a6c78486882e1711d7752cdf367b47e88be7
witness-size 3589
witness-type correctness_witness

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

Trying to find witnesses for program (cfbaa098b91d7d6e2fb23fb20bbccd7906bcc05119f8ccd4cb636ae3ab0c71c1, ../../../comp/sv-benchmarks/c/ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call_1.i).

Found 0 witnesses for program ../../../comp/sv-benchmarks/c/ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call_1.i, cfbaa098b91d7d6e2fb23fb20bbccd7906bcc05119f8ccd4cb636ae3ab0c71c1
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/cfbaa098b91d7d6e2fb23fb20bbccd7906bcc05119f8ccd4cb636ae3ab0c71c1.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 (cfbaa098b91d7d6e2fb23fb20bbccd7906bcc05119f8ccd4cb636ae3ab0c71c1, ../../../comp/sv-benchmarks/c/ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call_1.i).

Found 0 witnesses for program ../../../comp/sv-benchmarks/c/ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call_1.i, cfbaa098b91d7d6e2fb23fb20bbccd7906bcc05119f8ccd4cb636ae3ab0c71c1
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/cfbaa098b91d7d6e2fb23fb20bbccd7906bcc05119f8ccd4cb636ae3ab0c71c1.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 (cfbaa098b91d7d6e2fb23fb20bbccd7906bcc05119f8ccd4cb636ae3ab0c71c1, ../../../comp/sv-benchmarks/c/ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call_1.i).

Found 0 witnesses for program ../../../comp/sv-benchmarks/c/ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call_1.i, cfbaa098b91d7d6e2fb23fb20bbccd7906bcc05119f8ccd4cb636ae3ab0c71c1
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/cfbaa098b91d7d6e2fb23fb20bbccd7906bcc05119f8ccd4cb636ae3ab0c71c1.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 (cfbaa098b91d7d6e2fb23fb20bbccd7906bcc05119f8ccd4cb636ae3ab0c71c1, ../../../comp/sv-benchmarks/c/ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call_1.i).

Found 0 witnesses for program ../../../comp/sv-benchmarks/c/ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call_1.i, cfbaa098b91d7d6e2fb23fb20bbccd7906bcc05119f8ccd4cb636ae3ab0c71c1
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/cfbaa098b91d7d6e2fb23fb20bbccd7906bcc05119f8ccd4cb636ae3ab0c71c1.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 (cfbaa098b91d7d6e2fb23fb20bbccd7906bcc05119f8ccd4cb636ae3ab0c71c1, ../../../comp/sv-benchmarks/c/ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call_1.i).

Found 19 witnesses for program ../../../comp/sv-benchmarks/c/ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call_1.i, cfbaa098b91d7d6e2fb23fb20bbccd7906bcc05119f8ccd4cb636ae3ab0c71c1
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/cfbaa098b91d7d6e2fb23fb20bbccd7906bcc05119f8ccd4cb636ae3ab0c71c1.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 5e052fc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2019-12-04T00:03 CET (comp)
Download 68e4798 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-11T20:27:05+01:00 Download 826b0b3
Download faef5fb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-11T20:22:14+01:00 Download 5d89fb6
Download c83e3b7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-11T20:08:28+01:00 Download a1656a9
Download c6bcab5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-11T20:02:29+01:00 Download b3c6ed3
Download 950ff80 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-08T00:36:34+01:00 Download 6152229
Download 1dac7eb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-07T23:46:25+01:00 Download 6aaf6e0
Download bd11308 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-07T23:43:28+01:00 Download 125a0e1
Download f98be4d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-07T19:40:38+01:00 Download 68b6203
Download da22cca Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-06T01:48:18+01:00 Download 55afdfc
Download 25e4049 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-05T19:12:46+01:00 Download 3425c4c
Download 1cb7bb7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-05T19:02:59+01:00 Download 4406f03
Download f1371e2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-04T02:07:34+01:00 Download 5e052fc
Download 5579f39 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-11-30T19:49:41+01:00 Download c487cd1
Download 6da567c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-11-30T17:03:25+01:00 Download 1b96df2
Download 1b96df2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 4 2019-11-30T14:10:59+01:00
Download 6152229 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8 4 2019-12-07T23:54:49+01:00
Download a1656a9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 4 2019-12-01T09:28:56+01:00
Download 90076e5 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-03T21:44 CET (comp)

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

Trying to find witnesses for program (cfbaa098b91d7d6e2fb23fb20bbccd7906bcc05119f8ccd4cb636ae3ab0c71c1, ../../../comp/sv-benchmarks/c/ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call_1.i).

Found 24 witnesses for program ../../../comp/sv-benchmarks/c/ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call_1.i, cfbaa098b91d7d6e2fb23fb20bbccd7906bcc05119f8ccd4cb636ae3ab0c71c1
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/cfbaa098b91d7d6e2fb23fb20bbccd7906bcc05119f8ccd4cb636ae3ab0c71c1.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 365a28c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-08T07:01 CET (sv-comp)
Download c98ef9e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T13:08:23
Download 4b40503 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2018-12-07T07:51 CET (sv-comp)
Download 16178c8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 4 2018-12-08T00:09:36+01:00
Download 35f731d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-10T20:02:50+01:00 Download d238d7b
Download e834b8c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-10T10:31:20+01:00 Download d533995
Download 36b35fa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-09T20:15:06+01:00 Download fe57af0
Download f12c71f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-09T20:09:13+01:00 Download 8c6304f
Download d041cae Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-09T19:52:37+01:00 Download beb762a
Download 9693d69 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-08T23:17:36+01:00 Download 365a28c
Download de68ef2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-08T21:34:08+01:00 Download c98ef9e
Download bfbdd7a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-08T05:41:01+01:00 Download 16178c8
Download 8240e28 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-08T04:29:33+01:00 Download 70dfc1b
Download 75f19f3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-08T02:08:51+01:00 Download d533995
Download 363ca64 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-07T17:44:06+01:00 Download ab8ea38
Download da40b5d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-07T16:37:37+01:00 Download 4b40503
Download 7abbf3c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-07T08:44:45+01:00 Download 1164367
Download 039b3b3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T09:29:05+01:00 Download 452d9d5
Download 4c95de1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T09:00:47+01:00 Download 64a6176
Download ba08432 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T08:18:14+01:00 Download cc84607
Download 4218e5d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T07:28:45+01:00 Download fc57179
Download 64a6176 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-05T16:55:06+01:00
Download cbfdfcf Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T12:35 CET (sv-comp)
Download a6da086 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T05:54 CET (sv-comp)

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

Trying to find witnesses for program (cfbaa098b91d7d6e2fb23fb20bbccd7906bcc05119f8ccd4cb636ae3ab0c71c1, ../../../comp/sv-benchmarks/c/ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call_1.i).

Found 39 witnesses for program ../../../comp/sv-benchmarks/c/ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call_1.i, cfbaa098b91d7d6e2fb23fb20bbccd7906bcc05119f8ccd4cb636ae3ab0c71c1
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/cfbaa098b91d7d6e2fb23fb20bbccd7906bcc05119f8ccd4cb636ae3ab0c71c1.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download ab8ea38 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness skink 3 2017-12-01T22:06 CET (sv-comp)
Download d204c5f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Taipan 5 2017-12-02T23:16Z
Download 33e71a8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2017-12-01T23:14 CET (sv-comp)
Download 1164367 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness PredatorHP 4 2017-12-01T20:34 CET (sv-comp)
Download 8de63c8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Map2Check 2 2017-12-01T20:15 CET (sv-comp)
Download 05f630f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Kojak 5 2017-12-02T10:04Z
Download 59ec560 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-03T01:51:51.640526
Download fcecfd6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T12:21:44.530534
Download 3755abf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-01T17:39:10.549398
Download 781f0cb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-01T11:06:32.690575
Download b377157 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 4 2017-12-01T15:44 CET (sv-comp)
Download 510c4b6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 4 2017-12-02T21:53:30+01:00
Download 3dc7022 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 4 2017-12-01T04:03:07+01:00
Download cd60c78 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-03T06:50:51+01:00 75f6a6a
Download 89a4f94 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-03T04:18:24+01:00 5f2741a
Download eb835ab Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-03T02:44:13+01:00 31b994f
Download 829d0a4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-03T01:46:25+01:00 29b43f7
Download 4a21dd0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-02T20:27:41+01:00 0ca41d6
Download d7670f0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-02T15:00:51+01:00 dcfca4f
Download 8afff68 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-02T08:36:24+01:00 273f3c4
Download 0193ed4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-02T00:16:07+01:00 6b1a260
Download 8a25c08 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T22:29:22+01:00 c11f9ce
Download 7105aec Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T22:04:45+01:00 0d5b0b0
Download 2c64265 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T21:03:59+01:00 dc74406
Download 3acb5fe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T08:13:05+01:00 82c7774
Download a571aa2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T06:36:17+01:00 2a2234e
Download 1a92d41 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T06:09:30+01:00 dbdd5b0
Download d6637a9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T06:07:17+01:00 1757eb7
Download e10a3fa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T05:44:52+01:00 024d148
Download 3d41aa9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T04:32:12+01:00 3a27b3b
Download bd717ea Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T01:57:01+01:00
Download 3f95af9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 7 2017-12-01T00:15:54+01:00
Download 6e15273 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26725 4 2017-11-30T22:55:37+01:00
Download e46d0f7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker (unknown version) 4 2017-12-01T20:52:25+01:00
Download 43089c2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CBMC 4 2017-11-30T19:40 CET (sv-comp)
Download 51817e5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 5 2017-12-02T18:53Z
Download 157732d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness 2LS 7 2017-11-30T16:32 CET (sv-comp)
Download 9ded441 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 4 2017-12-01T15:51 CET (sv-comp)
Download aa2599e Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 7 2017-12-01T16:36 CET (sv-comp)

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

Trying to find witnesses for program (cfbaa098b91d7d6e2fb23fb20bbccd7906bcc05119f8ccd4cb636ae3ab0c71c1, ../../../comp/sv-benchmarks/c/ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call_1.i).

Found 0 witnesses for program ../../../comp/sv-benchmarks/c/ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call_1.i, cfbaa098b91d7d6e2fb23fb20bbccd7906bcc05119f8ccd4cb636ae3ab0c71c1
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/cfbaa098b91d7d6e2fb23fb20bbccd7906bcc05119f8ccd4cb636ae3ab0c71c1.json

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