Index

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

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
0d45b04d124b14716a01d7069e6c55fe40fa1e6d Apalache And Constant True Passed
f51b6b3f7a51b7fe9d53a8de51510277df8248ec Apalache And Constant False Passed
c8a7a08493833db470fb8163cc959c78c4b01178 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine Constant True Passed
9c91a0317f4c4a1f0a214d8bc96b45245d5675d1 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine Constant False Passed
c95eb0c06b20753525261fc7569b83c6acf12d71 Apalache Imply Constant True Passed
a06105ab3d2a02c80a13f780a6a2382a1da6c512 Apalache Imply Constant False Passed
cae863783d1eb7a2467d87a957f5902d2ef4439b Apalache Not Constant True Passed
7ef82559de8da974331ccc17ac483a62b0b87752 Apalache Not Constant False Passed
c7407fc893f6048d2d13e2fbab2e83aeb278958e TLC with reduction strategy:
  • Case Feature: A \/ B == ~(~A /\ ~B)
Or Constant True Passed
4dcfd8745867d478288ee48fbd44c099664f3565 TLC with reduction strategy:
  • Case Feature: A \/ B == ~(~A /\ ~B)
Or Constant False Passed
cf5b8b10bc1469d4cfcb8c8ed0e3e3ba254c879f TLC with reduction strategy:
  • Case Feature:
    \/ A
    \/ B
    == (A \/ B)
OrMultiLine Constant True Passed
4a1e57a7509b64326916c3de8c479c50c68605fc TLC with reduction strategy:
  • Case Feature:
    \/ A
    \/ B
    == (A \/ B)
