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/ex3b_true-termination_true-no-overflow.c
programSHA d412468cd64aacfdcefc246e93a3ecceac718c99c9cbd69d8c14d9acc4927672
witnessName results-verified/esbmc-kind.2018-12-06_1103.logfiles/sv-comp19_prop-termination.ex3b_true-termination_true-no-overflow.c.files/witness.graphml
witnessSHA a68626f2ec7b6afad652f3df615c278823b80eb865240da48944a4185a483813

Information about the Witness from Competition Database

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

Key Value
architecture 64bit
creationtime 2018-12-06T10:38:09.618753
producer ESBMC 6.0.0
programfile ../../sv-benchmarks/c/termination-restricted-15/ex3b_true-termination_true-no-overflow.c
programhash 3896b84414a1398b8b83fc7620275d5a148e91b6
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/a68626f2ec7b6afad652f3df615c278823b80eb865240da48944a4185a483813.graphml
witness-sha256 a68626f2ec7b6afad652f3df615c278823b80eb865240da48944a4185a483813
witness-size 3415
witness-type correctness_witness

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download e674644 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.4.0 3 2023-12-03T06:52:08Z
Download 97928bd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 7 2023-12-17T21:36:58+01:00 Download cc06809
Download 591bc26 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-24 4 2023-12-03T17:17:08+01:00
Download 0f0b629 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness crux-llvm-0.5.0.99 3 2023-12-18T05:06:26+01:00
Download ef79aa0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness VeriOover 1 2023-12-20T03:36 CET (comp)
Download dda183f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 8 2023-12-02T14:17:48Z
Download 25072f1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 3 2023-11-29T23:06:28Z
Download 2f11282 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Pinaka 3 2023-12-19T23:15:56
Download db59e33 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Mopsa (v1.0~pre2) 3 2023-11-29T14:58:55Z
Download 5c19d7f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Kojak 8 2023-12-02T20:38:35Z
Download a93b3ee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Goblint (tags/svcomp24-0-gc2e9465a7) 10 2023-12-01T01:01:05Z
Download 27da186 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness ESBMC 7.4.0 kind 3 2023-12-01T12:41:15Z
Download a39300e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-20T03:46:02+01:00 Download ef79aa0
Download 8de66e0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-20T02:38:12+01:00 Download 2f11282
Download 3d0f050 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-19T14:34:23+01:00 Download 783565f
Download 55b1a91 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-19T05:13:05+01:00 Download 2588852
Download 31717f2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-18T06:21:28+01:00 Download 0f0b629
Download 6abdceb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-05T14:27:05+01:00 Download ff6f70a
Download f24030b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-04T16:34:38+01:00 Download aec339c
Download eacd7f0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-04T11:41:30+01:00 Download dda183f
Download 8d31761 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-04T01:55:18+01:00 Download bb33dfa
Download 80f1b99 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-03T18:36:50+01:00 Download 591bc26
Download 4971d44 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-03T10:01:25+01:00 Download e674644
Download e222874 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-03T06:10:47+01:00 Download 5c19d7f
Download 980a16f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-01T22:53:29+01:00 Download 209da80
Download af148cd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-01T17:46:49+01:00 Download 27da186
Download 06b52a7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-01T03:46:13+01:00 Download a93b3ee
Download 9fccd7f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-01T00:08:47+01:00 Download d2a321d
Download bf926ec Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-11-30T12:51:15+01:00 Download 5f95220
Download 5f95220 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-11-30T05:19:22+01:00
Download 75eaa77 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-11-30T02:44:19+01:00 Download 25072f1
Download 704f27a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-11-29T18:15:59+01:00 Download db59e33
Download 2908f54 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-11-29T07:57:05+01:00 Download 30ea64b
Download bb33dfa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-e677b7cd46+ 5 2023-12-03T22:17:43+01:00
Download 2588852 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 5 2023-12-18T18:05:50+01:00
Download cc06809 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CBMC 10 2023-12-17T12:04:17+01:00
Download ff6f70a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Bubaak 3 2023-12-05T09:35:34Z
Download aec339c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Bubaak 3 2023-12-04T08:52:01Z
Download 209da80 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Bubaak 3 2023-12-01T21:04:42Z
Download 30ea64b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 8 2023-11-29T01:39:25Z
Download d2a321d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness 2LS 10 2023-11-30T22:03:11+01:00
Download bca83a7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 7.4.0 3 2023-12-01T16:49:50Z
Download 52566c6 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.0.1-svn-a45b42da2f+ 5 2023-12-18T17:38:42+01:00
Download ee1c3e9 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 3 2023-11-29T20:07:18Z
Download 7e23113 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2023-12-19T20:19:22
Download ffeaf6d Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 9 2023-12-17T19:15:02+01:00
Download cb59892 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Bubaak 3 2023-12-05T11:53:15Z
Download 843ef6c Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Bubaak 3 2023-12-04T13:27:08Z
Download ece4705 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 9 2023-11-30T09:38:05+01:00
Download c0acc3c Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: '2.0' uuid: a4fcdbd3-0079-4889-87d0-c8c2acccb336 creation_time: '2023-12-02T21:38:35+01:00' producer: name: Kojak version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_15abc6b0-662a-48dc-aad5-5112254b35da/sv-benchmarks/c/termination-restricted-15/ex3b.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_15abc6b0-662a-48dc-aad5-5112254b35da/sv-benchmarks/c/termination-restricted-15/ex3b.c : d412468cd64aacfdcefc246e93a3ecceac718c99c9cbd69d8c14d9acc4927672 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_15abc6b0-662a-48dc-aad5-5112254b35da/sv-benchmarks/c/termination-restricted-15/ex3b.c file_hash: d412468cd64aacfdcefc246e93a3ecceac718c99c9cbd69d8c14d9acc4927672 line: 11 column: 0 function: main value: (((((((c <= 1) && (0 < c)) && (y <= 46340)) || (((c <= 4) && (3 < c)) && (y <= 46340))) || (((y <= 46340) && (0 <= c)) && (c <= 0))) || (((2 < c) && (y <= 46340)) && (c <= 3))) || (((1 < c) && (y <= 46340)) && (c <= 2))) format: c_expression correctness_witness CPAchecker 2.3 6 2023-12-03T05:37:04+01:00
Download 4704c52 Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: '2.0' uuid: 8a9ff3ef-da7b-4cae-9f9a-6569a087195f creation_time: '2023-11-29T02:39:25+01:00' producer: name: Automizer version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_d2c42d2e-ce82-4b9b-ad13-ca93442728cb/sv-benchmarks/c/termination-restricted-15/ex3b.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_d2c42d2e-ce82-4b9b-ad13-ca93442728cb/sv-benchmarks/c/termination-restricted-15/ex3b.c : d412468cd64aacfdcefc246e93a3ecceac718c99c9cbd69d8c14d9acc4927672 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_d2c42d2e-ce82-4b9b-ad13-ca93442728cb/sv-benchmarks/c/termination-restricted-15/ex3b.c file_hash: d412468cd64aacfdcefc246e93a3ecceac718c99c9cbd69d8c14d9acc4927672 line: 11 column: 0 function: main value: (((((((c <= 4) && (y <= 46340)) && (0 <= c)) || (((y <= 46340) && (0 <= c)) && (c <= 2))) || (((c <= 1) && (y <= 46340)) && (0 <= c))) || (((y <= 46340) && (0 <= c)) && (c <= 3))) || ((c == 0) && (y <= 46340))) format: c_expression correctness_witness CPAchecker 2.3 6 2023-11-29T07:50:25+01:00
Download 0d7b289 Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: '2.0' uuid: 7d16ceeb-8fcd-4fff-aee7-dbaab392b3ea creation_time: '2023-12-02T15:17:48+01:00' producer: name: Taipan version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_63ca8b64-52c6-4bdd-b46d-2c6d82c18c07/sv-benchmarks/c/termination-restricted-15/ex3b.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_63ca8b64-52c6-4bdd-b46d-2c6d82c18c07/sv-benchmarks/c/termination-restricted-15/ex3b.c : d412468cd64aacfdcefc246e93a3ecceac718c99c9cbd69d8c14d9acc4927672 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_63ca8b64-52c6-4bdd-b46d-2c6d82c18c07/sv-benchmarks/c/termination-restricted-15/ex3b.c file_hash: d412468cd64aacfdcefc246e93a3ecceac718c99c9cbd69d8c14d9acc4927672 line: 11 column: 0 function: main value: (((((((c <= 1) && (y <= 46340)) && (0 <= c)) || (((y <= 46340) && (0 <= c)) && (c <= 2))) || (((y <= 46340) && (0 <= c)) && (c <= 3))) || ((c == 0) && (y <= 46340))) || (((c <= 4) && (y <= 46340)) && (0 <= c))) format: c_expression correctness_witness CPAchecker 2.3 6 2023-12-04T12:09:49+01:00
Download 6d0b6bb Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: "2.0" uuid: ef031792-a495-4ebe-85fb-b6211c4b81a6 creation_time: 2023-12-01T01:01:05Z 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/ex3b.c''' task: input_files: - ../../sv-benchmarks/c/termination-restricted-15/ex3b.c input_file_hashes: ../../sv-benchmarks/c/termination-restricted-15/ex3b.c: d412468cd64aacfdcefc246e93a3ecceac718c99c9cbd69d8c14d9acc4927672 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/ex3b.c file_hash: d412468cd64aacfdcefc246e93a3ecceac718c99c9cbd69d8c14d9acc4927672 line: 11 column: 12 function: main value: y <= 46340 format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-restricted-15/ex3b.c file_hash: d412468cd64aacfdcefc246e93a3ecceac718c99c9cbd69d8c14d9acc4927672 line: 11 column: 12 function: main value: (((((x <= 2147302921 && (2147256581LL - (long long )x) + (long long )y >= 0LL) && (2147349261LL - (long long )x) - (long long )y >= 0LL) && y != 0) && ((((((((((((((((((257 <= y && 65536 <= x) && (-65793LL + (long long )x) + (long long )y >= 0LL) && (-65540LL + (long long )c) + (long long )x >= 0LL) && (-261LL + (long long )c) + (long long )y >= 0LL) && (-65532LL - (long long )c) + (long long )x >= 0LL) && (-253LL - (long long )c) + (long long )y >= 0LL) && (-19196LL + (long long )x) - (long long )y >= 0LL) && (46336LL + (long long )c) - (long long )y >= 0LL) && (2147302917LL + (long long )c) - (long long )x >= 0LL) && (46344LL - (long long )c) - (long long )y >= 0LL) && (2147302925LL - (long long )c) - (long long )x >= 0LL) && c == 4) || (((((((((((((17 <= y && 256 <= x) && (-273LL + (long long )x) + (long long )y >= 0LL) && (-259LL + (long long )c) + (long long )x >= 0LL) && (-20LL + (long long )c) + (long long )y >= 0LL) && (-253LL - (long long )c) + (long long )x >= 0LL) && (-14LL - (long long )c) + (long long )y >= 0LL) && (46084LL + (long long )x) - (long long )y >= 0LL) && (46337LL + (long long )c) - (long long )y >= 0LL) && (2147302918LL + (long long )c) - (long long )x >= 0LL) && (46343LL - (long long )c) - (long long )y >= 0LL) && (2147302924LL - (long long )c) - (long long )x >= 0LL) && c == 3) && x != 0)) || ((((((((((((17 <= y && 256 <= x) && (-273LL + (long long )x) + (long long )y >= 0LL) && (-259LL + (long long )c) + (long long )x >= 0LL) && (-20LL + (long long )c) + (long long )y >= 0LL) && (-253LL - (long long )c) + (long long )x >= 0LL) && (-14LL - (long long )c) + (long long )y >= 0LL) && (46084LL + (long long )x) - (long long )y >= 0LL) && (46337LL + (long long )c) - (long long )y >= 0LL) && (2147302918LL + (long long )c) - (long long )x >= 0LL) && (46343LL - (long long )c) - (long long )y >= 0LL) && (2147302924LL - (long long )c) - (long long )x >= 0LL) && c == 3)) || (((((((((((((5 <= y && 16 <= x) && (-21LL + (long long )x) + (long long )y >= 0LL) && (-18LL + (long long )c) + (long long )x >= 0LL) && (-7LL + (long long )c) + (long long )y >= 0LL) && (-14LL - (long long )c) + (long long )x >= 0LL) && (-3LL - (long long )c) + (long long )y >= 0LL) && (46324LL + (long long )x) - (long long )y >= 0LL) && (46338LL + (long long )c) - (long long )y >= 0LL) && (2147302919LL + (long long )c) - (long long )x >= 0LL) && (46342LL - (long long )c) - (long long )y >= 0LL) && (2147302923LL - (long long )c) - (long long )x >= 0LL) && c == 2) && x != 0)) || ((((((((((((5 <= y && 16 <= x) && (-21LL + (long long )x) + (long long )y >= 0LL) && (-18LL + (long long )c) + (long long )x >= 0LL) && (-7LL + (long long )c) + (long long )y >= 0LL) && (-14LL - (long long )c) + (long long )x >= 0LL) && (-3LL - (long long )c) + (long long )y >= 0LL) && (46324LL + (long long )x) - (long long )y >= 0LL) && (46338LL + (long long )c) - (long long )y >= 0LL) && (2147302919LL + (long long )c) - (long long )x >= 0LL) && (46342LL - (long long )c) - (long long )y >= 0LL) && (2147302923LL - (long long )c) - (long long )x >= 0LL) && c == 2)) || (((((((((((((3 <= y && 4 <= x) && (-7LL + (long long )x) + (long long )y >= 0LL) && (-5LL + (long long )c) + (long long )x >= 0LL) && (-4LL + (long long )c) + (long long )y >= 0LL) && (-3LL - (long long )c) + (long long )x >= 0LL) && (-2LL - (long long )c) + (long long )y >= 0LL) && (46336LL + (long long )x) - (long long )y >= 0LL) && (46339LL + (long long )c) - (long long )y >= 0LL) && (2147302920LL + (long long )c) - (long long )x >= 0LL) && (46341LL - (long long )c) - (long long )y >= 0LL) && (2147302922LL - (long long )c) - (long long )x >= 0LL) && c == 1) && x != 0)) || ((((((((((((3 <= y && 4 <= x) && (-7LL + (long long )x) + (long long )y >= 0LL) && (-5LL + (long long )c) + (long long )x >= 0LL) && (-4LL + (long long )c) + (long long )y >= 0LL) && (-3LL - (long long )c) + (long long )x >= 0LL) && (-2LL - (long long )c) + (long long )y >= 0LL) && (46336LL + (long long )x) - (long long )y >= 0LL) && (46339LL + (long long )c) - (long long )y >= 0LL) && (2147302920LL + (long long )c) - (long long )x >= 0LL) && (46341LL - (long long )c) - (long long )y >= 0LL) && (2147302922LL - (long long )c) - (long long )x >= 0LL) && c == 1))) || ((((((((2 <= x && (-2LL + (long long )c) + (long long )x >= 0LL) && (-2LL - (long long )c) + (long long )x >= 0LL) && (46338LL + (long long )x) - (long long )y >= 0LL) && (46340LL + (long long )c) - (long long )y >= 0LL) && (46340LL - (long long )c) - (long long )y >= 0LL) && 0 == c) && c == 0) && x != 0)) || ((((46340LL + (long long )c) - (long long )y >= 0LL && (46340LL - (long long )c) - (long long )y >= 0LL) && 0 == c) && c == 0) format: c_expression correctness_witness CPAchecker 2.3 12 2023-12-01T05:18:45+01:00

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 8431e6f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.4.0 3 2022-12-09T10:11:55Z
Download 3798f1f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 7 2023-01-28T03:55:45+01:00 Download 4f40d7f
Download e26ddda Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-22 4 2022-12-11T01:52:47+01:00
Download 2b947ad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness crux-llvm-0.5.0.99 3 2022-12-09T05:01:24+01:00
Download ef79aa0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness VeriOover 1 2022-12-12T11:01 CET (comp)
Download 2c51a00 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 7 2022-12-14T08:34:34Z
Download cec2368 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 3 2022-12-12T16:10:06Z
Download e48c239 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Pinaka 3 2022-12-11T14:11:47
Download 4e61008 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Kojak 7 2022-12-14T17:27:54Z
Download 8321193 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Goblint (tags/svcomp23-0-g4f5dcf38f) 30 2022-12-10T09:15:41Z
Download 7a21c4b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness ESBMC 7.0.0 kind 3 2022-12-18T16:31:13Z
Download 60be326 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness ESBMC 6.8.0 kind 3 2022-12-25T11:50:44Z
Download 1db2e5b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T11:36:58+01:00 Download ef79aa0
Download 1508bf1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T11:11:58+01:00 Download 2c51a00
Download 239bf64 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T07:36:25+01:00 Download 6bebef9
Download faa9711 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T06:29:35+01:00 Download 4e61008
Download e9e8fbb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T05:27:38+01:00 Download cec2368
Download 0b5dde7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T04:56:20+01:00 Download e48c239
Download 5e60272 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T03:06:25+01:00 Download a66a2cb
Download 758b079 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T00:14:00+01:00 Download ae3183e
Download acb9370 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T22:59:00+01:00 Download e26ddda
Download 44b3173 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T22:28:58+01:00 Download 8321193
Download cd1c8f8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T18:48:49+01:00 Download aa9d8e0
Download 3fe01dd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T17:46:53+01:00 Download 8431e6f
Download 1cd397f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T15:06:45+01:00 Download 7a21c4b
Download c7ecaeb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T11:19:24+01:00 Download 2841ef1
Download 93cb919 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T08:33:17+01:00 Download 2b947ad
Download 8c55c57 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T00:37:10+01:00 Download 60be326
Download 9631591 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-27T23:49:24+01:00 Download eade03f
Download 48195e8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-27T23:02:54+01:00 Download 88df93b
Download 2841ef1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2022-12-10T15:29:36+01:00
Download a66a2cb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-1715bd67dc+ 5 2022-12-11T20:29:13+01:00
Download aa9d8e0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 5 2022-12-09T17:56:22+01:00
Download 4f40d7f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CBMC 10 2022-12-08T11:38:56+01:00
Download eade03f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Bubaak 3 2022-12-08T18:20:26Z
Download 6bebef9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 7 2022-12-13T19:19:14Z
Download 88df93b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness 2LS 10 2022-12-07T21:19:21+01:00
Download f9433b3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(reach_error())) ) correctness_witness ESBMC 6.8.0 3 2022-12-25T11:04:00Z
Download 0fa80cf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 7.0.0 3 2022-12-18T18:48:49Z
Download 39273b6 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.0.1-svn-a45b42da2f+ 5 2022-12-09T23:50:01+01:00
Download 855c49d Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 3 2022-12-12T15:48:54Z
Download 8263a29 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2022-12-11T16:56:15
Download 30736db Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 9 2022-12-08T13:10:46+01:00
Download 218347c Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Bubaak 3 2022-12-08T16:32:35Z
Download 3f35ef7 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 9 2022-12-07T23:19:20+01:00

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download d366eda Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(reach_error())) ) correctness_witness ESBMC 6.8.0 3 2021-12-08T03:18:01Z
Download 4332b7f Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.0.1-svn-fe6f522dd3+ 5 2021-12-08T18:03:30+01:00
Download 4dddbbf Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.0.1-svn-eda176372c+ 5 2021-12-09T14:36:10+01:00
Download 1d8a8d2 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 3 2021-12-07T16:16:12Z
Download ca887ab Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2021-12-09T06:51:43
Download be3b570 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 9 2021-12-06T09:45:51+01:00
Download f1d03a1 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 9 2021-12-06T00:13:09+01:00

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 49b7db5 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.0 5 2020-12-05T16:45:54+01:00
Download 5a369f1 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.0.1-svn-eda176372c+ 5 2020-12-07T23:45:41+01:00
Download ecdfa9f Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 2 2020-12-11T16:58:02
Download d44adad Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 2 2020-12-09T00:38:01
Download d407cbd Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2020-12-08T08:45:17

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 3963f21 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-04T00:27 CET (comp)

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 2b3f4cc Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T00:42 CET (sv-comp)
Download 23fc0fa Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T10:29 CET (sv-comp)

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 0c54c0d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T22:37:43.519890
Download d182c34 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T11:27:08.402703
Download 53aa23f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 5 2017-12-01T18:03 CET (sv-comp)
Download 1f1fe49 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 10 2017-12-01T14:58 CET (sv-comp)
Download 2d3f168 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 9 2017-12-01T13:27 CET (sv-comp)

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

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

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

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