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).

This link does not point to a witness, but below is a list of witnesses for the same program.

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

Trying to find witnesses for program (709a9fb1525fc89256c547fbe03fef24399be5d6458f17d55fb4fce36419b886, ../../../comp/sv-benchmarks/c/termination-crafted/Cairo_step2_true-no-overflow_true-termination_true-valid-memsafety.c).

Found 20 witnesses for program ../../../comp/sv-benchmarks/c/termination-crafted/Cairo_step2_true-no-overflow_true-termination_true-valid-memsafety.c, 709a9fb1525fc89256c547fbe03fef24399be5d6458f17d55fb4fce36419b886
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/709a9fb1525fc89256c547fbe03fef24399be5d6458f17d55fb4fce36419b886.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download b77e058 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.4.0 3 2023-12-03T06:22:34Z
Download d5be043 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness VeriOover 1 2023-12-20T03:37 CET (comp)
Download 704d750 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 5 2023-12-02T15:25:11Z
Download bdb1d83 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Kojak 5 2023-12-02T20:50:57Z
Download 1513234 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-20T03:55:56+01:00 Download d5be043
Download 4917103 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-19T04:06:50+01:00 Download dea60e7
Download c36b6d9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-04T12:01:10+01:00 Download 704d750
Download 9d03c26 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-04T01:48:29+01:00 Download c14fe74
Download 222ae2b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-03T09:58:00+01:00 Download b77e058
Download 67b7578 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-03T06:19:17+01:00 Download bdb1d83
Download 9d17721 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-11-30T12:57:43+01:00 Download a7a97ca
Download a7a97ca Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-11-30T07:57:11+01:00
Download c1604d5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-11-29T08:33:30+01:00 Download 6fa1f64
Download c14fe74 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-e677b7cd46+ 4 2023-12-03T22:19:21+01:00
Download dea60e7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 4 2023-12-19T00:03:40+01:00
Download 6fa1f64 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 5 2023-11-29T03:16:57Z
Download 4a518be Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: '2.0' uuid: c8c22e4f-19b3-41fe-9c63-f3e855e78903 creation_time: '2023-11-29T04:16:57+01:00' producer: name: Automizer version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_7e92a614-134f-46de-8033-950395deae14/sv-benchmarks/c/termination-crafted/Cairo_step2-1.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_7e92a614-134f-46de-8033-950395deae14/sv-benchmarks/c/termination-crafted/Cairo_step2-1.c : 709a9fb1525fc89256c547fbe03fef24399be5d6458f17d55fb4fce36419b886 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_7e92a614-134f-46de-8033-950395deae14/sv-benchmarks/c/termination-crafted/Cairo_step2-1.c file_hash: 709a9fb1525fc89256c547fbe03fef24399be5d6458f17d55fb4fce36419b886 line: 16 column: 0 function: main value: ((x <= 2147483647) && (0 <= (x + 1))) format: c_expression correctness_witness CPAchecker 2.3 6 2023-11-29T08:02:13+01:00
Download e179f77 Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: '2.0' uuid: b8e604bb-4e4d-4166-b9a5-23cfd11f8856 creation_time: '2023-12-02T21:50:57+01:00' producer: name: Kojak version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_eba80934-5b49-4bed-b0f4-7b572de1099a/sv-benchmarks/c/termination-crafted/Cairo_step2-1.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_eba80934-5b49-4bed-b0f4-7b572de1099a/sv-benchmarks/c/termination-crafted/Cairo_step2-1.c : 709a9fb1525fc89256c547fbe03fef24399be5d6458f17d55fb4fce36419b886 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_eba80934-5b49-4bed-b0f4-7b572de1099a/sv-benchmarks/c/termination-crafted/Cairo_step2-1.c file_hash: 709a9fb1525fc89256c547fbe03fef24399be5d6458f17d55fb4fce36419b886 line: 16 column: 0 function: main value: (((x <= 2147483647) && (1 <= x)) || ((x < 1) && (0 <= (x + 1)))) format: c_expression correctness_witness CPAchecker 2.3 6 2023-12-03T05:51:48+01:00
Download 93d5583 Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: '2.0' uuid: 12fe02ef-df5c-444f-81d3-b69d2d4d3df2 creation_time: '2023-12-02T16:25:12+01:00' producer: name: Taipan version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_49473b37-5680-4224-8ad0-7c453e6324de/sv-benchmarks/c/termination-crafted/Cairo_step2-1.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_49473b37-5680-4224-8ad0-7c453e6324de/sv-benchmarks/c/termination-crafted/Cairo_step2-1.c : 709a9fb1525fc89256c547fbe03fef24399be5d6458f17d55fb4fce36419b886 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_49473b37-5680-4224-8ad0-7c453e6324de/sv-benchmarks/c/termination-crafted/Cairo_step2-1.c file_hash: 709a9fb1525fc89256c547fbe03fef24399be5d6458f17d55fb4fce36419b886 line: 16 column: 0 function: main value: ((x <= 2147483647) && (0 <= (x + 1))) format: c_expression correctness_witness CPAchecker 2.3 6 2023-12-04T12:19:20+01:00
Download 727e315 Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: "2.0" uuid: 511e247f-f30f-4ca7-9b1a-f4c72b2ae22d creation_time: 2023-12-01T01:12:45Z 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-crafted/Cairo_step2-1.c''' task: input_files: - ../../sv-benchmarks/c/termination-crafted/Cairo_step2-1.c input_file_hashes: ../../sv-benchmarks/c/termination-crafted/Cairo_step2-1.c: 709a9fb1525fc89256c547fbe03fef24399be5d6458f17d55fb4fce36419b886 data_model: LP64 language: C specification: CHECK( init(main()), LTL(G ! overflow) ) content: - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-crafted/Cairo_step2-1.c file_hash: 709a9fb1525fc89256c547fbe03fef24399be5d6458f17d55fb4fce36419b886 line: 16 column: 12 function: main value: (((((x != -3 && x != -2) && ((((((x != -5 && x != -4) && ((((((x != -7 && x != -6) && ((((((x != -9 && x != -8) && ((((((x != -11 && x != -10) && ((((((x != -13 && x != -12) && ((((((x != -15 && x != -14) && ((((((x != -17 && x != -16) && ((((((x != -19 && x != -18) && ((((((x != -21 && x != -20) && ((((((x != -23 && x != -22) && ((((((x != -25 && x != -24) && (((((-24 <= x && x <= 2147483621) && x != -27) && x != -26) || ((-22 <= x && x <= 2147483623) && x != 0)) || (-22 <= x && x <= 2147483623))) || ((-20 <= x && x <= 2147483625) && x != 0)) || (-20 <= x && x <= 2147483625)) || (((((((((((((((((((((((((((((x <= 2147483597 && x != -51) && x != -50) && x != -49) && x != -48) && x != -47) && x != -46) && x != -45) && x != -44) && x != -43) && x != -42) && x != -41) && x != -40) && x != -39) && x != -38) && x != -37) && x != -36) && x != -35) && x != -34) && x != -33) && x != -32) && x != -31) && x != -30) && x != -29) && x != -28) && x != -27) && x != -26) && x != -25) && x != -24) && x != 0)) || ((((((((((((((((((((((((((((x <= 2147483597 && x != -51) && x != -50) && x != -49) && x != -48) && x != -47) && x != -46) && x != -45) && x != -44) && x != -43) && x != -42) && x != -41) && x != -40) && x != -39) && x != -38) && x != -37) && x != -36) && x != -35) && x != -34) && x != -33) && x != -32) && x != -31) && x != -30) && x != -29) && x != -28) && x != -27) && x != -26) && x != -25) && x != -24))) || ((-18 <= x && x <= 2147483627) && x != 0)) || (-18 <= x && x <= 2147483627)) || ((((((((((((((((((((((((((((((-46 <= x && x <= 2147483599) && x != -49) && x != -48) && x != -47) && x != -46) && x != -45) && x != -44) && x != -43) && x != -42) && x != -41) && x != -40) && x != -39) && x != -38) && x != -37) && x != -36) && x != -35) && x != -34) && x != -33) && x != -32) && x != -31) && x != -30) && x != -29) && x != -28) && x != -27) && x != -26) && x != -25) && x != -24) && x != -23) && x != -22) && x != 0)) || (((((((((((((((((((((((((((((-46 <= x && x <= 2147483599) && x != -49) && x != -48) && x != -47) && x != -46) && x != -45) && x != -44) && x != -43) && x != -42) && x != -41) && x != -40) && x != -39) && x != -38) && x != -37) && x != -36) && x != -35) && x != -34) && x != -33) && x != -32) && x != -31) && x != -30) && x != -29) && x != -28) && x != -27) && x != -26) && x != -25) && x != -24) && x != -23) && x != -22))) || ((-16 <= x && x <= 2147483629) && x != 0)) || (-16 <= x && x <= 2147483629)) || ((((((((((((((((((((((((((((((-44 <= x && x <= 2147483601) && x != -47) && x != -46) && x != -45) && x != -44) && x != -43) && x != -42) && x != -41) && x != -40) && x != -39) && x != -38) && x != -37) && x != -36) && x != -35) && x != -34) && x != -33) && x != -32) && x != -31) && x != -30) && x != -29) && x != -28) && x != -27) && x != -26) && x != -25) && x != -24) && x != -23) && x != -22) && x != -21) && x != -20) && x != 0)) || (((((((((((((((((((((((((((((-44 <= x && x <= 2147483601) && x != -47) && x != -46) && x != -45) && x != -44) && x != -43) && x != -42) && x != -41) && x != -40) && x != -39) && x != -38) && x != -37) && x != -36) && x != -35) && x != -34) && x != -33) && x != -32) && x != -31) && x != -30) && x != -29) && x != -28) && x != -27) && x != -26) && x != -25) && x != -24) && x != -23) && x != -22) && x != -21) && x != -20))) || ((-14 <= x && x <= 2147483631) && x != 0)) || (-14 <= x && x <= 2147483631)) || ((((((((((((((((((((((((((((((-42 <= x && x <= 2147483603) && x != -45) && x != -44) && x != -43) && x != -42) && x != -41) && x != -40) && x != -39) && x != -38) && x != -37) && x != -36) && x != -35) && x != -34) && x != -33) && x != -32) && x != -31) && x != -30) && x != -29) && x != -28) && x != -27) && x != -26) && x != -25) && x != -24) && x != -23) && x != -22) && x != -21) && x != -20) && x != -19) && x != -18) && x != 0)) || (((((((((((((((((((((((((((((-42 <= x && x <= 2147483603) && x != -45) && x != -44) && x != -43) && x != -42) && x != -41) && x != -40) && x != -39) && x != -38) && x != -37) && x != -36) && x != -35) && x != -34) && x != -33) && x != -32) && x != -31) && x != -30) && x != -29) && x != -28) && x != -27) && x != -26) && x != -25) && x != -24) && x != -23) && x != -22) && x != -21) && x != -20) && x != -19) && x != -18))) || ((-12 <= x && x <= 2147483633) && x != 0)) || (-12 <= x && x <= 2147483633)) || ((((((((((((((((((((((((((((((-40 <= x && x <= 2147483605) && x != -43) && x != -42) && x != -41) && x != -40) && x != -39) && x != -38) && x != -37) && x != -36) && x != -35) && x != -34) && x != -33) && x != -32) && x != -31) && x != -30) && x != -29) && x != -28) && x != -27) && x != -26) && x != -25) && x != -24) && x != -23) && x != -22) && x != -21) && x != -20) && x != -19) && x != -18) && x != -17) && x != -16) && x != 0)) || (((((((((((((((((((((((((((((-40 <= x && x <= 2147483605) && x != -43) && x != -42) && x != -41) && x != -40) && x != -39) && x != -38) && x != -37) && x != -36) && x != -35) && x != -34) && x != -33) && x != -32) && x != -31) && x != -30) && x != -29) && x != -28) && x != -27) && x != -26) && x != -25) && x != -24) && x != -23) && x != -22) && x != -21) && x != -20) && x != -19) && x != -18) && x != -17) && x != -16))) || ((-10 <= x && x <= 2147483635) && x != 0)) || (-10 <= x && x <= 2147483635)) || ((((((((((((((((((((((((((((((-38 <= x && x <= 2147483607) && x != -41) && x != -40) && x != -39) && x != -38) && x != -37) && x != -36) && x != -35) && x != -34) && x != -33) && x != -32) && x != -31) && x != -30) && x != -29) && x != -28) && x != -27) && x != -26) && x != -25) && x != -24) && x != -23) && x != -22) && x != -21) && x != -20) && x != -19) && x != -18) && x != -17) && x != -16) && x != -15) && x != -14) && x != 0)) || (((((((((((((((((((((((((((((-38 <= x && x <= 2147483607) && x != -41) && x != -40) && x != -39) && x != -38) && x != -37) && x != -36) && x != -35) && x != -34) && x != -33) && x != -32) && x != -31) && x != -30) && x != -29) && x != -28) && x != -27) && x != -26) && x != -25) && x != -24) && x != -23) && x != -22) && x != -21) && x != -20) && x != -19) && x != -18) && x != -17) && x != -16) && x != -15) && x != -14))) || ((-8 <= x && x <= 2147483637) && x != 0)) || (-8 <= x && x <= 2147483637)) || ((((((((((((((((((((((((((((((-36 <= x && x <= 2147483609) && x != -39) && x != -38) && x != -37) && x != -36) && x != -35) && x != -34) && x != -33) && x != -32) && x != -31) && x != -30) && x != -29) && x != -28) && x != -27) && x != -26) && x != -25) && x != -24) && x != -23) && x != -22) && x != -21) && x != -20) && x != -19) && x != -18) && x != -17) && x != -16) && x != -15) && x != -14) && x != -13) && x != -12) && x != 0)) || (((((((((((((((((((((((((((((-36 <= x && x <= 2147483609) && x != -39) && x != -38) && x != -37) && x != -36) && x != -35) && x != -34) && x != -33) && x != -32) && x != -31) && x != -30) && x != -29) && x != -28) && x != -27) && x != -26) && x != -25) && x != -24) && x != -23) && x != -22) && x != -21) && x != -20) && x != -19) && x != -18) && x != -17) && x != -16) && x != -15) && x != -14) && x != -13) && x != -12))) || ((-6 <= x && x <= 2147483639) && x != 0)) || (-6 <= x && x <= 2147483639)) || ((((((((((((((((((((((((((((((-34 <= x && x <= 2147483611) && x != -37) && x != -36) && x != -35) && x != -34) && x != -33) && x != -32) && x != -31) && x != -30) && x != -29) && x != -28) && x != -27) && x != -26) && x != -25) && x != -24) && x != -23) && x != -22) && x != -21) && x != -20) && x != -19) && x != -18) && x != -17) && x != -16) && x != -15) && x != -14) && x != -13) && x != -12) && x != -11) && x != -10) && x != 0)) || (((((((((((((((((((((((((((((-34 <= x && x <= 2147483611) && x != -37) && x != -36) && x != -35) && x != -34) && x != -33) && x != -32) && x != -31) && x != -30) && x != -29) && x != -28) && x != -27) && x != -26) && x != -25) && x != -24) && x != -23) && x != -22) && x != -21) && x != -20) && x != -19) && x != -18) && x != -17) && x != -16) && x != -15) && x != -14) && x != -13) && x != -12) && x != -11) && x != -10))) || ((-4 <= x && x <= 2147483641) && x != 0)) || (-4 <= x && x <= 2147483641)) || ((((((((((((((((((((((((((((((-32 <= x && x <= 2147483613) && x != -35) && x != -34) && x != -33) && x != -32) && x != -31) && x != -30) && x != -29) && x != -28) && x != -27) && x != -26) && x != -25) && x != -24) && x != -23) && x != -22) && x != -21) && x != -20) && x != -19) && x != -18) && x != -17) && x != -16) && x != -15) && x != -14) && x != -13) && x != -12) && x != -11) && x != -10) && x != -9) && x != -8) && x != 0)) || (((((((((((((((((((((((((((((-32 <= x && x <= 2147483613) && x != -35) && x != -34) && x != -33) && x != -32) && x != -31) && x != -30) && x != -29) && x != -28) && x != -27) && x != -26) && x != -25) && x != -24) && x != -23) && x != -22) && x != -21) && x != -20) && x != -19) && x != -18) && x != -17) && x != -16) && x != -15) && x != -14) && x != -13) && x != -12) && x != -11) && x != -10) && x != -9) && x != -8))) || ((-2 <= x && x <= 2147483643) && x != 0)) || (-2 <= x && x <= 2147483643)) || ((((((((((((((((((((((((((((((-30 <= x && x <= 2147483615) && x != -33) && x != -32) && x != -31) && x != -30) && x != -29) && x != -28) && x != -27) && x != -26) && x != -25) && x != -24) && x != -23) && x != -22) && x != -21) && x != -20) && x != -19) && x != -18) && x != -17) && x != -16) && x != -15) && x != -14) && x != -13) && x != -12) && x != -11) && x != -10) && x != -9) && x != -8) && x != -7) && x != -6) && x != 0)) || (((((((((((((((((((((((((((((-30 <= x && x <= 2147483615) && x != -33) && x != -32) && x != -31) && x != -30) && x != -29) && x != -28) && x != -27) && x != -26) && x != -25) && x != -24) && x != -23) && x != -22) && x != -21) && x != -20) && x != -19) && x != -18) && x != -17) && x != -16) && x != -15) && x != -14) && x != -13) && x != -12) && x != -11) && x != -10) && x != -9) && x != -8) && x != -7) && x != -6))) || ((-1 <= x && x <= 2147483645) && x != 0)) || (-1 <= x && x <= 2147483645)) || ((((((((((((((((((((((((((((((-28 <= x && x <= 2147483617) && x != -31) && x != -30) && x != -29) && x != -28) && x != -27) && x != -26) && x != -25) && x != -24) && x != -23) && x != -22) && x != -21) && x != -20) && x != -19) && x != -18) && x != -17) && x != -16) && x != -15) && x != -14) && x != -13) && x != -12) && x != -11) && x != -10) && x != -9) && x != -8) && x != -7) && x != -6) && x != -5) && x != -4) && x != 0)) || (((((((((((((((((((((((((((((-28 <= x && x <= 2147483617) && x != -31) && x != -30) && x != -29) && x != -28) && x != -27) && x != -26) && x != -25) && x != -24) && x != -23) && x != -22) && x != -21) && x != -20) && x != -19) && x != -18) && x != -17) && x != -16) && x != -15) && x != -14) && x != -13) && x != -12) && x != -11) && x != -10) && x != -9) && x != -8) && x != -7) && x != -6) && x != -5) && x != -4))) || (1 <= x && x != 0)) || (1 <= x && x != 0)) || ((((((((((((((((((((((((((((((-26 <= x && x <= 2147483619) && x != -29) && x != -28) && x != -27) && x != -26) && x != -25) && x != -24) && x != -23) && x != -22) && x != -21) && x != -20) && x != -19) && x != -18) && x != -17) && x != -16) && x != -15) && x != -14) && x != -13) && x != -12) && x != -11) && x != -10) && x != -9) && x != -8) && x != -7) && x != -6) && x != -5) && x != -4) && x != -3) && x != -2) && x != 0)) || (((((((((((((((((((((((((((((-26 <= x && x <= 2147483619) && x != -29) && x != -28) && x != -27) && x != -26) && x != -25) && x != -24) && x != -23) && x != -22) && x != -21) && x != -20) && x != -19) && x != -18) && x != -17) && x != -16) && x != -15) && x != -14) && x != -13) && x != -12) && x != -11) && x != -10) && x != -9) && x != -8) && x != -7) && x != -6) && x != -5) && x != -4) && x != -3) && x != -2) format: c_expression correctness_witness CPAchecker 2.3 25 2023-12-01T05:18:21+01:00

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

Trying to find witnesses for program (709a9fb1525fc89256c547fbe03fef24399be5d6458f17d55fb4fce36419b886, ../../../comp/sv-benchmarks/c/termination-crafted/Cairo_step2_true-no-overflow_true-termination_true-valid-memsafety.c).

Found 18 witnesses for program ../../../comp/sv-benchmarks/c/termination-crafted/Cairo_step2_true-no-overflow_true-termination_true-valid-memsafety.c, 709a9fb1525fc89256c547fbe03fef24399be5d6458f17d55fb4fce36419b886
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/709a9fb1525fc89256c547fbe03fef24399be5d6458f17d55fb4fce36419b886.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download affd3e9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.4.0 3 2022-12-09T12:17:44Z
Download c1bef09 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-22 4 2022-12-10T22:18:26+01:00
Download d5be043 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness VeriOover 1 2022-12-12T11:01 CET (comp)
Download a385444 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 5 2022-12-14T04:25:32Z
Download 7611e1d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Kojak 5 2022-12-14T17:46:19Z
Download 058201f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T11:46:57+01:00 Download d5be043
Download 371fbf3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T11:20:31+01:00 Download a385444
Download d6f593c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T07:39:48+01:00 Download 8b494f2
Download 869a617 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T06:43:56+01:00 Download 7611e1d
Download a16e284 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T03:24:18+01:00 Download b330f02
Download cffafcc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T23:07:05+01:00 Download c1bef09
Download f1b57e9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T18:46:47+01:00 Download dedc107
Download f74f8bd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T17:47:26+01:00 Download affd3e9
Download f676562 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T11:55:34+01:00 Download 7045edd
Download 7045edd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2022-12-10T18:32:13+01:00
Download b330f02 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-1715bd67dc+ 4 2022-12-11T21:51:54+01:00
Download dedc107 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 4 2022-12-10T04:35:59+01:00
Download 8b494f2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 5 2022-12-13T16:45:49Z

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

Trying to find witnesses for program (709a9fb1525fc89256c547fbe03fef24399be5d6458f17d55fb4fce36419b886, ../../../comp/sv-benchmarks/c/termination-crafted/Cairo_step2_true-no-overflow_true-termination_true-valid-memsafety.c).

Found 15 witnesses for program ../../../comp/sv-benchmarks/c/termination-crafted/Cairo_step2_true-no-overflow_true-termination_true-valid-memsafety.c, 709a9fb1525fc89256c547fbe03fef24399be5d6458f17d55fb4fce36419b886
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/709a9fb1525fc89256c547fbe03fef24399be5d6458f17d55fb4fce36419b886.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 84b5c89 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.2.8 3 2021-12-13T22:19:41Z
Download 05cbdf5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-22 4 2021-12-06T14:17:32+01:00
Download ad27f6f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 5 2021-12-10T06:32:12Z
Download bd49ae8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Kojak 5 2021-12-10T11:52:55Z
Download 106fd29 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2021-12-10T17:42:37+01:00 Download bd49ae8
Download fbe3127 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2021-12-10T09:05:37+01:00 Download ad27f6f
Download 281fc7f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2021-12-09T16:07:34+01:00 Download fb9e413
Download af93817 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2021-12-08T22:32:05+01:00 Download 71727b6
Download 59641fc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2021-12-07T03:08:41+01:00 Download e21b8c0
Download b323f06 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2021-12-06T15:00:04+01:00 Download 05cbdf5
Download 77a0c26 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2021-12-05T20:11:28+01:00 Download 0363102
Download 0363102 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 4 2021-12-05T17:39:16+01:00
Download 71727b6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-fe6f522dd3+ 4 2021-12-08T19:37:53+01:00
Download fb9e413 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-eda176372c+ 4 2021-12-09T11:34:45+01:00
Download e21b8c0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 5 2021-12-06T21:16:48Z

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

Trying to find witnesses for program (709a9fb1525fc89256c547fbe03fef24399be5d6458f17d55fb4fce36419b886, ../../../comp/sv-benchmarks/c/termination-crafted/Cairo_step2_true-no-overflow_true-termination_true-valid-memsafety.c).

Found 9 witnesses for program ../../../comp/sv-benchmarks/c/termination-crafted/Cairo_step2_true-no-overflow_true-termination_true-valid-memsafety.c, 709a9fb1525fc89256c547fbe03fef24399be5d6458f17d55fb4fce36419b886
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/709a9fb1525fc89256c547fbe03fef24399be5d6458f17d55fb4fce36419b886.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download c55f454 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.2.1 3 2020-12-06T23:50:15
Download 2492ba0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) unknown_witness Goblint (svcomp21-0-g82e03b87) 3 2020-12-07T12:17:54
Download 565b00d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 5 2020-12-09T22:23:50+01:00 Download 58f9e21
Download 2d73cfd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 5 2020-12-09T21:27:07+01:00 Download 92a7a8e
Download 3082d49 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 5 2020-12-09T02:49:37+01:00 Download 360ba2a
Download af07855 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 5 2020-12-08T06:46:47+01:00 Download 0ab2f08
Download 79f283c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 5 2020-12-06T14:30:21+01:00 Download 0a11914
Download 0a11914 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 4 2020-12-05T12:32:56+01:00
Download 0ab2f08 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-eda176372c+ 4 2020-12-08T04:22:12+01:00

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

Trying to find witnesses for program (709a9fb1525fc89256c547fbe03fef24399be5d6458f17d55fb4fce36419b886, ../../../comp/sv-benchmarks/c/termination-crafted/Cairo_step2_true-no-overflow_true-termination_true-valid-memsafety.c).

Found 4 witnesses for program ../../../comp/sv-benchmarks/c/termination-crafted/Cairo_step2_true-no-overflow_true-termination_true-valid-memsafety.c, 709a9fb1525fc89256c547fbe03fef24399be5d6458f17d55fb4fce36419b886
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/709a9fb1525fc89256c547fbe03fef24399be5d6458f17d55fb4fce36419b886.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 8980bf5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ 5 2019-12-01T06:05:31+01:00
Download 4c35d10 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 1.9 5 2019-11-30T14:49:44+01:00
Download 34e27aa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.9 4 2019-11-29T15:02:02+01:00
Download e0bf5ad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ 4 2019-12-01T02:21:52+01:00

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

Trying to find witnesses for program (709a9fb1525fc89256c547fbe03fef24399be5d6458f17d55fb4fce36419b886, ../../../comp/sv-benchmarks/c/termination-crafted/Cairo_step2_true-no-overflow_true-termination_true-valid-memsafety.c).

Found 3 witnesses for program ../../../comp/sv-benchmarks/c/termination-crafted/Cairo_step2_true-no-overflow_true-termination_true-valid-memsafety.c, 709a9fb1525fc89256c547fbe03fef24399be5d6458f17d55fb4fce36419b886
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/709a9fb1525fc89256c547fbe03fef24399be5d6458f17d55fb4fce36419b886.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download ff0b5b1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness SMACK 1.9.3 3 2018-12-08T17:19:02
Download b25ddd7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 5 2018-12-08T02:53:14+01:00
Download e674d62 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T08:01:45+01:00

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

Trying to find witnesses for program (709a9fb1525fc89256c547fbe03fef24399be5d6458f17d55fb4fce36419b886, ../../../comp/sv-benchmarks/c/termination-crafted/Cairo_step2_true-no-overflow_true-termination_true-valid-memsafety.c).

Found 4 witnesses for program ../../../comp/sv-benchmarks/c/termination-crafted/Cairo_step2_true-no-overflow_true-termination_true-valid-memsafety.c, 709a9fb1525fc89256c547fbe03fef24399be5d6458f17d55fb4fce36419b886
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/709a9fb1525fc89256c547fbe03fef24399be5d6458f17d55fb4fce36419b886.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download efbb860 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 5 2017-12-03T07:43Z
Download ab7c633 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Kojak 5 2017-12-03T10:30Z
Download b64fcf1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 5 2017-12-03T10:31Z
Download 0daf727 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 4 2017-12-01T17:33 CET (sv-comp)

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

Trying to find witnesses for program (709a9fb1525fc89256c547fbe03fef24399be5d6458f17d55fb4fce36419b886, ../../../comp/sv-benchmarks/c/termination-crafted/Cairo_step2_true-no-overflow_true-termination_true-valid-memsafety.c).

Found 0 witnesses for program ../../../comp/sv-benchmarks/c/termination-crafted/Cairo_step2_true-no-overflow_true-termination_true-valid-memsafety.c, 709a9fb1525fc89256c547fbe03fef24399be5d6458f17d55fb4fce36419b886
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/709a9fb1525fc89256c547fbe03fef24399be5d6458f17d55fb4fce36419b886.json

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