OrMultiLine Constant False Passed
e3e620a621b1859c385ec33aae610cfd4000de4d Apalache Boxed Constant True Passed
6ac7d4b5cabe51e2ddb400b0acb32fda2b04604a Apalache Boxed Constant False Passed
8ef541073e9371ac43ee93ea8c78080463642a16 Apalache Eq Constant True Passed
b46d7d65b7b4a03d939f86c6eb01b3a7e57c381b Apalache Eq Constant False Passed
cfe05173e1c28aa2d4106e3a90f7655aa2bc1501 Apalache Ne Constant True Passed
565344f638b10b3116a5ee46996782fe417c1dee Apalache Ne Constant False Passed
4c21cf0ea14ba06e45141b146e321e9b06b9e7d3 Apalache Let Constant True Passed
bdcdcd7da54f2be6cc057c628371ba19b72a823d Apalache Let Constant False Passed
1bdd74791f67fa5f1ec498b82851beda6b8b0fd2 Apalache Set0 Constant True Passed
c850ee40575f6fd44ed86c8155f764e7fe2aca3d Apalache Set0 Constant False Passed
f2d0a7a08248db23e908684049e753a10f2b1f20 Apalache Set1 Constant True Passed
f09350010ab82a5fc7020abfd4583d8bc5855070 Apalache Set1 Constant False Passed
35858d9c6257ff800b95abd64492c2eec2abbbbc Apalache Set2 Constant True Passed
d6cc032c0ca0161c9d88943b920baf84dc75a4b6 Apalache Set2 Constant False Passed
d46d66536ffee62ed667cab1f8f5d379f761e10e Apalache Fun Constant True Passed
fae1f1f00096af905cfb46abafa3a54ded7c7fd5 Apalache Fun Constant False Passed
1c2260baad40918920bc7f7626bffbb0079e5cfe Apalache In Constant True Passed
c2a71ef48401966fc89b7dbdf4bb48e2b2527cbc Apalache In Constant False Passed
53af9434b42bb20a7c2d9408b26b1c982f658857 Apalache NotIn Constant True Passed
6296764243a0c8b92f033799b3b0b909aa629ac1 Apalache NotIn Constant False Passed
2c3145216ad21e6cd743576dc48f17b67028ebb1 Apalache Exists Constant True Passed
5e992921269c5391abcc879a7ae029cc589dc944 Apalache Exists Constant False Passed
5d9c4138647fd2ee227b5375e5e1797eaa9245a2 Apalache Forall Constant True Passed
13c8235e1cbc456ff68c31592dde588ca5d74dc3 Apalache Forall Constant False Passed
aec99a3ff506fb71d22117eff190d47d1a16631f Apalache Choose Constant True Passed
e5566e14788027609ec28153bafe73c9d8943c49 Apalache Choose Constant False Passed
23352b711b2c896b9be035d415efbf74849dbf2c Apalache Record Constant True Passed
2a5a0d3c1124f93b706f3679e4db02293b9af908 Apalache Record Constant False Passed
72710a698f04e3448b202d50b937355e113b1da4 Apalache Tuple Constant True Passed
b22f645a63240c3ba819cedcfd9edca70634c63e Apalache Tuple Constant False Passed
e02f94f25e26882bad51a8eea3886822df2e56fb Apalache FunApp Constant True Passed
07b8bdadf8d9d748e67c4237b62583fe3ba4fa76 Apalache FunApp Constant False Passed
cd19bae2b8f597702e4fc04cff55f97e29774e58 Apalache Except0 Constant True Passed
b2d94019fa4044624126734261bd171726ec46be Apalache Except0 Constant False Passed
5571804e115ae405a51f992b2eea3dde5608c4cb Apalache Except1Fun Constant True Passed
7e8346f3f147f192c89853ca0199585265230190 Apalache Except1Fun Constant False Passed
dc3ce7fbdb4d08ce95bb87da0aa6b48f24db829d TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
Except1FunWithAt Constant True Passed
c711a82d3f7503fec587a5b698fed737a0292ba7 TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
Except1FunWithAt Constant False Passed
19c96ae118d9dfdffc49cf24afbbff1a96d9f4e7 Apalache Except1Rec Constant True Passed
da78073e6c96b61705887df26e5559e42c3814ed Apalache Except1Rec Constant False Passed
5ca4ea991c730f53f9cb20814bbcc147add8cb7b TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Constant True Passed
d56ffb3b89d63b0500f47065a5992d8dd6ba866f TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Constant False Passed
5538db2148d9a53814d85e7a5157bb9f61e0bb23 Apalache Except2Fun Constant True Passed
2818e7960e1f5d5d31fe7d2b08a1739623759a4b Apalache Except2Fun Constant False Passed
c88589b0fa382c4d4f772afdc6d3a6ef32db3e01 Apalache Except2FunTuple Constant True Passed
24371f0e84b87d8ac71484b912c661c1d178b90a Apalache Except2FunTuple Constant False Passed
8a8f5b84b44ea914355b7ddf6e07beeb6ab93172 Apalache Prime Constant True Passed
c94dfb79fc4affcb4e3ea84cb02ec6abefa10f95 Apalache Prime Constant False Passed
877910410d7e927ae5e45c1dcb555be34f30eb2c Apalache NumUnaryMinus Constant True Passed
8ba86cf7984e5bea759a4002340b283632d2d538 Apalache NumUnaryMinus Constant False Passed
9c390d87d1eb1b6da097a7e5300a84146d781cb1 Apalache NumPlus Constant True Passed
840f9412ba4d6a6322f9e8f647fe40bb8b2b34d6 Apalache NumPlus Constant False Passed
3fd97338ab9276ee9049d7ac55a8082090a431d3 Apalache NumMinus Constant True Passed
fbfb2e5bbc1cdb0355551c9c1c4b1afa7b0b1619 Apalache NumMinus Constant False Passed
c067c50cf0d2f4b66e8956fe6402b22cac4f913a Apalache NumMul Constant True Passed
95f1b46ea7ae667d2e38bc83bedcd8dc3b90c261 Apalache NumMul Constant False Passed
95fad5c9595b84bcee41af78a94e697a4139cb47 Apalache NumDiv Constant True Passed
4b9953991c1dc3c6dfd81c5c816a9ff479483baa Apalache NumDiv Constant False Passed
76f6c9e4a43cb3a4ebb37874108ad30246dcbdc1 Apalache NumMod Constant True Passed
5842adadf1d72d205167bd32815ac0172c87050e Apalache NumMod Constant False Passed
487fe31b651aad3581eb021cf699002dbb886721 Apalache NumPow Constant True Passed
b76e1c17dc6648c1a02e17c324ad5d39da1d4595 Apalache NumPow Constant False Passed
baf5929610dc9e85cdf6aa061948cf7132de817f Apalache NumGt Constant True Passed
61419e13f1af24490524dc682ce00ab2629a5764 Apalache NumGt Constant False Passed
710e8f9e356be9c7803876e6995d8d22ea9a41e9 Apalache NumGe Constant True Passed
7eca69f296e6a0dd7f78eca76a3e8ae0faedb636 Apalache NumGe Constant False Passed
29a476a212c76d7bf166c417046799f8d6f3fe10 Apalache NumLt Constant True Passed
20024aaf64e6054cc8279cab91077c6fddbaa110 Apalache NumLt Constant False Passed
a41364330744712a6b2d8314ffe0705010de7a9b Apalache NumLe Constant True Passed
72e432c6273c46678efc104381d0f961af3cf0f6 Apalache NumLe Constant False Passed
d690d6c17fcc428987bbd65357da4cf4b9efc6d2 Apalache DefFun Constant True Passed
83a1beb8256d9c75fc8229d50148beb98f0e44a9 Apalache DefFun Constant False Passed
f49efdc23a48a06191d7a20ee04076d472138c31 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Constant True Passed
02af59e6148e33352e7238c3c6d849223520c839 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Constant False Passed
a3d91f9ce2acacae5103c7ec67bd68708251cdd5 Apalache DefFunRecursive Constant True Passed
c61735051cea90677df17a0307d9bf47540154da Apalache DefFunRecursive Constant False Passed
7097dd1f25ed2b403f4b710b3b5653fd8b8b2e25 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Constant True Passed
03cb836786ec57cf178a6dc3dcc14dfe1e528801 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Constant False Passed
fb6b6901ba80c9ea238a34a3767975f383ee05d3 Apalache Def0 Constant True Passed
3f8d0bf20c8b9c8fca132ffa26715ace108f5ecc Apalache Def0 Constant False Passed
4397356b437e2202bc0a3d361e3bfe9009d587e4 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Constant True Passed
2ed3ea142a949dd9590103ef25b9948a0a00cf9b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Constant False Passed
9903f0eff835545930a923674a4412c108914939 Apalache Def1 Constant True Passed
161213d9ed29eeb9e5124d3282a33a70e83c7e87 Apalache Def1 Constant False Passed
ddb31b1c64d97e6a4df4c37c136edc8025b71baa TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Constant True Passed
b6b9b96a9ac144331d2ceb4bbd204aacdc2e9631 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Constant False Passed
63f11c4391bef89f03302708a499d73fb1bf0a9b Apalache Def2 Constant True Passed
29194c0ca895d1bdee2f0a07721977301f11a81b Apalache Def2 Constant False Passed
fe9fcf564b6c4d5127831f7d8ef70347800d1fa3 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Constant True Passed
44019ac5eed98e3e4d3f1c1dd7824a0efc992a31 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Constant False Passed
6590bc6e331e5cf454f3f54dabd238f35094fef0 Apalache Def1Recursive Constant True Passed
8435457fb1bdbdf2be5dd269ef5b2709413a967d Apalache Def1Recursive Constant False Passed
16ba014d8a4d4d24bfecfd7ae3ff98790189e04d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Constant True Passed
2797d02a3553fe5e834bfcad48e53f1c00a99906 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Constant False Passed
40b95583b4ee7d7aa8ed8204305bd3df04185bb2 Apalache Extends Constant True Passed
e136c58ac07edcf0a0bd809c89ee4850538b13fd Apalache Extends Constant False Passed
c7f79cd6b134fe0e8d8996f3be050f785a7e137f Apalache ExtendsInDifferentFolder Constant True Passed
d584d8caca04d9841e3129cb6568dda3e41d8629 Apalache ExtendsInDifferentFolder Constant False Passed
5d5e84435804e79a68e07c0dfd5f551b250416aa Apalache Constant Constant True Passed
72cb3b57850517852df9783a41d50191f9f7ec7e Apalache Constant Constant False Passed
bdd246705e9267bc8a6601324d9a657e964c3234 Apalache ConstantRank1 Constant True Passed
11cbddc3d98256f3304a281d08e8472aa63cf6e2 Apalache ConstantRank1 Constant False Passed
5e643b52979b09d877d48de998d4b193c256ebfd Apalache Instance Constant True Passed
0a89aca417cc1c918d3785ab6eb0e384f8cbf9ca Apalache Instance Constant False Passed
ad9497e2c410cb199bba2ff7b098f5fac9aabddd Apalache InstanceWith Constant True Passed
c4acb9128211dbe842f2e6fc64354a66980fb183 Apalache InstanceWith Constant False Passed
8bc0cf2c804b1db6a6c8277a3814cfbfa5a90191 Apalache InstanceNamed Constant True Passed
100a9fe9890380c8ef3549099cd054afbe1d2150 Apalache InstanceNamed Constant False Passed
de45ffe501d3b592785265a6b9bab260e1659ca0 Apalache InstanceNamedWith Constant True Passed
0ab2ba161fe8388d38811f25fedc8678f0ae7b3a Apalache InstanceNamedWith Constant False Passed
4eec80d032f6c382c980ad19f3513a6a5b9cfcd3 Apalache InstanceInFolder Constant True Passed
4995a4c6f4c20804115c8b920bac8ead6ecea3a6 Apalache InstanceInFolder Constant False Passed
9ee7c7d13e1cb840f588a0f93949fee5d9a152c8 Apalache InstanceWithInFolder Constant True Passed
2be063591fe01a2913e50d53a7a1a8d8abb9ab73 Apalache InstanceWithInFolder Constant False Passed
f730b100613e70ecaf6b79d425208ed1c0a275a5 Apalache InstanceNamedInFolder Constant True Passed
68f56b2b22e14da64c506e4dec6324389484b176 Apalache InstanceNamedInFolder Constant False Passed
f034acb7ad00341f2591d02cd9a312545f5d1e4d Apalache InstanceNamedWithInFolder Constant True Passed
0510e9e02889c7dc4ffb4ac470276b665412ce63 Apalache InstanceNamedWithInFolder Constant False Passed
944c987479ada9daec55c916096602dbb81edc02 Apalache Enabled Constant True Passed
d588b3e8929b12474459566f7c45d3450c961447 Apalache Enabled Constant False Passed
2212d5722e3ba11be7fa3bd778f8bcefccc4c238 Apalache Assume Constant True Passed
30fc56d37c1c1b3003277d4889b88169bc981030 Apalache Assume Constant False Passed
f13db52e76cdd0a40c5ed37c5a5f1d3d14bd8464 Apalache AssumeNamed Constant True Passed
a75106f43f8dd203adae5e69e7f0437d9fd936ac Apalache AssumeNamed Constant False Passed
29046a9cfee3dc21eac4e7c5ad8ac79d014e5a72 Apalache Lambda Constant True Passed
ee5e539f73b8d1769896b7544bf62a436e09f99b Apalache Lambda Constant False Passed
385e7c25d438531edd8279a6c22330e12dff1e07 Apalache Cross2 Constant True Passed
e2d6949b3275346c84d2170ccc85c1ffb1b7f256 Apalache Cross2 Constant False Passed
1a17d2c8e0e58c0617cdd4888623c9a2f2239c80 Apalache Cross3 Constant True Passed
dc630b2de5b4ffc6a3b9e2b6c9e58644b0c8ea49 Apalache Cross3 Constant False Passed
61055c3ed28785867bead219bed0671ef040b37b 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 Constant True Passed
07a389c9375e09386fe04535a4f880a57667308a 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 Constant False Passed
bfe2f1ad27ded5e7ba79048a46c3c8da01b4498e 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 Constant True Passed
57eba05a37acb9b09c423409502d7e572e9cc109 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 Constant False Passed
568a4ed98fd0092bcd9568f301d880b9c8748aef Apalache SetDiff Constant True Passed
4eea0664065806df26bffe1f9fb7e345046ebcb6 Apalache SetDiff Constant False Passed
ac82e340201cb1188c52f708147c00205549c5fd Apalache SetUnion Constant True Passed
5421614295135363ed3e4f560ca65ddd11e92d00 Apalache SetUnion Constant False Passed
af386044586415e7a279101c6d633ef2e3fe2cc7 Apalache SetIntersect Constant True Passed
ca062121c259cc238420a32fce68647708e6bb15 Apalache SetIntersect Constant False Passed
ed94fe845c78a14910437291d972515e000f4727 Apalache SubsetEq Constant True Passed
3e96633d2ce4e7960a9e3be9893f577848d845f7 Apalache SubsetEq Constant False Passed
1bf43839d8dea50fa0b51353cd8fd4906d9f35c8 Apalache IfCond Constant True Passed
a3cec76ed273153491897a1b80c14153329fa8c4 Apalache IfCond Constant False Passed
933b23c130b0246419e82cfcc65f620534392135 Apalache IfThen Constant True Passed
1f26d0ef466db125d43f9f6b7dbaa4df63313a76 Apalache IfThen Constant False Passed
1d599e93aabc38e36712ba035112ed2b9918d363 Apalache IfElse Constant True Passed
8bd2d64e819ee1559d520b3b33b53d8876c063e0 Apalache IfElse Constant False Passed
c5246ab4bb8616da31e0efd80402b74b7a1104d7 Apalache Subset Constant True Passed
1a5d1dc7f94856fa7f0c3f90b3ad4320b6c80811 Apalache Subset Constant False Passed
39ee78787bf8ef298d12c573aeaceeb499e0539d Apalache Domain Constant True Passed
5c58e70d0b84a7bc85d38170a208e07548e4d176 Apalache Domain Constant False Passed
456aaadc7a4d938331d745f912282a76b0ce72da Apalache Union Constant True Passed
1d91330ba83e16739c671118260c20c791256e0c Apalache Union Constant False Passed
8f2c1041f2bc8231c5bfbf3bbd0ff287c1795ed6 Apalache Equivalence Constant True Passed
750c25282e2eba88508a19847b354dbc35f87db9 Apalache Equivalence Constant False Passed
236f807959fdb3628a6b81f87552ec64d6740550 Apalache SeqLen Constant True Passed
816981eeabbbe6c0b67568a700d76bcce0ac5bc8 Apalache SeqLen Constant False Passed
cedc3efca3aef46e7177305983f2bc3ad54b7fd9 Apalache SeqConcat Constant True Passed
adff17b4ff664d17e4bc4a2a9ee069f332a4b424 Apalache SeqConcat Constant False Passed
4ecc3ac22aa111fd81bf4f09711c82c681c350ba Apalache SeqSeq Constant True Passed
31f0987dd363ed09707c53d3233125078aa75775 Apalache SeqSeq Constant False Passed
a4b1393716081f67f725c38af21eda4a55411e24 Apalache SeqSelectSeq Constant True Passed
9c72ed3c2d2dd6a69d2a65459ee7ffb830088c21 Apalache SeqSelectSeq Constant False Passed
c9f34e957e523e32e31204e9b2c910a24faeb11d Apalache SeqSubSeq Constant True Passed
ace8d0edac134c6b10b8033578c5560a409efdf0 Apalache SeqSubSeq Constant False Passed
9a47e65c5b3cf192ee7c341f01418b37eac7cfca TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange Constant True Passed
6ac511a93ecfb91ac1c47b34285d8a1943c2c5d6 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange Constant False Passed
c3758783101a59985b944aead01d04f93bc93b29 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Constant True Passed
62235f434a2a5f837b0aa01a9958475fa6eaa805 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Constant False Passed
6def6af5c5b110c4665a2d712ef3200ebb038949 TLC with reduction strategy:
  • Case Feature: f @@ g is replaced with equivalent: LET DomF == DOMAIN f IN [u \in DomF \union DOMAIN g |-> IF u \in DomF THEN f[u] ELSE g[x]]
TlcExtendFun Constant True Passed
c754876bb7701349e925160e55555e68cd285b42 TLC with reduction strategy:
  • Case Feature: f @@ g is replaced with equivalent: LET DomF == DOMAIN f IN [u \in DomF \union DOMAIN g |-> IF u \in DomF THEN f[u] ELSE g[x]]
TlcExtendFun Constant False Passed
965930c2b44bc60bcdd58f193dd32bf7d066eb90 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun Constant True Passed
25d7db20b9ca06c572086471131bfe5568001394 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun Constant False Passed
c7cf9f68b2fd61647ea20713812a541b0c7919a4 TLC with reduction strategy:
  • Case Feature: SortSeq(S) is reduced to equivalent sort implementation
TlcSortSeq Constant True Passed
99999d4816fa6af380a01a85f6f0ba00bb25b39a TLC with reduction strategy:
  • Case Feature: SortSeq(S) is reduced to equivalent sort implementation
TlcSortSeq Constant False Passed
66afb7288bd2e11a4a7e924f772eec019989373b TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Constant True Passed
e3d66ad28a39ccf79fd7240d1705a43a3c8699e7 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Constant False Passed
4a3f9786c3da2053febcc86b563399248a0f557d Apalache BagBagToSet Constant True Passed
fa08eadf513650f60be539fc02d9effc93b33b4f Apalache BagBagToSet Constant False Passed
c92a046b015336c66fe254e9133234d1b058f3ca Apalache BagSetToBag Constant True Passed
ef315f1d6274a35cca06855502a173df187d76d1 Apalache BagSetToBag Constant False Passed
17ed8a59b8b9c45e7125b0c5c271705bc3d17a8e Apalache BagBagIn Constant True Passed
eda87fe58e70bbec5260c1742ad31ff75d1bc67a Apalache BagBagIn Constant False Passed
c6dde885ea10efd1ec9e58797effa1a850b29778 Apalache BagAddBag Constant True Passed
753b133439df9b2a82147215af516f3a1f6ba841 Apalache BagAddBag Constant False Passed
535e88e5488139e7aead6ed5f2711ff403bc043c Apalache BagBagSub Constant True Passed
1607977c4ff960ac17dd6562735f97dabc952a7b Apalache BagBagSub Constant False Passed
c3d2edb952172246e5ea5b1f32a81d1cb05ca4f7 Apalache BagCopiesIn Constant True Passed
403afdaf9e85aa88d03515a2527cfbd965bf5842 Apalache BagCopiesIn Constant False Passed
d7885e829a906ef66d70159f85892db817da1772 Apalache BagSubsetEqBag Constant True Passed
094c2d72bdf7e20b5364a4d16f73ceb186c02c89 Apalache BagSubsetEqBag Constant False Passed
79c94bc3ea9bbc3f1786bae16c912f1c75b79d44 Apalache BagBagUnion Constant True Passed
883cbec0115bdc2ddd37724aecf8d7693ca9c60b Apalache BagBagUnion Constant False Passed
e2e84c50ad1bba1cb5ed6bc51c86bac98a5ba40e Apalache BagBagCardinality Constant True Passed
35434316981a0c1b3ea5b643ce041667fd9e1ff8 Apalache BagBagCardinality Constant False Passed
03ec01f33107e8e397de015f4e4f1dd0787b75cf Apalache BagBagOfAll Constant True Passed
b9e2c9db29ae767fbb2441733e4095d054a88bc1 Apalache BagBagOfAll Constant False Passed
d0fa4e771f861eee23d50ea0dfb48f4a95dce113 TLC with reduction strategy:
  • Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation
BagSubBag Constant True Passed
fb2b9019b7b16ab601bb24e9fbdfe376c04db142 TLC with reduction strategy:
  • Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation
BagSubBag Constant False Passed
8f4feed34f9caadf55a82eedf5dc0f57fbb815ec 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 Constant True Passed
30a53113af8981ee708fbb1cf8d74f25bbc30c67 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 Constant False Passed
2d51080a43ebb1c1ec32ee99a0abd9efc5d26ae2 Apalache FiniteSetsCardinality Constant True Passed
c71b3f2ef3d8ddf3f7f386adb55bc9495d2b7633 Apalache FiniteSetsCardinality Constant False Passed
a2bde81f0e9128308fa2ac4c2d613a1abdbb7d92 Apalache SeqHead Constant True Passed
1f9e677357eeeb9b220d95727d72bbc204be1b82 Apalache SeqHead Constant False Passed
fc06736535bbbf861f78a1d78ae4a5a5c53155e0 Apalache SeqTail Constant True Passed
079a5ad267659b13b41561b4c67391530fd594d5 Apalache SeqTail Constant False Passed
2c915dc20df141cbfe0b18a9a94f97579c19bfe1 Apalache SeqAppend Constant True Passed
2f6d841d1fe7d05eacedc5592990cf90757313e0 Apalache SeqAppend Constant False Passed