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/PastaB17_true-termination_true-no-overflow.c
programSHA 5d77ccce06a5eb83fb368250e0baa3072703c85ca9ba919f17c4260cdb623930
witnessName results-verified/2ls.2017-12-01_1141.logfiles/sv-comp18.PastaB17_true-termination_true-no-overflow.c.files/witness.graphml
witnessSHA 6ce86adfb0304360bab7bb05955419461b7a6fb8040982f10bf93aea3d5871da

Information about the Witness from Competition Database

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

Key Value
architecture 64bit
creationtime 2017-12-01T15:13 CET (sv-comp)
producer 2LS
program-sha256 5d77ccce06a5eb83fb368250e0baa3072703c85ca9ba919f17c4260cdb623930
programfile ../../sv-benchmarks/c/termination-restricted-15/PastaB17_true-termination_true-no-overflow.c
programhash b15653f6a2dde479fee065502d45075dfcaf4f25
sourcecodelang C
specification CHECK( init(main()), LTL(F end) )
witness-file witnessFileByHash/6ce86adfb0304360bab7bb05955419461b7a6fb8040982f10bf93aea3d5871da.graphml
witness-sha256 6ce86adfb0304360bab7bb05955419461b7a6fb8040982f10bf93aea3d5871da
witness-size 8760
witness-type correctness_witness

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

Trying to find witnesses for program (5d77ccce06a5eb83fb368250e0baa3072703c85ca9ba919f17c4260cdb623930, sv-benchmarks/c/termination-restricted-15/PastaB17_true-termination_true-no-overflow.c).

