Index


  • Introduction

  • Skipped feature combinations
  • Failed test cases
  • Tests by feature combinations
  • SYMMETRY tests
  • Tests under anomalous conditions

  • Tests by feature combinations: -workers 2
  • SYMMETRY tests: -workers 2

  • Tests by feature combinations: -workers auto
  • SYMMETRY tests: -workers auto

Tests by plug feature Cross2; CLI Option: -workers 1

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
2bb335496f6224ca4e09e31dbcff9eab68c6da77 Apalache Eq Cross2 True Passed
  • Model Under Test
  • Equivalent Model
152e231066b06663a2f08177182562d308ac338b Apalache Eq Cross2 False Passed
  • Model Under Test
  • Equivalent Model
a03365fad35c5f5b5c40410d4558b5a857a28148 Apalache Ne Cross2 True Passed
  • Model Under Test
  • Equivalent Model
dc14621abde83c60e566d133244c02e622b69929 Apalache Ne Cross2 False Passed
  • Model Under Test
  • Equivalent Model
3cad38ed1cbd5ebbce148223c437de95dc2a8c7e Apalache Let Cross2 True Passed
  • Model Under Test
  • Equivalent Model
9540c274709eef93d2abceee3210486c3ad0440a Apalache Let Cross2 False Passed
  • Model Under Test
  • Equivalent Model
9f550f24499d2ed1754fe335de7103b137cc20fc Apalache Set0 Cross2 True Passed
  • Model Under Test
  • Equivalent Model
aa7f3056b901b45d7a0e25f85cbf8f12e5744cdd Apalache Set0 Cross2 False Passed
  • Model Under Test
  • Equivalent Model
a20a4636cddb832fc1afd537123c00eb22f943b4 Apalache Set1 Cross2 True Passed
  • Model Under Test
  • Equivalent Model
e8c71bec3daa48276bab3da2c7053df4c8c97868 Apalache Set1 Cross2 False Passed
  • Model Under Test
  • Equivalent Model
f321686d1da654ca6f349e9a1830623a645db0b8 Apalache Set2 Cross2 True Passed
  • Model Under Test
  • Equivalent Model
22bcf1cc94bac734dd03d55651c43db919922f42 Apalache Set2 Cross2 False Passed
  • Model Under Test
  • Equivalent Model
dfa36751eebefb7522f305ccf313852439ceea24 Apalache Fun Cross2 True Passed
  • Model Under Test
  • Equivalent Model
a08f4594577a19c9cc95d41e226f48fe7ed0137c Apalache Fun Cross2 False Passed
  • Model Under Test
  • Equivalent Model
9b48bab97f695c94f7e9ab77d13e555a99611765 Apalache In Cross2 True Passed
  • Model Under Test
  • Equivalent Model
663b0d5250265fb9c9d591f12f506f4b8a7b48e9 Apalache In Cross2 False Passed
  • Model Under Test
  • Equivalent Model
75980893d9fabe871a5f3f15270d28e60bff9fc2 Apalache NotIn Cross2 True Passed
  • Model Under Test
  • Equivalent Model
88e7e90e5d191d7b82c7e5c17627d8a49fdfa2f3 Apalache NotIn Cross2 False Passed
  • Model Under Test
  • Equivalent Model
fe09de3dad08e69a6d0912d0df3c887010c9f22d Apalache Record Cross2 True Passed
  • Model Under Test
  • Equivalent Model
1beda44657277a46883946e1b1ca40eb5b85d7b7 Apalache Record Cross2 False Passed
  • Model Under Test
  • Equivalent Model
356e9807c79bb21eaeb56865048e6ca59cc5e229 Apalache Tuple Cross2 True Passed
  • Model Under Test
  • Equivalent Model
504943cdf3249bbd4730f08c51ee63de8fea6dbc Apalache Tuple Cross2 False Passed
  • Model Under Test
  • Equivalent Model
0d173ee986fd20474565425305c51fa46b6e4590 Apalache FunApp Cross2 True Passed
  • Model Under Test
  • Equivalent Model
38a3922457e7dbb24c2fc8b9de1e48152c62f7b6 Apalache FunApp Cross2 False Passed
  • Model Under Test
  • Equivalent Model
d147b9f16506daccbeff4526cc91e21896f017f8 Apalache Except1Fun Cross2 True Passed
  • Model Under Test
  • Equivalent Model
d55913f0c94f837a6fa09709901d377840ab3d5f Apalache Except1Fun Cross2 False Passed
  • Model Under Test
  • Equivalent Model
