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-restricted-15/ConvLower_false-termination_true-no-overflow.c
programSHA 53380e8569c70a1efdb918ce9289975051e88fe57ba0743af14839dd30306283
witnessName results-verified/cpa-seq.2017-12-01_1227.logfiles/sv-comp18.ConvLower_false-termination_true-no-overflow.c.files/witness.graphml
witnessSHA 59307100cad65c776d4f64ec852863a0e57c25dac7b0605a7f38ac5d5a993848

Information about the Witness from Competition Database

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

Key Value
architecture 64bit
creationtime 2017-12-01T15:54:40+01:00
producer CPAchecker 1.6.1-svn 26773
program-sha256 53380e8569c70a1efdb918ce9289975051e88fe57ba0743af14839dd30306283
programfile ../../sv-benchmarks/c/termination-restricted-15/ConvLower_false-termination_true-no-overflow.c
programhash 7bae4f7c3d0d0a015aa612e78087b008098dcb33
sourcecodelang C
specification CHECK( init(main()), LTL(F end) )
witness-file witnessFileByHash/59307100cad65c776d4f64ec852863a0e57c25dac7b0605a7f38ac5d5a993848.graphml
witness-sha256 59307100cad65c776d4f64ec852863a0e57c25dac7b0605a7f38ac5d5a993848
witness-size 5596
witness-type violation_witness

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

Trying to find witnesses for program (53380e8569c70a1efdb918ce9289975051e88fe57ba0743af14839dd30306283, sv-benchmarks/c/termination-restricted-15/ConvLower_false-termination_true-no-overflow.c).

