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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
63d235d9596878d6a664965222af25970b5f0797	Apalache	And	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
a5e33b2af42ae573ee872ad67611aa223645eb5c	Apalache	And	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
98d5fa954bcc5d0ba01b0fccff2441745db4c14c	TLC with reduction strategy: Case Feature: /\ A /\ B == (A /\ B)	AndMultiLine	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
92ac3ecfc3215e3198b23f003deccc198620c25d	TLC with reduction strategy: Case Feature: /\ A /\ B == (A /\ B)	AndMultiLine	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
2017c5b27f351420d445264cd7340f0342db884f	Apalache	Imply	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
649ff2715af43c7b73865f15ebe83ad616fc0d09	Apalache	Imply	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
d9f40d89306f0b401c7dfb073614c768d84736b2	Apalache	Not	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
25bed91170bb8e22d14503671762d2210788d52c	Apalache	Not	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
505ac40b6fe79bc9a7f8be0ad91d95c9f4185c49	TLC with reduction strategy: Case Feature: A \/ B == ~(~A /\ ~B)	Or	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
5941323127f8972cee49d1aa6c3f8b3ddc624d0c	TLC with reduction strategy: Case Feature: A \/ B == ~(~A /\ ~B)	Or	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
010e316c9edc5110a46ac4898b611b09128ba376	TLC with reduction strategy: Case Feature: \/ A \/ B == (A \/ B)	OrMultiLine	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
e553fdd38fc601efa544a490e95a5b4c93f81950	TLC with reduction strategy: Case Feature: \/ A \/ B == (A \/ B)	OrMultiLine	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
f0a8f8e4487b2e503a1bff1e09a82e1736d7e47d	Apalache	AndProp	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
c1cc2ea517ef45745c0c0699032bf0d0aa9f4597	Apalache	AndProp	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
93f3599377817c421746587fd54425340cff6b49	Apalache	Boxed	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
64e4fe86146bf3ad4deaa5caf0ee1099a7f85ea1	Apalache	Boxed	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
da7f556c51ff2432d0b3f8ecb58780e3d89b1572	Apalache	Eq	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
a35d292ab1fd9faa51b60bb174251bf9dae5ca17	Apalache	Eq	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
16f051cd173249423e0c499246f7b3c1548b7efe	Apalache	Ne	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
d4c52604fa0abccfc4d9eaf438fa40831791f564	Apalache	Ne	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
57bd81198ac39a0c5391c7266980b8c7566a4f5a	Apalache	Let	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
2e2df8211d8f37f7867d73d10019e06abec87c47	Apalache	Let	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
e0c1479c4d58b7a9420340b2b50a379b6c15393b	Apalache	Set0	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
c60df8df490b01e1ed447d8d288325960112d9f3	Apalache	Set0	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
c7785e7f66b6d58b65268c88659ca1e3fb0f5ed9	Apalache	Set1	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
c97119c56f360a7f6b88665d4977d70f4c67971c	Apalache	Set1	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
fef76ae84dc336b8aa312a6a8f9d39e435ccdaa5	Apalache	Set2	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
c669b4f3771be9a1364d754733970021d50a613b	Apalache	Set2	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
68412d933ec00a2f4e6ba684dce43a7a989c6e51	Apalache	Fun	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
62f59e01d6071be7497739f41ca679a200093cfb	Apalache	Fun	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
d70d074e58d09cec4676496166cacba56425be1e	Apalache	In	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
c6e9b487bef17cf38cf3ce57a3b878ce46380aaa	Apalache	In	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
f044ff10f0ae822e0e178fa4c29055dd81d95b49	Apalache	NotIn	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
89985e78e3be1a64e292bd5cee91375bea4f695d	Apalache	NotIn	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
9e504f622b038246b38b1e38c01992ee9a66dff8	Apalache	Exists	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
7c8a91da24e6d9432bdeb0a147b1cd15247ac9b7	Apalache	Exists	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
efd1e2dea51866d3bc9206387ea3f1b81938f0a5	Apalache	Forall	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
eb520450982ccb1d2220d533a078e362d903352e	Apalache	Forall	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
b45fd361cc284f10cc1b45ea7a1e68bd7dceed65	Apalache	Choose	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
f93dc26fe3564dd853c521a503b762ee0f57ec87	Apalache	Choose	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
193325e1678f972e1bedc850c3bb8f47f289de4b	Apalache	Record	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
21666dfeff8807d48b4cb56c6d28a5d0d452ba13	Apalache	Record	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
5e730473755d622e9fdc833f101067f5349988a0	Apalache	Tuple	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
789e04bf94c0aa45e9540e6379346fd492fade5f	Apalache	Tuple	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
66abd7a73566bab758fe1f5dc90c9563f4bd0886	Apalache	FunApp	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
f717adf41897f78dfac56f8fa50499ec418e057e	Apalache	FunApp	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
8bd4dd1ee6f024f7d000a76f95fbeb325934a193	Apalache	Except0	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
e711ba7d41b60f3596622f14b936b4f6532d3763	Apalache	Except0	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
fce4c0e13b916373f5a19ceb99c1168e27ba0be7	Apalache	Except1Fun	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
d0251913d9d823f682b078916ce0027296a7b8e0	Apalache	Except1Fun	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
31c941aee76dc57e254b48a85fabd59df35d2449	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
d7a8bd2f06d29845ebeb14e4190ffa559f2e11e0	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
05b29b170dc36e96b3cc6178bc2dce9d26b63ef5	Apalache	Except1Rec	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
b89be97e1820fd139ffa2f8ca15f0b1812ad6c9d	Apalache	Except1Rec	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
9622b9ca48c95154e909d896da669cd26c2a49fc	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
4f1f80beb412601b44fe415b6e795b301f3fd6e8	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
97bffc9fc03ff8b32c8390d7cb6f0f37b1ae7d1a	Apalache	Except2Fun	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
8eae7059920ae3fb05654a91b9f54bcef7606ff0	Apalache	Except2Fun	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
7d2d5e0b215e37a37e2ca40717a0385c3c2325d8	Apalache	Except2FunTuple	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
e5cc1a9b4633424d8718a60ab4110b495a0c18d2	Apalache	Except2FunTuple	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
65e5984f19f42dff6226280be5ff6f83ea9657bf	Apalache	Prime	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
1f81389fe5a13287045d6047a973f05c15773517	Apalache	Prime	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
03a2d108240815b4a0647c9ac7fd25ab513cd1f0	Apalache	NumUnaryMinus	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
8562eb6e065ec64fe36f2c7c17cd101639460fae	Apalache	NumUnaryMinus	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
369fd0b485c921c9815eab8ff0862ebb17308136	Apalache	NumPlus	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
a2c6873d7fcfa24322083847e282901bb8f942a8	Apalache	NumPlus	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
80c4d6d98a288ea5822bf6398e74c5c7b205e36b	Apalache	NumMinus	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
bebeb9177f1d9b563c1abb970814ffd053f18f23	Apalache	NumMinus	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
2c539dcd0b7488b852e06cf47805a005d8854165	Apalache	NumMul	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
5733886995c7a23623d430d6b9cafc9b9325b37f	Apalache	NumMul	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
aa353cc48266054323fe06d3c9734552cf4ce179	Apalache	NumDiv	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
bda11be87461adf28958e29cb06e3920347805dd	Apalache	NumDiv	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
9b6d157a6d0d95d34eb94436c42bcd6cf64a9c24	Apalache	NumMod	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
63f61d12530d37ef20572918861a88d599a59a78	Apalache	NumMod	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
22019640ff8010c5a0ad8702d01bf7bcbbec4d9e	Apalache	NumPow	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
2cb210cdf18727abbd127a74db1b16e4ef1f6684	Apalache	NumPow	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
ad5741f4f55ae185baf03e0ff84436865c197cd1	Apalache	NumGt	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
65ca1bdd5fc5b6f244c572e4b8379c5be27c1abe	Apalache	NumGt	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
9832bef57d7479068b84888d378414806da46408	Apalache	NumGe	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
476604d6b4c386986877d4960c860dedff8b2044	Apalache	NumGe	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
aef07d58af7249c78d8ae5ef4611a6bfdfd29d4d	Apalache	NumLt	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
76ca089ced6e13fef70e710548e81a1227cdf5e4	Apalache	NumLt	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
8dff929b3a45c2941e9a8d75bc81332cbb594737	Apalache	NumLe	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
279170c2307021fc0cec216880c338ef4da17134	Apalache	NumLe	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
2ab53761bf6bfb973b8799633e4054d3ea2c7d28	Apalache	DefFun	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
13359dfbc8f03b921859081d0c0c6375e3072104	Apalache	DefFun	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
bf33b92972fedb4ba0886f9727d2e92d449d7ed6	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
adf35c44a462737e9fb525c73fc689f58ef65157	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
bc44b3c39b4444c162ad88b7740fd2045887caf9	Apalache	DefFunRecursive	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
5b0ba5b1f5f74792452662b479592f0e83126e2f	Apalache	DefFunRecursive	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
08491c511895c87a43c331b323e34d503de23f52	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
76660961b16756c460fc92173acc79cf415143af	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
81375a52af06174e20a2e2f8ebedaeef6f8fcf30	Apalache	Def0	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
385684b6b16e6460b1cc90bec9bd6049da4531f4	Apalache	Def0	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
d603e15c374a260ab248ee129bc3c0c8167e0243	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
5f4cd1625ade66e51c06f1ea54d05d1ac09bc6ed	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
0aff824aa2aee5fd009f6fac03352dd4f53c8373	Apalache	Def1	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
61ba432282000c2daf56f0cc4992593da25138e0	Apalache	Def1	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
03003163005233277a9e8fc77761817cd34b28cb	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
1b5468dcfb66a8a876951f243f6da7f95b54953f	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
5752d1922be794e90cbe9dd03d7e141091624faa	Apalache	Def2	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
8d20b08a1cebee29ae264362539cc57de33244f9	Apalache	Def2	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
7fe7499713f05651352b11f23b125ac1f83d5f30	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
ea84216f9b958aef254dd3a5106a86f139e272da	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
21435816a521e597688c667db0e27beca0f0f89d	Apalache	Def1Recursive	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
fc3a9f17c9d4345e1c96a77ca039e478495b7dff	Apalache	Def1Recursive	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
4ae1c7c0cddf7a812780eb931ce8da6d1d38851f	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
c0933bb39ac31352bda6efd7e3554df53c1c4073	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
a5b48543d9fcb16c5c791d4b917f58b87549efab	Apalache	Extends	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
42ff7457cd658b73ad7f0f63ca2ffb0232c13483	Apalache	Extends	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
9835a259ce8415a9148cff24fe16b5c3859a5fdc	Apalache	ExtendsInDifferentFolder	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
6f894d604f4e35cfb59001add4536613c75d2907	Apalache	ExtendsInDifferentFolder	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
914d17705aa68d46c6653ccb6481862b9ebcec11	Apalache	Variable	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
f2bf05a841ffa0a17477c34b60e289e3ca58b38a	Apalache	Variable	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
8da1acea010a901d502893053e7297a4da2daa1d	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
9d9b701bc5a3a695720cf3b7a88ddd93ad9e6470	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
31642d818309d90c680641ca334c0c98da35efd6	Apalache	Constant	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
0569c8b1aa151bfe812a1d947bb5629e27914b81	Apalache	Constant	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
6f85350bc9046961504b7f66673fc1ed709ca0c1	Apalache	ConstantRank1	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
936ae4b7e449ea5b036bbf8845a88a6a930e9a09	Apalache	ConstantRank1	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
7ac7fba669bbf90bf6e094c4ad664092a9e42071	Apalache	Instance	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
91ecd9f9943069818924e453c493280a18f97256	Apalache	Instance	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
5571841034013bdbc44a109c499a7a4683e34373	Apalache	InstanceWith	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
84a0f26986e7a0b6524ac03798f96732f469dc46	Apalache	InstanceWith	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
007f802538e357fc92acb09d1292a144ccdab32d	Apalache	InstanceNamed	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
496355a495f4f3e7688d02ddf25febc1cefb871d	Apalache	InstanceNamed	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
7d9d3f928ab6b0bde7dde996a828c77a7b9cacf5	Apalache	InstanceNamedWith	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
f32da3ef926e6848a5fbc0538f81072a41802d25	Apalache	InstanceNamedWith	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
c33b7adb2d2800680b9882b8be2381f562078838	Apalache	InstanceInFolder	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
f7bed57b7c855c3f1b0f325ba8718965e49a1acc	Apalache	InstanceInFolder	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
84323cf5e2935f2817554cf725a654ba9eafaf92	Apalache	InstanceWithInFolder	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
3892035bd67a02e0d4d90980c1637058b66ec583	Apalache	InstanceWithInFolder	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
ebd0db1849bcb7413c4a18fc785b4e6fb92d9c17	Apalache	InstanceNamedInFolder	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
b5c5f87895c44027d0344a7a1b616911aef98416	Apalache	InstanceNamedInFolder	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
c9bc752ca3d1974bdc33dece5408cb6477d18a76	Apalache	InstanceNamedWithInFolder	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
a604f4c1346de3438d132df1e69c82353f2b2df1	Apalache	InstanceNamedWithInFolder	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
18fce6f34fe5a4a5505f7d56b0faabbf32048bea	Apalache	Enabled	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
02d6b13cd73c047f63b6d2a7eb40acd5685ffacd	Apalache	Enabled	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
041308f3b634d781f8ffebd1fdec336bcfa51fff	Apalache	Assume	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
6cb00451704e1800383c7a8245c173544b98ce7e	Apalache	Assume	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
71679645f67dd0495bdfe3a09581dbb7d0301f4c	Apalache	AssumeNamed	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
a2312f54618e614613d1b5ba965ccc306e45fd43	Apalache	AssumeNamed	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
25cc50f9c786a5183f518bbc48ca74a572856bf5	Apalache	Lambda	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
be995b813cb36b978dd658f491ea68b931cbce48	Apalache	Lambda	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
237c7df2e8ed68c7561a9b254f931ec4d893a98e	Apalache	Cross2	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
ea8f087ca656c8fe2b6d94d7a5537265b748b0dd	Apalache	Cross2	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
788f400514986243f529880387f4b453b8dfd7b9	Apalache	Cross3	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
5084941c75a0b45a8b42f52711aa658281059163	Apalache	Cross3	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
99c2b64836f3020f1ae195c0cc13e4f2d3737464	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	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
51e8c8ec78aa9a32e62a43862d05031b0ffda44b	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	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
8f43a56eb1bf8ec1a2c49fa51d141894844cfef3	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	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
c62ccbd29d878efd9662a1605da76645ee9f984d	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	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
e9e8b5d07ebfdaf22ff8e34ec08af72ffbf84bb4	Apalache	SetDiff	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
c40696204950162cef22ded7825de24387ecebf7	Apalache	SetDiff	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
dc6ab01420ca7bfa24abd29dd84d1f2831a9f1e8	Apalache	SetUnion	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
9c72909226a7872b0e7261ef8e00497fa62ade8a	Apalache	SetUnion	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
e1fe29fb1e2cf8d051f92bf0cace68143ff0b8e8	Apalache	SetIntersect	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
066a3eefb06dcdfdb2fc10631324a2be9fb55cbf	Apalache	SetIntersect	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
19630b1935c8108e87757da07e3de21cd4439e7c	Apalache	SubsetEq	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
b4a0f257cbfa9a3a90f46599fffa299ae749a816	Apalache	SubsetEq	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
6e1f2b564d41d04db6c8cf48c54a1bc52cc5d8a4	Apalache	IfCond	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
10bf34aecdc82347ec9a2dc7969ee8fdddf14316	Apalache	IfCond	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
008eecb34ccfbae1ca1a7ad15cc52a4af8a64a1d	Apalache	IfThen	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
bea960e7e4a5b82c5ab167aef9d59dcb0583b86c	Apalache	IfThen	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
c4168525b0b93c8327f7075916ec2e856e9cb078	Apalache	IfElse	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
1859785d3914520f1a6d87b4dd647b790ff19eab	Apalache	IfElse	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
d92a93b17484960bf9f05df55d3ca20b107c9224	Apalache	Subset	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
17913933a22d345fab2e713d9f1cae987afb36d8	Apalache	Subset	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
09c9de832d8e66c7f9bc1908d3671fed2071efc4	Apalache	Domain	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
008951f1c9701bbc8eacc89e756d3a8ca5963b09	Apalache	Domain	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
af7d7eba1a86ac885d9427ff57b1d38378b44b7e	Apalache	Union	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
660d8e5f25b6fa14b426c4fd6529aa29dbc01960	Apalache	Union	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
ab1008325129beea78743bc02d00a58aa0bbd33b	Apalache	Unchanged	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
59f17fc9546dab1303a2265f6d295b1f3456c428	Apalache	Unchanged	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
5e17ecfb317a8b548afd81792ec5527b33da9700	Apalache	Equivalence	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
8b7bd9c894c5ff1c1a2801c462d6b1c616cec133	Apalache	Equivalence	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
162567b7045e637eac0be80b9e47f51de013b01c	Apalache	SeqLen	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
612cd371054bb5ac0ab6c89b2728b225c03c20cf	Apalache	SeqLen	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
e5b7180de3a659419f2c4a8f24a4c3ab134843e1	Apalache	SeqConcat	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
ae3a19f5ae78f3986ae6952c835fb79c7338e0a9	Apalache	SeqConcat	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
1e9e6e8268376503aedca3ade781c599b3b9566e	Apalache	SeqSeq	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
7d0992f3e8a14984573a1528500f6b2f7bb41c0b	Apalache	SeqSeq	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
5e4a024797570162475e88188307b54a3a53b219	Apalache	SeqSelectSeq	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
be32485802cff28f034908c455a06a0b92cef617	Apalache	SeqSelectSeq	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
d445b48016754746555a13000849fd247c49dcfc	Apalache	SeqSubSeq	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
beb660ba3506f4b78ad04e02674a72f1b375b968	Apalache	SeqSubSeq	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
ad7b2e682410f5cabebb8576fdb6b3013decb91c	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	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
db2b4e3d567eca100da1300ef076f34e494877bc	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	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
68450499ad4ec583a8f008025b48b8bd9961751f	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
c2303bde107871a87dd1eae61601bbdafe054413	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
dd7faffaccd864d07ec32b9df637d77c092d5e65	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	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
2431aaa544d13e12b41a47d9d3400ec1b0562bbe	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	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
878a7f22fa3e12d025fe5cf98bfc87c0ced4d06e	TLC with reduction strategy: Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	TlcPermuteFun	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
5ef6d249ae92fa89b45c002ad6eb373e131013e4	TLC with reduction strategy: Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	TlcPermuteFun	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
77bfc4a19b981d3cc57c909ec8869ac642ae0ee4	TLC with reduction strategy: Case Feature: SortSeq(S) is reduced to equivalent sort implementation	TlcSortSeq	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
050e79caad969877350c09b18ffb7cf5ca54f070	TLC with reduction strategy: Case Feature: SortSeq(S) is reduced to equivalent sort implementation	TlcSortSeq	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
c6da8dcc81c1eb72a4c2d23c5cf516fa19fc5d83	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
86392c24a6bf1ddd30ad673d89374220f54d63b4	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
9d620ca611fbbfa2ebf1bb148f983c310f9722be	Apalache	BagBagToSet	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
8548a016dd00ab15b286c33c3fba057d94200c5d	Apalache	BagBagToSet	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
0f5cdba97577b0a9ca8693a2af73181ef3d8c2fb	Apalache	BagSetToBag	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
a2278b225b115124dd10f5499cd5c07e992bafde	Apalache	BagSetToBag	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
8ab1fc8f12fa42dd48db16088ea002566214c67f	Apalache	BagBagIn	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
24dad216dcdab88b6120f6323567a31683d4a7ef	Apalache	BagBagIn	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
87ab3d6cfbe6e7aaa3731dcb7968e2048cd5ccf8	Apalache	BagAddBag	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
451447df503c08ec96dc1b6dbf346a14ecfb7716	Apalache	BagAddBag	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
3ae226248b05d4df8a77cdc28255870a8028baa2	Apalache	BagBagSub	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
b1860fbcd6204091eaefaa7c48d533fef32dbc61	Apalache	BagBagSub	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
124df8786197a189015c3ec21d27ef08c07b6c89	Apalache	BagCopiesIn	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
4d0afcf0ccd5f3770dae3f26a79123ed1fefdd94	Apalache	BagCopiesIn	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
dfa4a6137a8984730c6b4060fd632df0fc2a16cf	Apalache	BagSubsetEqBag	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
e6f9ef1702ab418e67a362ca3d5463c4cc0a3566	Apalache	BagSubsetEqBag	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
9912352cf389eac2e00b0700bffaf7af7abe2ac9	Apalache	BagBagUnion	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
305e7996d622ff178fd7a5f3620b752d354b8056	Apalache	BagBagUnion	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
88af90f592470eaee1c022b12a46453a13122734	Apalache	BagBagCardinality	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
5eda41bcb964b1e25eb63c7b54c0d398948be86b	Apalache	BagBagCardinality	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
6202a5cd567d5f40f352e901230411a4fd788ce1	Apalache	BagBagOfAll	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
479cf5af85e01f5204e72dd71ab7950fcf659b98	Apalache	BagBagOfAll	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
bc80ea5de7d69d69d3b8f596e2c3cb8a4e2a96c9	TLC with reduction strategy: Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation	BagSubBag	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
42bfd393cb6c5291aa112af68a40bc36dacb714f	TLC with reduction strategy: Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation	BagSubBag	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
73eeec7a14be76b78983bdaae6439272fcd9b6b8	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	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
bc842f9549d7b407990449d71e2696294aa304ea	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	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
8e0fde4cc78a6e3e6cae2607c64a129b146d32f8	Apalache	FiniteSetsCardinality	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
4c2484c4649848443df8b5cc90eb9c1f8eebfab1	Apalache	FiniteSetsCardinality	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
10ef17cf0d45ba39248c49339e98474caf9d4cdf	Apalache	SeqHead	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
e98885d78b2ba4c7843e7b34708b0ee2b6bd15b9	Apalache	SeqHead	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
48f38e3084d918e172a6a2186bf04b7e173414b7	Apalache	SeqTail	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
736d0e6f79b2352121c1cb0021556e2932c13fce	Apalache	SeqTail	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
ea0fd72deb4ddecc939a299e8644e9cc94876e66	Apalache	SeqAppend	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
51d1851e382e88563a07bf6f745fa28705a39c5d	Apalache	SeqAppend	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model

Index

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