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/Nested_true-termination_true-no-overflow.c
programSHA 689bfa137c7ec291c9da872b4c0ae907dc49890ce91238f2d64af583a7257b4a
witnessName results-verified/cbmc.2017-12-01_1300.logfiles/sv-comp18.Nested_true-termination_true-no-overflow.c.files/witness.graphml
witnessSHA 6db2e20fc2d57430077ddcea7396d2e543e63c2a15b2511609e738f60abb10ed

Information about the Witness from Competition Database

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

Key Value
architecture 64bit
creationtime 2017-12-01T14:34 CET (sv-comp)
producer CBMC
program-sha256 689bfa137c7ec291c9da872b4c0ae907dc49890ce91238f2d64af583a7257b4a
programfile ../../sv-benchmarks/c/termination-restricted-15/Nested_true-termination_true-no-overflow.c
programhash 5f36db653fc1ba72ccbb6cf21df7b84599ee28f0
sourcecodelang C
specification CHECK( init(main()), LTL(F end) )
witness-file witnessFileByHash/6db2e20fc2d57430077ddcea7396d2e543e63c2a15b2511609e738f60abb10ed.graphml
witness-sha256 6db2e20fc2d57430077ddcea7396d2e543e63c2a15b2511609e738f60abb10ed
witness-size 15752
witness-type correctness_witness

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download c8a69ea Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.4.0 3 2023-12-03T07:25:13Z
Download dd75d72 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 6 2023-12-19T03:39:17+01:00 Download e9d4953
Download 1b17980 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 7 2023-12-17T21:37:16+01:00 Download 91fa79c
Download ea50774 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 4 2023-12-01T03:45:58+01:00 Download 1659a89
Download 57ab664 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 4 2023-11-30T23:56:22+01:00 Download b3fef18
Download 8ba52a7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-24 4 2023-12-03T17:54:08+01:00
Download 5b41bbf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness crux-llvm-0.5.0.99 3 2023-12-18T04:59:29+01:00
Download 606bcf5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness VeriOover 1 2023-12-20T03:37 CET (comp)
Download 42a7ab3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 7 2023-12-02T18:40:23Z
Download 57c2ba6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 3 2023-11-29T21:19:25Z
Download 046c5b7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Pinaka 3 2023-12-19T21:54:06
Download f0dc32f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Mopsa (v1.0~pre2) 3 2023-11-29T13:30:01Z
Download c20b26d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Kojak 7 2023-12-02T23:23:55Z
Download 1659a89 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Goblint (tags/svcomp24-0-gc2e9465a7) 12 2023-12-01T01:34:36Z
Download 62e7344 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness ESBMC 7.4.0 kind 3 2023-12-01T14:51:05Z
Download 0345155 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-12-20T03:41:17+01:00 Download 606bcf5
Download 7043075 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-12-20T02:33:30+01:00 Download 046c5b7
Download 527bf5e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-12-19T14:28:29+01:00 Download 529d7ff
Download d39b8da Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-12-18T06:16:39+01:00 Download 5b41bbf
Download a97669a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-12-05T14:22:34+01:00 Download f741306
Download 0aeb412 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-12-04T16:28:39+01:00 Download 1da9d3b
Download 9799465 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-12-04T11:43:23+01:00 Download 42a7ab3
Download 05cf1e8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-04T01:50:58+01:00 Download 55b984e
Download a07154e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-12-03T18:31:01+01:00 Download 8ba52a7
Download 596bc18 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-12-03T10:00:16+01:00 Download c8a69ea
Download 344bc20 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-03T06:01:32+01:00 Download c20b26d
Download 38a5f00 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-12-01T22:45:52+01:00 Download 2ba3223
Download a1517f5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-12-01T17:53:23+01:00 Download 62e7344
Download e4a8611 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-11-30T11:41:52+01:00 Download 84baf8e
Download 84baf8e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-11-30T06:00:22+01:00
Download 09a482b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-11-30T02:27:07+01:00 Download 57c2ba6
Download 536e95b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-11-29T18:26:38+01:00 Download f0dc32f
Download f09fb51 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-11-29T07:52:36+01:00 Download 6841c94
Download 55b984e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-e677b7cd46+ 8 2023-12-03T21:32:43+01:00
Download e9d4953 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 8 2023-12-18T20:14:41+01:00
Download 91fa79c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CBMC 15 2023-12-17T09:49:37+01:00
Download f741306 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Bubaak 3 2023-12-05T09:45:41Z
Download 1da9d3b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Bubaak 3 2023-12-04T14:37:55Z
Download 2ba3223 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Bubaak 3 2023-12-01T20:37:09Z
Download 6841c94 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 7 2023-11-28T19:37:47Z
Download b3fef18 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness 2LS 9 2023-11-30T22:15:32+01:00
Download e44c014 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 7.4.0 3 2023-12-01T10:40:20Z
Download 3119cf9 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 3 2023-11-30T00:30:46Z
Download db48a67 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2023-12-19T23:09:36
Download 0a66515 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Goblint (tags/svcomp24-0-gc2e9465a7) 3 2023-12-01T01:26:16Z
Download e7d3df9 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 15 2023-12-17T10:03:59+01:00
Download 475e93f Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Bubaak 3 2023-12-05T09:00:28Z
Download 147ce23 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Bubaak 3 2023-12-04T14:03:05Z
Download d2fd0af Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Bubaak 3 2023-12-01T20:12:52Z
Download c4b9fc0 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 8 2023-11-30T23:04:59+01:00
Download 40a8a54 Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: '2.0' uuid: fb82ab6e-619e-4ae0-b702-f9ddc613ab0a creation_time: '2023-12-02T19:40:23+01:00' producer: name: Taipan version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_348af23e-2460-4ee7-8213-87a48f50c908/sv-benchmarks/c/termination-restricted-15/Nested-2.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_348af23e-2460-4ee7-8213-87a48f50c908/sv-benchmarks/c/termination-restricted-15/Nested-2.c : 689bfa137c7ec291c9da872b4c0ae907dc49890ce91238f2d64af583a7257b4a 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_348af23e-2460-4ee7-8213-87a48f50c908/sv-benchmarks/c/termination-restricted-15/Nested-2.c file_hash: 689bfa137c7ec291c9da872b4c0ae907dc49890ce91238f2d64af583a7257b4a line: 11 column: 0 function: main value: ((3 <= j) && (0 <= i)) format: c_expression - invariant: type: loop_invariant location: file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_348af23e-2460-4ee7-8213-87a48f50c908/sv-benchmarks/c/termination-restricted-15/Nested-2.c file_hash: 689bfa137c7ec291c9da872b4c0ae907dc49890ce91238f2d64af583a7257b4a line: 12 column: 0 function: main value: (((3 <= j) && (0 <= i)) && (i <= 9)) format: c_expression correctness_witness CPAchecker 2.3 10 2023-12-04T11:56:30+01:00
Download bf7d80d Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: '2.0' uuid: ec214380-6c9b-40f7-b38e-6fae399f9430 creation_time: '2023-11-28T20:37:47+01:00' producer: name: Automizer version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_89b1956a-ff01-4f05-9630-4fa9d6bbaf44/sv-benchmarks/c/termination-restricted-15/Nested-2.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_89b1956a-ff01-4f05-9630-4fa9d6bbaf44/sv-benchmarks/c/termination-restricted-15/Nested-2.c : 689bfa137c7ec291c9da872b4c0ae907dc49890ce91238f2d64af583a7257b4a 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_89b1956a-ff01-4f05-9630-4fa9d6bbaf44/sv-benchmarks/c/termination-restricted-15/Nested-2.c file_hash: 689bfa137c7ec291c9da872b4c0ae907dc49890ce91238f2d64af583a7257b4a line: 11 column: 0 function: main value: ((3 <= j) && (0 <= i)) format: c_expression - invariant: type: loop_invariant location: file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_89b1956a-ff01-4f05-9630-4fa9d6bbaf44/sv-benchmarks/c/termination-restricted-15/Nested-2.c file_hash: 689bfa137c7ec291c9da872b4c0ae907dc49890ce91238f2d64af583a7257b4a line: 12 column: 0 function: main value: (((3 <= j) && (0 <= i)) && (i <= 9)) format: c_expression correctness_witness CPAchecker 2.3 10 2023-11-29T07:46:52+01:00
Download 673b125 Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: '2.0' uuid: 5dd82d48-1fbe-47eb-bf4b-cfc371d20fa2 creation_time: '2023-12-03T00:23:55+01:00' producer: name: Kojak version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_92763829-2f6a-484f-9493-194ed897f3e7/sv-benchmarks/c/termination-restricted-15/Nested-2.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_92763829-2f6a-484f-9493-194ed897f3e7/sv-benchmarks/c/termination-restricted-15/Nested-2.c : 689bfa137c7ec291c9da872b4c0ae907dc49890ce91238f2d64af583a7257b4a 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_92763829-2f6a-484f-9493-194ed897f3e7/sv-benchmarks/c/termination-restricted-15/Nested-2.c file_hash: 689bfa137c7ec291c9da872b4c0ae907dc49890ce91238f2d64af583a7257b4a line: 11 column: 0 function: main value: (((0 < i) && (11 < j)) || ((((3 <= j) && (i <= 0)) && (j <= 3)) && (0 <= i))) format: c_expression - invariant: type: loop_invariant location: file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_92763829-2f6a-484f-9493-194ed897f3e7/sv-benchmarks/c/termination-restricted-15/Nested-2.c file_hash: 689bfa137c7ec291c9da872b4c0ae907dc49890ce91238f2d64af583a7257b4a line: 12 column: 0 function: main value: ((((3 <= j) && (i <= 0)) && (0 <= i)) || (((0 < i) && (11 < j)) && (i <= 9))) format: c_expression correctness_witness CPAchecker 2.3 10 2023-12-03T05:32:09+01:00
Download bcf3c7e Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: "2.0" uuid: a8dfe339-8f47-4ae2-bda7-0a8ce052d93e creation_time: 2023-12-01T01:34:36Z 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/Nested-2.c''' task: input_files: - ../../sv-benchmarks/c/termination-restricted-15/Nested-2.c input_file_hashes: ../../sv-benchmarks/c/termination-restricted-15/Nested-2.c: 689bfa137c7ec291c9da872b4c0ae907dc49890ce91238f2d64af583a7257b4a 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/Nested-2.c file_hash: 689bfa137c7ec291c9da872b4c0ae907dc49890ce91238f2d64af583a7257b4a line: 12 column: 15 function: main value: 0 <= i format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-restricted-15/Nested-2.c file_hash: 689bfa137c7ec291c9da872b4c0ae907dc49890ce91238f2d64af583a7257b4a line: 12 column: 15 function: main value: i <= 9 format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-restricted-15/Nested-2.c file_hash: 689bfa137c7ec291c9da872b4c0ae907dc49890ce91238f2d64af583a7257b4a line: 12 column: 15 function: main value: (12LL + (long long )i) - (long long )j >= 0LL format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-restricted-15/Nested-2.c file_hash: 689bfa137c7ec291c9da872b4c0ae907dc49890ce91238f2d64af583a7257b4a line: 12 column: 15 function: main value: ((((((((((((-12LL + (long long )i) + (long long )j >= 0LL && (-10LL - (long long )i) + (long long )j >= 0LL) && (14LL - (long long )i) - (long long )j >= 0LL) && j == 12) || (((((11 <= j && j <= 12) && (-11LL + (long long )i) + (long long )j >= 0LL) && (-9LL - (long long )i) + (long long )j >= 0LL) && (15LL - (long long )i) - (long long )j >= 0LL) && j != 8)) || (((((10 <= j && j <= 12) && (-10LL + (long long )i) + (long long )j >= 0LL) && (-8LL - (long long )i) + (long long )j >= 0LL) && (16LL - (long long )i) - (long long )j >= 0LL) && j != 7)) || (((((9 <= j && j <= 12) && (-9LL + (long long )i) + (long long )j >= 0LL) && (-7LL - (long long )i) + (long long )j >= 0LL) && (17LL - (long long )i) - (long long )j >= 0LL) && j != 6)) || (((((8 <= j && j <= 12) && (-8LL + (long long )i) + (long long )j >= 0LL) && (-6LL - (long long )i) + (long long )j >= 0LL) && (18LL - (long long )i) - (long long )j >= 0LL) && j != 5)) || (((((7 <= j && j <= 12) && (-7LL + (long long )i) + (long long )j >= 0LL) && (-5LL - (long long )i) + (long long )j >= 0LL) && (19LL - (long long )i) - (long long )j >= 0LL) && j != 4)) || (((((6 <= j && j <= 12) && (-6LL + (long long )i) + (long long )j >= 0LL) && (-4LL - (long long )i) + (long long )j >= 0LL) && (20LL - (long long )i) - (long long )j >= 0LL) && j != 3)) || (((((5 <= j && j <= 12) && (-5LL + (long long )i) + (long long )j >= 0LL) && (-3LL - (long long )i) + (long long )j >= 0LL) && (21LL - (long long )i) - (long long )j >= 0LL) && j != 2)) || (((((4 <= j && j <= 12) && (-4LL + (long long )i) + (long long )j >= 0LL) && (-2LL - (long long )i) + (long long )j >= 0LL) && (21LL - (long long )i) - (long long )j >= 0LL) && j != 1)) || (((((3 <= j && j <= 12) && (-3LL + (long long )i) + (long long )j >= 0LL) && (-1LL - (long long )i) + (long long )j >= 0LL) && (21LL - (long long )i) - (long long )j >= 0LL) && j != 0) format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-restricted-15/Nested-2.c file_hash: 689bfa137c7ec291c9da872b4c0ae907dc49890ce91238f2d64af583a7257b4a line: 11 column: 11 function: main value: 0 <= i format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-restricted-15/Nested-2.c file_hash: 689bfa137c7ec291c9da872b4c0ae907dc49890ce91238f2d64af583a7257b4a line: 11 column: 11 function: main value: 3 <= j format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-restricted-15/Nested-2.c file_hash: 689bfa137c7ec291c9da872b4c0ae907dc49890ce91238f2d64af583a7257b4a line: 11 column: 11 function: main value: i <= 10 format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-restricted-15/Nested-2.c file_hash: 689bfa137c7ec291c9da872b4c0ae907dc49890ce91238f2d64af583a7257b4a line: 11 column: 11 function: main value: j <= 12 format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-restricted-15/Nested-2.c file_hash: 689bfa137c7ec291c9da872b4c0ae907dc49890ce91238f2d64af583a7257b4a line: 11 column: 11 function: main value: (-3LL + (long long )i) + (long long )j >= 0LL format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-restricted-15/Nested-2.c file_hash: 689bfa137c7ec291c9da872b4c0ae907dc49890ce91238f2d64af583a7257b4a line: 11 column: 11 function: main value: (-1LL - (long long )i) + (long long )j >= 0LL format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-restricted-15/Nested-2.c file_hash: 689bfa137c7ec291c9da872b4c0ae907dc49890ce91238f2d64af583a7257b4a line: 11 column: 11 function: main value: (12LL + (long long )i) - (long long )j >= 0LL format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-restricted-15/Nested-2.c file_hash: 689bfa137c7ec291c9da872b4c0ae907dc49890ce91238f2d64af583a7257b4a line: 11 column: 11 function: main value: (22LL - (long long )i) - (long long )j >= 0LL format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-restricted-15/Nested-2.c file_hash: 689bfa137c7ec291c9da872b4c0ae907dc49890ce91238f2d64af583a7257b4a line: 11 column: 11 function: main value: j != 0 format: c_expression correctness_witness CPAchecker 2.3 16 2023-12-01T04:58:11+01:00

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 607f9a0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.4.0 3 2022-12-09T10:07:09Z
Download 43ac28e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 2 2023-01-28T22:38:29+01:00 Download 1c1e6ca
Download 0264b2d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 7 2023-01-28T03:58:45+01:00 Download 479e067
Download a6376a7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 4 2023-01-27T23:03:06+01:00 Download a281e00
Download 10e9849 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-22 4 2022-12-11T01:48:38+01:00
Download 158f64a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness crux-llvm-0.5.0.99 3 2022-12-09T03:43:24+01:00
Download 606bcf5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness VeriOover 1 2022-12-12T11:01 CET (comp)
Download 0d4b202 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 7 2022-12-14T11:29:27Z
Download a844fe8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 3 2022-12-12T16:26:10Z
Download 07fa7cb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Pinaka 3 2022-12-11T16:22:58
Download 4d374ae Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Mopsa (v1.0~pre2) 3 2022-12-11T11:17:02Z
Download afdad8d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Kojak 7 2022-12-15T00:35:01Z
Download 1c1e6ca Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Goblint (tags/svcomp23-0-g4f5dcf38f) 27 2022-12-10T08:48:05Z
Download c51bce8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness ESBMC 7.0.0 kind 3 2022-12-19T00:14:33Z
Download 9fbd7db Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness ESBMC 6.8.0 kind 3 2022-12-25T10:52:22Z
Download ad7d211 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2023-01-29T11:32:13+01:00 Download 606bcf5
Download e6b3f7a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2023-01-29T11:06:02+01:00 Download 0d4b202
Download 49f5d07 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2023-01-29T07:16:19+01:00 Download 1294ae6
Download f5e6a73 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2023-01-29T06:33:00+01:00 Download afdad8d
Download b647642 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2023-01-29T05:28:51+01:00 Download a844fe8
Download a110343 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2023-01-29T04:50:16+01:00 Download 07fa7cb
Download 40f6b3c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2023-01-29T03:45:43+01:00 Download 4d374ae
Download e8a4cbf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T03:03:13+01:00 Download b51f490
Download 872744e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2023-01-29T00:06:55+01:00 Download 6182cca
Download 01a2cd2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2023-01-28T22:53:14+01:00 Download 10e9849
Download 394c66b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T18:53:11+01:00 Download 5f9ab3d
Download ca15128 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2023-01-28T17:45:49+01:00 Download 607f9a0
Download 5f389c5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2023-01-28T14:46:42+01:00 Download c51bce8
Download fe6ea64 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T10:54:05+01:00 Download 0c899ee
Download 2ef09f7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2023-01-28T08:19:26+01:00 Download 158f64a
Download 4d46b47 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2023-01-28T00:32:00+01:00 Download 9fbd7db
Download 440a921 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2023-01-27T23:43:27+01:00 Download edd6a0e
Download 0c899ee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2022-12-10T18:07:58+01:00
Download b51f490 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-1715bd67dc+ 8 2022-12-12T00:11:24+01:00
Download 5f9ab3d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 8 2022-12-09T21:38:36+01:00
Download 479e067 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CBMC 15 2022-12-08T07:08:30+01:00
Download edd6a0e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Bubaak 3 2022-12-08T14:34:55Z
Download 1294ae6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 7 2022-12-13T11:43:36Z
Download a281e00 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness 2LS 9 2022-12-07T22:32:25+01:00
Download 7208b21 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(reach_error())) ) correctness_witness ESBMC 6.8.0 3 2022-12-25T09:30:31Z
Download c414014 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 7.0.0 3 2022-12-19T00:41:50Z
Download 719844c Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 3 2022-12-12T10:37:56Z
Download b84775c Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2022-12-11T16:39:53
Download 7c08739 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 15 2022-12-08T13:43:12+01:00
Download ca1bdd9 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Bubaak 3 2022-12-08T17:19:31Z
Download 6d92a6a Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 8 2022-12-07T22:34:55+01:00

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 8176c11 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(reach_error())) ) correctness_witness ESBMC 6.8.0 3 2021-12-08T11:19:06Z
Download 9a694f5 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 3 2021-12-07T17:13:03Z
Download 580c3c9 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2021-12-09T06:01:32
Download b61f3c3 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 15 2021-12-06T08:51:57+01:00
Download e47cd10 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 8 2021-12-05T19:32:38+01:00

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download eda87db Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 2 2020-12-11T23:37:32
Download cde4939 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 2 2020-12-09T02:16:14
Download f80d54d Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2020-12-08T10:38:18

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download d43dc05 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 (689bfa137c7ec291c9da872b4c0ae907dc49890ce91238f2d64af583a7257b4a, sv-benchmarks/c/termination-restricted-15/Nested_true-termination_true-no-overflow.c).

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download b38f632 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T03:55 CET (sv-comp)
Download 7d2f0a6 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T07:15 CET (sv-comp)

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download e1234bd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T22:22:37.401684
Download 8a1ffbe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T14:22:42.707877
Download d2ed79f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 6 2017-12-01T16:12 CET (sv-comp)
Download 6db2e20 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 16 2017-12-01T14:34 CET (sv-comp)
Download 5ffabb2 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 8 2017-12-01T12:37 CET (sv-comp)

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

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

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

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