Found 41 witnesses for program sv-benchmarks/c/termination-restricted-15/ConvLower_false-termination_true-no-overflow.c, 53380e8569c70a1efdb918ce9289975051e88fe57ba0743af14839dd30306283
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/53380e8569c70a1efdb918ce9289975051e88fe57ba0743af14839dd30306283.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download fa8f3f8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.4.0 3 2023-12-03T06:30:34Z
Download e9165ee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-24 4 2023-12-03T17:25:14+01:00
Download db571e9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness VeriOover 1 2023-12-20T03:37 CET (comp)
Download 6e37ffb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 5 2023-12-02T17:50:18Z
Download 80ee303 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Mopsa (v1.0~pre2) 3 2023-11-29T14:26:40Z
Download 060fb1f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Kojak 5 2023-12-03T01:03:24Z
Download b1238ce Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Goblint (tags/svcomp24-0-gc2e9465a7) 31 2023-12-01T01:20:34Z
Download acc6456 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-20T03:41:10+01:00 Download db571e9
Download df77d4d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-19T14:28:45+01:00 Download 2366bbb
Download 32248cb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-19T03:55:12+01:00 Download 57b577c
Download e20c468 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-17T06:25:29+01:00 Download d559464
Download f92e572 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-04T11:53:47+01:00 Download 6e37ffb
Download 8510ff7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-04T01:46:10+01:00 Download 14d89ed
Download 4b1fb76 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-03T18:35:32+01:00 Download e9165ee
Download 11194a6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-03T10:00:07+01:00 Download fa8f3f8
Download 946f937 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-03T05:53:45+01:00 Download 060fb1f
Download 600aaab Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-01T03:37:09+01:00 Download b1238ce
Download ee460db Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-11-30T23:59:00+01:00 Download bf2e804
Download 1dda6a9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-11-30T11:47:00+01:00 Download d166121
Download d166121 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-11-30T08:25:19+01:00
Download 8e0572e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-11-29T18:17:33+01:00 Download 80ee303
Download 32efa30 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-11-29T08:16:25+01:00 Download 2b612fa
Download 14d89ed Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-e677b7cd46+ 4 2023-12-03T18:04:49+01:00
Download d559464 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 4 2023-12-17T01:58:03+01:00
Download 57b577c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 4 2023-12-19T01:54:17+01:00
Download 2b612fa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 5 2023-11-28T23:37:53Z
Download bf2e804 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness 2LS 6 2023-11-30T21:12:00+01:00
Download 6f3bdc7 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness VERIFUZZ 3 2023-12-01T22:30:06Z
Download 2abc81b Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Symbiotic 3 2023-12-17T04:10:15Z
Download c768da3 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Symbiotic 3 2023-11-29T20:16:52Z
Download 3a7ff24 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.3 6 2023-11-30T06:06:02+01:00
Download 11b436f Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.2.1-svn-e677b7cd46+ 6 2023-12-04T00:02:00+01:00
Download 2a19c16 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.0.1-svn-a45b42da2f+ 6 2023-12-19T00:10:36+01:00
Download 293282d Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Bubaak 3 2023-12-05T11:00:24Z
Download 59e3258 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Bubaak 3 2023-12-04T12:37:11Z
Download d0f4c4a Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Automizer 4 2023-11-29T02:19:52Z
Download abc7b82 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness 2LS 4 2023-11-30T22:42:50+01:00
Download 57eb6f3 Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: '2.0' uuid: d74ca6a4-3bc4-46d2-8238-69e71646afca creation_time: '2023-12-02T18:50:18+01:00' producer: name: Taipan version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_adf19462-db0f-4d4b-bf11-1a8388ea5776/sv-benchmarks/c/termination-restricted-15/ConvLower.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_adf19462-db0f-4d4b-bf11-1a8388ea5776/sv-benchmarks/c/termination-restricted-15/ConvLower.c : 53380e8569c70a1efdb918ce9289975051e88fe57ba0743af14839dd30306283 specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: - invariant: type: loop_invariant location: file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_adf19462-db0f-4d4b-bf11-1a8388ea5776/sv-benchmarks/c/termination-restricted-15/ConvLower.c file_hash: 53380e8569c70a1efdb918ce9289975051e88fe57ba0743af14839dd30306283 line: 9 column: 0 function: main value: (i <= 2147483647) format: c_expression correctness_witness CPAchecker 2.3 6 2023-12-04T12:02:29+01:00
Download c22925f Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: '2.0' uuid: 81fc6db7-7655-4b56-a5a8-f98d0aee2ba4 creation_time: '2023-12-03T02:03:24+01:00' producer: name: Kojak version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_d89bfc81-c647-4113-9734-a2e954225c44/sv-benchmarks/c/termination-restricted-15/ConvLower.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_d89bfc81-c647-4113-9734-a2e954225c44/sv-benchmarks/c/termination-restricted-15/ConvLower.c : 53380e8569c70a1efdb918ce9289975051e88fe57ba0743af14839dd30306283 specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: - invariant: type: loop_invariant location: file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_d89bfc81-c647-4113-9734-a2e954225c44/sv-benchmarks/c/termination-restricted-15/ConvLower.c file_hash: 53380e8569c70a1efdb918ce9289975051e88fe57ba0743af14839dd30306283 line: 9 column: 0 function: main value: (i <= 2147483647) format: c_expression correctness_witness CPAchecker 2.3 6 2023-12-03T05:41:34+01:00
Download 1b2b739 Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: '2.0' uuid: 3d6e2300-163d-4ed2-9873-c20837a881d6 creation_time: '2023-11-29T00:37:53+01:00' producer: name: Automizer version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_e813de21-048d-4b6f-a78d-bfb530ac632b/sv-benchmarks/c/termination-restricted-15/ConvLower.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_e813de21-048d-4b6f-a78d-bfb530ac632b/sv-benchmarks/c/termination-restricted-15/ConvLower.c : 53380e8569c70a1efdb918ce9289975051e88fe57ba0743af14839dd30306283 specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: - invariant: type: loop_invariant location: file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_e813de21-048d-4b6f-a78d-bfb530ac632b/sv-benchmarks/c/termination-restricted-15/ConvLower.c file_hash: 53380e8569c70a1efdb918ce9289975051e88fe57ba0743af14839dd30306283 line: 9 column: 0 function: main value: (i <= 2147483647) format: c_expression correctness_witness CPAchecker 2.3 6 2023-11-29T07:47:36+01:00
Download c05fb50 Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: "2.0" uuid: aaf37784-e756-4f47-8e2b-bc1443d978d3 creation_time: 2023-12-01T01:20:34Z 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-restricted-15/ConvLower.c''' task: input_files: - ../../sv-benchmarks/c/termination-restricted-15/ConvLower.c input_file_hashes: ../../sv-benchmarks/c/termination-restricted-15/ConvLower.c: 53380e8569c70a1efdb918ce9289975051e88fe57ba0743af14839dd30306283 data_model: LP64 language: C specification: CHECK( init(main()), LTL(G ! overflow) ) content: [] correctness_witness CPAchecker 2.3 5 2023-12-01T05:12:33+01:00

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

Trying to find witnesses for program (53380e8569c70a1efdb918ce9289975051e88fe57ba0743af14839dd30306283, sv-benchmarks/c/termination-restricted-15/ConvLower_false-termination_true-no-overflow.c).

Found 35 witnesses for program sv-benchmarks/c/termination-restricted-15/ConvLower_false-termination_true-no-overflow.c, 53380e8569c70a1efdb918ce9289975051e88fe57ba0743af14839dd30306283
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/53380e8569c70a1efdb918ce9289975051e88fe57ba0743af14839dd30306283.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 6ece520 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.4.0 3 2022-12-09T11:41:56Z
Download 007ef22 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-22 4 2022-12-10T22:00:45+01:00
Download db571e9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness VeriOover 1 2022-12-12T11:00 CET (comp)
Download 9d27d50 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 5 2022-12-14T08:49:32Z
Download 789c243 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Mopsa (v1.0~pre2) 3 2022-12-11T10:33:44Z
Download 828bc60 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Kojak 5 2022-12-14T17:56:27Z
Download bcdf155 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Goblint (tags/svcomp23-0-g4f5dcf38f) 78 2022-12-10T07:26:51Z
Download 26c9fda Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T11:32:16+01:00 Download db571e9
Download ea3ae44 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T11:08:18+01:00 Download 9d27d50
Download 321a8ba Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T07:27:37+01:00 Download 1318e24
Download 0f22b13 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T06:30:26+01:00 Download 828bc60
Download 7953751 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T03:50:14+01:00 Download 789c243
Download a71e442 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T03:03:16+01:00 Download 26b1fed
Download 2ff4d58 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T00:06:41+01:00 Download d0cede0
Download 2658328 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T22:50:47+01:00 Download 007ef22
Download 2886f64 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T22:41:25+01:00 Download bcdf155
Download 3588689 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T18:29:07+01:00 Download 8e29d0a
Download ece32a0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T17:44:18+01:00 Download 6ece520
Download 1099101 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T12:00:20+01:00 Download c01aaf1
Download a113a98 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T01:02:53+01:00 Download 3157326
Download bcbc7e9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-27T23:07:26+01:00 Download c99aac7
Download c01aaf1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2022-12-10T20:39:42+01:00
Download 26b1fed Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-1715bd67dc+ 4 2022-12-12T00:30:32+01:00
Download 3157326 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 4 2022-12-25T12:34:11+01:00
Download 8e29d0a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 4 2022-12-09T16:49:40+01:00
Download 1318e24 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 5 2022-12-13T17:27:57Z
Download c99aac7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness 2LS 6 2022-12-07T23:58:17+01:00
Download bdb2554 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Symbiotic 3 2022-12-25T11:26:40Z
Download 4ab10e4 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Symbiotic 3 2022-12-12T11:02:12Z
Download 7371c3f Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.2 6 2022-12-10T20:55:22+01:00
Download fa14ead Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.2.1-svn-1715bd67dc+ 6 2022-12-11T23:02:09+01:00
Download c753d7d Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.0.1-svn-a45b42da2f+ 6 2022-12-09T23:17:22+01:00
Download 293074f Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Bubaak 3 2022-12-08T21:31:29Z
Download d8f06db Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Automizer 4 2022-12-13T09:56:16Z
Download d466029 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness 2LS 4 2022-12-08T01:20:47+01:00

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

Trying to find witnesses for program (53380e8569c70a1efdb918ce9289975051e88fe57ba0743af14839dd30306283, sv-benchmarks/c/termination-restricted-15/ConvLower_false-termination_true-no-overflow.c).

Found 8 witnesses for program sv-benchmarks/c/termination-restricted-15/ConvLower_false-termination_true-no-overflow.c, 53380e8569c70a1efdb918ce9289975051e88fe57ba0743af14839dd30306283
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/53380e8569c70a1efdb918ce9289975051e88fe57ba0743af14839dd30306283.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 4c8093d Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Symbiotic 3 2021-12-10T15:57:49
Download 3795022 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Symbiotic 3 2021-12-07T17:03:57Z
Download 50d0f93 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.1 6 2021-12-05T14:29:08+01:00
Download 83ff440 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.0.1-svn-fe6f522dd3+ 6 2021-12-08T19:33:20+01:00
Download aabbd12 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.0.1-svn-eda176372c+ 6 2021-12-09T14:06:22+01:00
Download ad004b7 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Automizer 4 2021-12-06T23:45:43Z
Download 71ec2fe Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness AProVE 5 2021-12-05T12:13:19Z
Download 3ffac68 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness 2LS 4 2021-12-05T22:33:15+01:00

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

Trying to find witnesses for program (53380e8569c70a1efdb918ce9289975051e88fe57ba0743af14839dd30306283, sv-benchmarks/c/termination-restricted-15/ConvLower_false-termination_true-no-overflow.c).

Found 4 witnesses for program sv-benchmarks/c/termination-restricted-15/ConvLower_false-termination_true-no-overflow.c, 53380e8569c70a1efdb918ce9289975051e88fe57ba0743af14839dd30306283
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/53380e8569c70a1efdb918ce9289975051e88fe57ba0743af14839dd30306283.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download a08378e Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Symbiotic 3 2020-12-11T20:47:40
Download 0a449d4 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Symbiotic 2 2020-12-09T00:00:05
Download 3ecdac5 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.0 6 2020-12-05T14:29:16+01:00
Download 75b1fe3 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.0.1-svn-eda176372c+ 6 2020-12-07T23:36:27+01:00

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

Trying to find witnesses for program (53380e8569c70a1efdb918ce9289975051e88fe57ba0743af14839dd30306283, sv-benchmarks/c/termination-restricted-15/ConvLower_false-termination_true-no-overflow.c).

Found 3 witnesses for program sv-benchmarks/c/termination-restricted-15/ConvLower_false-termination_true-no-overflow.c, 53380e8569c70a1efdb918ce9289975051e88fe57ba0743af14839dd30306283
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/53380e8569c70a1efdb918ce9289975051e88fe57ba0743af14839dd30306283.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 3e32007 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Symbiotic 1 2019-12-01 06:00:15
Download 14e655c Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.9 6 2019-11-30T14:36:59+01:00
Download b5189b9 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ 6 2019-12-01T02:26:10+01:00

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

Trying to find witnesses for program (53380e8569c70a1efdb918ce9289975051e88fe57ba0743af14839dd30306283, sv-benchmarks/c/termination-restricted-15/ConvLower_false-termination_true-no-overflow.c).

Found 5 witnesses for program sv-benchmarks/c/termination-restricted-15/ConvLower_false-termination_true-no-overflow.c, 53380e8569c70a1efdb918ce9289975051e88fe57ba0743af14839dd30306283
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/53380e8569c70a1efdb918ce9289975051e88fe57ba0743af14839dd30306283.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 51c4ca9 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 6 2018-12-07T10:26:29+01:00
Download ae7d338 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-09T20:39:47+01:00
Download 874cadb Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-06T09:42:41+01:00
Download ab067c4 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-05T13:31:43+01:00
Download 73becbc Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-05T09:27:25+01:00

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

Trying to find witnesses for program (53380e8569c70a1efdb918ce9289975051e88fe57ba0743af14839dd30306283, sv-benchmarks/c/termination-restricted-15/ConvLower_false-termination_true-no-overflow.c).

Found 4 witnesses for program sv-benchmarks/c/termination-restricted-15/ConvLower_false-termination_true-no-overflow.c, 53380e8569c70a1efdb918ce9289975051e88fe57ba0743af14839dd30306283
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/53380e8569c70a1efdb918ce9289975051e88fe57ba0743af14839dd30306283.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download a5ee9fc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 5 2017-12-01T19:55 CET (sv-comp)
Download 5930710 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T15:54:40+01:00
Download c5b0b6a Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Automizer 4 2017-12-03T11:13Z
Download 667e3b8 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness 2LS 4 2017-12-01T14:36 CET (sv-comp)

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

Trying to find witnesses for program (53380e8569c70a1efdb918ce9289975051e88fe57ba0743af14839dd30306283, sv-benchmarks/c/termination-restricted-15/ConvLower_false-termination_true-no-overflow.c).

Found 0 witnesses for program sv-benchmarks/c/termination-restricted-15/ConvLower_false-termination_true-no-overflow.c, 53380e8569c70a1efdb918ce9289975051e88fe57ba0743af14839dd30306283
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/53380e8569c70a1efdb918ce9289975051e88fe57ba0743af14839dd30306283.json

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