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 (68bdf78f6f996480ccfcf11b22cc3b7892db15596cae3edf06123d71c4506b1f, sv-benchmarks/c/termination-restricted-15/LogAG_true-termination_true-no-overflow.c).

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 5afc074 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.4.0 3 2023-12-03T04:09:45Z
Download 7e0b795 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-24 4 2023-12-03T17:55:46+01:00
Download 6d36477 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness VeriOover 1 2023-12-20T03:37 CET (comp)
Download 849e2a8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 1498 2023-12-20T03:55:43+01:00 Download 6d36477
Download 3cbc125 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 112 2023-12-03T18:44:07+01:00 Download 7e0b795
Download 11865d6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 6 2023-12-03T10:01:14+01:00 Download 5afc074
Download c660132 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 592 2023-11-30T05:07:38+01:00
Download e5ee225 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-e677b7cd46+ 1633 2023-12-03T22:04:47+01:00
Download dac613f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 1717 2023-12-18T18:09:26+01:00
Download 125b296 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Goblint (tags/svcomp24-0-gc2e9465a7) 3 2023-11-30T22:38:00Z
Download b3cefe9 Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: "2.0" uuid: 846120f0-7fc9-474f-ac31-a44d167ec659 creation_time: 2023-12-01T00:57:23Z 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/LogAG.c''' task: input_files: - ../../sv-benchmarks/c/termination-restricted-15/LogAG.c input_file_hashes: ../../sv-benchmarks/c/termination-restricted-15/LogAG.c: 68bdf78f6f996480ccfcf11b22cc3b7892db15596cae3edf06123d71c4506b1f 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/LogAG.c file_hash: 68bdf78f6f996480ccfcf11b22cc3b7892db15596cae3edf06123d71c4506b1f line: 17 column: 15 function: main value: 0 <= xtmp format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-restricted-15/LogAG.c file_hash: 68bdf78f6f996480ccfcf11b22cc3b7892db15596cae3edf06123d71c4506b1f 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/LogAG.c file_hash: 68bdf78f6f996480ccfcf11b22cc3b7892db15596cae3edf06123d71c4506b1f 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/LogAG.c file_hash: 68bdf78f6f996480ccfcf11b22cc3b7892db15596cae3edf06123d71c4506b1f line: 17 column: 15 function: main value: (long long )res + (long long )xtmp >= 0LL format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-restricted-15/LogAG.c file_hash: 68bdf78f6f996480ccfcf11b22cc3b7892db15596cae3edf06123d71c4506b1f 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/LogAG.c file_hash: 68bdf78f6f996480ccfcf11b22cc3b7892db15596cae3edf06123d71c4506b1f line: 17 column: 15 function: main value: xtmp != -2 format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-restricted-15/LogAG.c file_hash: 68bdf78f6f996480ccfcf11b22cc3b7892db15596cae3edf06123d71c4506b1f line: 17 column: 15 function: main value: (xtmp != -4 && ((xtmp != -6 && ((xtmp != -8 && ((xtmp != -10 && ((xtmp != -12 && ((xtmp != -14 && ((xtmp != -16 && ((xtmp != -18 && ((xtmp != -20 && ((xtmp != -22 && ((xtmp != -24 && ((((((((((((((((((((12 <= restmp && xtmp <= 2147483621) && (-38LL + (long long )restmp) + (long long )x >= 0LL) && (-26LL + (long long )x) + (long long )xtmp >= 0LL) && (-26LL + (long long )res) + (long long )x >= 0LL) && (-12LL + (long long )res) + (long long )restmp >= 0LL) && (-12LL + (long long )restmp) + (long long )xtmp >= 0LL) && (-26LL + (long long )x) - (long long )xtmp >= 0LL) && xtmp != -26) && restmp != 1) && restmp != 2) && restmp != 3) && restmp != 4) && restmp != 5) && restmp != 6) && restmp != 7) && restmp != 8) && restmp != 9) && restmp != 10) && restmp != 11) || (((((((((((xtmp <= 2147483623 && (-35LL + (long long )restmp) + (long long )x >= 0LL) && (-24LL + (long long )x) + (long long )xtmp >= 0LL) && (-24LL + (long long )res) + (long long )x >= 0LL) && (-11LL + (long long )res) + (long long )restmp >= 0LL) && (-11LL + (long long )restmp) + (long long )xtmp >= 0LL) && (-13LL - (long long )restmp) + (long long )x >= 0LL) && (11LL - (long long )restmp) + (long long )xtmp >= 0LL) && (24LL - (long long )x) + (long long )xtmp >= 0LL) && (-24LL + (long long )x) - (long long )xtmp >= 0LL) && (11LL + (long long )res) - (long long )restmp >= 0LL) && restmp == 11))) || (((((((((((xtmp <= 2147483625 && (-32LL + (long long )restmp) + (long long )x >= 0LL) && (-22LL + (long long )x) + (long long )xtmp >= 0LL) && (-22LL + (long long )res) + (long long )x >= 0LL) && (-10LL + (long long )res) + (long long )restmp >= 0LL) && (-10LL + (long long )restmp) + (long long )xtmp >= 0LL) && (-12LL - (long long )restmp) + (long long )x >= 0LL) && (10LL - (long long )restmp) + (long long )xtmp >= 0LL) && (22LL - (long long )x) + (long long )xtmp >= 0LL) && (-22LL + (long long )x) - (long long )xtmp >= 0LL) && (10LL + (long long )res) - (long long )restmp >= 0LL) && restmp == 10))) || (((((((((((xtmp <= 2147483627 && (-29LL + (long long )restmp) + (long long )x >= 0LL) && (-20LL + (long long )x) + (long long )xtmp >= 0LL) && (-20LL + (long long )res) + (long long )x >= 0LL) && (-9LL + (long long )res) + (long long )restmp >= 0LL) && (-9LL + (long long )restmp) + (long long )xtmp >= 0LL) && (-11LL - (long long )restmp) + (long long )x >= 0LL) && (9LL - (long long )restmp) + (long long )xtmp >= 0LL) && (20LL - (long long )x) + (long long )xtmp >= 0LL) && (-20LL + (long long )x) - (long long )xtmp >= 0LL) && (9LL + (long long )res) - (long long )restmp >= 0LL) && restmp == 9))) || (((((((((((xtmp <= 2147483629 && (-26LL + (long long )restmp) + (long long )x >= 0LL) && (-18LL + (long long )x) + (long long )xtmp >= 0LL) && (-18LL + (long long )res) + (long long )x >= 0LL) && (-8LL + (long long )res) + (long long )restmp >= 0LL) && (-8LL + (long long )restmp) + (long long )xtmp >= 0LL) && (-10LL - (long long )restmp) + (long long )x >= 0LL) && (8LL - (long long )restmp) + (long long )xtmp >= 0LL) && (18LL - (long long )x) + (long long )xtmp >= 0LL) && (-18LL + (long long )x) - (long long )xtmp >= 0LL) && (8LL + (long long )res) - (long long )restmp >= 0LL) && restmp == 8))) || (((((((((((xtmp <= 2147483631 && (-23LL + (long long )restmp) + (long long )x >= 0LL) && (-16LL + (long long )x) + (long long )xtmp >= 0LL) && (-16LL + (long long )res) + (long long )x >= 0LL) && (-7LL + (long long )res) + (long long )restmp >= 0LL) && (-7LL + (long long )restmp) + (long long )xtmp >= 0LL) && (-9LL - (long long )restmp) + (long long )x >= 0LL) && (7LL - (long long )restmp) + (long long )xtmp >= 0LL) && (16LL - (long long )x) + (long long )xtmp >= 0LL) && (-16LL + (long long )x) - (long long )xtmp >= 0LL) && (7LL + (long long )res) - (long long )restmp >= 0LL) && restmp == 7))) || (((((((((((xtmp <= 2147483633 && (-20LL + (long long )restmp) + (long long )x >= 0LL) && (-14LL + (long long )x) + (long long )xtmp >= 0LL) && (-14LL + (long long )res) + (long long )x >= 0LL) && (-6LL + (long long )res) + (long long )restmp >= 0LL) && (-6LL + (long long )restmp) + (long long )xtmp >= 0LL) && (-8LL - (long long )restmp) + (long long )x >= 0LL) && (6LL - (long long )restmp) + (long long )xtmp >= 0LL) && (14LL - (long long )x) + (long long )xtmp >= 0LL) && (-14LL + (long long )x) - (long long )xtmp >= 0LL) && (6LL + (long long )res) - (long long )restmp >= 0LL) && restmp == 6))) || (((((((((((xtmp <= 2147483635 && (-17LL + (long long )restmp) + (long long )x >= 0LL) && (-12LL + (long long )x) + (long long )xtmp >= 0LL) && (-12LL + (long long )res) + (long long )x >= 0LL) && (-5LL + (long long )res) + (long long )restmp >= 0LL) && (-5LL + (long long )restmp) + (long long )xtmp >= 0LL) && (-7LL - (long long )restmp) + (long long )x >= 0LL) && (5LL - (long long )restmp) + (long long )xtmp >= 0LL) && (12LL - (long long )x) + (long long )xtmp >= 0LL) && (-12LL + (long long )x) - (long long )xtmp >= 0LL) && (5LL + (long long )res) - (long long )restmp >= 0LL) && restmp == 5))) || (((((((((((xtmp <= 2147483637 && (-14LL + (long long )restmp) + (long long )x >= 0LL) && (-10LL + (long long )x) + (long long )xtmp >= 0LL) && (-10LL + (long long )res) + (long long )x >= 0LL) && (-4LL + (long long )res) + (long long )restmp >= 0LL) && (-4LL + (long long )restmp) + (long long )xtmp >= 0LL) && (-6LL - (long long )restmp) + (long long )x >= 0LL) && (4LL - (long long )restmp) + (long long )xtmp >= 0LL) && (10LL - (long long )x) + (long long )xtmp >= 0LL) && (-10LL + (long long )x) - (long long )xtmp >= 0LL) && (4LL + (long long )res) - (long long )restmp >= 0LL) && restmp == 4))) || (((((((((((xtmp <= 2147483639 && (-11LL + (long long )restmp) + (long long )x >= 0LL) && (-8LL + (long long )x) + (long long )xtmp >= 0LL) && (-8LL + (long long )res) + (long long )x >= 0LL) && (-3LL + (long long )res) + (long long )restmp >= 0LL) && (-3LL + (long long )restmp) + (long long )xtmp >= 0LL) && (-5LL - (long long )restmp) + (long long )x >= 0LL) && (3LL - (long long )restmp) + (long long )xtmp >= 0LL) && (8LL - (long long )x) + (long long )xtmp >= 0LL) && (-8LL + (long long )x) - (long long )xtmp >= 0LL) && (3LL + (long long )res) - (long long )restmp >= 0LL) && restmp == 3))) || (((((((((((xtmp <= 2147483641 && (-8LL + (long long )restmp) + (long long )x >= 0LL) && (-6LL + (long long )x) + (long long )xtmp >= 0LL) && (-6LL + (long long )res) + (long long )x >= 0LL) && (-2LL + (long long )res) + (long long )restmp >= 0LL) && (-2LL + (long long )restmp) + (long long )xtmp >= 0LL) && (-4LL - (long long )restmp) + (long long )x >= 0LL) && (2LL - (long long )restmp) + (long long )xtmp >= 0LL) && (6LL - (long long )x) + (long long )xtmp >= 0LL) && (-6LL + (long long )x) - (long long )xtmp >= 0LL) && (2LL + (long long )res) - (long long )restmp >= 0LL) && restmp == 2))) || (((((((((((xtmp <= 2147483643 && (-5LL + (long long )restmp) + (long long )x >= 0LL) && (-4LL + (long long )x) + (long long )xtmp >= 0LL) && (-4LL + (long long )res) + (long long )x >= 0LL) && (-1LL + (long long )res) + (long long )restmp >= 0LL) && (-1LL + (long long )restmp) + (long long )xtmp >= 0LL) && (-3LL - (long long )restmp) + (long long )x >= 0LL) && (1LL - (long long )restmp) + (long long )xtmp >= 0LL) && (4LL - (long long )x) + (long long )xtmp >= 0LL) && (-4LL + (long long )x) - (long long )xtmp >= 0LL) && (1LL + (long long )res) - (long long )restmp >= 0LL) && restmp == 1))) || ((((((((((((xtmp <= 2147483645 && (-2LL + (long long )x) + (long long )xtmp >= 0LL) && (-2LL + (long long )res) + (long long )x >= 0LL) && (-2LL + (long long )restmp) + (long long )x >= 0LL) && (-2LL - (long long )restmp) + (long long )x >= 0LL) && (0LL - (long long )restmp) + (long long )xtmp >= 0LL) && (2LL - (long long )x) + (long long )xtmp >= 0LL) && (long long )res + (long long )restmp >= 0LL) && (long long )restmp + (long long )xtmp >= 0LL) && (-2LL + (long long )x) - (long long )xtmp >= 0LL) && (long long )res - (long long )restmp >= 0LL) && 0 == restmp) && restmp == 0) format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-restricted-15/LogAG.c file_hash: 68bdf78f6f996480ccfcf11b22cc3b7892db15596cae3edf06123d71c4506b1f 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/LogAG.c file_hash: 68bdf78f6f996480ccfcf11b22cc3b7892db15596cae3edf06123d71c4506b1f 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/LogAG.c file_hash: 68bdf78f6f996480ccfcf11b22cc3b7892db15596cae3edf06123d71c4506b1f 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/LogAG.c file_hash: 68bdf78f6f996480ccfcf11b22cc3b7892db15596cae3edf06123d71c4506b1f 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/LogAG.c file_hash: 68bdf78f6f996480ccfcf11b22cc3b7892db15596cae3edf06123d71c4506b1f 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/LogAG.c file_hash: 68bdf78f6f996480ccfcf11b22cc3b7892db15596cae3edf06123d71c4506b1f line: 13 column: 11 function: main value: (4294967295LL + (long long )restmp) - (long long )xtmp >= 0LL format: c_expression correctness_witness CPAchecker 2.3 1121 2023-12-01T04:20:12+01:00

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download c8493d3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.4.0 3 2022-12-09T13:41:05Z
Download a4c8fa0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 4 2023-01-28T17:59:17+01:00 Download 0a7abf7
Download f8a2de6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 4 2023-01-28T11:39:32+01:00 Download 0cbf16a
Download 80fbd4a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-22 4 2022-12-11T01:49:44+01:00
Download 6d36477 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness VeriOover 1 2022-12-12T10:59 CET (comp)
Download 0cc9ac4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 6 2023-01-29T11:46:41+01:00 Download 6d36477
Download 9df9ca4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 1498 2023-01-28T23:05:34+01:00 Download 80fbd4a
Download 9fb4d88 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 191 2023-01-28T17:46:55+01:00 Download c8493d3
Download 0cbf16a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 6 2022-12-10T16:56:17+01:00
Download 7882b7b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-1715bd67dc+ 1803 2022-12-12T02:46:25+01:00
Download 0a7abf7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 6 2022-12-10T03:28:50+01:00

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

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

Found 0 witnesses for program sv-benchmarks/c/termination-restricted-15/LogAG_true-termination_true-no-overflow.c, 68bdf78f6f996480ccfcf11b22cc3b7892db15596cae3edf06123d71c4506b1f
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/68bdf78f6f996480ccfcf11b22cc3b7892db15596cae3edf06123d71c4506b1f.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 '21

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

Found 0 witnesses for program sv-benchmarks/c/termination-restricted-15/LogAG_true-termination_true-no-overflow.c, 68bdf78f6f996480ccfcf11b22cc3b7892db15596cae3edf06123d71c4506b1f
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/68bdf78f6f996480ccfcf11b22cc3b7892db15596cae3edf06123d71c4506b1f.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 '20

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

Found 0 witnesses for program sv-benchmarks/c/termination-restricted-15/LogAG_true-termination_true-no-overflow.c, 68bdf78f6f996480ccfcf11b22cc3b7892db15596cae3edf06123d71c4506b1f
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/68bdf78f6f996480ccfcf11b22cc3b7892db15596cae3edf06123d71c4506b1f.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 (68bdf78f6f996480ccfcf11b22cc3b7892db15596cae3edf06123d71c4506b1f, sv-benchmarks/c/termination-restricted-15/LogAG_true-termination_true-no-overflow.c).

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 3a72c0b Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T08:56 CET (sv-comp)

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

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

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

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

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

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

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

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