4a9bab24032ba1559d3646e7a39834d06ef3b132 TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
Except1FunWithAt Cross2 True Passed
  • Model Under Test
  • Equivalent Model
d2f86f72a400a4b201a110c6fb6584ce4b6dbd8a TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
Except1FunWithAt Cross2 False Passed
  • Model Under Test
  • Equivalent Model
17efcc310847df67b39434410eed44001a6e3cfb Apalache Except1Rec Cross2 True Passed
  • Model Under Test
  • Equivalent Model
fe22b0c9498448282795e71b1647e57fb8d70a2f Apalache Except1Rec Cross2 False Passed
  • Model Under Test
  • Equivalent Model
b58d86f78362c31042a32b9df6134178fdb8066f TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Cross2 True Passed
  • Model Under Test
  • Equivalent Model
a085d69614e523cf96c10605b17e62b913c6bf38 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Cross2 False Passed
  • Model Under Test
  • Equivalent Model
b79ae6facd0ea8cbbf8e17b30f5e53fe9f86c890 Apalache Except2Fun Cross2 True Passed
  • Model Under Test
  • Equivalent Model
2aeaa139c4ba479a5909532864255e4a1b392f6f Apalache Except2Fun Cross2 False Passed
  • Model Under Test
  • Equivalent Model
74784d2d653c2eb03695c207ff8cef195702905a Apalache Prime Cross2 True Passed
  • Model Under Test
  • Equivalent Model
0a796f7d961cd3175781a3819308acf6861d2a66 Apalache Prime Cross2 False Passed
  • Model Under Test
  • Equivalent Model
403c2ebd6abedaf05d5571df390736e5345d641f Apalache DefFun Cross2 True Passed
  • Model Under Test
  • Equivalent Model
134f5d3cd54bc0744059d2c49b06b11afd4623c7 Apalache DefFun Cross2 False Passed
  • Model Under Test
  • Equivalent Model
a23232685d1faaf8bef41b1f4be163a2fc229d61 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Cross2 True Passed
  • Model Under Test
  • Equivalent Model
6db2e714ccbcbca87eae7fba1f42475ed6688b65 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Cross2 False Passed
  • Model Under Test
  • Equivalent Model
a5a0b8f6b59bd647ea623d95c209c4a81d09355c Apalache DefFunRecursive Cross2 True Passed
  • Model Under Test
  • Equivalent Model
4c08fa1d3a15b3855eb87384099af038b3676503 Apalache DefFunRecursive Cross2 False Passed
  • Model Under Test
  • Equivalent Model
c10ebf7b76047473ae694a9561d168485d4224fe TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Cross2 True Passed
  • Model Under Test
  • Equivalent Model
47ccec197734a29ceb3aaa53680e2b96d3515350 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Cross2 False Passed
  • Model Under Test
  • Equivalent Model
b827ea892250fe00a42ae6ddc970a97e526d99f0 Apalache Def0 Cross2 True Passed
  • Model Under Test
  • Equivalent Model
dad8d80468fec87489f09df06e9ed5c19936a63a Apalache Def0 Cross2 False Passed
  • Model Under Test
  • Equivalent Model
f9ebe48103bb4fbc19776b48ba18bf6b175ddd20 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Cross2 True Passed
  • Model Under Test
  • Equivalent Model
34b2116e190a3618016c1e0e80103db1a1194c21 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Cross2 False Passed
  • Model Under Test
  • Equivalent Model
e0320857d1e6af37ea868a45948a9d68964bf4d5 Apalache Def1 Cross2 True Passed
  • Model Under Test
  • Equivalent Model
475394aea60e80cf2da523cf4e51e4ec3244cf97 Apalache Def1 Cross2 False Passed
  • Model Under Test
  • Equivalent Model
5e07f120e9cb98738540b748a420e11432381ee6 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Cross2 True Passed
  • Model Under Test
  • Equivalent Model
50ece3b8b5d3e4899280e15d38b2a68a9de26fc2 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Cross2 False Passed
  • Model Under Test
  • Equivalent Model
2fe476cecc01ab3f24040cfb23605d05fc9347a5 Apalache Def2 Cross2 True Passed
  • Model Under Test
  • Equivalent Model
d99fe496d634eca4a383ef80f9e4ad276447c204 Apalache Def2 Cross2 False Passed
  • Model Under Test
  • Equivalent Model
7c81b240841ca512bc000ecba75867115198fa6e TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Cross2 True Passed
  • Model Under Test
  • Equivalent Model
5ce83d4b90a146986c42ebcef3d329355ead323b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Cross2 False Passed
  • Model Under Test
  • Equivalent Model
