Witness Inspection
A description of this web service can be found in the CAV paper
"Verification-Aided Debugging: An Interactive Web-Service for Exploring Error Witnesses"
(more material).
View and Validate the Witness
Input Given to this Service about the Witness (URL Query)
Key |
Value |
programName |
sv-benchmarks/c/termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c |
programSHA |
de331d1f778f147a4d32c0286c0018cb5b5cf61f2b6c0952b6bed68b0f715eaf |
witnessName |
results-verified/depthk.2018-12-05_0936.logfiles/sv-comp19_prop-termination.HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c.files/witness.graphml |
witnessSHA |
da23e273276a0d5fe08a28e27ccb1968282142b4e3b82c4f2b142c56a27ce6c7 |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/da23e273276a0d5fe08a28e27ccb1968282142b4e3b82c4f2b142c56a27ce6c7.json
Key |
Value |
architecture |
32bit |
creationtime |
2018-12-06T05:51:36.205511 |
producer |
DepthK v3.0 |
programfile |
/tmp/vcloud-vcloud-master/worker/working_dir_192b3136-affb-4345-86cf-15b0f4b5171c/sv-benchmarks/c/termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c |
programhash |
c0bce2603970e0a002a5b33cfd00ef3446011286 |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file |
witnessFileByHash/da23e273276a0d5fe08a28e27ccb1968282142b4e3b82c4f2b142c56a27ce6c7.graphml |
witness-sha256 |
da23e273276a0d5fe08a28e27ccb1968282142b4e3b82c4f2b142c56a27ce6c7 |
witness-size |
3519 |
witness-type |
correctness_witness |
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 |
3d22aa0 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
frama-c-sv version 0.4.0 |
3 |
2023-12-03T04:27:55Z |
|
208e61a |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
sv-comp-24 |
4 |
2023-12-03T18:02:11+01:00 |
|
f0b752a |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
VeriOover |
1 |
2023-12-20T03:37 CET (comp) |
|
dc2bee6 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-12-03T18:44:35+01:00 |
208e61a |
9af482e |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-12-03T10:02:05+01:00 |
3d22aa0 |
87007f9 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-11-30T12:41:35+01:00 |
1eb6b05 |
1eb6b05 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-11-30T05:53:28+01:00 |
|
80fc508 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.0.1-svn-a45b42da2f+ |
8 |
2023-12-18T22:18:30+01:00 |
|
5353ea2 |
Inspect |
|
- 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 |
1eb43d2 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
frama-c-sv version 0.4.0 |
3 |
2022-12-09T12:15:12Z |
|
0c3fbaa |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
sv-comp-22 |
4 |
2022-12-10T22:10:08+01:00 |
|
f0b752a |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
VeriOover |
1 |
2022-12-12T10:59 CET (comp) |
|
69da39c |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2 |
8 |
2023-01-29T02:47:58+01:00 |
70999bf |
4ffaca7 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2 |
8 |
2023-01-28T23:05:46+01:00 |
0c3fbaa |
c141512 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2 |
8 |
2023-01-28T17:49:14+01:00 |
1eb43d2 |
a4f5964 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2 |
8 |
2023-01-28T12:27:17+01:00 |
0e0a38a |
0e0a38a |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2 |
8 |
2022-12-10T16:08:49+01:00 |
|
70999bf |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2.1-svn-1715bd67dc+ |
8 |
2022-12-11T23:28:52+01:00 |
|
5d8a160 |
Inspect |
|
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 |
7252549 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
frama-c-sv version 0.2.8 |
3 |
2021-12-13T20:09:48Z |
|
f4ff524 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
sv-comp-22 |
4 |
2021-12-06T13:34:58+01:00 |
|
a99c001 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.1 |
8 |
2021-12-05T20:11:33+01:00 |
09f6392 |
09f6392 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.1 |
8 |
2021-12-05T15:11:31+01:00 |
|
fb58b5d |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.0.1-svn-fe6f522dd3+ |
8 |
2021-12-08T19:15:19+01:00 |
|
ac2a762 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.0.1-svn-eda176372c+ |
8 |
2021-12-09T11:49:17+01:00 |
|
cb3747f |
Inspect |
|
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 |
c7bf475 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
frama-c-sv version 0.2.1 |
3 |
2020-12-06T23:34:18 |
|
eeee594 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
unknown_witness |
Goblint (svcomp21-0-g82e03b87) |
3 |
2020-12-07T17:17:38 |
|
6cdd42e |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.0 |
8 |
2020-12-06T13:44:16+01:00 |
90bbf8d |
90bbf8d |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.0 |
8 |
2020-12-05T14:20:39+01:00 |
|
7a0a844 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.0.1-svn-eda176372c+ |
8 |
2020-12-08T01:57:09+01:00 |
|
9d35e44 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Symbiotic |
2 |
2020-12-11T17:41:46 |
|
a341c89 |
Inspect |
|
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 |
d285591 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 1.7-svn b8d6131600+ |
8 |
2018-12-07T08:03:23+01:00 |
|
c4b25ac |
Inspect |
|
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 |
2614faf |
Inspect |
|
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 |