Found 33 witnesses for program sv-benchmarks/c/termination-restricted-15/PastaB17_true-termination_true-no-overflow.c, 5d77ccce06a5eb83fb368250e0baa3072703c85ca9ba919f17c4260cdb623930
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/5d77ccce06a5eb83fb368250e0baa3072703c85ca9ba919f17c4260cdb623930.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download f210547 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.4.0 3 2023-12-03T06:07:02Z
Download 5006a53 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-24 4 2023-12-03T18:01:01+01:00
Download cfc3ecb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness VeriOover 1 2023-12-20T03:37 CET (comp)
Download 4249a24 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 8 2023-12-02T13:45:47Z
Download a5a8bda Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Mopsa (v1.0~pre2) 3 2023-11-29T09:08:22Z
Download 5b4a10c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Kojak 8 2023-12-02T23:52:51Z
Download 784498c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Goblint (tags/svcomp24-0-gc2e9465a7) 22 2023-12-01T00:56:08Z
Download 06f1541 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-20T03:41:15+01:00 Download cfc3ecb
Download 90b3e79 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-19T15:11:18+01:00 Download 7438ccf
Download 6483da8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-19T05:11:17+01:00 Download 9c82923
Download 507c23a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-17T06:08:38+01:00 Download d08b5f2
Download 99786e3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-04T11:38:18+01:00 Download 4249a24
Download aad29ee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-04T01:29:55+01:00 Download 70155db
Download a6cc697 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-03T18:31:30+01:00 Download 5006a53
Download 4fb932e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-03T09:58:58+01:00 Download f210547
Download 4cb18a6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-03T05:55:17+01:00 Download 5b4a10c
Download ca7d0ee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-01T03:47:19+01:00 Download 784498c
Download 4c72004 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-01T00:11:16+01:00 Download f31fd7d
Download bd2bba6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-11-30T13:02:09+01:00 Download a6fe78a
Download a6fe78a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-11-30T05:53:04+01:00
Download 93ba355 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-11-29T18:30:58+01:00 Download a5a8bda
Download e883e35 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-11-29T08:16:16+01:00 Download 0dae2dc
Download 70155db Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-e677b7cd46+ 5 2023-12-03T21:15:53+01:00
Download d08b5f2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2023-12-17T03:32:17+01:00
Download 9c82923 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 5 2023-12-18T18:40:00+01:00
Download 0dae2dc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 8 2023-11-29T01:09:20Z
Download f31fd7d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness 2LS 9 2023-11-30T20:43:00+01:00
Download e0b177f Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Goblint (tags/svcomp24-0-gc2e9465a7) 3 2023-12-01T01:19:32Z
Download 86f5568 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 8 2023-11-30T21:59:52+01:00
Download 08141e4 Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: '2.0' uuid: eb383b31-14a7-4223-b18e-1bc5e81fe944 creation_time: '2023-12-03T00:52:51+01:00' producer: name: Kojak version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_2ffaa12a-b42d-406e-9b8b-bed071fc54d1/sv-benchmarks/c/termination-restricted-15/PastaB17.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_2ffaa12a-b42d-406e-9b8b-bed071fc54d1/sv-benchmarks/c/termination-restricted-15/PastaB17.c : 5d77ccce06a5eb83fb368250e0baa3072703c85ca9ba919f17c4260cdb623930 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_2ffaa12a-b42d-406e-9b8b-bed071fc54d1/sv-benchmarks/c/termination-restricted-15/PastaB17.c file_hash: 5d77ccce06a5eb83fb368250e0baa3072703c85ca9ba919f17c4260cdb623930 line: 13 column: 0 function: main value: ((((0 <= (z + 2147483648)) && (x <= 2147483647)) && (y <= 2147483647)) || (((y < (z + 1)) && (2147483647 < y)) && (x <= 2147483646))) format: c_expression - invariant: type: loop_invariant location: file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_2ffaa12a-b42d-406e-9b8b-bed071fc54d1/sv-benchmarks/c/termination-restricted-15/PastaB17.c file_hash: 5d77ccce06a5eb83fb368250e0baa3072703c85ca9ba919f17c4260cdb623930 line: 14 column: 0 function: main value: ((((0 <= (z + 2147483648)) && (x <= 2147483647)) && (0 <= (2147483647 + x))) && (y <= 2147483647)) format: c_expression correctness_witness CPAchecker 2.3 7 2023-12-03T05:44:33+01:00
Download 98148a5 Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: '2.0' uuid: bc66ba26-f97e-47cb-a674-b8fabdf2c316 creation_time: '2023-12-02T14:45:47+01:00' producer: name: Taipan version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_a52bbcea-dbe6-458d-a412-fa714a8bc6e9/sv-benchmarks/c/termination-restricted-15/PastaB17.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_a52bbcea-dbe6-458d-a412-fa714a8bc6e9/sv-benchmarks/c/termination-restricted-15/PastaB17.c : 5d77ccce06a5eb83fb368250e0baa3072703c85ca9ba919f17c4260cdb623930 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_a52bbcea-dbe6-458d-a412-fa714a8bc6e9/sv-benchmarks/c/termination-restricted-15/PastaB17.c file_hash: 5d77ccce06a5eb83fb368250e0baa3072703c85ca9ba919f17c4260cdb623930 line: 13 column: 0 function: main value: (((0 <= (z + 2147483648)) && (x <= 2147483647)) && (y <= 2147483647)) format: c_expression - invariant: type: loop_invariant location: file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_a52bbcea-dbe6-458d-a412-fa714a8bc6e9/sv-benchmarks/c/termination-restricted-15/PastaB17.c file_hash: 5d77ccce06a5eb83fb368250e0baa3072703c85ca9ba919f17c4260cdb623930 line: 14 column: 0 function: main value: ((((0 <= (z + 2147483648)) && (x <= 2147483647)) && (0 <= (2147483647 + x))) && (y <= 2147483647)) format: c_expression correctness_witness CPAchecker 2.3 7 2023-12-04T11:54:20+01:00
Download 9cdd237 Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: '2.0' uuid: 1c2f0068-b672-4bfb-8e6f-ccad26c13a88 creation_time: '2023-11-29T02:09:20+01:00' producer: name: Automizer version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_45edc113-2fd1-46f5-a5a0-b7a295660b62/sv-benchmarks/c/termination-restricted-15/PastaB17.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_45edc113-2fd1-46f5-a5a0-b7a295660b62/sv-benchmarks/c/termination-restricted-15/PastaB17.c : 5d77ccce06a5eb83fb368250e0baa3072703c85ca9ba919f17c4260cdb623930 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_45edc113-2fd1-46f5-a5a0-b7a295660b62/sv-benchmarks/c/termination-restricted-15/PastaB17.c file_hash: 5d77ccce06a5eb83fb368250e0baa3072703c85ca9ba919f17c4260cdb623930 line: 13 column: 0 function: main value: (((0 <= (z + 2147483648)) && (x <= 2147483647)) && (y <= 2147483647)) format: c_expression - invariant: type: loop_invariant location: file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_45edc113-2fd1-46f5-a5a0-b7a295660b62/sv-benchmarks/c/termination-restricted-15/PastaB17.c file_hash: 5d77ccce06a5eb83fb368250e0baa3072703c85ca9ba919f17c4260cdb623930 line: 14 column: 0 function: main value: ((((0 <= (z + 2147483648)) && (x <= 2147483647)) && (0 <= (2147483647 + x))) && (y <= 2147483647)) format: c_expression correctness_witness CPAchecker 2.3 7 2023-11-29T07:49:48+01:00
Download 0ac0178 Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: "2.0" uuid: 2bda713d-2b77-4670-a7db-ff225a0cc9ad creation_time: 2023-12-01T00:56:08Z 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/PastaB17.c''' task: input_files: - ../../sv-benchmarks/c/termination-restricted-15/PastaB17.c input_file_hashes: ../../sv-benchmarks/c/termination-restricted-15/PastaB17.c: 5d77ccce06a5eb83fb368250e0baa3072703c85ca9ba919f17c4260cdb623930 data_model: LP64 language: C specification: CHECK( init(main()), LTL(G ! overflow) ) content: - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-restricted-15/PastaB17.c file_hash: 5d77ccce06a5eb83fb368250e0baa3072703c85ca9ba919f17c4260cdb623930 line: 14 column: 15 function: main value: -2147483647 <= x format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-restricted-15/PastaB17.c file_hash: 5d77ccce06a5eb83fb368250e0baa3072703c85ca9ba919f17c4260cdb623930 line: 14 column: 15 function: main value: (-1LL + (long long )x) - (long long )z >= 0LL format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-restricted-15/PastaB17.c file_hash: 5d77ccce06a5eb83fb368250e0baa3072703c85ca9ba919f17c4260cdb623930 line: 14 column: 15 function: main value: ((((long long )y - (long long )z >= 0LL && (((((((((((((((((((((((y <= 2147483631 && z <= 2147483631) || (y <= 2147483632 && z <= 2147483632)) || (y <= 2147483633 && z <= 2147483633)) || (y <= 2147483634 && z <= 2147483634)) || (y <= 2147483635 && z <= 2147483635)) || (y <= 2147483636 && z <= 2147483636)) || (y <= 2147483637 && z <= 2147483637)) || (y <= 2147483638 && z <= 2147483638)) || (y <= 2147483639 && z <= 2147483639)) || (y <= 2147483640 && z <= 2147483640)) || (y <= 2147483622 && z <= 2147483622)) || (y <= 2147483641 && z <= 2147483641)) || (y <= 2147483623 && z <= 2147483623)) || (y <= 2147483642 && z <= 2147483642)) || (y <= 2147483624 && z <= 2147483624)) || (y <= 2147483643 && z <= 2147483643)) || (y <= 2147483625 && z <= 2147483625)) || (y <= 2147483644 && z <= 2147483644)) || (y <= 2147483626 && z <= 2147483626)) || (y <= 2147483645 && z <= 2147483645)) || (y <= 2147483627 && z <= 2147483627)) || (y <= 2147483646 && z <= 2147483646)) || (y <= 2147483628 && z <= 2147483628))) || z <= 2147483646) || ((y <= 2147483629 && z <= 2147483629) && (long long )y - (long long )z >= 0LL)) || ((y <= 2147483630 && z <= 2147483630) && (long long )y - (long long )z >= 0LL) format: c_expression correctness_witness CPAchecker 2.3 9 2023-12-01T04:16:22+01:00

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

Trying to find witnesses for program (5d77ccce06a5eb83fb368250e0baa3072703c85ca9ba919f17c4260cdb623930, sv-benchmarks/c/termination-restricted-15/PastaB17_true-termination_true-no-overflow.c).

Found 28 witnesses for program sv-benchmarks/c/termination-restricted-15/PastaB17_true-termination_true-no-overflow.c, 5d77ccce06a5eb83fb368250e0baa3072703c85ca9ba919f17c4260cdb623930
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/5d77ccce06a5eb83fb368250e0baa3072703c85ca9ba919f17c4260cdb623930.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 1fb95b3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.4.0 3 2022-12-09T10:14:11Z
Download 2c6962f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-22 4 2022-12-10T22:02:17+01:00
Download cfc3ecb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness VeriOover 1 2022-12-12T11:01 CET (comp)
Download faa7e37 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 7 2022-12-14T14:14:55Z
Download 81ed113 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Mopsa (v1.0~pre2) 3 2022-12-11T10:40:24Z
Download 671f232 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Kojak 8 2022-12-15T01:37:59Z
Download b4aa2d5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Goblint (tags/svcomp23-0-g4f5dcf38f) 43 2022-12-10T08:53:40Z
Download 3e6a0b4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T11:32:16+01:00 Download cfc3ecb
Download 305f060 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T10:51:34+01:00 Download faa7e37
Download fae5cb7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T07:16:27+01:00 Download f7ac6e7
Download b45cf07 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T06:23:23+01:00 Download 671f232
Download 7f39678 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T03:52:32+01:00 Download 81ed113
Download e42a7fd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T02:37:43+01:00 Download 0a9df9d
Download c204181 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T00:08:15+01:00 Download e2de95a
Download 7373976 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T22:50:57+01:00 Download 2c6962f
Download 54630e0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T22:23:44+01:00 Download b4aa2d5
Download 7ff6243 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T18:30:02+01:00 Download 588559d
Download dfa3590 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T17:44:10+01:00 Download 1fb95b3
Download 9fa44b7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T11:37:04+01:00 Download 722d052
Download 4022fe8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T00:32:00+01:00 Download f04e242
Download 88dac63 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-27T22:59:00+01:00 Download a7e09d8
Download 722d052 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2022-12-10T15:46:35+01:00
Download 0a9df9d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-1715bd67dc+ 5 2022-12-12T01:02:19+01:00
Download f04e242 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2022-12-25T09:59:58+01:00
Download 588559d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 5 2022-12-09T17:47:09+01:00
Download f7ac6e7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 8 2022-12-13T16:49:49Z
Download a7e09d8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness 2LS 9 2022-12-07T21:19:26+01:00
Download 64d0d8d Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 8 2022-12-07T22:05:50+01:00

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

Trying to find witnesses for program (5d77ccce06a5eb83fb368250e0baa3072703c85ca9ba919f17c4260cdb623930, sv-benchmarks/c/termination-restricted-15/PastaB17_true-termination_true-no-overflow.c).

Found 1 witnesses for program sv-benchmarks/c/termination-restricted-15/PastaB17_true-termination_true-no-overflow.c, 5d77ccce06a5eb83fb368250e0baa3072703c85ca9ba919f17c4260cdb623930
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/5d77ccce06a5eb83fb368250e0baa3072703c85ca9ba919f17c4260cdb623930.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 67fb9c8 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 8 2021-12-05T23:03:37+01:00

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

Trying to find witnesses for program (5d77ccce06a5eb83fb368250e0baa3072703c85ca9ba919f17c4260cdb623930, sv-benchmarks/c/termination-restricted-15/PastaB17_true-termination_true-no-overflow.c).

Found 0 witnesses for program sv-benchmarks/c/termination-restricted-15/PastaB17_true-termination_true-no-overflow.c, 5d77ccce06a5eb83fb368250e0baa3072703c85ca9ba919f17c4260cdb623930
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/5d77ccce06a5eb83fb368250e0baa3072703c85ca9ba919f17c4260cdb623930.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 (5d77ccce06a5eb83fb368250e0baa3072703c85ca9ba919f17c4260cdb623930, sv-benchmarks/c/termination-restricted-15/PastaB17_true-termination_true-no-overflow.c).

Found 0 witnesses for program sv-benchmarks/c/termination-restricted-15/PastaB17_true-termination_true-no-overflow.c, 5d77ccce06a5eb83fb368250e0baa3072703c85ca9ba919f17c4260cdb623930
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/5d77ccce06a5eb83fb368250e0baa3072703c85ca9ba919f17c4260cdb623930.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 '19

Trying to find witnesses for program (5d77ccce06a5eb83fb368250e0baa3072703c85ca9ba919f17c4260cdb623930, sv-benchmarks/c/termination-restricted-15/PastaB17_true-termination_true-no-overflow.c).

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 7f0348f Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T14:17 CET (sv-comp)

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

Trying to find witnesses for program (5d77ccce06a5eb83fb368250e0baa3072703c85ca9ba919f17c4260cdb623930, sv-benchmarks/c/termination-restricted-15/PastaB17_true-termination_true-no-overflow.c).

Found 2 witnesses for program sv-benchmarks/c/termination-restricted-15/PastaB17_true-termination_true-no-overflow.c, 5d77ccce06a5eb83fb368250e0baa3072703c85ca9ba919f17c4260cdb623930
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/5d77ccce06a5eb83fb368250e0baa3072703c85ca9ba919f17c4260cdb623930.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 29b4cb4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 6 2017-12-01T17:13 CET (sv-comp)
Download 6ce86ad Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 9 2017-12-01T15:13 CET (sv-comp)

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

Trying to find witnesses for program (5d77ccce06a5eb83fb368250e0baa3072703c85ca9ba919f17c4260cdb623930, sv-benchmarks/c/termination-restricted-15/PastaB17_true-termination_true-no-overflow.c).

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

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