28434f038094674b834dd1bf2c5d5e619dac6f68 Apalache Def1Recursive Cross2 True Passed
  • Model Under Test
  • Equivalent Model
43892743957ab247cd1fc07582b577688a355124 Apalache Def1Recursive Cross2 False Passed
  • Model Under Test
  • Equivalent Model
13f774636da960903c9c323c15f1da13e1e674ce TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Cross2 True Passed
  • Model Under Test
  • Equivalent Model
6a750dd22e60119ddd0469d7cd5ee0b5f32bbef4 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Cross2 False Passed
  • Model Under Test
  • Equivalent Model
d0f929d244e399d8f39bf19cd29e00689977d12d Apalache Extends Cross2 True Passed
  • Model Under Test
  • Equivalent Model
96cf90c5c513b5578dce2a717210591de61084cf Apalache Extends Cross2 False Passed
  • Model Under Test
  • Equivalent Model
134dc5e0aab4756de0ea60e4a66552bc9792934e Apalache ExtendsInDifferentFolder Cross2 True Passed
  • Model Under Test
  • Equivalent Model
b4cee79def0070d951e476313f9607a826050b13 Apalache ExtendsInDifferentFolder Cross2 False Passed
  • Model Under Test
  • Equivalent Model
3de3fe5ddf31635e703a35918b173fbb54d68130 Apalache Variable Cross2 True Passed
  • Model Under Test
  • Equivalent Model
1b2ae0ecaeaa4240569a9bf95987d8f3d4fff0d9 Apalache Variable Cross2 False Passed
  • Model Under Test
  • Equivalent Model
0c91cc2f4e2d535ef11553e4627adc42bbc7b951 TLC with reduction strategy:
  • Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior
VariableViewExclude Cross2 True Passed
  • Model Under Test
  • Equivalent Model
8874ce65878d55fd564db4c39b6970c43cea4047 TLC with reduction strategy:
  • Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior
VariableViewExclude Cross2 False Passed
  • Model Under Test
  • Equivalent Model
57bd2cbd62a5de21b3b920935a7b53fbaed8e94d Apalache Constant Cross2 True Passed
  • Model Under Test
  • Equivalent Model
9bf15066470575745126b1a6348f690af04c4730 Apalache Constant Cross2 False Passed
  • Model Under Test
  • Equivalent Model
1da76a059f93d708bdbf4be0218f38c8c79422e2 Apalache ConstantRank1 Cross2 True Passed
  • Model Under Test
  • Equivalent Model
8029dcc3eb8b8929726860cb30d73d9d81f53fe4 Apalache ConstantRank1 Cross2 False Passed
  • Model Under Test
  • Equivalent Model
24bb52eb2ac92ad02e758f209a9ed94d0cb8a8e6 Apalache Instance Cross2 True Passed
  • Model Under Test
  • Equivalent Model
34bd82046c6bc6b01ca4d3955ba9046416d3a353 Apalache Instance Cross2 False Passed
  • Model Under Test
  • Equivalent Model
fe8f4649f2f4e2c7e4ea9891e85a8ccfca9b9114 Apalache InstanceWith Cross2 True Passed
  • Model Under Test
  • Equivalent Model
8715c5a0eba88204c02dd19ceb5f39cf085c1058 Apalache InstanceWith Cross2 False Passed
  • Model Under Test
  • Equivalent Model
d31d305024ea1b66fc8a8671e47518b1d7540d6e Apalache InstanceNamed Cross2 True Passed
  • Model Under Test
  • Equivalent Model
974bb7a10bf0ab5380fbc5b5a58e4c9e8098b8e1 Apalache InstanceNamed Cross2 False Passed
  • Model Under Test
  • Equivalent Model
a5446564b8ceab35aa7c8cb6988fb2be70d0f464 Apalache InstanceNamedWith Cross2 True Passed
  • Model Under Test
  • Equivalent Model
17ba020249c1ecdb9268970e185faad4160b18cd Apalache InstanceNamedWith Cross2 False Passed
  • Model Under Test
  • Equivalent Model
75b8f0ea65d99ef5bd9dec97a2c49d7478c7a906 Apalache InstanceInFolder Cross2 True Passed
  • Model Under Test
  • Equivalent Model
9f312d448ef43f7a0ae905adcb528a64b1a46232 Apalache InstanceInFolder Cross2 False Passed
  • Model Under Test
  • Equivalent Model
4bd82f646a09c5d7d7221d8f0241233842535ed3 Apalache InstanceWithInFolder Cross2 True Passed
  • Model Under Test
  • Equivalent Model
