Index

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

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
af9950a4b1947f2ff2f3db488b1e8e328703b1b6 TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
Constant OneLineComment True Passed
3c36ea45574aeeae2161e19c98dc9865c2952892 TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
Constant OneLineComment False Passed
6fb6613fefe98c0dc7e8e5961b375bd162ff815b TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
Constant MultiLineComment True Passed
0dc78c89c27a89d17ce48210e2349e8ee50d8df1 TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
Constant MultiLineComment False Passed
86899fe6e3a44df1840e4e93271e960ef4fcb096 Apalache Constant BoolTrue True Passed
069e1ebe318bf7843ad86be080a042bf8621b510 Apalache Constant BoolTrue False Passed
90a31cfe2351c3877a9c990aff476bd6f9d98ede Apalache Constant BoolFalse True Passed
290925cb1855d34e656eb10e0a817d00c36969fc Apalache Constant BoolFalse False Passed
7b6e8b00a7b20e5a7709363d409508b1a9d8e88c Apalache Constant BoolSet True Passed
38e2d989e55ab8e8ac17bd98a7b306faef2ffcea Apalache Constant BoolSet False Passed
105c1f186698b729cabdb22674f62d6b5027f2ed Apalache Constant And True Passed
b7cc29ac7b7d0ddd65a99b5d6c02cff8fbffb09e Apalache Constant And False Passed
0e884d81df22b36aa5c3917557505887d402e187 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Constant AndMultiLine True Passed
1269f819461424416d99ad6fe48babeddcaec2f0 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Constant AndMultiLine False Passed
48f14580b43534862031078f9f3d42a1b322155d Apalache Constant Imply True Passed
e2b11558c1251810bd90dd460d6f0522c055636e Apalache Constant Imply False Passed
d53641767d904b3303b9383508e4f61901dec04d Apalache Constant Not True Passed
ec052f170e4de95f1a12a720bf4be86003dd9a50 Apalache Constant Not False Passed
4493098dedcde6ed9367e1f0648205659e4e6da6 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Constant Or True Passed
4c5cd7add6f38ea879449588a0fbb8fb7b5906d7 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Constant Or False Passed
e9f82d8891b2651e3ccb9306c8a8cee8bf96a07f TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Constant OrMultiLine True Passed
081883f7e778b0ed7d8983e16f01f5b6e43402cf TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Constant OrMultiLine False Passed
51823473629f3815b382bbd624c0a0c3ad0ca75a Apalache Constant Eq True Passed
1157387e2e27b35d41d3ec15133262d8304df413 Apalache Constant Eq False Passed
4525be6078e66fea88d0daefdf2242dc8b12b79f Apalache Constant Ne True Passed
bd9c9d9cd403c62ec0dd1d1c76f23c94e61bccd1 Apalache Constant Ne False Passed
d9d4b1e57236056d92b1acaadfcd2add76dee40c Apalache Constant Let True Passed
6eae32dcaedf5e37e8cb819cd038ff7e5012cf5e Apalache Constant Let False Passed
93fcae04b17c6e853b1a2ae8ecf0add0aa3fd19f Apalache Constant SetEmpty True Passed
1442e0cab4d15696675502c665cfab2224fcdd82 Apalache Constant SetEmpty False Passed
94582b58d0f8c6100467a78f5f863059fa20fe8b Apalache Constant Set0 True Passed
e11683bdc34bda821efc34d168b4a2d9747ff3f1 Apalache Constant Set0 False Passed
8d93fc9b3a743c34fa1fd8c82891e8201164ed06 Apalache Constant Set1 True Passed
06c8f031f4ec3e7565109935165dd9024ecd8b11 Apalache Constant Set1 False Passed
46652d6017722908a269fd6273c67185c0623722 Apalache Constant Set2 True Passed
13f5ec9b0125028e75391dc202eb646a062ebc34 Apalache Constant Set2 False Passed
f5fe19425afdb9283d9b31718869f6fd618918cd Apalache Constant Fun True Passed
ee457b185c60158e1676d34ff57b9acc6edd0042 Apalache Constant Fun False Passed
a93ecc1de2e1d9139a8f0617738558bda9e4720e Apalache Constant In True Passed
9792170799911ca4b153dab021dec9c0ad241cf4 Apalache Constant In False Passed
ed9a736a3b9917c5e97639b28861fd33ca043789 Apalache Constant NotIn True Passed
c371ae08fbf90be7573b88f87bbb27468362c22a Apalache Constant NotIn False Passed
2b8e71360ffc1421c50b4c63a3487ed8a7553062 Apalache Constant Exists True Passed
72576b9a55b71d004e33dae885041afaed092d19 Apalache Constant Exists False Passed
47016140ab8e03d48748468aa6ecca8f5d50d34b Apalache Constant Forall True Passed
78ef43eac78a922ff92ed460b0d10f9c49f755a8 Apalache Constant Forall False Passed
8c172895771a9be8c81ad57128c198a7e694f8ca Apalache Constant Choose True Passed
8b33fd1777f0fe1ad89640a333f16a198b89fb99 Apalache Constant Choose False Passed
c498b9b1c3fbd83faeeb3d6e5891b300b1149181 Apalache Constant Record True Passed
21a86834fa378ae3f5f5b6cad28211b55de0b964 Apalache Constant Record False Passed
b6812154bca3aa5b2b712564f10b2596ffff3893 Apalache Constant Tuple True Passed
7a4b1ad604d852c0fe149df7b992ecf7ef781744 Apalache Constant Tuple False Passed
ce38612b87f91d04b1ce82f26d1f14b5b11b7847 Apalache Constant TupleEmpty True Passed
f3d91be799b0d7e8bee63cc480356f03f77b03ce Apalache Constant TupleEmpty False Passed
8638b27ed04a1d7c223dc426ca92b21a4130bd6a Apalache Constant FunApp True Passed
21067629af377f84c64dd04e827e81ae2588bd09 Apalache Constant FunApp False Passed
9799e0e2d606182132373ff918c002e4b682357d Apalache Constant NumZero True Passed
0f974caf36d4a01aa9a01efa21384f2da541754a Apalache Constant NumZero False Passed
8805d4394abfa4c09e82a8fe4274381493915e85 Apalache Constant NumOne True Passed
5e8246122d53fdedd50d6907677fa1e6d13f1e94 Apalache Constant NumOne False Passed
319b308afa835cf3c39e748679c003c3c592343f Apalache Constant NumMaxInt True Passed
27c55045af821b59b607db790300614edb1a2e79 Apalache Constant NumMaxInt False Passed
9614d483f8696f70936ab9147813fd47877da4be Apalache Constant NumUnaryMinus True Passed
2aa8fe8dd097d9b68cf60a209a49ec716b5a5b5d Apalache Constant NumUnaryMinus False Passed
efba448f830594eb31e640fb0bb5b093ad21ebe9 Apalache Constant NumPlus True Passed
564eedb63cdc3c572d7655907b2674a99dd7dbf7 Apalache Constant NumPlus False Passed
eda2a051dba74030f9b56b1a96136518c1f48383 Apalache Constant NumMinus True Passed
fe64f6f819ece95d9fe3566a06bbd250f4bc28dc Apalache Constant NumMinus False Passed
102d549791acaab592a334b6e10d8896fd97fed1 Apalache Constant NumMul True Passed
2ade0edf85ff90400fbdf93560ea162a6253bbd3 Apalache Constant NumMul False Passed
b42694e42b28426b83fd819f084a3fda693c8a0d Apalache Constant NumDiv True Passed
644c7c6cc78e5062e28f644510c4a49b0e133ba4 Apalache Constant NumDiv False Passed
d5a2f0c7ef67961bb464fa5274481c91b140ebbb Apalache Constant NumMod True Passed
e71a26ede4925a0b51c02a7305a15f86f46ea57e Apalache Constant NumMod False Passed
4ba48d5a2eb31001c93d93ed0d3153deb567b0d8 Apalache Constant NumPow True Passed
1aa8759bdcd789f835b76a700c41a1f08ba043a0 Apalache Constant NumPow False Passed
f98a177f83b2f346eab178e67dbe5650bdca91bd Apalache Constant NumGt True Passed
c4c4711c5e94766d85f6c5f4fffdbeafcaf0e247 Apalache Constant NumGt False Passed
92e8fd9ba963fba4365763709dc446b2dee2db68 Apalache Constant NumGe True Passed
010c79d17d23c88e47fba48763b0d754adb591d2 Apalache Constant NumGe False Passed
7f1a8b73a90f31670ed3ced1fe9c431a8bc9d690 Apalache Constant NumLt True Passed
62ceb4f48f76fc3c30e58a9d28e0ee62a0b01253 Apalache Constant NumLt False Passed
fb22d061423d72886dc6f923409740352ac64fd0 Apalache Constant NumLe True Passed
8599ce19893eaccd155e845f8e7eb520bd956b71 Apalache Constant NumLe False Passed
f726e23748c060e9a32827307094d1100761ea85 Apalache Constant DefFun True Passed
ec6ad61ed65e5a95ba32a8640901318b409fa4ba Apalache Constant DefFun False Passed
c964414d3b81c11c7d2bff2553cc739770fbb87a TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Constant LetDefFun True Passed
f1dac791534a1b620db456939135bf4a24448f90 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Constant LetDefFun False Passed
5a6b671a02f158cbcf52e11947dbd85d90c8e4aa Apalache Constant DefFunRecursive True Passed
ed6e9394fc54249d391f765d3f14c8b2d53f80a2 Apalache Constant DefFunRecursive False Passed
7f768def52e923012ace6301cb4669c89d8cd58c TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Constant LetDefFunRecursive True Passed
74bd1074664aa546ffe709156d232af9372074be TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Constant LetDefFunRecursive False Passed
b0a1ce531968fe999aab0137aa9e6247f133837a Apalache Constant Def0 True Passed
e3b95523e654f7316e21c4de16b4f213a0dedf9a Apalache Constant Def0 False Passed
6ba58c20f166d9b2c946223984fe932016a357fb TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Constant LetDef0 True Passed
c19c025189ae862b7c254dc1ee3976ed12d48294 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Constant LetDef0 False Passed
9033c17c7d0c24a48c8a07c8212f60f3946a8572 Apalache Constant Def1 True Passed
cccdf7347681eea3a2a1984c393602e61ef27ecf Apalache Constant Def1 False Passed
e7fc62a85989456228632b620f80d2c12337a276 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Constant LetDef1 True Passed
08617236af09bdd829bddbd7b90fe9d806a89429 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Constant LetDef1 False Passed
b208dd8c9d7355f1d676f55376a0fe7d1c5d71fb Apalache Constant Def2 True Passed
efb9d7f91e75d64800f03b83d3a921b92441cca2 Apalache Constant Def2 False Passed
447a0237d99b6c9743096f231a4f484acabebc7f TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Constant LetDef2 True Passed
c0984d44e62aaf077f9c8087f5b39256e8fa3d45 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Constant LetDef2 False Passed
80b6d29fe93c8dff158fcf33d1889d5e8bf3afd7 Apalache Constant Def1Recursive True Passed
592e9e8a7ea4e0e83a260cc6efd924d732a4cc73 Apalache Constant Def1Recursive False Passed
b4915ad98b84088781bdd5015665987bd465cfb6 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Constant LetDef1Recursive True Passed
cf79686a107ec7e1b6cc11e688432a33fb5c03b6 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Constant LetDef1Recursive False Passed
f54e82cd12ebca8df13adf0b4492e28aeb91c1b0 Apalache Constant Extends True Passed
87ba973c9c8b4968e03418b91f0ce102cc3bd56c Apalache Constant Extends False Passed
ddc96dbc4b64e1786491945d72d2eafbac81f861 Apalache Constant ExtendsInDifferentFolder True Passed
5b049dc45cad8234e07830bb079efff1e7e54274 Apalache Constant ExtendsInDifferentFolder False Passed
5d5e84435804e79a68e07c0dfd5f551b250416aa Apalache Constant Constant True Passed
72cb3b57850517852df9783a41d50191f9f7ec7e Apalache Constant Constant False Passed
4c3a5a66fdf4956b1a64c2cd7107f19d5b513748 Apalache Constant ConstantModelValue True Passed
33e7d75749a54e458135bf359b115fdda6eb9574 Apalache Constant ConstantModelValue False Passed
b7817f5a80e07c45580f5f57a53e156c356251f1 Apalache Constant ConstantRank1 True Passed
1a4a08ef829385b1c50813881464b2287c20825a Apalache Constant ConstantRank1 False Passed
8d32a5977f0f96d0ecbf9f8c246f9e3a1d9a3fce Apalache Constant Instance True Passed
1e82095b3ff76f538578b9aa87b85fb92c540fc5 Apalache Constant Instance False Passed
b706147ad1f73dbed8c2fccb5e2df391498e69ab Apalache Constant InstanceWith True Passed
fb6bf2991fd16870dc0e94c8ef5aca6edc08937a Apalache Constant InstanceWith False Passed
99a0e5e807e7416e7979f9b15e76c01e2beef15c Apalache Constant InstanceNamed True Passed
7ab73cfff59faf78f57c95ab29c2603fae1cde00 Apalache Constant InstanceNamed False Passed
31642d818309d90c680641ca334c0c98da35efd6 Apalache Constant InstanceNamedWith True Passed
0569c8b1aa151bfe812a1d947bb5629e27914b81 Apalache Constant InstanceNamedWith False Passed
03886f0012832242035880e5849e2101728384bc Apalache Constant InstanceInFolder True Passed
64169b8c11814e7bc0eff3ecb4870cf46688b566 Apalache Constant InstanceInFolder False Passed
166dcebeb15b2196c06555173741cb461ca9f437 Apalache Constant InstanceWithInFolder True Passed
dc16ebc19b928f20b82c2704a0574417d4661526 Apalache Constant InstanceWithInFolder False Passed
a4b33743c9b3a276cf393a20be879b6228d765f4 Apalache Constant InstanceNamedInFolder True Passed
08f5d6497a1283f5f9bf71240e149bb4fb3b5315 Apalache Constant InstanceNamedInFolder False Passed
8c24eb12313b3b1386cdbf4cfc17e57885d22fa7 Apalache Constant InstanceNamedWithInFolder True Passed
a9f39d770f2f55ea6d1e101ee4dec032796d5d91 Apalache Constant InstanceNamedWithInFolder False Passed
57bd2cbd62a5de21b3b920935a7b53fbaed8e94d Apalache Constant Cross2 True Passed
9bf15066470575745126b1a6348f690af04c4730 Apalache Constant Cross2 False Passed
2f21bc1a04e371c732193685d3b946d15e672d88 Apalache Constant Cross3 True Passed
a2e06e2f81ba730581eed59f45947da81d7b7277 Apalache Constant Cross3 False Passed
0a71e982c41a8fdc506fea64674a8d6089611df5 TLC with reduction strategy:
  • Plug 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))
Constant FunSet True Passed
f4f28900d03d76bd5dc28b341f096448b9a07ede TLC with reduction strategy:
  • Plug 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))
Constant FunSet False Passed
2ef80eea0e0c954aa92ed3b988ba959cc96955eb TLC with reduction strategy:
  • Plug 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)
Constant RecordSet True Passed
e1e783757670d3b2fb000d16c0ca9e139f11b2e6 TLC with reduction strategy:
  • Plug 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)
Constant RecordSet False Passed
982d3317b3662c02910ccba3e8c75863842bd9ad Apalache Constant SetDiff True Passed
207ddef06de8a79ba424836f1b662f392456ea05 Apalache Constant SetDiff False Passed
8da36dc7512c9b94c83ae9cf018ff7187b19450f Apalache Constant SetUnion True Passed
0db4733b7920f45dd7bb1a6777365fd67e6ab0c1 Apalache Constant SetUnion False Passed
fa415e86ed0593d803cf847948dacf7c9fcff8a6 Apalache Constant SetIntersect True Passed
a7017cb5937fb7ab6ef1f85774f54ae67af8eedd Apalache Constant SetIntersect False Passed
c7d010bc39d687b5e54d80093ec35e0b9a8fcfe2 Apalache Constant SubsetEq True Passed
d37a36590b8d62d8bc00fb299ef777a0de66f8bb Apalache Constant SubsetEq False Passed
e478bc98aa9104da20c9eff254fbf00e12c1d401 Apalache Constant IfCond True Passed
aab7ee1873d503ddf564d24f20174f89240c1014 Apalache Constant IfCond False Passed
f813bc2d515bb7b8dbafac2b40aff5004be5eb2d Apalache Constant IfThen True Passed
85f36be59da6d4e8be046849aa4f7cee1416462a Apalache Constant IfThen False Passed
3d6a9416499716b53cc523d104e6e1f7fc002d09 Apalache Constant IfElse True Passed
e658703c97382dc11887fbcc6b027e87e33d1e02 Apalache Constant IfElse False Passed
ca6c1fd94417f2d9b4623434587eb479efaf6dd1 Apalache Constant Subset True Passed
c77e1ad5cca7382d090b1986ac49795e88a93dc8 Apalache Constant Subset False Passed
65279afbc1e1be09d22ff753d4afce5a9afc4895 Apalache Constant Domain True Passed
f7d55417b41b07e1352ed8e45cee402845e68fbc Apalache Constant Domain False Passed
a2fd03945f8a82b703865a8191afb9202d6834da Apalache Constant Union True Passed
2548e12dc3285ad958cc8d1f5f3d3fe37bc0d608 Apalache Constant Union False Passed
c7cd4b28c0098f65f12ebd1c0fd5d1a96909ab75 Apalache Constant Equivalence True Passed
8ff753205d8fdcfe24efbd25ee58f09d6d0b25a6 Apalache Constant Equivalence False Passed
0e3c4ae11c9de01c4e16a08db413c4cf60df1560 Apalache Constant StringEmpty True Passed
fd135a00a4caa5d48cb6f539776a1d2a9e27c5b8 Apalache Constant StringEmpty False Passed
4989f2eff5f66fd9599f1552a74e5addf2f9a376 Apalache Constant String True Passed
8471a56d80d2e5a4ca90b2f8ba11ea2dd3352808 Apalache Constant String False Passed
68abf4910499f1d7cd22d3e659e86fe8a50a2f77 Apalache Constant SeqLen True Passed
5f6d8cca86e102585073bcf71bde0116acb32975 Apalache Constant SeqLen False Passed
8153ff7ea68fd0a7c27bdd9508b4fbea5de3753b Apalache Constant SeqConcat True Passed
65d87087b66b73d08541a6e29e9e88cd949bc4da Apalache Constant SeqConcat False Passed
2206e5689b7c578f6accf457e58405fa11f42e27 Apalache Constant SeqSelectSeq True Passed
f02be9160f4b487b4dbce060ed3cd5866fd2e49a Apalache Constant SeqSelectSeq False Passed
ab9a5a34eddd92d45db2f57abc19db6070efbb20 Apalache Constant SeqSubSeq True Passed
ce5c4902ebeb36e185e29a3daae8b0203c8ab264 Apalache Constant SeqSubSeq False Passed
4ce666bd2e976a677bc2dc4782d79a31fb822435 TLC with reduction strategy:
  • Plug 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
Constant NumRange True Passed
8a4baa2eacbc81957fd07a24b7eba74385703b37 TLC with reduction strategy:
  • Plug 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
Constant NumRange False Passed
578db5d627b6b4a5ae8effa44099abd31eb9e2fb TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Constant TlcSingletonFun True Passed
2224f0c40272875b6226aaa0a400ad687c40e7f7 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Constant TlcSingletonFun False Passed
f387deaeaa4ba21aee2aa0ac8b28b5b2f698a91b TLC with reduction strategy:
  • Plug 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]]
Constant TlcExtendFun True Passed
90c00019f974d4dbc7c38701c40bdcee4f987f0d TLC with reduction strategy:
  • Plug 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]]
Constant TlcExtendFun False Passed
45beeeb4753d06bd0f01514b1c2a16826f1f6926 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Constant TlcPermuteFun True Passed
b657c06c52e6670765e47e057c3ee45069b3a77c TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Constant TlcPermuteFun False Passed
d63a9cdacb9bec2a6cb9066ff1e1d7c04662cbef TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Constant TlcSortSeq True Passed
eaf7802795731aa84a136499e59fe376d6e22723 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Constant TlcSortSeq False Passed
46af2ae2b7565d3163d148fc6c70f7198555ce06 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Constant TlcEval True Passed
781dd8023fec9d21ad0b77e16de89b5dfda6d3cf TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Constant TlcEval False Passed
5c38a8efdd67537b339ada1cf7ebae103e9110ae Apalache Constant BagBagToSet True Passed
3d9d27eb0d5aebab5ef89c69e64895097e365f76 Apalache Constant BagBagToSet False Passed
78d10328d630694dfcd2cf29990cba383a57595b Apalache Constant BagSetToBag True Passed
775f534e916571c1dbfda94885f1c926a41fc64c Apalache Constant BagSetToBag False Passed
300ca175d0ba0bf32e375dfe8b888ce43ad2e32d Apalache Constant BagBagIn True Passed
21410d8c4dcc3be0fa7d0cb3833ecafa60052817 Apalache Constant BagBagIn False Passed
b13dc209c35b75588ddf0af11742fe933f37959c Apalache Constant BagEmptyBag True Passed
60cf328adee3184605846e30b14544d70e5de073 Apalache Constant BagEmptyBag False Passed
8c2ef6d5380ef988bf72664ad21ec8a1e482a83a Apalache Constant BagAddBag True Passed
a19f71e372c56bbad6fea128be6e7d9a2665fde9 Apalache Constant BagAddBag False Passed
3b5b96f98f7c04e106d31854ebffe299187a3a96 Apalache Constant BagBagSub True Passed
50a368548e55d753dd3849963846a7ca12787ef3 Apalache Constant BagBagSub False Passed
08d1c2553eafae97d344e4a85be329ae2fc5c63b Apalache Constant BagCopiesIn True Passed
d464eb65551fadf7d43a2b093d63fbe045aca0ee Apalache Constant BagCopiesIn False Passed
52864ab0a252c94ca9dfb56a5348fe952fd8caad Apalache Constant BagSubsetEqBag True Passed
4ea72fe228ee8c62e51d5fba6583b9372dbacd75 Apalache Constant BagSubsetEqBag False Passed
67d5dfb8eb7f190867386cfcadeccb66556fd325 Apalache Constant BagBagUnion True Passed
adba8dd8bf1f334919822b3087a6de3d0cb6b921 Apalache Constant BagBagUnion False Passed
1644986eeed9a332b1c5ddfa1b2ebbed7322adca Apalache Constant BagBagCardinality True Passed
ec769e1e8401fcc95320e805f692ab5c6a15cc9d Apalache Constant BagBagCardinality False Passed
6a9768ddb8bd6bd47902075027bddda29d336786 Apalache Constant BagBagOfAll True Passed
a9acdb1ef0bc14f804e06e13897542bc7228f003 Apalache Constant BagBagOfAll False Passed
5c13e0d942038ccbde957509b2fae1d9605a3fcb TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Constant BagSubBag True Passed
1e19ad6fb6c9daad009828dac5cbbb587041e69f TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Constant BagSubBag False Passed
677176c770397b8ea4f487eb50e28a2e5fb87088 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Constant FiniteSetsIsFiniteSet True Passed
0aa62e3042f2c6898608d52e4624c29c0cc4bc61 TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Constant FiniteSetsIsFiniteSet False Passed
a8bedccf54e7e3671373518600e323e22b9cb484 Apalache Constant FiniteSetsCardinality True Passed
4eb072d2cfa3acd3211693fad5298b1fedfd5b81 Apalache Constant FiniteSetsCardinality False Passed
7d0c5acb441de688f3fdb838a121a8faa6f9cfbc Apalache Constant SeqHead True Passed
45027525c9daac475db0d6f379e3d0b0d56e5fd6 Apalache Constant SeqHead False Passed
ed00b33cc5edde4b895e2172f222ee066625c1dc Apalache Constant SeqTail True Passed
e17d71f419666b7da6d350aac89678b352ab0abb Apalache Constant SeqTail False Passed
199051aea8c5d371a79630ce380e4a7664de9975 Apalache Constant SeqAppend True Passed
515f75e9e4f949f8cb66f5fbef2a41e172078a24 Apalache Constant SeqAppend False Passed