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 (de331d1f778f147a4d32c0286c0018cb5b5cf61f2b6c0952b6bed68b0f715eaf, sv-benchmarks/c/termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c).

Found 9 witnesses for program sv-benchmarks/c/termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c, de331d1f778f147a4d32c0286c0018cb5b5cf61f2b6c0952b6bed68b0f715eaf
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/de331d1f778f147a4d32c0286c0018cb5b5cf61f2b6c0952b6bed68b0f715eaf.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 3d22aa0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.4.0 3 2023-12-03T04:27:55Z
Download 208e61a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-24 4 2023-12-03T18:02:11+01:00
Download f0b752a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness VeriOover 1 2023-12-20T03:37 CET (comp)
Download dc2bee6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-12-03T18:44:35+01:00 Download 208e61a
Download 9af482e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-12-03T10:02:05+01:00 Download 3d22aa0
Download 87007f9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-11-30T12:41:35+01:00 Download 1eb6b05
Download 1eb6b05 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-11-30T05:53:28+01:00
Download 80fc508 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 8 2023-12-18T22:18:30+01:00
Download 5353ea2 Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: "2.0" uuid: a3c7957a-95aa-4fe9-98bd-3ae2288ea108 creation_time: 2023-12-01T01:40:55Z 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-lit/HarrisLalNoriRajamani-SAS2010-Fig1.c''' task: input_files: - ../../sv-benchmarks/c/termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1.c input_file_hashes: ../../sv-benchmarks/c/termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1.c: de331d1f778f147a4d32c0286c0018cb5b5cf61f2b6c0952b6bed68b0f715eaf 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-lit/HarrisLalNoriRajamani-SAS2010-Fig1.c file_hash: de331d1f778f147a4d32c0286c0018cb5b5cf61f2b6c0952b6bed68b0f715eaf line: 27 column: 8 function: f value: 0 <= d format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1.c file_hash: de331d1f778f147a4d32c0286c0018cb5b5cf61f2b6c0952b6bed68b0f715eaf line: 27 column: 8 function: f value: 1 <= d format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1.c file_hash: de331d1f778f147a4d32c0286c0018cb5b5cf61f2b6c0952b6bed68b0f715eaf line: 27 column: 8 function: f value: d <= 2 format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1.c file_hash: de331d1f778f147a4d32c0286c0018cb5b5cf61f2b6c0952b6bed68b0f715eaf line: 27 column: 8 function: f value: d <= 127 format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1.c file_hash: de331d1f778f147a4d32c0286c0018cb5b5cf61f2b6c0952b6bed68b0f715eaf line: 27 column: 8 function: f value: k <= 1073741823 format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1.c file_hash: de331d1f778f147a4d32c0286c0018cb5b5cf61f2b6c0952b6bed68b0f715eaf line: 27 column: 8 function: f value: z <= 2147483644 format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1.c file_hash: de331d1f778f147a4d32c0286c0018cb5b5cf61f2b6c0952b6bed68b0f715eaf line: 27 column: 8 function: f value: (1073741822LL + (long long )d) - (long long )k >= 0LL format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1.c file_hash: de331d1f778f147a4d32c0286c0018cb5b5cf61f2b6c0952b6bed68b0f715eaf line: 27 column: 8 function: f value: (2147483646LL + (long long )d) - (long long )z >= 0LL format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1.c file_hash: de331d1f778f147a4d32c0286c0018cb5b5cf61f2b6c0952b6bed68b0f715eaf line: 27 column: 8 function: f value: (1073741825LL - (long long )d) - (long long )k >= 0LL format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1.c file_hash: de331d1f778f147a4d32c0286c0018cb5b5cf61f2b6c0952b6bed68b0f715eaf line: 27 column: 8 function: f value: (2147483648LL - (long long )d) - (long long )z >= 0LL format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1.c file_hash: de331d1f778f147a4d32c0286c0018cb5b5cf61f2b6c0952b6bed68b0f715eaf line: 27 column: 8 function: f value: (3221225470LL - (long long )k) - (long long )z >= 0LL format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1.c file_hash: de331d1f778f147a4d32c0286c0018cb5b5cf61f2b6c0952b6bed68b0f715eaf line: 27 column: 8 function: f value: d != 0 format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1.c file_hash: de331d1f778f147a4d32c0286c0018cb5b5cf61f2b6c0952b6bed68b0f715eaf line: 27 column: 8 function: f value: d == 1 || d == 2 format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1.c file_hash: de331d1f778f147a4d32c0286c0018cb5b5cf61f2b6c0952b6bed68b0f715eaf line: 27 column: 8 function: f value: ((2147483646LL + (long long )x) - (long long )z >= 0LL && ((((((((((1 <= x && (-2LL + (long long )d) + (long long )x >= 0LL) && (1LL - (long long )d) + (long long )x >= 0LL) && (1073741822LL - (long long )k) + (long long )x >= 0LL) && x != 0) || (((-1 <= x && (-1LL + (long long )d) + (long long )x >= 0LL) && (3LL - (long long )d) + (long long )x >= 0LL) && (1073741824LL - (long long )k) + (long long )x >= 0LL)) || (((((((((-1 <= z && 1 <= x) && (-2LL + (long long )d) + (long long )x >= 0LL) && (1LL - (long long )d) + (long long )x >= 0LL) && (2LL - (long long )k) + (long long )z >= 0LL) && (3LL - (long long )d) + (long long )z >= 0LL) && (1073741822LL - (long long )k) + (long long )x >= 0LL) && (long long )d + (long long )z >= 0LL) && (long long )x + (long long )z >= 0LL) && x != 0)) || ((((((((-1 <= x && -1 <= z) && (-1LL + (long long )d) + (long long )x >= 0LL) && (2LL + (long long )x) + (long long )z >= 0LL) && (2LL - (long long )k) + (long long )z >= 0LL) && (3LL - (long long )d) + (long long )x >= 0LL) && (3LL - (long long )d) + (long long )z >= 0LL) && (1073741824LL - (long long )k) + (long long )x >= 0LL) && (long long )d + (long long )z >= 0LL)) || (((((((((0 <= z && 1 <= x) && (-2LL + (long long )d) + (long long )x >= 0LL) && (-1LL + (long long )d) + (long long )z >= 0LL) && (-1LL + (long long )x) + (long long )z >= 0LL) && (1LL - (long long )d) + (long long )x >= 0LL) && (1LL - (long long )k) + (long long )z >= 0LL) && (2LL - (long long )d) + (long long )z >= 0LL) && (1073741822LL - (long long )k) + (long long )x >= 0LL) && x != 0)) || ((((((((-1 <= x && 0 <= z) && (-1LL + (long long )d) + (long long )x >= 0LL) && (-1LL + (long long )d) + (long long )z >= 0LL) && (1LL + (long long )x) + (long long )z >= 0LL) && (1LL - (long long )k) + (long long )z >= 0LL) && (2LL - (long long )d) + (long long )z >= 0LL) && (3LL - (long long )d) + (long long )x >= 0LL) && (1073741824LL - (long long )k) + (long long )x >= 0LL)) || ((((((((((1 <= x && 1 <= z) && (-2LL + (long long )d) + (long long )x >= 0LL) && (-2LL + (long long )d) + (long long )z >= 0LL) && (-2LL + (long long )x) + (long long )z >= 0LL) && (0LL - (long long )k) + (long long )z >= 0LL) && (1LL - (long long )d) + (long long )x >= 0LL) && (1LL - (long long )d) + (long long )z >= 0LL) && (1073741822LL - (long long )k) + (long long )x >= 0LL) && x != 0) && z != 0))) || ((((1 <= z && (-2LL + (long long )d) + (long long )z >= 0LL) && (0LL - (long long )k) + (long long )z >= 0LL) && (1LL - (long long )d) + (long long )z >= 0LL) && z != 0) format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1.c file_hash: de331d1f778f147a4d32c0286c0018cb5b5cf61f2b6c0952b6bed68b0f715eaf line: 23 column: 8 function: f value: 0 <= d format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1.c file_hash: de331d1f778f147a4d32c0286c0018cb5b5cf61f2b6c0952b6bed68b0f715eaf line: 23 column: 8 function: f value: 1 <= d format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1.c file_hash: de331d1f778f147a4d32c0286c0018cb5b5cf61f2b6c0952b6bed68b0f715eaf line: 23 column: 8 function: f value: d <= 2 format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1.c file_hash: de331d1f778f147a4d32c0286c0018cb5b5cf61f2b6c0952b6bed68b0f715eaf line: 23 column: 8 function: f value: d <= 127 format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1.c file_hash: de331d1f778f147a4d32c0286c0018cb5b5cf61f2b6c0952b6bed68b0f715eaf line: 23 column: 8 function: f value: k <= 1073741823 format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1.c file_hash: de331d1f778f147a4d32c0286c0018cb5b5cf61f2b6c0952b6bed68b0f715eaf line: 23 column: 8 function: f value: (1073741822LL + (long long )d) - (long long )k >= 0LL format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1.c file_hash: de331d1f778f147a4d32c0286c0018cb5b5cf61f2b6c0952b6bed68b0f715eaf line: 23 column: 8 function: f value: (1073741825LL - (long long )d) - (long long )k >= 0LL format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1.c file_hash: de331d1f778f147a4d32c0286c0018cb5b5cf61f2b6c0952b6bed68b0f715eaf line: 23 column: 8 function: f value: d != 0 format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1.c file_hash: de331d1f778f147a4d32c0286c0018cb5b5cf61f2b6c0952b6bed68b0f715eaf line: 23 column: 8 function: f value: d == 1 || d == 2 format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1.c file_hash: de331d1f778f147a4d32c0286c0018cb5b5cf61f2b6c0952b6bed68b0f715eaf line: 23 column: 8 function: f value: (((k != 0 && (((((((((((((((((((((((((((((((((32769 <= k && (-98305LL + (long long )k) + (long long )z >= 0LL) && (-65537LL + (long long )d) + (long long )z >= 0LL) && (-32770LL + (long long )d) + (long long )k >= 0LL) && (-65534LL - (long long )d) + (long long )z >= 0LL) && (-32767LL - (long long )d) + (long long )k >= 0LL) && (1073676287LL - (long long )k) + (long long )z >= 0LL) && (32767LL + (long long )k) - (long long )z >= 0LL) && (65535LL + (long long )d) - (long long )z >= 0LL) && (65538LL - (long long )d) - (long long )z >= 0LL) && (1073807359LL - (long long )k) - (long long )z >= 0LL) && z == 65536) || (((((((((((16385 <= k && (-49153LL + (long long )k) + (long long )z >= 0LL) && (-32769LL + (long long )d) + (long long )z >= 0LL) && (-16386LL + (long long )d) + (long long )k >= 0LL) && (-32766LL - (long long )d) + (long long )z >= 0LL) && (-16383LL - (long long )d) + (long long )k >= 0LL) && (1073709055LL - (long long )k) + (long long )z >= 0LL) && (16383LL + (long long )k) - (long long )z >= 0LL) && (32767LL + (long long )d) - (long long )z >= 0LL) && (32770LL - (long long )d) - (long long )z >= 0LL) && (1073774591LL - (long long )k) - (long long )z >= 0LL) && z == 32768)) || (((((((((((8193 <= k && (-24577LL + (long long )k) + (long long )z >= 0LL) && (-16385LL + (long long )d) + (long long )z >= 0LL) && (-8194LL + (long long )d) + (long long )k >= 0LL) && (-16382LL - (long long )d) + (long long )z >= 0LL) && (-8191LL - (long long )d) + (long long )k >= 0LL) && (1073725439LL - (long long )k) + (long long )z >= 0LL) && (8191LL + (long long )k) - (long long )z >= 0LL) && (16383LL + (long long )d) - (long long )z >= 0LL) && (16386LL - (long long )d) - (long long )z >= 0LL) && (1073758207LL - (long long )k) - (long long )z >= 0LL) && z == 16384)) || (((((((((((4097 <= k && (-12289LL + (long long )k) + (long long )z >= 0LL) && (-8193LL + (long long )d) + (long long )z >= 0LL) && (-4098LL + (long long )d) + (long long )k >= 0LL) && (-8190LL - (long long )d) + (long long )z >= 0LL) && (-4095LL - (long long )d) + (long long )k >= 0LL) && (1073733631LL - (long long )k) + (long long )z >= 0LL) && (4095LL + (long long )k) - (long long )z >= 0LL) && (8191LL + (long long )d) - (long long )z >= 0LL) && (8194LL - (long long )d) - (long long )z >= 0LL) && (1073750015LL - (long long )k) - (long long )z >= 0LL) && z == 8192)) || (((((((((((2049 <= k && (-6145LL + (long long )k) + (long long )z >= 0LL) && (-4097LL + (long long )d) + (long long )z >= 0LL) && (-2050LL + (long long )d) + (long long )k >= 0LL) && (-4094LL - (long long )d) + (long long )z >= 0LL) && (-2047LL - (long long )d) + (long long )k >= 0LL) && (1073737727LL - (long long )k) + (long long )z >= 0LL) && (2047LL + (long long )k) - (long long )z >= 0LL) && (4095LL + (long long )d) - (long long )z >= 0LL) && (4098LL - (long long )d) - (long long )z >= 0LL) && (1073745919LL - (long long )k) - (long long )z >= 0LL) && z == 4096)) || (((((((((((1025 <= k && (-3073LL + (long long )k) + (long long )z >= 0LL) && (-2049LL + (long long )d) + (long long )z >= 0LL) && (-1026LL + (long long )d) + (long long )k >= 0LL) && (-2046LL - (long long )d) + (long long )z >= 0LL) && (-1023LL - (long long )d) + (long long )k >= 0LL) && (1073739775LL - (long long )k) + (long long )z >= 0LL) && (1023LL + (long long )k) - (long long )z >= 0LL) && (2047LL + (long long )d) - (long long )z >= 0LL) && (2050LL - (long long )d) - (long long )z >= 0LL) && (1073743871LL - (long long )k) - (long long )z >= 0LL) && z == 2048)) || (((((((((((513 <= k && (-1537LL + (long long )k) + (long long )z >= 0LL) && (-1025LL + (long long )d) + (long long )z >= 0LL) && (-514LL + (long long )d) + (long long )k >= 0LL) && (-1022LL - (long long )d) + (long long )z >= 0LL) && (-511LL - (long long )d) + (long long )k >= 0LL) && (1073740799LL - (long long )k) + (long long )z >= 0LL) && (511LL + (long long )k) - (long long )z >= 0LL) && (1023LL + (long long )d) - (long long )z >= 0LL) && (1026LL - (long long )d) - (long long )z >= 0LL) && (1073742847LL - (long long )k) - (long long )z >= 0LL) && z == 1024)) || (((((((((((257 <= k && (-769LL + (long long )k) + (long long )z >= 0LL) && (-513LL + (long long )d) + (long long )z >= 0LL) && (-258LL + (long long )d) + (long long )k >= 0LL) && (-510LL - (long long )d) + (long long )z >= 0LL) && (-255LL - (long long )d) + (long long )k >= 0LL) && (1073741311LL - (long long )k) + (long long )z >= 0LL) && (255LL + (long long )k) - (long long )z >= 0LL) && (511LL + (long long )d) - (long long )z >= 0LL) && (514LL - (long long )d) - (long long )z >= 0LL) && (1073742335LL - (long long )k) - (long long )z >= 0LL) && z == 512)) || (((((((((((129 <= k && (-385LL + (long long )k) + (long long )z >= 0LL) && (-257LL + (long long )d) + (long long )z >= 0LL) && (-130LL + (long long )d) + (long long )k >= 0LL) && (-254LL - (long long )d) + (long long )z >= 0LL) && (-127LL - (long long )d) + (long long )k >= 0LL) && (1073741567LL - (long long )k) + (long long )z >= 0LL) && (127LL + (long long )k) - (long long )z >= 0LL) && (255LL + (long long )d) - (long long )z >= 0LL) && (258LL - (long long )d) - (long long )z >= 0LL) && (1073742079LL - (long long )k) - (long long )z >= 0LL) && z == 256)) || (((((((((((65 <= k && (-193LL + (long long )k) + (long long )z >= 0LL) && (-129LL + (long long )d) + (long long )z >= 0LL) && (-66LL + (long long )d) + (long long )k >= 0LL) && (-126LL - (long long )d) + (long long )z >= 0LL) && (-63LL - (long long )d) + (long long )k >= 0LL) && (1073741695LL - (long long )k) + (long long )z >= 0LL) && (63LL + (long long )k) - (long long )z >= 0LL) && (127LL + (long long )d) - (long long )z >= 0LL) && (130LL - (long long )d) - (long long )z >= 0LL) && (1073741951LL - (long long )k) - (long long )z >= 0LL) && z == 128)) || (((((((((((((16777217 <= k && 33554432 <= z) && z <= 2147483644) && (-50331649LL + (long long )k) + (long long )z >= 0LL) && (-33554433LL + (long long )d) + (long long )z >= 0LL) && (-16777218LL + (long long )d) + (long long )k >= 0LL) && (-33554430LL - (long long )d) + (long long )z >= 0LL) && (-16777215LL - (long long )d) + (long long )k >= 0LL) && (1040187391LL - (long long )k) + (long long )z >= 0LL) && (1073741824LL + (long long )k) - (long long )z >= 0LL) && (2147483646LL + (long long )d) - (long long )z >= 0LL) && (2147483648LL - (long long )d) - (long long )z >= 0LL) && (3221225470LL - (long long )k) - (long long )z >= 0LL) && z % 33554432 == 0)) || (((((((((((33 <= k && (-97LL + (long long )k) + (long long )z >= 0LL) && (-65LL + (long long )d) + (long long )z >= 0LL) && (-34LL + (long long )d) + (long long )k >= 0LL) && (-62LL - (long long )d) + (long long )z >= 0LL) && (-31LL - (long long )d) + (long long )k >= 0LL) && (1073741759LL - (long long )k) + (long long )z >= 0LL) && (31LL + (long long )k) - (long long )z >= 0LL) && (63LL + (long long )d) - (long long )z >= 0LL) && (66LL - (long long )d) - (long long )z >= 0LL) && (1073741887LL - (long long )k) - (long long )z >= 0LL) && z == 64)) || (((((((((((8388609 <= k && (-25165825LL + (long long )k) + (long long )z >= 0LL) && (-16777217LL + (long long )d) + (long long )z >= 0LL) && (-8388610LL + (long long )d) + (long long )k >= 0LL) && (-16777214LL - (long long )d) + (long long )z >= 0LL) && (-8388607LL - (long long )d) + (long long )k >= 0LL) && (1056964607LL - (long long )k) + (long long )z >= 0LL) && (8388607LL + (long long )k) - (long long )z >= 0LL) && (16777215LL + (long long )d) - (long long )z >= 0LL) && (16777218LL - (long long )d) - (long long )z >= 0LL) && (1090519039LL - (long long )k) - (long long )z >= 0LL) && z == 16777216)) || (((((((((((17 <= k && (-49LL + (long long )k) + (long long )z >= 0LL) && (-33LL + (long long )d) + (long long )z >= 0LL) && (-18LL + (long long )d) + (long long )k >= 0LL) && (-30LL - (long long )d) + (long long )z >= 0LL) && (-15LL - (long long )d) + (long long )k >= 0LL) && (1073741791LL - (long long )k) + (long long )z >= 0LL) && (15LL + (long long )k) - (long long )z >= 0LL) && (31LL + (long long )d) - (long long )z >= 0LL) && (34LL - (long long )d) - (long long )z >= 0LL) && (1073741855LL - (long long )k) - (long long )z >= 0LL) && z == 32)) || (((((((((((4194305 <= k && (-12582913LL + (long long )k) + (long long )z >= 0LL) && (-8388609LL + (long long )d) + (long long )z >= 0LL) && (-4194306LL + (long long )d) + (long long )k >= 0LL) && (-8388606LL - (long long )d) + (long long )z >= 0LL) && (-4194303LL - (long long )d) + (long long )k >= 0LL) && (1065353215LL - (long long )k) + (long long )z >= 0LL) && (4194303LL + (long long )k) - (long long )z >= 0LL) && (8388607LL + (long long )d) - (long long )z >= 0LL) && (8388610LL - (long long )d) - (long long )z >= 0LL) && (1082130431LL - (long long )k) - (long long )z >= 0LL) && z == 8388608)) || (((((((((((9 <= k && (-25LL + (long long )k) + (long long )z >= 0LL) && (-17LL + (long long )d) + (long long )z >= 0LL) && (-10LL + (long long )d) + (long long )k >= 0LL) && (-14LL - (long long )d) + (long long )z >= 0LL) && (-7LL - (long long )d) + (long long )k >= 0LL) && (1073741807LL - (long long )k) + (long long )z >= 0LL) && (7LL + (long long )k) - (long long )z >= 0LL) && (15LL + (long long )d) - (long long )z >= 0LL) && (18LL - (long long )d) - (long long )z >= 0LL) && (1073741839LL - (long long )k) - (long long )z >= 0LL) && z == 16)) || (((((((((((2097153 <= k && (-6291457LL + (long long )k) + (long long )z >= 0LL) && (-4194305LL + (long long )d) + (long long )z >= 0LL) && (-2097154LL + (long long )d) + (long long )k >= 0LL) && (-4194302LL - (long long )d) + (long long )z >= 0LL) && (-2097151LL - (long long )d) + (long long )k >= 0LL) && (1069547519LL - (long long )k) + (long long )z >= 0LL) && (2097151LL + (long long )k) - (long long )z >= 0LL) && (4194303LL + (long long )d) - (long long )z >= 0LL) && (4194306LL - (long long )d) - (long long )z >= 0LL) && (1077936127LL - (long long )k) - (long long )z >= 0LL) && z == 4194304)) || (((((((((((5 <= k && (-13LL + (long long )k) + (long long )z >= 0LL) && (-9LL + (long long )d) + (long long )z >= 0LL) && (-6LL + (long long )d) + (long long )k >= 0LL) && (-6LL - (long long )d) + (long long )z >= 0LL) && (-3LL - (long long )d) + (long long )k >= 0LL) && (1073741815LL - (long long )k) + (long long )z >= 0LL) && (3LL + (long long )k) - (long long )z >= 0LL) && (7LL + (long long )d) - (long long )z >= 0LL) && (10LL - (long long )d) - (long long )z >= 0LL) && (1073741831LL - (long long )k) - (long long )z >= 0LL) && z == 8)) || (((((((((((1048577 <= k && (-3145729LL + (long long )k) + (long long )z >= 0LL) && (-2097153LL + (long long )d) + (long long )z >= 0LL) && (-1048578LL + (long long )d) + (long long )k >= 0LL) && (-2097150LL - (long long )d) + (long long )z >= 0LL) && (-1048575LL - (long long )d) + (long long )k >= 0LL) && (1071644671LL - (long long )k) + (long long )z >= 0LL) && (1048575LL + (long long )k) - (long long )z >= 0LL) && (2097151LL + (long long )d) - (long long )z >= 0LL) && (2097154LL - (long long )d) - (long long )z >= 0LL) && (1075838975LL - (long long )k) - (long long )z >= 0LL) && z == 2097152)) || (((((((((((3 <= k && (-7LL + (long long )k) + (long long )z >= 0LL) && (-5LL + (long long )d) + (long long )z >= 0LL) && (-4LL + (long long )d) + (long long )k >= 0LL) && (-2LL - (long long )d) + (long long )z >= 0LL) && (-1LL - (long long )d) + (long long )k >= 0LL) && (1073741819LL - (long long )k) + (long long )z >= 0LL) && (1LL + (long long )k) - (long long )z >= 0LL) && (3LL + (long long )d) - (long long )z >= 0LL) && (6LL - (long long )d) - (long long )z >= 0LL) && (1073741827LL - (long long )k) - (long long )z >= 0LL) && z == 4)) || (((((((((((524289 <= k && (-1572865LL + (long long )k) + (long long )z >= 0LL) && (-1048577LL + (long long )d) + (long long )z >= 0LL) && (-524290LL + (long long )d) + (long long )k >= 0LL) && (-1048574LL - (long long )d) + (long long )z >= 0LL) && (-524287LL - (long long )d) + (long long )k >= 0LL) && (1072693247LL - (long long )k) + (long long )z >= 0LL) && (524287LL + (long long )k) - (long long )z >= 0LL) && (1048575LL + (long long )d) - (long long )z >= 0LL) && (1048578LL - (long long )d) - (long long )z >= 0LL) && (1074790399LL - (long long )k) - (long long )z >= 0LL) && z == 1048576)) || (((((((((((2 <= k && (-4LL + (long long )k) + (long long )z >= 0LL) && (-3LL + (long long )d) + (long long )k >= 0LL) && (-3LL + (long long )d) + (long long )z >= 0LL) && (0LL - (long long )d) + (long long )k >= 0LL) && (0LL - (long long )d) + (long long )z >= 0LL) && (1073741821LL - (long long )k) + (long long )z >= 0LL) && (1LL + (long long )d) - (long long )z >= 0LL) && (4LL - (long long )d) - (long long )z >= 0LL) && (1073741825LL - (long long )k) - (long long )z >= 0LL) && (long long )k - (long long )z >= 0LL) && z == 2)) || (((((((((((262145 <= k && (-786433LL + (long long )k) + (long long )z >= 0LL) && (-524289LL + (long long )d) + (long long )z >= 0LL) && (-262146LL + (long long )d) + (long long )k >= 0LL) && (-524286LL - (long long )d) + (long long )z >= 0LL) && (-262143LL - (long long )d) + (long long )k >= 0LL) && (1073217535LL - (long long )k) + (long long )z >= 0LL) && (262143LL + (long long )k) - (long long )z >= 0LL) && (524287LL + (long long )d) - (long long )z >= 0LL) && (524290LL - (long long )d) - (long long )z >= 0LL) && (1074266111LL - (long long )k) - (long long )z >= 0LL) && z == 524288))) || (((((((-2LL + (long long )d) + (long long )z >= 0LL && (1LL - (long long )d) + (long long )z >= 0LL) && (1073741822LL - (long long )k) + (long long )z >= 0LL) && (3LL - (long long )d) - (long long )z >= 0LL) && (1073741824LL - (long long )k) - (long long )z >= 0LL) && (long long )d - (long long )z >= 0LL) && z == 1)) || ((((((((((((131073 <= k && (-393217LL + (long long )k) + (long long )z >= 0LL) && (-262145LL + (long long )d) + (long long )z >= 0LL) && (-131074LL + (long long )d) + (long long )k >= 0LL) && (-262142LL - (long long )d) + (long long )z >= 0LL) && (-131071LL - (long long )d) + (long long )k >= 0LL) && (1073479679LL - (long long )k) + (long long )z >= 0LL) && (131071LL + (long long )k) - (long long )z >= 0LL) && (262143LL + (long long )d) - (long long )z >= 0LL) && (262146LL - (long long )d) - (long long )z >= 0LL) && (1074003967LL - (long long )k) - (long long )z >= 0LL) && z == 262144) && k != 0)) || ((((((((((((65537 <= k && (-196609LL + (long long )k) + (long long )z >= 0LL) && (-131073LL + (long long )d) + (long long )z >= 0LL) && (-65538LL + (long long )d) + (long long )k >= 0LL) && (-131070LL - (long long )d) + (long long )z >= 0LL) && (-65535LL - (long long )d) + (long long )k >= 0LL) && (1073610751LL - (long long )k) + (long long )z >= 0LL) && (65535LL + (long long )k) - (long long )z >= 0LL) && (131071LL + (long long )d) - (long long )z >= 0LL) && (131074LL - (long long )d) - (long long )z >= 0LL) && (1073872895LL - (long long )k) - (long long )z >= 0LL) && z == 131072) && k != 0) format: c_expression correctness_witness CPAchecker 2.3 40 2023-12-01T04:25:54+01:00

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

Trying to find witnesses for program (de331d1f778f147a4d32c0286c0018cb5b5cf61f2b6c0952b6bed68b0f715eaf, sv-benchmarks/c/termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c).

Found 10 witnesses for program sv-benchmarks/c/termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c, de331d1f778f147a4d32c0286c0018cb5b5cf61f2b6c0952b6bed68b0f715eaf
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/de331d1f778f147a4d32c0286c0018cb5b5cf61f2b6c0952b6bed68b0f715eaf.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 1eb43d2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.4.0 3 2022-12-09T12:15:12Z
Download 0c3fbaa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-22 4 2022-12-10T22:10:08+01:00
Download f0b752a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness VeriOover 1 2022-12-12T10:59 CET (comp)
Download 69da39c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2023-01-29T02:47:58+01:00 Download 70999bf
Download 4ffaca7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2023-01-28T23:05:46+01:00 Download 0c3fbaa
Download c141512 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2023-01-28T17:49:14+01:00 Download 1eb43d2
Download a4f5964 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2023-01-28T12:27:17+01:00 Download 0e0a38a
Download 0e0a38a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2022-12-10T16:08:49+01:00
Download 70999bf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-1715bd67dc+ 8 2022-12-11T23:28:52+01:00
Download 5d8a160 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 8 2022-12-10T03:10:11+01:00

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

Trying to find witnesses for program (de331d1f778f147a4d32c0286c0018cb5b5cf61f2b6c0952b6bed68b0f715eaf, sv-benchmarks/c/termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c).

Found 7 witnesses for program sv-benchmarks/c/termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c, de331d1f778f147a4d32c0286c0018cb5b5cf61f2b6c0952b6bed68b0f715eaf
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/de331d1f778f147a4d32c0286c0018cb5b5cf61f2b6c0952b6bed68b0f715eaf.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 7252549 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.2.8 3 2021-12-13T20:09:48Z
Download f4ff524 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-22 4 2021-12-06T13:34:58+01:00
Download a99c001 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 8 2021-12-05T20:11:33+01:00 Download 09f6392
Download 09f6392 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 8 2021-12-05T15:11:31+01:00
Download fb58b5d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-fe6f522dd3+ 8 2021-12-08T19:15:19+01:00
Download ac2a762 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-eda176372c+ 8 2021-12-09T11:49:17+01:00
Download cb3747f Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 2 2021-12-10T18:22:23

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

Trying to find witnesses for program (de331d1f778f147a4d32c0286c0018cb5b5cf61f2b6c0952b6bed68b0f715eaf, sv-benchmarks/c/termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c).

Found 7 witnesses for program sv-benchmarks/c/termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c, de331d1f778f147a4d32c0286c0018cb5b5cf61f2b6c0952b6bed68b0f715eaf
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/de331d1f778f147a4d32c0286c0018cb5b5cf61f2b6c0952b6bed68b0f715eaf.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download c7bf475 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.2.1 3 2020-12-06T23:34:18
Download eeee594 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) unknown_witness Goblint (svcomp21-0-g82e03b87) 3 2020-12-07T17:17:38
Download 6cdd42e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 8 2020-12-06T13:44:16+01:00 Download 90bbf8d
Download 90bbf8d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 8 2020-12-05T14:20:39+01:00
Download 7a0a844 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-eda176372c+ 8 2020-12-08T01:57:09+01:00
Download 9d35e44 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 2 2020-12-11T17:41:46
Download a341c89 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 2 2020-12-08T15:00:51

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

Trying to find witnesses for program (de331d1f778f147a4d32c0286c0018cb5b5cf61f2b6c0952b6bed68b0f715eaf, sv-benchmarks/c/termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c).

Found 0 witnesses for program sv-benchmarks/c/termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c, de331d1f778f147a4d32c0286c0018cb5b5cf61f2b6c0952b6bed68b0f715eaf
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/de331d1f778f147a4d32c0286c0018cb5b5cf61f2b6c0952b6bed68b0f715eaf.json

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

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

Trying to find witnesses for program (de331d1f778f147a4d32c0286c0018cb5b5cf61f2b6c0952b6bed68b0f715eaf, sv-benchmarks/c/termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c).

Found 2 witnesses for program sv-benchmarks/c/termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c, de331d1f778f147a4d32c0286c0018cb5b5cf61f2b6c0952b6bed68b0f715eaf
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/de331d1f778f147a4d32c0286c0018cb5b5cf61f2b6c0952b6bed68b0f715eaf.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download d285591 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 8 2018-12-07T08:03:23+01:00
Download c4b25ac Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-05T15:37:20+01:00

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

Trying to find witnesses for program (de331d1f778f147a4d32c0286c0018cb5b5cf61f2b6c0952b6bed68b0f715eaf, sv-benchmarks/c/termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c).

Found 1 witnesses for program sv-benchmarks/c/termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c, de331d1f778f147a4d32c0286c0018cb5b5cf61f2b6c0952b6bed68b0f715eaf
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/de331d1f778f147a4d32c0286c0018cb5b5cf61f2b6c0952b6bed68b0f715eaf.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 2614faf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 16 2017-12-01T18:27 CET (sv-comp)

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

Trying to find witnesses for program (de331d1f778f147a4d32c0286c0018cb5b5cf61f2b6c0952b6bed68b0f715eaf, sv-benchmarks/c/termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c).

Found 0 witnesses for program sv-benchmarks/c/termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c, de331d1f778f147a4d32c0286c0018cb5b5cf61f2b6c0952b6bed68b0f715eaf
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/de331d1f778f147a4d32c0286c0018cb5b5cf61f2b6c0952b6bed68b0f715eaf.json

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