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).
Found 12 witnesses for program sv-benchmarks/c/termination-restricted-15/Log_true-termination_true-no-overflow.c, 08d23a4fccc00925380f274033d6bce2f9ea0cd5a54ce734e93b963eb060b109
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/08d23a4fccc00925380f274033d6bce2f9ea0cd5a54ce734e93b963eb060b109.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
fb1765c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | frama-c-sv version 0.4.0 | 3 | 2023-12-03T04:23:24Z | ||
42d296f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-24 | 4 | 2023-12-03T17:53:18+01:00 | ||
ea6cb03 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | VeriOover | 1 | 2023-12-20T03:37 CET (comp) | ||
77b754d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 681 | 2023-12-20T03:55:49+01:00 | ea6cb03 | |
6110baf | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 641 | 2023-12-03T18:45:47+01:00 | 42d296f | |
f21a20b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 106 | 2023-12-03T10:01:31+01:00 | fb1765c | |
37546fc | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 681 | 2023-11-30T08:19:53+01:00 | ||
88c1faa | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 692 | 2023-12-03T21:54:49+01:00 | ||
74ae8cb | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 681 | 2023-12-18T19:38:35+01:00 | ||
9f681a1 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Goblint (tags/svcomp24-0-gc2e9465a7) | 3 | 2023-12-01T02:08:01Z | ||
7771a3a | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 9 | 2023-11-30T21:17:19+01:00 | ||
ee1a375 | Inspect | - entry_type: invariant_set metadata: format_version: "2.0" uuid: 5d32cb67-3baa-4771-b541-cb19bfe0b2f4 creation_time: 2023-12-01T01:47: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-restricted-15/Log.c''' task: input_files: - ../../sv-benchmarks/c/termination-restricted-15/Log.c input_file_hashes: ../../sv-benchmarks/c/termination-restricted-15/Log.c: 08d23a4fccc00925380f274033d6bce2f9ea0cd5a54ce734e93b963eb060b109 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/Log.c file_hash: 08d23a4fccc00925380f274033d6bce2f9ea0cd5a54ce734e93b963eb060b109 line: 13 column: 11 function: main value: 0 <= res format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-restricted-15/Log.c file_hash: 08d23a4fccc00925380f274033d6bce2f9ea0cd5a54ce734e93b963eb060b109 line: 13 column: 11 function: main value: (2147483648LL + (long long )res) + (long long )xtmp >= 0LL format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-restricted-15/Log.c file_hash: 08d23a4fccc00925380f274033d6bce2f9ea0cd5a54ce734e93b963eb060b109 line: 13 column: 11 function: main value: (2147483648LL + (long long )res) + (long long )restmp >= 0LL format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-restricted-15/Log.c file_hash: 08d23a4fccc00925380f274033d6bce2f9ea0cd5a54ce734e93b963eb060b109 line: 13 column: 11 function: main value: (4294967296LL + (long long )restmp) + (long long )xtmp >= 0LL format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-restricted-15/Log.c file_hash: 08d23a4fccc00925380f274033d6bce2f9ea0cd5a54ce734e93b963eb060b109 line: 13 column: 11 function: main value: (2147483647LL + (long long )res) - (long long )xtmp >= 0LL format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-restricted-15/Log.c file_hash: 08d23a4fccc00925380f274033d6bce2f9ea0cd5a54ce734e93b963eb060b109 line: 13 column: 11 function: main value: (4294967295LL + (long long )restmp) - (long long )xtmp >= 0LL format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-restricted-15/Log.c file_hash: 08d23a4fccc00925380f274033d6bce2f9ea0cd5a54ce734e93b963eb060b109 line: 17 column: 15 function: main value: 0 <= res format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-restricted-15/Log.c file_hash: 08d23a4fccc00925380f274033d6bce2f9ea0cd5a54ce734e93b963eb060b109 line: 17 column: 15 function: main value: 2 <= x format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-restricted-15/Log.c file_hash: 08d23a4fccc00925380f274033d6bce2f9ea0cd5a54ce734e93b963eb060b109 line: 17 column: 15 function: main value: x != 0 format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-restricted-15/Log.c file_hash: 08d23a4fccc00925380f274033d6bce2f9ea0cd5a54ce734e93b963eb060b109 line: 17 column: 15 function: main value: (((0 <= xtmp && (long long )res + (long long )xtmp >= 0LL) && xtmp != -2) && ((xtmp != -4 && ((xtmp != -6 && ((xtmp != -8 && ((xtmp != -10 && ((xtmp != -12 && ((xtmp != -14 && ((xtmp != -16 && ((xtmp != -18 && ((xtmp != -20 && ((xtmp != -22 && ((((((((((((((((((((12 <= restmp && xtmp <= 2147483623) && (-36LL + (long long )restmp) + (long long )x >= 0LL) && (-24LL + (long long )x) + (long long )xtmp >= 0LL) && (-24LL + (long long )res) + (long long )x >= 0LL) && (-12LL + (long long )res) + (long long )restmp >= 0LL) && (-12LL + (long long )restmp) + (long long )xtmp >= 0LL) && (-24LL + (long long )x) - (long long )xtmp >= 0LL) && xtmp != -24) && restmp != 1) && restmp != 2) && restmp != 3) && restmp != 4) && restmp != 5) && restmp != 6) && restmp != 7) && restmp != 8) && restmp != 9) && restmp != 10) && restmp != 11) || (((((((((((xtmp <= 2147483625 && (-33LL + (long long )restmp) + (long long )x >= 0LL) && (-22LL + (long long )x) + (long long )xtmp >= 0LL) && (-22LL + (long long )res) + (long long )x >= 0LL) && (-11LL + (long long )res) + (long long )restmp >= 0LL) && (-11LL + (long long )restmp) + (long long )xtmp >= 0LL) && (-11LL - (long long )restmp) + (long long )x >= 0LL) && (11LL - (long long )restmp) + (long long )xtmp >= 0LL) && (22LL - (long long )x) + (long long )xtmp >= 0LL) && (-22LL + (long long )x) - (long long )xtmp >= 0LL) && (11LL + (long long )res) - (long long )restmp >= 0LL) && restmp == 11))) || (((((((((((xtmp <= 2147483627 && (-30LL + (long long )restmp) + (long long )x >= 0LL) && (-20LL + (long long )x) + (long long )xtmp >= 0LL) && (-20LL + (long long )res) + (long long )x >= 0LL) && (-10LL + (long long )res) + (long long )restmp >= 0LL) && (-10LL + (long long )restmp) + (long long )xtmp >= 0LL) && (-10LL - (long long )restmp) + (long long )x >= 0LL) && (10LL - (long long )restmp) + (long long )xtmp >= 0LL) && (20LL - (long long )x) + (long long )xtmp >= 0LL) && (-20LL + (long long )x) - (long long )xtmp >= 0LL) && (10LL + (long long )res) - (long long )restmp >= 0LL) && restmp == 10))) || (((((((((((xtmp <= 2147483629 && (-27LL + (long long )restmp) + (long long )x >= 0LL) && (-18LL + (long long )x) + (long long )xtmp >= 0LL) && (-18LL + (long long )res) + (long long )x >= 0LL) && (-9LL + (long long )res) + (long long )restmp >= 0LL) && (-9LL + (long long )restmp) + (long long )xtmp >= 0LL) && (-9LL - (long long )restmp) + (long long )x >= 0LL) && (9LL - (long long )restmp) + (long long )xtmp >= 0LL) && (18LL - (long long )x) + (long long )xtmp >= 0LL) && (-18LL + (long long )x) - (long long )xtmp >= 0LL) && (9LL + (long long )res) - (long long )restmp >= 0LL) && restmp == 9))) || (((((((((((xtmp <= 2147483631 && (-24LL + (long long )restmp) + (long long )x >= 0LL) && (-16LL + (long long )x) + (long long )xtmp >= 0LL) && (-16LL + (long long )res) + (long long )x >= 0LL) && (-8LL + (long long )res) + (long long )restmp >= 0LL) && (-8LL + (long long )restmp) + (long long )xtmp >= 0LL) && (-8LL - (long long )restmp) + (long long )x >= 0LL) && (8LL - (long long )restmp) + (long long )xtmp >= 0LL) && (16LL - (long long )x) + (long long )xtmp >= 0LL) && (-16LL + (long long )x) - (long long )xtmp >= 0LL) && (8LL + (long long )res) - (long long )restmp >= 0LL) && restmp == 8))) || (((((((((((xtmp <= 2147483633 && (-21LL + (long long )restmp) + (long long )x >= 0LL) && (-14LL + (long long )x) + (long long )xtmp >= 0LL) && (-14LL + (long long )res) + (long long )x >= 0LL) && (-7LL + (long long )res) + (long long )restmp >= 0LL) && (-7LL + (long long )restmp) + (long long )xtmp >= 0LL) && (-7LL - (long long )restmp) + (long long )x >= 0LL) && (7LL - (long long )restmp) + (long long )xtmp >= 0LL) && (14LL - (long long )x) + (long long )xtmp >= 0LL) && (-14LL + (long long )x) - (long long )xtmp >= 0LL) && (7LL + (long long )res) - (long long )restmp >= 0LL) && restmp == 7))) || (((((((((((xtmp <= 2147483635 && (-18LL + (long long )restmp) + (long long )x >= 0LL) && (-12LL + (long long )x) + (long long )xtmp >= 0LL) && (-12LL + (long long )res) + (long long )x >= 0LL) && (-6LL + (long long )res) + (long long )restmp >= 0LL) && (-6LL + (long long )restmp) + (long long )xtmp >= 0LL) && (-6LL - (long long )restmp) + (long long )x >= 0LL) && (6LL - (long long )restmp) + (long long )xtmp >= 0LL) && (12LL - (long long )x) + (long long )xtmp >= 0LL) && (-12LL + (long long )x) - (long long )xtmp >= 0LL) && (6LL + (long long )res) - (long long )restmp >= 0LL) && restmp == 6))) || (((((((((((xtmp <= 2147483637 && (-15LL + (long long )restmp) + (long long )x >= 0LL) && (-10LL + (long long )x) + (long long )xtmp >= 0LL) && (-10LL + (long long )res) + (long long )x >= 0LL) && (-5LL + (long long )res) + (long long )restmp >= 0LL) && (-5LL + (long long )restmp) + (long long )xtmp >= 0LL) && (-5LL - (long long )restmp) + (long long )x >= 0LL) && (5LL - (long long )restmp) + (long long )xtmp >= 0LL) && (10LL - (long long )x) + (long long )xtmp >= 0LL) && (-10LL + (long long )x) - (long long )xtmp >= 0LL) && (5LL + (long long )res) - (long long )restmp >= 0LL) && restmp == 5))) || (((((((((((xtmp <= 2147483639 && (-12LL + (long long )restmp) + (long long )x >= 0LL) && (-8LL + (long long )x) + (long long )xtmp >= 0LL) && (-8LL + (long long )res) + (long long )x >= 0LL) && (-4LL + (long long )res) + (long long )restmp >= 0LL) && (-4LL + (long long )restmp) + (long long )xtmp >= 0LL) && (-4LL - (long long )restmp) + (long long )x >= 0LL) && (4LL - (long long )restmp) + (long long )xtmp >= 0LL) && (8LL - (long long )x) + (long long )xtmp >= 0LL) && (-8LL + (long long )x) - (long long )xtmp >= 0LL) && (4LL + (long long )res) - (long long )restmp >= 0LL) && restmp == 4))) || (((((((((((xtmp <= 2147483641 && (-9LL + (long long )restmp) + (long long )x >= 0LL) && (-6LL + (long long )x) + (long long )xtmp >= 0LL) && (-6LL + (long long )res) + (long long )x >= 0LL) && (-3LL + (long long )res) + (long long )restmp >= 0LL) && (-3LL + (long long )restmp) + (long long )xtmp >= 0LL) && (-3LL - (long long )restmp) + (long long )x >= 0LL) && (3LL - (long long )restmp) + (long long )xtmp >= 0LL) && (6LL - (long long )x) + (long long )xtmp >= 0LL) && (-6LL + (long long )x) - (long long )xtmp >= 0LL) && (3LL + (long long )res) - (long long )restmp >= 0LL) && restmp == 3))) || (((((((((((xtmp <= 2147483643 && (-6LL + (long long )restmp) + (long long )x >= 0LL) && (-4LL + (long long )x) + (long long )xtmp >= 0LL) && (-4LL + (long long )res) + (long long )x >= 0LL) && (-2LL + (long long )res) + (long long )restmp >= 0LL) && (-2LL + (long long )restmp) + (long long )xtmp >= 0LL) && (-2LL - (long long )restmp) + (long long )x >= 0LL) && (2LL - (long long )restmp) + (long long )xtmp >= 0LL) && (4LL - (long long )x) + (long long )xtmp >= 0LL) && (-4LL + (long long )x) - (long long )xtmp >= 0LL) && (2LL + (long long )res) - (long long )restmp >= 0LL) && restmp == 2))) || (((((((((((xtmp <= 2147483645 && (-3LL + (long long )restmp) + (long long )x >= 0LL) && (-2LL + (long long )x) + (long long )xtmp >= 0LL) && (-2LL + (long long )res) + (long long )x >= 0LL) && (-1LL + (long long )res) + (long long )restmp >= 0LL) && (-1LL + (long long )restmp) + (long long )xtmp >= 0LL) && (-1LL - (long long )restmp) + (long long )x >= 0LL) && (1LL - (long long )restmp) + (long long )xtmp >= 0LL) && (2LL - (long long )x) + (long long )xtmp >= 0LL) && (-2LL + (long long )x) - (long long )xtmp >= 0LL) && (1LL + (long long )res) - (long long )restmp >= 0LL) && restmp == 1))) || (((((((((((((((2 <= xtmp && (-4LL + (long long )x) + (long long )xtmp >= 0LL) && (-2LL + (long long )res) + (long long )x >= 0LL) && (-2LL + (long long )res) + (long long )xtmp >= 0LL) && (-2LL + (long long )restmp) + (long long )x >= 0LL) && (-2LL + (long long )restmp) + (long long )xtmp >= 0LL) && (-2LL - (long long )restmp) + (long long )x >= 0LL) && (-2LL - (long long )restmp) + (long long )xtmp >= 0LL) && (0LL - (long long )x) + (long long )xtmp >= 0LL) && (long long )res + (long long )restmp >= 0LL) && (long long )x - (long long )xtmp >= 0LL) && (long long )res - (long long )restmp >= 0LL) && 0 == restmp) && x == xtmp) && restmp == 0) && xtmp != 0) format: c_expression | correctness_witness | CPAchecker 2.3 | 53 | 2023-12-01T05:25:02+01:00 |
Found 10 witnesses for program sv-benchmarks/c/termination-restricted-15/Log_true-termination_true-no-overflow.c, 08d23a4fccc00925380f274033d6bce2f9ea0cd5a54ce734e93b963eb060b109
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/08d23a4fccc00925380f274033d6bce2f9ea0cd5a54ce734e93b963eb060b109.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
9221177 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | frama-c-sv version 0.4.0 | 3 | 2022-12-09T09:51:36Z | ||
8c5aaab | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-22 | 4 | 2022-12-11T01:49:54+01:00 | ||
ea6cb03 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | VeriOover | 1 | 2022-12-12T11:00 CET (comp) | ||
e54f1b0 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 692 | 2023-01-29T11:46:49+01:00 | ea6cb03 | |
6047057 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 681 | 2023-01-28T23:08:11+01:00 | 8c5aaab | |
a15d610 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 120 | 2023-01-28T17:45:42+01:00 | 9221177 | |
f021814 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 755 | 2022-12-10T19:31:18+01:00 | ||
e486b8a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 755 | 2022-12-11T21:58:57+01:00 | ||
2205ced | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 766 | 2022-12-09T23:13:21+01:00 | ||
61b881c | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 9 | 2022-12-08T01:17:49+01:00 |
Found 1 witnesses for program sv-benchmarks/c/termination-restricted-15/Log_true-termination_true-no-overflow.c, 08d23a4fccc00925380f274033d6bce2f9ea0cd5a54ce734e93b963eb060b109
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/08d23a4fccc00925380f274033d6bce2f9ea0cd5a54ce734e93b963eb060b109.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
b0a63e0 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 9 | 2021-12-05T22:51:15+01:00 |
Found 0 witnesses for program sv-benchmarks/c/termination-restricted-15/Log_true-termination_true-no-overflow.c, 08d23a4fccc00925380f274033d6bce2f9ea0cd5a54ce734e93b963eb060b109
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/08d23a4fccc00925380f274033d6bce2f9ea0cd5a54ce734e93b963eb060b109.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/termination-restricted-15/Log_true-termination_true-no-overflow.c, 08d23a4fccc00925380f274033d6bce2f9ea0cd5a54ce734e93b963eb060b109
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/08d23a4fccc00925380f274033d6bce2f9ea0cd5a54ce734e93b963eb060b109.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 1 witnesses for program sv-benchmarks/c/termination-restricted-15/Log_true-termination_true-no-overflow.c, 08d23a4fccc00925380f274033d6bce2f9ea0cd5a54ce734e93b963eb060b109
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/08d23a4fccc00925380f274033d6bce2f9ea0cd5a54ce734e93b963eb060b109.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
51f36d5 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T08:12 CET (sv-comp) |
Found 2 witnesses for program sv-benchmarks/c/termination-restricted-15/Log_true-termination_true-no-overflow.c, 08d23a4fccc00925380f274033d6bce2f9ea0cd5a54ce734e93b963eb060b109
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/08d23a4fccc00925380f274033d6bce2f9ea0cd5a54ce734e93b963eb060b109.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
7216647 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 8 | 2017-12-01T16:42 CET (sv-comp) | ||
44fc6f7 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 10 | 2017-12-01T13:15 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/termination-restricted-15/Log_true-termination_true-no-overflow.c, 08d23a4fccc00925380f274033d6bce2f9ea0cd5a54ce734e93b963eb060b109
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/08d23a4fccc00925380f274033d6bce2f9ea0cd5a54ce734e93b963eb060b109.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |