Index

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

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
c83339c65fad9b504e0b7f456154a0ea5b0078b2 TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
Let OneLineComment True Passed
8ec2827f396bb39605d184fdf389035147bca8cc TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
Let OneLineComment False Passed
ad802033f2fb567d0f9d75e5d071c21da95a4846 TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
Let MultiLineComment True Passed
f0c8ac077dcdd067b41b03a12c9d7d487ed6f399 TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
Let MultiLineComment False Passed
06cb41f6d429e5df49e3648fa0c09fcd9dd41244 Apalache Let BoolTrue True Passed
afb5a158cc0289c80fb1a9285d646ce5c9483562 Apalache Let BoolTrue False Passed
3870929418abe4114f36583a9a4d04798480ce4f Apalache Let BoolFalse True Passed
db34a439da0a07814aeb80e65ca4fdb76d980551 Apalache Let BoolFalse False Passed
0f3f1c02e21c33dfb676a9059e4dbd0073a1cb65 Apalache Let BoolSet True Passed
0639a174117014c70222431a97ed3122a43363af Apalache Let BoolSet False Passed
4590c0d29ca74d0f554a4612ae59ec9b70b8ac90 Apalache Let And True Passed
3452634f7ed56b53b96306eeb7f5b4d876187680 Apalache Let And False Passed
040790120d4c3ab24af47ab00381776b60b8a6b4 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Let AndMultiLine True Passed
ccea67a010bc7fb12ded5345dbb137aece52527a TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Let AndMultiLine False Passed
173a5569eb4eff7c700953b6242e427b296691f4 Apalache Let Imply True Passed
4f76102ea96a539955227bbff77d4efd52596efa Apalache Let Imply False Passed
c85781eb0f6d5a54314ee18d24c81854477a4c70 Apalache Let Not True Passed
bf21403654892c5050acbeedd8bc42af1f006d37 Apalache Let Not False Passed
ee67b6597be8da458c6fb184d86fd9657e022b98 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Let Or True Passed
474a3294934c58238f30940655e379e5a8fb9345 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Let Or False Passed
03190783de6897d460f05fb0ffbe5befd203cf2c TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Let OrMultiLine True Passed
cf216d66495ab7f1191f405ef79e6c972821cecf TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Let OrMultiLine False Passed
2ed391362fa8262b533c40a83e4958c16ff8d7ee Apalache Let Eq True Passed
af8417db8fb598f2645f064a5e891adf4bfeadce Apalache Let Eq False Passed
914b71041b9c93dac4afed8c5a0baf0e90c07f1a Apalache Let Ne True Passed
5c63c3c6dc4d45de7c2d164b600e9273c50a7fa5 Apalache Let Ne False Passed
fd5bba37f7dcb973d109eba71e90d9b374214ac7 Apalache Let Let True Passed
3824cad01a99a912935462b68af6984838e52835 Apalache Let Let False Passed
67130891bccc937c05d79e9b669aa0369a3b5ada Apalache Let SetEmpty True Passed
634a4485f6e784c5e5e1453fb3b0f08e150f3e83 Apalache Let SetEmpty False Passed
36e11df36d388fa59151f8a030f1007a58342517 Apalache Let Set0 True Passed
8323236f5fb44f69c7a667c9203d492dcfe665ce Apalache Let Set0 False Passed
fbc15e4dd73d8ef1f136a9af5b4ff222d9be9922 Apalache Let Set1 True Passed
04931032ba178e883eddfa429b5b251e0388948f Apalache Let Set1 False Passed
bb60025931e9e5e07634bd3983d02ef77dc1dea0 Apalache Let Set2 True Passed
016b357f030cc6dd41907c8023313e0318c50955 Apalache Let Set2 False Passed
2e7fed07380564b1444046b8b28430de4b73ea80 Apalache Let Fun True Passed
907f7569697850a7b34ec996ec71e6243866f5ad Apalache Let Fun False Passed
7b381ca36d140705ea9dc070980d745f1ba39463 Apalache Let In True Passed
f0741947d3e4de05021b66e226547ca656a15efd Apalache Let In False Passed
98e3356685f785c882aaa53fa4ad3246c0bee7f1 Apalache Let NotIn True Passed
f50a5badbefd638945edc5b71b0739c7175ac673 Apalache Let NotIn False Passed
a5da83a5ff27fdf544d45e52184f5273d41f7931 Apalache Let Exists True Passed
aea5feec63a83011e2b7d60efd981fe0f0876f1d Apalache Let Exists False Passed
7cead322b6dfec7148998104d4cbea07e716b2e6 Apalache Let Forall True Passed
d7dd33e61eed14cbc1fa39470263a3d3d5973568 Apalache Let Forall False Passed
a798420ab75707e589d4a511f3335b8be062a03c Apalache Let Choose True Passed
dbbd6d9fb610ac8656945bd56dece9cff949c89f Apalache Let Choose False Passed
9dfac4bcbe9c3449d35c9b168980126fce1e6d1c Apalache Let Record True Passed
96a9b20fbe058325144acdefab4da3796cb4456a Apalache Let Record False Passed
758743c466e14370651525121b0366067792d9ca Apalache Let Tuple True Passed
eb471cc3abf2996e582249bfecce1206fc780ed0 Apalache Let Tuple False Passed
74340ccc150151054ac448024f270aac209e1866 Apalache Let TupleEmpty True Passed
065cfac74aea21d7813618399a487289721f761f Apalache Let TupleEmpty False Passed
d75d4f484312da2e4d3d65d88c2af3cba1b323a7 Apalache Let FunApp True Passed
f7a56637239b89afe0a7b7b28a294aca64f620ac Apalache Let FunApp False Passed
fecb1c8c5bbfcf5e455f8bd2941bf294787427bd Apalache Let Prime True Passed
f4d648a5920cd0e3cec194dced5ccb1bba3d9e85 Apalache Let Prime False Passed
2b037cb7c85641e3b76ab1c57fccaf1bbbe5d83c Apalache Let NumZero True Passed
76734c5c8a2b05ea60b3b6bdce59d8b2051f3809 Apalache Let NumZero False Passed
c8df92b0f82ebd59a675b6460bc21e3d8e1427c6 Apalache Let NumOne True Passed
4c263f9841f2913152e82e709cb55cffce6f6e40 Apalache Let NumOne False Passed
51e3eba388510a7fc13e867910f78c42f69eeb87 Apalache Let NumMaxInt True Passed
f1c9ac5d012045620d2a74e43309da1177773303 Apalache Let NumMaxInt False Passed
383b13ec460045744dd5e9262cd7a36cf407c334 Apalache Let NumUnaryMinus True Passed
42466a59d054323253cf4cfb1740c9372224837e Apalache Let NumUnaryMinus False Passed
cd9d58b53fdf6eadbb842e865a69def8890396f9 Apalache Let NumPlus True Passed
3d9cfbce17f322b8ba1f3c2c1628949b9352375a Apalache Let NumPlus False Passed
0f48895547aaddf330d1f0f2e8ad57880f9dd6a9 Apalache Let NumMinus True Passed
016ffa323fdb78bce685fc198637e57189e01ac8 Apalache Let NumMinus False Passed
c1af3efdbc8f3f8b13abff52e9c41fd781840650 Apalache Let NumMul True Passed
f3f132305293e0d6b5d37ef4aab927e2fe520929 Apalache Let NumMul False Passed
c56f9709af7d639b852c45c766f572433a6b1e81 Apalache Let NumDiv True Passed
d6666a37b541a3be27bbe34878551c099a73fc7d Apalache Let NumDiv False Passed
2abdb626b5324ea278c80541f0da7d6d3b799fc1 Apalache Let NumMod True Passed
c3b59277785b3b7ec46f2b77f23088904326c04e Apalache Let NumMod False Passed
95b17ff0cc7ea84c652874023ffe4227befcc77b Apalache Let NumPow True Passed
42263614bd6e86ec1849dea3ec16802da67b7abc Apalache Let NumPow False Passed
5d3257779203f72b31c9175ccf9ac6b53c48d636 Apalache Let NumGt True Passed
348d674b1d51b558416b1a5e5e562c760be60eb0 Apalache Let NumGt False Passed
1bb34d51d0781a550d4edd33f2c9d2093f86a1b8 Apalache Let NumGe True Passed
7c9b9ad7bd41500db7b5dde69ba0aab5fa90d9d4 Apalache Let NumGe False Passed
cc54e75bca07f9d7874c527e00ed7d307d6b4a10 Apalache Let NumLt True Passed
4bdaa0e6e14f7fc1a06adaf4c81a286e89ab0fe5 Apalache Let NumLt False Passed
28068509151cfb9839a60b4481adf17667159abb Apalache Let NumLe True Passed
560173feb1b63c4fd9acccbcd24b1ee185750e21 Apalache Let NumLe False Passed
36dfd9b662283c3f4f0d53020a6c0c0a37488922 Apalache Let DefFun True Passed
dc7b623fc85abf1b81ff6dcc6f1a22968e5d0827 Apalache Let DefFun False Passed
c7208accf7193fdfcd1e3afb9c05bde5e395dfea TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Let LetDefFun True Passed
23464eff7fad3bfeab1516c24515194cbee9dfae TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Let LetDefFun False Passed
bf6053f24ebf0c6227d7cf5b30943032deb0f86a Apalache Let DefFunRecursive True Passed
f807f627d8c2b85b64609a65e06dc44190a1a42f Apalache Let DefFunRecursive False Passed
0e389d39d61fa1f90b3b71103ac179c35e6922e3 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Let LetDefFunRecursive True Passed
c952898242464708fd7e79e950920b960f77b549 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Let LetDefFunRecursive False Passed
68ec03057badb4c04781e87e8f3580962e508a17 Apalache Let Def0 True Passed
5409acadd520c495f33ea074e8a19e8a10608ff1 Apalache Let Def0 False Passed
e3d3210278e3cabf3378f074cf17e506539ab120 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Let LetDef0 True Passed
3043cd522b14362d6482121d66d5463d8b265a5a TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Let LetDef0 False Passed
282ae46252aa369e97af588199f41d0a258a97d0 Apalache Let Def1 True Passed
d68dba880710cf727935f65d9def6c095243e78f Apalache Let Def1 False Passed
a1b4ea3f6997feffa65d5d11640a232f2e35cad3 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Let LetDef1 True Passed
d4ce37d06c93cf88545692e9c613c88eec6b39b1 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Let LetDef1 False Passed
2bfa6d0efb91e4e2988c58991e90e7e94e25dce7 Apalache Let Def2 True Passed
6642b7ef676e4fce8c79a71f721d97821c4f203f Apalache Let Def2 False Passed
40c2798d052465adbf3889ca87c468613ae98d0f TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Let LetDef2 True Passed
1d91b440081b49997783ff7fbbae4394d033e127 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Let LetDef2 False Passed
34ad5a557cc07357fcdeb21e388c1cdff45925b2 Apalache Let Def1Recursive True Passed
941c0efef5183bd02182ad365ae658b9b2157168 Apalache Let Def1Recursive False Passed
94c76226b33f151c592ccedee097e75a132f9ae7 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Let LetDef1Recursive True Passed
cd3d2278b223f8f0af72eb151b6eb0e2c300fd8f TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Let LetDef1Recursive False Passed
d358fd1ad91071d1109faae3b95bf5e94441c78c Apalache Let Extends True Passed
b2ec72c2170b904cc1cdd40f917bcffd88f6fe6f Apalache Let Extends False Passed
eb1b51e99a3fc91dba9474edaf4d54c88ac90995 Apalache Let ExtendsInDifferentFolder True Passed
7e34b889b060a50d868207eaefa9b93798d26ccb Apalache Let ExtendsInDifferentFolder False Passed
2ae0e9e6726b4218c8083246b3f2943db9367fa6 Apalache Let Variable True Passed
acf116d245f359e6f81913dc17cd215e526d907b Apalache Let Variable False Passed
4c21cf0ea14ba06e45141b146e321e9b06b9e7d3 Apalache Let Constant True Passed
bdcdcd7da54f2be6cc057c628371ba19b72a823d Apalache Let Constant False Passed
45911ff45fdb44587ad3268228e37be1fc8760a7 Apalache Let ConstantModelValue True Passed
cf587dc75800a7de0fa6e0594898732df9a9af32 Apalache Let ConstantModelValue False Passed
dce00ecb69a24037e69982e1f954582a826a964a Apalache Let ConstantRank1 True Passed
17db1e59351f20a5c36433bd8f91edf3ebae3e85 Apalache Let ConstantRank1 False Passed
a78f33bfb1881e1b55f1647c98cb22a50cdba44b Apalache Let Instance True Passed
3cc797661d38f6af98d846ea6ac65dd01b8516a4 Apalache Let Instance False Passed
6b49036f1700aaf6e07fdd31b49eb3ad3eb84a9f Apalache Let InstanceWith True Passed
41aff8e558ef0bbd5f694e4564099d233ffaf2ea Apalache Let InstanceWith False Passed
905c8ec97dae649f5945a47a71a650f8f82d927f Apalache Let InstanceNamed True Passed
d469016fbaf54f7e41491cc6abe78659ce67a74f Apalache Let InstanceNamed False Passed
57bd81198ac39a0c5391c7266980b8c7566a4f5a Apalache Let InstanceNamedWith True Passed
2e2df8211d8f37f7867d73d10019e06abec87c47 Apalache Let InstanceNamedWith False Passed
01184f48bb8fd128bbad86f60d2da02d331996ef Apalache Let InstanceInFolder True Passed
8dd1690c9e60c7de15c8aabf4a2dc2dd5256c7bc Apalache Let InstanceInFolder False Passed
01fa4943cf5bb59279b536035a68ae1ed92466ce Apalache Let InstanceWithInFolder True Passed
2b4007bc0f6632bb0940d49914ed52670b08c087 Apalache Let InstanceWithInFolder False Passed
7da0785415a64b079154fcaa81dba41c72dd7dd6 Apalache Let InstanceNamedInFolder True Passed
e0a8f20d84f463e058f2ba69e11d36f3d275759f Apalache Let InstanceNamedInFolder False Passed
214f3996be096f0dda0ca0212849da496504af88 Apalache Let InstanceNamedWithInFolder True Passed
ae8a3cc2ceadd2d07567787649edba23bfdddfa3 Apalache Let InstanceNamedWithInFolder False Passed
9b7eecbff91185fc4be51b620f933f7d71a7eff6 Apalache Let Enabled True Passed
b355a2a324ef62377da62023dd4ca4367b9d8396 Apalache Let Enabled False Passed
3cad38ed1cbd5ebbce148223c437de95dc2a8c7e Apalache Let Cross2 True Passed
9540c274709eef93d2abceee3210486c3ad0440a Apalache Let Cross2 False Passed
d5e451fa0edaeeada91799c31a11ad65c5b26e94 Apalache Let Cross3 True Passed
6a0c4e2edc1002d392e68f84bab279e1569c7515 Apalache Let Cross3 False Passed
7208bf20593c7a627e0f3aed3797d803e412dbda 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))
Let FunSet True Passed
2406b977891363b427ff170bdf0a4ceb8a256811 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))
Let FunSet False Passed
322b21d2a3fb0e99c8fc3e4793c7a8a98cf75239 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)
Let RecordSet True Passed
df5a0b923cb7a1bf20dd134df23c4859fd9dfffb 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)
Let RecordSet False Passed
587e9c2addfdda9a63def638d79020902156efc1 Apalache Let SetDiff True Passed
87bb30445d6c5d8b90a22f65680598686c232cd8 Apalache Let SetDiff False Passed
7424f24f83e7b3dbfefd52892f59d0b775efa5a7 Apalache Let SetUnion True Passed
27456c38179d0f4d767e9298a4a24c72370e9b5d Apalache Let SetUnion False Passed
28d1c4162783c360e91f48f20aee7d0ce018307f Apalache Let SetIntersect True Passed
b4934d844e731b2f23a01fceb7f1368732ea83f6 Apalache Let SetIntersect False Passed
daa68428b7b23a665da6bb6342fb194b7a092ccc Apalache Let SubsetEq True Passed
8e46b29ec711e83a6edbf6dfa04ab71a3a4a3bc3 Apalache Let SubsetEq False Passed
21cc17eaaa6d50307ffb77a0c9baa380bd98f411 Apalache Let IfCond True Passed
cc11b8cc68fbfd572a320b902332bb039e8459b9 Apalache Let IfCond False Passed
6eb47e4baf39bdfcb8366217c9fef57e4de7a70c Apalache Let IfThen True Passed
20c363dab8b8426d996609b98986b27c092276c3 Apalache Let IfThen False Passed
1223b4ead3300de738379a33313a969072323bba Apalache Let IfElse True Passed
e0fa5fbd5e6ad70b06ac3810cb290bf9aa5fc75b Apalache Let IfElse False Passed
b183581e0692fbddc2cf0c7ac68fbdf8a60ba522 Apalache Let Subset True Passed
6fdcd5cfa4abc859be5758bef01c8f0550b1a4ea Apalache Let Subset False Passed
30158e1b34b749cb2984eea202c10e8a9d2a3285 Apalache Let Domain True Passed
32aa710f43cbb68cf8c4d4b801a3cd871188a2ca Apalache Let Domain False Passed
353ca0090b880ef9d289598d8726980ab9f3b777 Apalache Let Union True Passed
3e92ee09979dbd9469cb7722bd8739a8810fa501 Apalache Let Union False Passed
72135ef59caf0753d8a44eb3b307b58980b6f1db Apalache Let Unchanged True Passed
47ac9f66298cfd3924b7044b4abbc882c5a69036 Apalache Let Unchanged False Passed
77f3ad6c299d6b891a724a1c95613da866fd27cd Apalache Let Equivalence True Passed
788e27c552c3c3fd03623686a08e83ca8a839e1c Apalache Let Equivalence False Passed
02c0a9ccdf77f987fcd2f90c3c6306b83da3b6b6 Apalache Let StringEmpty True Passed
af65d341f4d3a4f94fe61d1ce81b8ab867c7998e Apalache Let StringEmpty False Passed
5e8dc2fd86c1d44311ca97b42c247f01ba06edbc Apalache Let String True Passed
01ea371bc4395544a124e7513048dd1a8a8c97ef Apalache Let String False Passed
0427a1d7a77a11d2151c606a1e626ef0f6ab0fd8 Apalache Let SeqLen True Passed
a95541ec83ae43e3e8fae8cfe24aa1a0eb1433d2 Apalache Let SeqLen False Passed
cd500fbde7d4221191e0399329a28fb2cbc5331f Apalache Let SeqConcat True Passed
4c37adaef03b332589bac03d5b12d6d06c355958 Apalache Let SeqConcat False Passed
b25a4c8bb58e4e677155665542395ffbc924abfd Apalache Let SeqSelectSeq True Passed
4d59222795212edde98c3b0c160b744dbaba3efa Apalache Let SeqSelectSeq False Passed
0ac54ff005396a6396945f0b8f1e561bb3ebc84f Apalache Let SeqSubSeq True Passed
b9dd7c05be6c428d7a638c480a66eddd6f139848 Apalache Let SeqSubSeq False Passed
6b4d386b2ed21550ef74261fb5d57ef626512bfc 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
Let NumRange True Passed
efd1c9d27cc8e8e36cce7770cbceaf3e4044080c 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
Let NumRange False Passed
a6b577531c74e95e0018c5c50d74d8603ceceac4 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Let TlcSingletonFun True Passed
af7d1d44027366bd44b76d8a81cfc8b5df20a7ec TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Let TlcSingletonFun False Passed
da72186db927fdcac2ccd1db22592239d8ed6f7a 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]]
Let TlcExtendFun True Passed
c6eb0f281de72c4e99ca4ff5aa668ee542f9166b 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]]
Let TlcExtendFun False Passed
ba87d89e64399593674afb676df3bae293ac6aaf TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Let TlcPermuteFun True Passed
c5576fbad91e5c43ee63a63144dc1adae6002026 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Let TlcPermuteFun False Passed
761a7c68b590aa08311dd3f1e069844c4295676f TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Let TlcSortSeq True Passed
57670d48df740c3ddf7ecf895bcb96db3307e970 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Let TlcSortSeq False Passed
a8fd05265f1752a6b1be235dacbf1c854428fae8 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Let TlcEval True Passed
f69af7561d7b8ffccc368d43740eba1f159ab37a TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Let TlcEval False Passed
fd05cb04bea487348e130f4b4163afb36e6eefb6 Apalache Let BagBagToSet True Passed
f38735307a11f553857b97e7d18083111e06abe5 Apalache Let BagBagToSet False Passed
39ba3934ec648b51e02f75ba61d5e63b4300ca2e Apalache Let BagSetToBag True Passed
86cb16b16571c8a5af575272a6e1808d58e039a1 Apalache Let BagSetToBag False Passed
d492346b4558f2c0d0875e50e4ed13b7bd8e40a9 Apalache Let BagBagIn True Passed
b4147996b5263ed9c22f79372135999f3df647a5 Apalache Let BagBagIn False Passed
86ea72a9c9a07f9b21462476e880a6522d6f7d3a Apalache Let BagEmptyBag True Passed
4b4c1a90f6ef1f9e887958fe30bde84dc18351c6 Apalache Let BagEmptyBag False Passed
f0f402d524c72d2a7358609147c1786c12a28e94 Apalache Let BagAddBag True Passed
0bae3fa75bece1818bbf711094d21015064b9c18 Apalache Let BagAddBag False Passed
25caf1c7ed489bb3b6fa60fd370e47f5f9bb6bd4 Apalache Let BagBagSub True Passed
82f6d680ce095cb724bc905ebf31d315e0cb3e8c Apalache Let BagBagSub False Passed
c3830ff7be1cb535755aa840c37a65d5472ecc13 Apalache Let BagCopiesIn True Passed
2ee1fefefb74a4ec3d14ac1e498344d2a9642626 Apalache Let BagCopiesIn False Passed
d6512937b39d463ac4f2ed52ef626d0f873cdfa6 Apalache Let BagSubsetEqBag True Passed
8fd900bda06b5b937a1f3bde13998d69ad802e04 Apalache Let BagSubsetEqBag False Passed
24c0d556ba634efa0faaa6a1404abbfc49182980 Apalache Let BagBagUnion True Passed
23aea2b29a99e01f895397c296c135efeb1f65a4 Apalache Let BagBagUnion False Passed
1e39c54b38f1c210bc3101339d64b314c5d18f49 Apalache Let BagBagCardinality True Passed
51d70c1739dd3421d454d9114f48fe62c8cd2a97 Apalache Let BagBagCardinality False Passed
e2c5a6b07d0944e3bfd39caf281556ecae6e4bd1 Apalache Let BagBagOfAll True Passed
25389eee8747c2dc13ba81df46b8b8a7bde2e6ed Apalache Let BagBagOfAll False Passed
2e5845ce70d7d1bf7363bb199d7c1f0483982037 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Let BagSubBag True Passed
08324b9e1cd370be6158462910355b9144c23735 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Let BagSubBag False Passed
7c3d45eab1e94c2d036c16db930595e85d70511b 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)
Let FiniteSetsIsFiniteSet True Passed
30fdfb178b0379347bcde61197b9a857973f452b 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)
Let FiniteSetsIsFiniteSet False Passed
ec48d973c687946a1edb38041ceb21cdcc1c19ec Apalache Let FiniteSetsCardinality True Passed
a47c972f65faa012fe3e8e1f782347af3313af13 Apalache Let FiniteSetsCardinality False Passed
b2b471d147a98c7c6c4192bad1e0dff94a250d25 Apalache Let SeqHead True Passed
b7473182780da65ad1067325217ec909e3892cf5 Apalache Let SeqHead False Passed
d8c2c95ba67036fdeb382f3cf292fb2d1dcd535a Apalache Let SeqTail True Passed
999175260707bd9d1a518606385e1098e3100c31 Apalache Let SeqTail False Passed
f94782943e93881e37e996b0b2ba77c90abc2068 Apalache Let SeqAppend True Passed
73c3462e1a3d848552b95b0ef26a625e2e3a880e Apalache Let SeqAppend False Passed