c6f28de34d20614750e3b15ea48ac3362bed77c7 Apalache InstanceWithInFolder Cross2 False Passed
  • Model Under Test
  • Equivalent Model
118b8f66d5e8adb71fcfd3bc99c1db747e86bd57 Apalache InstanceNamedInFolder Cross2 True Passed
  • Model Under Test
  • Equivalent Model
c5ef6090162c17268110867c6c319c717d2cc0d2 Apalache InstanceNamedInFolder Cross2 False Passed
  • Model Under Test
  • Equivalent Model
18f659a24fb591457acf0352c1ee7e441a1f0743 Apalache InstanceNamedWithInFolder Cross2 True Passed
  • Model Under Test
  • Equivalent Model
3767fc15ecf75061580407a3643691bd39eec501 Apalache InstanceNamedWithInFolder Cross2 False Passed
  • Model Under Test
  • Equivalent Model
f64a4b1d07b2c43b922294aaa4c6073014cebc59 Apalache Lambda Cross2 True Passed
  • Model Under Test
  • Equivalent Model
68690b8f3bb2b9d820a7a3082649336792bc46b9 Apalache Lambda Cross2 False Passed
  • Model Under Test
  • Equivalent Model
33d0e0043ebd96e008ff7b4204504d31eb0f2619 Apalache Cross2 Cross2 True Passed
  • Model Under Test
  • Equivalent Model
4e7775b1d4e75a4cccf83126a541d8f6148cc471 Apalache Cross2 Cross2 False Passed
  • Model Under Test
  • Equivalent Model
df8dcffaaf2733d36eb7ba128eecb85f5ec2f2ee Apalache Cross3 Cross2 True Passed
  • Model Under Test
  • Equivalent Model
844f8abd903f5333fe33009758b519fdeacc052d Apalache Cross3 Cross2 False Passed
  • Model Under Test
  • Equivalent Model
cdfa0752a1a9abfe3a569d9d16f18b1901efd31e TLC with reduction strategy:
  • Case Feature: For finite R replace [D -> R] with explicit function set enumeration; for infinite R replace (f \in [D -> R]) with conjunction (DOMAIN f = D /\ (\A x \in D : f[x] \in R))
FunSet Cross2 True Passed
  • Model Under Test
  • Equivalent Model
0a1ff74402a79050bc4793bcc0554143f9164490 TLC with reduction strategy:
  • Case Feature: For finite R replace [D -> R] with explicit function set enumeration; for infinite R replace (f \in [D -> R]) with conjunction (DOMAIN f = D /\ (\A x \in D : f[x] \in R))
FunSet Cross2 False Passed
  • Model Under Test
  • Equivalent Model
0e45c00eabbc3f4a5fed0fcdc746f387bf45c1af TLC with reduction strategy:
  • Case Feature: For finite R replace [field : R] with explicit function set enumeration; for infinite R replace (f \in [field : R]) with conjunction (DOMAIN f = {'field'} /\ f['field'] \in R)
RecordSet Cross2 True Passed
  • Model Under Test
  • Equivalent Model
d4d76e356627df9410fee7cb30b79cbd7d29c6b2 TLC with reduction strategy:
  • Case Feature: For finite R replace [field : R] with explicit function set enumeration; for infinite R replace (f \in [field : R]) with conjunction (DOMAIN f = {'field'} /\ f['field'] \in R)
RecordSet Cross2 False Passed
  • Model Under Test
  • Equivalent Model
6e7ef9f9df2448f1a10d64003f6390ccd1e12cbf Apalache SetDiff Cross2 True Passed
  • Model Under Test
  • Equivalent Model
879bd9822e8a0652244bdc7bf2e62b31a1e2a4ae Apalache SetDiff Cross2 False Passed
  • Model Under Test
  • Equivalent Model
0c6ee13e1ed9abff3d0add31f25a62407b03a926 Apalache SetUnion Cross2 True Passed
  • Model Under Test
  • Equivalent Model
a530cb73ce103387228e62d3bd8c08ce3a4b9613 Apalache SetUnion Cross2 False Passed
  • Model Under Test
  • Equivalent Model
45c715ae5732a5efceed52112e85d7c24560e0f4 Apalache SetIntersect Cross2 True Passed
  • Model Under Test
  • Equivalent Model
f9b9a863b1c6dd2c783631d9e2149d1a9c900b41 Apalache SetIntersect Cross2 False Passed
  • Model Under Test
  • Equivalent Model
6ac8c72d431ce50768066074aa9a91cb717e2104 Apalache SubsetEq Cross2 True Passed
  • Model Under Test
  • Equivalent Model
