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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
3231ad2afc09b3722a423023e0431198d71ab3be	Apalache	And	ConstantRank1	True	Passed	Model Under Test Equivalent Model
31effcd0fa642aa46e30fd5b38157c6da51feac8	Apalache	And	ConstantRank1	False	Passed	Model Under Test Equivalent Model
fd778bb0029d4ccf1b88318a26f5fca0d8808cf1	TLC with reduction strategy: Case Feature: /\ A /\ B == (A /\ B)	AndMultiLine	ConstantRank1	True	Passed	Model Under Test Equivalent Model
3113f710c346730e825ef53409ae8c0db727ba83	TLC with reduction strategy: Case Feature: /\ A /\ B == (A /\ B)	AndMultiLine	ConstantRank1	False	Passed	Model Under Test Equivalent Model
bfa8be86b02376bea68dc5ad6b948bdafc9007b0	Apalache	Imply	ConstantRank1	True	Passed	Model Under Test Equivalent Model
34d984f5c13db2329df820684741d4a4e561ce4f	Apalache	Imply	ConstantRank1	False	Passed	Model Under Test Equivalent Model
75a38b6ee73c21a109d286c0d491532d23280b90	Apalache	Not	ConstantRank1	True	Passed	Model Under Test Equivalent Model
104109ca0379f178e46cee4a878fa9abb4ba3a28	Apalache	Not	ConstantRank1	False	Passed	Model Under Test Equivalent Model
1c64a448aad6acd9b89836504cbb62aad65e99cb	TLC with reduction strategy: Case Feature: A \/ B == ~(~A /\ ~B)	Or	ConstantRank1	True	Passed	Model Under Test Equivalent Model
9fe0fe1f6c218b528a515ec10bb2e3f84523183f	TLC with reduction strategy: Case Feature: A \/ B == ~(~A /\ ~B)	Or	ConstantRank1	False	Passed	Model Under Test Equivalent Model
fb86b646f57cc8c29aeb19bfff82083702516592	TLC with reduction strategy: Case Feature: \/ A \/ B == (A \/ B)	OrMultiLine	ConstantRank1	True	Passed	Model Under Test Equivalent Model
ae50b32e3a27dc6683a28c202515c37e9964b61f	TLC with reduction strategy: Case Feature: \/ A \/ B == (A \/ B)	OrMultiLine	ConstantRank1	False	Passed	Model Under Test Equivalent Model
505c1b9a11ed4b846e55dc0b8cc74630901c54ce	Apalache	Boxed	ConstantRank1	True	Passed	Model Under Test Equivalent Model
eb64378a777339054d56c3738555bce24607f832	Apalache	Boxed	ConstantRank1	False	Passed	Model Under Test Equivalent Model
68534a5d56ab699737204fc5f8b0929cb3fe2055	Apalache	Eq	ConstantRank1	True	Passed	Model Under Test Equivalent Model
449b590ae2331729a8e948de9a08396c29d3920d	Apalache	Eq	ConstantRank1	False	Passed	Model Under Test Equivalent Model
157d637f923b54b41d9d4bc6bcf45103543e9ba2	Apalache	Ne	ConstantRank1	True	Passed	Model Under Test Equivalent Model
b561b1b899128f490611c0a465bc9e82e28d0751	Apalache	Ne	ConstantRank1	False	Passed	Model Under Test Equivalent Model
dce00ecb69a24037e69982e1f954582a826a964a	Apalache	Let	ConstantRank1	True	Passed	Model Under Test Equivalent Model
17db1e59351f20a5c36433bd8f91edf3ebae3e85	Apalache	Let	ConstantRank1	False	Passed	Model Under Test Equivalent Model
dbc861e1e3dd71a2945f9cd4c940741110810d51	Apalache	Set0	ConstantRank1	True	Passed	Model Under Test Equivalent Model
0d74f7c5c26b51f1e9bad6d8a52de6a337f5fc8d	Apalache	Set0	ConstantRank1	False	Passed	Model Under Test Equivalent Model
0ba96423fa072eb702ad1817f55174efb7fe5d56	Apalache	Set1	ConstantRank1	True	Passed	Model Under Test Equivalent Model
a75edd0e190fd08d5f06004e9fd1602eaee168ec	Apalache	Set1	ConstantRank1	False	Passed	Model Under Test Equivalent Model
aa52804299fa0901d8286ee4d52f297a598c47e7	Apalache	Set2	ConstantRank1	True	Passed	Model Under Test Equivalent Model
f3e1078d502edf6aa52418a550c6080df8f2578e	Apalache	Set2	ConstantRank1	False	Passed	Model Under Test Equivalent Model
44dd31d0e57a1dd42807254ca9993bdf1fd8c703	Apalache	Fun	ConstantRank1	True	Passed	Model Under Test Equivalent Model
6a851d1ea01bd5eebba7be6fb59719ab64b921b0	Apalache	Fun	ConstantRank1	False	Passed	Model Under Test Equivalent Model
9d7433eeb66bdadf90e54af6e4ac346c7cbc0a1b	Apalache	In	ConstantRank1	True	Passed	Model Under Test Equivalent Model
f912d0d3e6254c97da41e0d60aca17fee05cb7f1	Apalache	In	ConstantRank1	False	Passed	Model Under Test Equivalent Model
3f5ee8a027335a73ea5b9401941e605ed3e792ec	Apalache	NotIn	ConstantRank1	True	Passed	Model Under Test Equivalent Model
19f1709798ecc0347dc62e7d7bd7e393627afb45	Apalache	NotIn	ConstantRank1	False	Passed	Model Under Test Equivalent Model
d4c0e3d0f6cb5bc488111f25fa16607e88b54e88	Apalache	Exists	ConstantRank1	True	Passed	Model Under Test Equivalent Model
2da2951fa4e7196827aeea4494f5b3e00e58b317	Apalache	Exists	ConstantRank1	False	Passed	Model Under Test Equivalent Model
d593590aea3743c81f5e058313906c64694f4c4a	Apalache	Forall	ConstantRank1	True	Passed	Model Under Test Equivalent Model
fdd1e4f9e161e4bc03b49e12366e5f2fd1a4ca63	Apalache	Forall	ConstantRank1	False	Passed	Model Under Test Equivalent Model
aae12e511b8a937f651e97e3c625efdaf2b03693	Apalache	Choose	ConstantRank1	True	Passed	Model Under Test Equivalent Model
f76fc5758e6214f4288a34f048a233291d12f933	Apalache	Choose	ConstantRank1	False	Passed	Model Under Test Equivalent Model
2685a854371d63881a4ca0bc7715750135e3b5bc	Apalache	Record	ConstantRank1	True	Passed	Model Under Test Equivalent Model
35ff38dfcf598e85451221d56e84aa483137cd89	Apalache	Record	ConstantRank1	False	Passed	Model Under Test Equivalent Model
707225cecdc27d6006c7797de09670acefbf0b1a	Apalache	Tuple	ConstantRank1	True	Passed	Model Under Test Equivalent Model
93fe9d3a8d62b1fbe8f6a137ae4481e08c1075d0	Apalache	Tuple	ConstantRank1	False	Passed	Model Under Test Equivalent Model
b993d28cf283ab1f94475dc287b3dec57c69ae4f	Apalache	FunApp	ConstantRank1	True	Passed	Model Under Test Equivalent Model
e0e0e142cf9d32aa85f72612999a27f3106c05e2	Apalache	FunApp	ConstantRank1	False	Passed	Model Under Test Equivalent Model
c4c245352cfc7dba33845b5e8ac60928998ac8d8	Apalache	Except0	ConstantRank1	True	Passed	Model Under Test Equivalent Model
ca39a25d008f217453ba0239b8e571284d4d6bbd	Apalache	Except0	ConstantRank1	False	Passed	Model Under Test Equivalent Model
4ca3238aa4ad7ecb343c3b9dbdef6a57cb4a2b5b	Apalache	Except1Fun	ConstantRank1	True	Passed	Model Under Test Equivalent Model
65265f0b39f1c909626de1c80560e364f1b48286	Apalache	Except1Fun	ConstantRank1	False	Passed	Model Under Test Equivalent Model
58f463294fc83b3f49be953ecd14163d70c6bb72	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	ConstantRank1	True	Passed	Model Under Test Equivalent Model
163ea0382f8c70cca5058ea8e59e8101dfd7f2ff	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	ConstantRank1	False	Passed	Model Under Test Equivalent Model
589112f4a0317a41a1023a936d9c38077fd1d707	Apalache	Except1Rec	ConstantRank1	True	Passed	Model Under Test Equivalent Model
549d41ac6eb7ca954d5884e6c00fdd7c624693f6	Apalache	Except1Rec	ConstantRank1	False	Passed	Model Under Test Equivalent Model
af79c12240bd21c520c889b4a933a36ff1ba3a8c	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	ConstantRank1	True	Passed	Model Under Test Equivalent Model
f89a11650d91c57e240d7d13705cbe85c12fcad9	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	ConstantRank1	False	Passed	Model Under Test Equivalent Model
c73ab9b1ff74db60cfe179d531a35f17673882e5	Apalache	Except2Fun	ConstantRank1	True	Passed	Model Under Test Equivalent Model
37d71a712725188d07866ff6a6348184bc45ef10	Apalache	Except2Fun	ConstantRank1	False	Passed	Model Under Test Equivalent Model
b257d96f2065dfbf975635ef8d8c181b38bb3a05	Apalache	Except2FunTuple	ConstantRank1	True	Passed	Model Under Test Equivalent Model
f8a87faa4a1c965a4f0e5bcd9032c2a18144ef57	Apalache	Except2FunTuple	ConstantRank1	False	Passed	Model Under Test Equivalent Model
e7b805ee68422172316e9f876708443ae0b0d23d	Apalache	Prime	ConstantRank1	True	Passed	Model Under Test Equivalent Model
e17576b8f0ab16c7d87041e1e037360449d06326	Apalache	Prime	ConstantRank1	False	Passed	Model Under Test Equivalent Model
de16ca2634a1f91670d9ef64097debba119004b7	Apalache	NumUnaryMinus	ConstantRank1	True	Passed	Model Under Test Equivalent Model
6ed6e59d1ce50e5db1b5e9bc1763f0ec94f6a394	Apalache	NumUnaryMinus	ConstantRank1	False	Passed	Model Under Test Equivalent Model
f51b24522476fc0401c2cb5ec64cf8c31c20414a	Apalache	NumPlus	ConstantRank1	True	Passed	Model Under Test Equivalent Model
62337c4079b844b6b140e0913291de08a661c164	Apalache	NumPlus	ConstantRank1	False	Passed	Model Under Test Equivalent Model
98f863751c45ebab690fae17364307c1a749f3b7	Apalache	NumMinus	ConstantRank1	True	Passed	Model Under Test Equivalent Model
eae58c60e09307b0ef151bf5db92c798cf223fde	Apalache	NumMinus	ConstantRank1	False	Passed	Model Under Test Equivalent Model
95b76802fc4a3ab9625eda590930545a58734816	Apalache	NumMul	ConstantRank1	True	Passed	Model Under Test Equivalent Model
24bbfaa02b3a3b4cb7b2838344c1d0587c565167	Apalache	NumMul	ConstantRank1	False	Passed	Model Under Test Equivalent Model
435fff60c5f52d6638ad93b08b29dd9cb6a745a5	Apalache	NumDiv	ConstantRank1	True	Passed	Model Under Test Equivalent Model
6d54df0276fa8fcb9a34df544f4f185003b5660e	Apalache	NumDiv	ConstantRank1	False	Passed	Model Under Test Equivalent Model
471be2068d9b1238ffa4eb41a15c8273cb872498	Apalache	NumMod	ConstantRank1	True	Passed	Model Under Test Equivalent Model
114fe751455c2f477fcb2d5f4ec13739452255f6	Apalache	NumMod	ConstantRank1	False	Passed	Model Under Test Equivalent Model
530931a088af289fc2f578e937e683ae820f15d2	Apalache	NumPow	ConstantRank1	True	Passed	Model Under Test Equivalent Model
ad7e9e06329da5dd0c7322b9d1bb33484bc219f8	Apalache	NumPow	ConstantRank1	False	Passed	Model Under Test Equivalent Model
e9adbb23c429e7effb3c5bd9cd39053a9d1155aa	Apalache	NumGt	ConstantRank1	True	Passed	Model Under Test Equivalent Model
cad38f9315abce6a8e7af9cce1cddf6cfa1bdb4e	Apalache	NumGt	ConstantRank1	False	Passed	Model Under Test Equivalent Model
3b3043b806130ec4c71ca78b418d2c4ea8fd431c	Apalache	NumGe	ConstantRank1	True	Passed	Model Under Test Equivalent Model
5063748a93ada52325e2fb42510f11f862fdfa02	Apalache	NumGe	ConstantRank1	False	Passed	Model Under Test Equivalent Model
0e8f73c597b5bed3e5fef79f2266af5f42641133	Apalache	NumLt	ConstantRank1	True	Passed	Model Under Test Equivalent Model
bc3611c5d9295e520c58ea2c332a67b66b235db6	Apalache	NumLt	ConstantRank1	False	Passed	Model Under Test Equivalent Model
0772ce55e2b6eaf7836fea37571b1ebe331bb88b	Apalache	NumLe	ConstantRank1	True	Passed	Model Under Test Equivalent Model
3c7efe2a92f6443d6e331e1118505dee0dce5d54	Apalache	NumLe	ConstantRank1	False	Passed	Model Under Test Equivalent Model
28c4351c65b090353d8119226f7643764164292d	Apalache	DefFun	ConstantRank1	True	Passed	Model Under Test Equivalent Model
5276954c8a6deba4546580bbfc606ca6104c3663	Apalache	DefFun	ConstantRank1	False	Passed	Model Under Test Equivalent Model
1c0293c1b76463ee2dc9d8570a2d1c003f827906	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	ConstantRank1	True	Passed	Model Under Test Equivalent Model
a90511896f92dfda876cfe55e9bdfa1a7a4f6272	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	ConstantRank1	False	Passed	Model Under Test Equivalent Model
9952d43287b67b3c7da32cdc9fd60732013d2242	Apalache	DefFunRecursive	ConstantRank1	True	Passed	Model Under Test Equivalent Model
76d88883356026da40eef97c79716dc20db2efe2	Apalache	DefFunRecursive	ConstantRank1	False	Passed	Model Under Test Equivalent Model
ea3e1d9b1d4c6e612083a9148bc2a34287534bf4	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	ConstantRank1	True	Passed	Model Under Test Equivalent Model
66142f6879248950669978c9f726617c55e0537f	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	ConstantRank1	False	Passed	Model Under Test Equivalent Model
ca61a4d415b64e078fb8e7f039b382e464873a03	Apalache	Def0	ConstantRank1	True	Passed	Model Under Test Equivalent Model
135f9866e9f7592ece8eb70ecf5c9ff16f639ab2	Apalache	Def0	ConstantRank1	False	Passed	Model Under Test Equivalent Model
c0bbb48bb07b6567ac50b3b4de2759b75d820f4c	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	ConstantRank1	True	Passed	Model Under Test Equivalent Model
91b2183e978a9312bd726869850c404b89334a9d	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	ConstantRank1	False	Passed	Model Under Test Equivalent Model
02640d4cebd3814e5eb0c6da60c07ec17a75dc89	Apalache	Def1	ConstantRank1	True	Passed	Model Under Test Equivalent Model
95698b2ffb904d7f6f9a1d046cb8ced281d1e893	Apalache	Def1	ConstantRank1	False	Passed	Model Under Test Equivalent Model
f8789d0acee781b6d19f971714c8c3520d0117f5	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	ConstantRank1	True	Passed	Model Under Test Equivalent Model
f3ff79e9fcb329c551f3d59dbb8d72d9de4fb31c	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	ConstantRank1	False	Passed	Model Under Test Equivalent Model
4cec99b460a522eaa437a76659511157105b5e87	Apalache	Def2	ConstantRank1	True	Passed	Model Under Test Equivalent Model
61fa30f69767e6de44c58411acfa0e2607637348	Apalache	Def2	ConstantRank1	False	Passed	Model Under Test Equivalent Model
cfd5e4a34bbda2a0deda790a430887c968d2cc72	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	ConstantRank1	True	Passed	Model Under Test Equivalent Model
b75ab081f5267b4897857a8545e90c247a757e70	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	ConstantRank1	False	Passed	Model Under Test Equivalent Model
045202c75ecda7ecc6c54110937d0be3596357aa	Apalache	Def1Recursive	ConstantRank1	True	Passed	Model Under Test Equivalent Model
e9c2ac4457d1f029b9c9b3d2aac6fbe07e7fe7b0	Apalache	Def1Recursive	ConstantRank1	False	Passed	Model Under Test Equivalent Model
709d35b6464a209e966586b6bb5c86fc58c18eb1	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	ConstantRank1	True	Passed	Model Under Test Equivalent Model
bd0c3a2bf69b32f5109819f6ec6289ac35a26a66	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	ConstantRank1	False	Passed	Model Under Test Equivalent Model
161eb8e7b9a295a940a1ef7dc53569b3e469e123	Apalache	Extends	ConstantRank1	True	Passed	Model Under Test Equivalent Model
41752ce9a53801934478a858ef85513e5f0ad5b9	Apalache	Extends	ConstantRank1	False	Passed	Model Under Test Equivalent Model
27358d9780170f973dc7db97f747145e7cd18cdb	Apalache	ExtendsInDifferentFolder	ConstantRank1	True	Passed	Model Under Test Equivalent Model
fad6d146ff5b54fd80185386104f6c2f274bd78e	Apalache	ExtendsInDifferentFolder	ConstantRank1	False	Passed	Model Under Test Equivalent Model
b7817f5a80e07c45580f5f57a53e156c356251f1	Apalache	Constant	ConstantRank1	True	Passed	Model Under Test Equivalent Model
1a4a08ef829385b1c50813881464b2287c20825a	Apalache	Constant	ConstantRank1	False	Passed	Model Under Test Equivalent Model
2f0bb8c183b4afc95546b875ffc45beb24e13230	Apalache	ConstantRank1	ConstantRank1	True	Failed: TLC doesn't allow to use constant as a replacement value for another constant in CFG, even though the former constant is fully defined at this point	Model Under Test Equivalent Model
fddb90daec356c4b98a52883ae4cff1fb9b6875e	Apalache	ConstantRank1	ConstantRank1	False	Failed: TLC doesn't allow to use constant as a replacement value for another constant in CFG, even though the former constant is fully defined at this point	Model Under Test Equivalent Model
4357caa0d5ee29a7a2c02fa36f7b42fc2ce10479	Apalache	Instance	ConstantRank1	True	Passed	Model Under Test Equivalent Model
e9cc3a09fbbf3e92ddadf3d661ac89ee33de8dfb	Apalache	Instance	ConstantRank1	False	Passed	Model Under Test Equivalent Model
e6dc50404282317a692d0204a60d0de5f6f03605	Apalache	InstanceWith	ConstantRank1	True	Passed	Model Under Test Equivalent Model
552328426bd9defeb729a13d70b2dd62f93cccca	Apalache	InstanceWith	ConstantRank1	False	Passed	Model Under Test Equivalent Model
d6a65681c2282b472c6962a4267433154b333a86	Apalache	InstanceNamed	ConstantRank1	True	Passed	Model Under Test Equivalent Model
ea0dea27de63500cbd6d02e68e16633135b4b982	Apalache	InstanceNamed	ConstantRank1	False	Passed	Model Under Test Equivalent Model
70d428c652e52bc2e3f7671ec2d24ed1795c2533	Apalache	InstanceNamedWith	ConstantRank1	True	Passed	Model Under Test Equivalent Model
b446ec0e40a7c9c2ac503e6661d5a3a0bb241c36	Apalache	InstanceNamedWith	ConstantRank1	False	Passed	Model Under Test Equivalent Model
6b91705ef0c93b655d4e95ad5679757ccc0bc061	Apalache	InstanceInFolder	ConstantRank1	True	Passed	Model Under Test Equivalent Model
8a583d1737abeaac5d330f9eb39b09fe452d7035	Apalache	InstanceInFolder	ConstantRank1	False	Passed	Model Under Test Equivalent Model
c81a07108d00dcf72c4b0ada9232aece1191e9f7	Apalache	InstanceWithInFolder	ConstantRank1	True	Passed	Model Under Test Equivalent Model
6512aec031c7d955441e969387eea9f1fb7bf91f	Apalache	InstanceWithInFolder	ConstantRank1	False	Passed	Model Under Test Equivalent Model
e02369d89e9804f1db464ef3c60ceff415b2b352	Apalache	InstanceNamedInFolder	ConstantRank1	True	Passed	Model Under Test Equivalent Model
af1c4ea50693289827e9f786491d52d0db0d6cc0	Apalache	InstanceNamedInFolder	ConstantRank1	False	Passed	Model Under Test Equivalent Model
a2f56b2b9a234dbc193b00eb92d31e3480f78eb0	Apalache	InstanceNamedWithInFolder	ConstantRank1	True	Passed	Model Under Test Equivalent Model
2f7f4c38ba8144a563df474dd1f654ab466b72ac	Apalache	InstanceNamedWithInFolder	ConstantRank1	False	Passed	Model Under Test Equivalent Model
8e4b53cfc246696c75b2ced2c983d87c25e140e6	Apalache	Enabled	ConstantRank1	True	Passed	Model Under Test Equivalent Model
acfccac88ea1418444694c7c67b1d7764bf6d756	Apalache	Enabled	ConstantRank1	False	Passed	Model Under Test Equivalent Model
f0ef9fc1a561d95b941efc3372a20bd184ac92dd	Apalache	Assume	ConstantRank1	True	Passed	Model Under Test Equivalent Model
1e23a52d63459f10c3ce338256e9959884348313	Apalache	Assume	ConstantRank1	False	Passed	Model Under Test Equivalent Model
576768a0c81e57138e551a1b43bb581452514b39	Apalache	AssumeNamed	ConstantRank1	True	Passed	Model Under Test Equivalent Model
c2b7547ec7f032a3ad404bf88f685c22e67139c5	Apalache	AssumeNamed	ConstantRank1	False	Passed	Model Under Test Equivalent Model
c6ba49d5151b7cbcd08913b38dff4d4463e9b7a0	Apalache	Lambda	ConstantRank1	True	Passed	Model Under Test Equivalent Model
10c7023c1764d1225b9ce4e7607cba5d23b2a7b9	Apalache	Lambda	ConstantRank1	False	Passed	Model Under Test Equivalent Model
426ec8df2f3291a35e2800f084325489a0a16313	Apalache	Cross2	ConstantRank1	True	Passed	Model Under Test Equivalent Model
16ba6561695a5c3a0be3441f5607fefa91d623eb	Apalache	Cross2	ConstantRank1	False	Passed	Model Under Test Equivalent Model
f5912d2ab28fad87223afde195baf93fa3a1fbb7	Apalache	Cross3	ConstantRank1	True	Passed	Model Under Test Equivalent Model
7f5d33eda4ceaeaca9c5678122984d8fe0c579ef	Apalache	Cross3	ConstantRank1	False	Passed	Model Under Test Equivalent Model
e6647354c591d85f2c3d27bd09fc54b780871420	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	ConstantRank1	True	Passed	Model Under Test Equivalent Model
50ec8ce4db74154ce1c645a00e36fb32ee20c09c	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	ConstantRank1	False	Passed	Model Under Test Equivalent Model
eb3f569bd74d63bdc12c79298fc9746bd5de1cc2	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	ConstantRank1	True	Passed	Model Under Test Equivalent Model
31e942e405f2dd125facda86364b8cf83cfacdcb	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	ConstantRank1	False	Passed	Model Under Test Equivalent Model
9917d4610b835ba3c8a66257d5200a8e1824281f	Apalache	SetDiff	ConstantRank1	True	Passed	Model Under Test Equivalent Model
4848fe673ee12b63a6a63750bdf064572a9b8a9d	Apalache	SetDiff	ConstantRank1	False	Passed	Model Under Test Equivalent Model
66ada128343813c98b3682f218b5bb4eced24c87	Apalache	SetUnion	ConstantRank1	True	Passed	Model Under Test Equivalent Model
ebf5c60a1fa2548a66208c723681651f28e32ddb	Apalache	SetUnion	ConstantRank1	False	Passed	Model Under Test Equivalent Model
1d55a4696a9b14b89dd4dc5d91bc953741df4c40	Apalache	SetIntersect	ConstantRank1	True	Passed	Model Under Test Equivalent Model
b579306c0405a5861befd896af2f780353c955e4	Apalache	SetIntersect	ConstantRank1	False	Passed	Model Under Test Equivalent Model
4f3f115b7e191fff4d383f739521241ecb93b20b	Apalache	SubsetEq	ConstantRank1	True	Passed	Model Under Test Equivalent Model
46b38f55f3892bdee50e0c3e83d1f86b9a25f428	Apalache	SubsetEq	ConstantRank1	False	Passed	Model Under Test Equivalent Model
2f77d4be7050474cbc95791d0cd0d8e4f2765b5b	Apalache	IfCond	ConstantRank1	True	Passed	Model Under Test Equivalent Model
7075187047528f63e9d37ba870763791fa20fbbf	Apalache	IfCond	ConstantRank1	False	Passed	Model Under Test Equivalent Model
c915e75da2d887cab3a50e422d8b3cceb9352e62	Apalache	IfThen	ConstantRank1	True	Passed	Model Under Test Equivalent Model
d64d6c8925a5681740971be6ba969885e151f375	Apalache	IfThen	ConstantRank1	False	Passed	Model Under Test Equivalent Model
0d4972f58689683fdb3e768525e10fc2eadb659e	Apalache	IfElse	ConstantRank1	True	Passed	Model Under Test Equivalent Model
76b51c2ea74fd971faff2a3eeee2a085ff66a7f2	Apalache	IfElse	ConstantRank1	False	Passed	Model Under Test Equivalent Model
9030748409e14cbeecfe73a5eca9fee67f479c83	Apalache	Subset	ConstantRank1	True	Passed	Model Under Test Equivalent Model
5d8386d32a502b456256faa280912f49fa4d644c	Apalache	Subset	ConstantRank1	False	Passed	Model Under Test Equivalent Model
e20f92bb3074ed09fa3ecec11fb6724a5b8549c6	Apalache	Domain	ConstantRank1	True	Passed	Model Under Test Equivalent Model
f08fb8c741cec77f1c12a9f6ebefb1129c74f707	Apalache	Domain	ConstantRank1	False	Passed	Model Under Test Equivalent Model
88df97e16507577a30f057ee6f21f03648c2de91	Apalache	Union	ConstantRank1	True	Passed	Model Under Test Equivalent Model
5ceb6ff9110f6c62fbace991d63fdcb2c528c1a1	Apalache	Union	ConstantRank1	False	Passed	Model Under Test Equivalent Model
d2a117eaf1ff274903c5405299f1860fbe74a38c	Apalache	Equivalence	ConstantRank1	True	Passed	Model Under Test Equivalent Model
c475e4e78c8735a3db4af71a0437f48cf94fe097	Apalache	Equivalence	ConstantRank1	False	Passed	Model Under Test Equivalent Model
522df6a97af2e892480810e536fda5fc39bc614b	Apalache	SeqLen	ConstantRank1	True	Passed	Model Under Test Equivalent Model
064f5e85116b7c8588fbd68791e1a8ec6af79c73	Apalache	SeqLen	ConstantRank1	False	Passed	Model Under Test Equivalent Model
bf24383be16776f49e88952b304f96f09da4a754	Apalache	SeqConcat	ConstantRank1	True	Passed	Model Under Test Equivalent Model
81523d777bf197bfa56e4786b54f534c0475ac07	Apalache	SeqConcat	ConstantRank1	False	Passed	Model Under Test Equivalent Model
ef4fc1847bda9a95f8d116b4abbf4f33aadb4041	Apalache	SeqSeq	ConstantRank1	True	Passed	Model Under Test Equivalent Model
ba759383cfe2e9ac7a27d5b5ff299bd0da770679	Apalache	SeqSeq	ConstantRank1	False	Passed	Model Under Test Equivalent Model
4aee1e4fc04606ac86c1381ad1d33babb9a111f1	Apalache	SeqSelectSeq	ConstantRank1	True	Passed	Model Under Test Equivalent Model
07c01c28d0a0c198fbac50ba659d468192a5b421	Apalache	SeqSelectSeq	ConstantRank1	False	Passed	Model Under Test Equivalent Model
742ea498c1140cb1115f9b0cf39d5c9e94d72759	Apalache	SeqSubSeq	ConstantRank1	True	Passed	Model Under Test Equivalent Model
37ec52b864e13fe693dd6bb3d01db0a0a9c98ba1	Apalache	SeqSubSeq	ConstantRank1	False	Passed	Model Under Test Equivalent Model
ddea6a60307bedfeef92fe3a2a05de4468727ad7	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	ConstantRank1	True	Passed	Model Under Test Equivalent Model
d3fb3c55c925f1b000f8c3c5810e2e2a4cdba253	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	ConstantRank1	False	Passed	Model Under Test Equivalent Model
373f8e58a87e7b25cb68b3c6ad16a9f65fed152d	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	ConstantRank1	True	Passed	Model Under Test Equivalent Model
3c890897cf76ce29b9b49547adf55c10d631abe4	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	ConstantRank1	False	Passed	Model Under Test Equivalent Model
b9ed4f964dcedbbd2daebc0627bc99e62ad52d98	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	ConstantRank1	True	Passed	Model Under Test Equivalent Model
56798a72cb8df5b53570a24b60b4928573c27a12	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	ConstantRank1	False	Passed	Model Under Test Equivalent Model
fe5d70f9989255d3a7932aa2ac781937b2c3723b	TLC with reduction strategy: Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	TlcPermuteFun	ConstantRank1	True	Passed	Model Under Test Equivalent Model
1c3b56b68ac5fc968027abc9765cabd119045730	TLC with reduction strategy: Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	TlcPermuteFun	ConstantRank1	False	Passed	Model Under Test Equivalent Model
0d99b5034f11bacf165b15f29c57f8e39c04c7ba	TLC with reduction strategy: Case Feature: SortSeq(S) is reduced to equivalent sort implementation	TlcSortSeq	ConstantRank1	True	Passed	Model Under Test Equivalent Model
fc27e96385ecaa72116d262ac67dbafd80908242	TLC with reduction strategy: Case Feature: SortSeq(S) is reduced to equivalent sort implementation	TlcSortSeq	ConstantRank1	False	Passed	Model Under Test Equivalent Model
c0e84e2f701c09dfc9094d2e965398186f35599e	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	ConstantRank1	True	Passed	Model Under Test Equivalent Model
c8f2d2cbed13422fdd0239a4c28db39d552055bf	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	ConstantRank1	False	Passed	Model Under Test Equivalent Model
92391c97df39fe264f6eff68da2dd33e86cec5a4	Apalache	BagBagToSet	ConstantRank1	True	Passed	Model Under Test Equivalent Model
8ea4b58783303b2a86b3bfc1a037c53bbaa72497	Apalache	BagBagToSet	ConstantRank1	False	Passed	Model Under Test Equivalent Model
86540ae656e84f30fc8575aa85a7a41dd0243ab1	Apalache	BagSetToBag	ConstantRank1	True	Passed	Model Under Test Equivalent Model
f073e4d80676dff6110897fb55e25215af08fdde	Apalache	BagSetToBag	ConstantRank1	False	Passed	Model Under Test Equivalent Model
2ef7b2b81f4d42fc575c1f26b283d99da8896a81	Apalache	BagBagIn	ConstantRank1	True	Passed	Model Under Test Equivalent Model
090288f6f666b42ba5b2965cb24966be0944d25c	Apalache	BagBagIn	ConstantRank1	False	Passed	Model Under Test Equivalent Model
f004e36164414112bfcc5ab8bdcfa9b90cf05003	Apalache	BagAddBag	ConstantRank1	True	Passed	Model Under Test Equivalent Model
9d80187eecc0f01b1ac65a52c46af2c85529d5fa	Apalache	BagAddBag	ConstantRank1	False	Passed	Model Under Test Equivalent Model
3fece4a0ace37b4eb3193b2e93f7539d7ec2d07e	Apalache	BagBagSub	ConstantRank1	True	Passed	Model Under Test Equivalent Model
925c68a0633b94a299cf691de8d74b4e1fe192e7	Apalache	BagBagSub	ConstantRank1	False	Passed	Model Under Test Equivalent Model
f34adaa74819d3488d298413ef823ad5e8c25bf2	Apalache	BagCopiesIn	ConstantRank1	True	Passed	Model Under Test Equivalent Model
6bc2d828549a21ad2f510cc8f8a43634f43baf73	Apalache	BagCopiesIn	ConstantRank1	False	Passed	Model Under Test Equivalent Model
5c1f96b51a5d97532127d70ad1dde9df853ec5c6	Apalache	BagSubsetEqBag	ConstantRank1	True	Passed	Model Under Test Equivalent Model
0f32d90c32659aa3582615350c9c529309b88d8e	Apalache	BagSubsetEqBag	ConstantRank1	False	Passed	Model Under Test Equivalent Model
6a7476b208205241083369cbf8c1784ac683de24	Apalache	BagBagUnion	ConstantRank1	True	Passed	Model Under Test Equivalent Model
4a0de05d1eb5e9045aea4ddd18ae9a877bfd6f98	Apalache	BagBagUnion	ConstantRank1	False	Passed	Model Under Test Equivalent Model
e7bf89ec680ff044d3bc81bd58a7cc6622a6db5a	Apalache	BagBagCardinality	ConstantRank1	True	Passed	Model Under Test Equivalent Model
e05612c8e0bf6e0539008f67fd48a19679dd17b8	Apalache	BagBagCardinality	ConstantRank1	False	Passed	Model Under Test Equivalent Model
2bb3769ec540c5760aa521e8cefd1e7deee5d72f	Apalache	BagBagOfAll	ConstantRank1	True	Passed	Model Under Test Equivalent Model
af2dd815ef9c859883679a574376b8706f7bc7de	Apalache	BagBagOfAll	ConstantRank1	False	Passed	Model Under Test Equivalent Model
37a2f36ae494b96c25f6184cca454e65c12d69ad	TLC with reduction strategy: Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation	BagSubBag	ConstantRank1	True	Passed	Model Under Test Equivalent Model
ad60489f1a2097a15b633665d79950731f3a96a4	TLC with reduction strategy: Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation	BagSubBag	ConstantRank1	False	Passed	Model Under Test Equivalent Model
147e294cef7b7413c3665132b5073f9857355f61	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	ConstantRank1	True	Passed	Model Under Test Equivalent Model
3cf7ff7e2015b3a87b3ef50a8781e00abfe213be	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	ConstantRank1	False	Passed	Model Under Test Equivalent Model
afb9703ab9937044f16eb1089d5e0832230a75b8	Apalache	FiniteSetsCardinality	ConstantRank1	True	Passed	Model Under Test Equivalent Model
2fdd0cfda9c5e9b60b2d581586fa5db9b629b64a	Apalache	FiniteSetsCardinality	ConstantRank1	False	Passed	Model Under Test Equivalent Model
ddce54f39124250621b1b6e6cebb35b47d0b8c5b	Apalache	SeqHead	ConstantRank1	True	Passed	Model Under Test Equivalent Model
26dd5f9817be25dbde29d358ef2c2fd48491217d	Apalache	SeqHead	ConstantRank1	False	Passed	Model Under Test Equivalent Model
cb9823860af88cd0027548e51f951bb902adee0a	Apalache	SeqTail	ConstantRank1	True	Passed	Model Under Test Equivalent Model
7fc6e199618306db5ff47a17f833e27cec5c11b8	Apalache	SeqTail	ConstantRank1	False	Passed	Model Under Test Equivalent Model
2d2bfd294f2b45d8c47f071cc341dc124569489f	Apalache	SeqAppend	ConstantRank1	True	Passed	Model Under Test Equivalent Model
2c3197b8ad0ff146732aebbabe0f0a66ad938001	Apalache	SeqAppend	ConstantRank1	False	Passed	Model Under Test Equivalent Model

Index

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