bdd2e16d8dd3d3cff67ab94c94c5f98475b16092 Apalache SubsetEq Cross2 False Passed
  • Model Under Test
  • Equivalent Model
1436211d5c7ca258e11c6d67431fa0b377bc3436 Apalache IfThen Cross2 True Passed
  • Model Under Test
  • Equivalent Model
bbbc27a6805538e7a3581b28d06837e52fe2a6db Apalache IfThen Cross2 False Passed
  • Model Under Test
  • Equivalent Model
2f94b1643eed8192d901c4a6ee0ab197ebe7ef34 Apalache IfElse Cross2 True Passed
  • Model Under Test
  • Equivalent Model
31660ecdc786018a3250f5ce1d07d3114136dad5 Apalache IfElse Cross2 False Passed
  • Model Under Test
  • Equivalent Model
5c2450777a041aef3d0f9a452da232c83f4a333b Apalache Subset Cross2 True Passed
  • Model Under Test
  • Equivalent Model
d6d92c7c69b5ecf01beca5edfa4c8988e7b77db6 Apalache Subset Cross2 False Passed
  • Model Under Test
  • Equivalent Model
d48eb14d757d039e3b1ca5b4176cf09fbe38527b Apalache Unchanged Cross2 True Passed
  • Model Under Test
  • Equivalent Model
399931044d316b24936b3a983d1b1b32ec68f021 Apalache Unchanged Cross2 False Passed
  • Model Under Test
  • Equivalent Model
73d35e6303f8197f8a10b163ed888fb5c5d325c8 Apalache SeqSeq Cross2 True Passed
  • Model Under Test
  • Equivalent Model
f8f6fb20d7a432b697756458b82b7b06198018a0 Apalache SeqSeq Cross2 False Passed
  • Model Under Test
  • Equivalent Model
b869f2e0c10ffc0eee088c134a233754d28edc51 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Cross2 True Passed
  • Model Under Test
  • Equivalent Model
c8757a40bed5287be80be978141e8035be7c2e3a TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Cross2 False Passed
  • Model Under Test
  • Equivalent Model
b5cfe56d9b10614b465391dfd6e1ffe34d687b13 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun Cross2 True Passed
  • Model Under Test
  • Equivalent Model
1fd49406e892ebf24ae846d66f64ee95a517f253 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun Cross2 False Passed
  • Model Under Test
  • Equivalent Model
793802826d937495e8b8f784a127e3badeb17124 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Cross2 True Passed
  • Model Under Test
  • Equivalent Model
06be4169e967304abb4b51499b52b9bfcccfbc2e TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Cross2 False Passed
  • Model Under Test
  • Equivalent Model
783e86572d2e99ab83207a8e2d18ecea3922a213 Apalache BagSetToBag Cross2 True Passed
  • Model Under Test
  • Equivalent Model
b91f6c2b3ae4531ec1520f9c1a90d4c931cd6540 Apalache BagSetToBag Cross2 False Passed
  • Model Under Test
  • Equivalent Model
cfcf507393e5f792110ca2657b51dccb10198fd2 Apalache BagBagIn Cross2 True Passed
  • Model Under Test
  • Equivalent Model
e45399d7d9db542f193762c883a4fd85ce4ada9f Apalache BagBagIn Cross2 False Passed
  • Model Under Test
  • Equivalent Model
9f4ad3704bbed4a1f92f766050fd58f7f5b30d9e Apalache BagCopiesIn Cross2 True Passed
  • Model Under Test
  • Equivalent Model
9c34d873f8872cec0c7fe8d304892a3c9b04ba2e Apalache BagCopiesIn Cross2 False Passed
  • Model Under Test
  • Equivalent Model
56a1adbae62689317af1f5a77aa2b0c815608749 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet Cross2 True Passed
  • Model Under Test
  • Equivalent Model
6601bd2f759c2c5b2694014bacb9b82eddc6efe5 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet Cross2 False Passed
  • Model Under Test
  • Equivalent Model
fea5abb4a991ba4ec08acfbe5a478e2e375584ff Apalache FiniteSetsCardinality Cross2 True Passed
  • Model Under Test
  • Equivalent Model
1c164681619589519ea305b55e122ecaabcd6cb1 Apalache FiniteSetsCardinality Cross2 False Passed
  • Model Under Test
  • Equivalent Model
015087e5a2aee1c9c4ccb8e0baf90b39182e191a Apalache SeqAppend Cross2 True Passed
  • Model Under Test
  • Equivalent Model
9758e55a96d950da3cdf57f4d5040a8a49de08a0 Apalache SeqAppend Cross2 False Passed
  • Model Under Test
  • Equivalent Model