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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
6c03fd74eda3644f1387d6e451e5eb4aa273a580	Apalache	SeqAppend	BoolTrue	True	Passed	Model Under Test Equivalent Model
8d05eb06aa5d6aa6614fe56213eeb611a6175fd3	Apalache	SeqAppend	BoolTrue	False	Passed	Model Under Test Equivalent Model
a1ae4630261a6a4493e3f00e6516c7c56333ebc2	Apalache	SeqAppend	BoolFalse	True	Passed	Model Under Test Equivalent Model
efc523748bdf037cb5f3d4c2de2a0fb0112dd716	Apalache	SeqAppend	BoolFalse	False	Passed	Model Under Test Equivalent Model
ffee98d15801fe6ea76b3f397beaf24f0821469a	Apalache	SeqAppend	BoolSet	True	Passed	Model Under Test Equivalent Model
119bc071c28362b7161f726c39c721cde24b9f86	Apalache	SeqAppend	BoolSet	False	Passed	Model Under Test Equivalent Model
db560338d0005461bfe8bfd07306c75891a3eff5	Apalache	SeqAppend	And	True	Passed	Model Under Test Equivalent Model
b9c273c9df503d549bf1bbad11a0fe122a358cd1	Apalache	SeqAppend	And	False	Passed	Model Under Test Equivalent Model
0fe0dea1c994a033b09092a2ba2e845f0a69b9ec	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	SeqAppend	AndMultiLine	True	Passed	Model Under Test Equivalent Model
7059aaf7cb884aea6a86bf5c1f7c9a5e85429897	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	SeqAppend	AndMultiLine	False	Passed	Model Under Test Equivalent Model
62996240545b8c16474eb2ae0912f76227db9658	Apalache	SeqAppend	Imply	True	Passed	Model Under Test Equivalent Model
6692df160cc3bdeec80ed6a6caee9b18ea5a2064	Apalache	SeqAppend	Imply	False	Passed	Model Under Test Equivalent Model
98a41c14095285515cab89e526fc2222d5ed48cb	Apalache	SeqAppend	Not	True	Passed	Model Under Test Equivalent Model
d58248553bd09c8311a795b6dd061ab544f97d8a	Apalache	SeqAppend	Not	False	Passed	Model Under Test Equivalent Model
37bbb8979dd034391bd301e9b362f81020469ff4	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	SeqAppend	Or	True	Passed	Model Under Test Equivalent Model
31eeb45e923e58469ad04563c8c235f75a2d8862	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	SeqAppend	Or	False	Passed	Model Under Test Equivalent Model
374d6a6fb90027416d262ce7766d497f2150b067	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	SeqAppend	OrMultiLine	True	Passed	Model Under Test Equivalent Model
2a4b0d606bf170293f25fda9769731d6b494a635	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	SeqAppend	OrMultiLine	False	Passed	Model Under Test Equivalent Model
c3df1ae6598c04fbec8a9bd21beaa145f076c05e	Apalache	SeqAppend	Eq	True	Passed	Model Under Test Equivalent Model
f94ea88219bcce8465653eb29f41f9f8eeeb7352	Apalache	SeqAppend	Eq	False	Passed	Model Under Test Equivalent Model
1be8b83ee8105b0fa54626c5f947ad8265f8c25b	Apalache	SeqAppend	Ne	True	Passed	Model Under Test Equivalent Model
5d1f632604f40d07a6e21a55fc70ed71f0fc706a	Apalache	SeqAppend	Ne	False	Passed	Model Under Test Equivalent Model
4c638b305246399b6685937096a2daf0356b7e3c	Apalache	SeqAppend	Let	True	Passed	Model Under Test Equivalent Model
14b7ca60954ee2909acea0460c85053364025fe3	Apalache	SeqAppend	Let	False	Passed	Model Under Test Equivalent Model
9fb43ef3205087d11e89e9fd7ca9f23d20eae790	Apalache	SeqAppend	SetEmpty	True	Passed	Model Under Test Equivalent Model
e02b7924c9676f417c8569e182b9a25d8c152734	Apalache	SeqAppend	SetEmpty	False	Passed	Model Under Test Equivalent Model
2c4de9576975e5081fd6297a0a249aba8346f5af	Apalache	SeqAppend	Set0	True	Passed	Model Under Test Equivalent Model
4cf1f6bf20572f3b913b17621a91abf0f448ea7d	Apalache	SeqAppend	Set0	False	Passed	Model Under Test Equivalent Model
f68ff2552b826fac9b2f6ffe0b351e70e3ff5115	Apalache	SeqAppend	Set1	True	Passed	Model Under Test Equivalent Model
f20609d54b89e8746a992bbbfbada216030f6802	Apalache	SeqAppend	Set1	False	Passed	Model Under Test Equivalent Model
1eca01673111ba69ad04be7cbfa479283824cba7	Apalache	SeqAppend	Set2	True	Passed	Model Under Test Equivalent Model
b61108026eb379106586099c855d0a2eb5b42063	Apalache	SeqAppend	Set2	False	Passed	Model Under Test Equivalent Model
eca5f88abba6e2ccc90eb2eff7f9d013afe572f3	Apalache	SeqAppend	Fun	True	Passed	Model Under Test Equivalent Model
9c9c20ef464ee62b845889b691c7a044e05b991d	Apalache	SeqAppend	Fun	False	Passed	Model Under Test Equivalent Model
690cd76285ff0ebed61765d49a7f958f35077805	Apalache	SeqAppend	In	True	Passed	Model Under Test Equivalent Model
800a857faf98ac3d3f7aec8b8727ea07108e50e4	Apalache	SeqAppend	In	False	Passed	Model Under Test Equivalent Model
0a9086f1bd57722291e407595bfec052385f1bc9	Apalache	SeqAppend	NotIn	True	Passed	Model Under Test Equivalent Model
7899d5845031f1eef0d093bf13c8d2fad3a65275	Apalache	SeqAppend	NotIn	False	Passed	Model Under Test Equivalent Model
0a82954757914548879b9ea29ffc9c7b89614ab7	Apalache	SeqAppend	Exists	True	Passed	Model Under Test Equivalent Model
02c7a8eb9ec491c30096321f455d020a53cde63a	Apalache	SeqAppend	Exists	False	Passed	Model Under Test Equivalent Model
f9aab2f41dc3be4baacac53e91b1133ccd919c12	Apalache	SeqAppend	Forall	True	Passed	Model Under Test Equivalent Model
5860b4311c023aa2a2a167f090048d9ceaca408b	Apalache	SeqAppend	Forall	False	Passed	Model Under Test Equivalent Model
ba93ae4d12617289051428cb22e4c71339a67ab5	Apalache	SeqAppend	Choose	True	Passed	Model Under Test Equivalent Model
0dbbc3649d41569b746d22e28bf71da4983c87e4	Apalache	SeqAppend	Choose	False	Passed	Model Under Test Equivalent Model
e69d54c323ace67151e5990d06dbc387fa020e12	Apalache	SeqAppend	Record	True	Passed	Model Under Test Equivalent Model
758a8777d3d76f59165ff640187ab7323ee52cd7	Apalache	SeqAppend	Record	False	Passed	Model Under Test Equivalent Model
3783af571c202616f9b7ffda397c7f33f2ae41f8	Apalache	SeqAppend	Tuple	True	Passed	Model Under Test Equivalent Model
a2bdafb3745e092cc99a0be3cb317b10c35b6ced	Apalache	SeqAppend	Tuple	False	Passed	Model Under Test Equivalent Model
0f13194c40f0e06801e17e8ecc47eb526fd5731c	Apalache	SeqAppend	TupleEmpty	True	Passed	Model Under Test Equivalent Model
d5d1fff76a91fb83ac119f7f009df62e450ac195	Apalache	SeqAppend	TupleEmpty	False	Passed	Model Under Test Equivalent Model
c99aaf97a4af299b3048a49875271f6ab749fc92	Apalache	SeqAppend	FunApp	True	Passed	Model Under Test Equivalent Model
50e1a313ba783a27967dc405c4e8923936ac99b2	Apalache	SeqAppend	FunApp	False	Passed	Model Under Test Equivalent Model
bfc40f78f510ddeee00631190f10ac576d4f59a9	Apalache	SeqAppend	Prime	True	Passed	Model Under Test Equivalent Model
b3e3725733af50a0b86245c90caefb509b1562c5	Apalache	SeqAppend	Prime	False	Passed	Model Under Test Equivalent Model
925d92730b3d932a62ec1df9037b9ef18421ff0e	Apalache	SeqAppend	NumZero	True	Passed	Model Under Test Equivalent Model
67b272b6583643db63ad7146ce3a64cf765a23bd	Apalache	SeqAppend	NumZero	False	Passed	Model Under Test Equivalent Model
6ff7b70661956e818391eff7021e3fd72ae1ca20	Apalache	SeqAppend	NumOne	True	Passed	Model Under Test Equivalent Model
b9ba5078f805db5b93288aa059b5b37b47aa3087	Apalache	SeqAppend	NumOne	False	Passed	Model Under Test Equivalent Model
fa79cedd33c71f0b5ba2bf4c21d20f31ba3752d4	Apalache	SeqAppend	NumMaxInt	True	Passed	Model Under Test Equivalent Model
8edee398cfb456cc119637fcdb24cafbc5518d65	Apalache	SeqAppend	NumMaxInt	False	Passed	Model Under Test Equivalent Model
c5393fd5ac5a308ffa01ccf9f47c405cef08f554	Apalache	SeqAppend	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
a630d7e2d874d0c2ede15f87d2c208ebdba22504	Apalache	SeqAppend	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
76e38d7490c133a891f6fdb65ca161e84b697394	Apalache	SeqAppend	NumPlus	True	Passed	Model Under Test Equivalent Model
5bede1916c0fd7d572522de75ce7441c7056f9a0	Apalache	SeqAppend	NumPlus	False	Passed	Model Under Test Equivalent Model
5b7f3451c9dd78d1f60e706639458c83d4af1e71	Apalache	SeqAppend	NumMinus	True	Passed	Model Under Test Equivalent Model
2ef3ecc06e9f4092be5bd238d658cf3991e5b65b	Apalache	SeqAppend	NumMinus	False	Passed	Model Under Test Equivalent Model
ce8daac00603ed94d9b2b9c5c6333a35aba20e6a	Apalache	SeqAppend	NumMul	True	Passed	Model Under Test Equivalent Model
bd5a0dc5b0bcb6f03c318a61d1c20d91792ad72e	Apalache	SeqAppend	NumMul	False	Passed	Model Under Test Equivalent Model
8d38873b30142daa8b22ebb21e1bc4962d0f1073	Apalache	SeqAppend	NumDiv	True	Passed	Model Under Test Equivalent Model
6f3f57a2662bf797847c3e7cfb3404cd979003d0	Apalache	SeqAppend	NumDiv	False	Passed	Model Under Test Equivalent Model
8010ce266e3e7e10c86b43053c0d800cf0593a06	Apalache	SeqAppend	NumMod	True	Passed	Model Under Test Equivalent Model
9141eaaae379181cc134113bf75e4d6511fdeb9d	Apalache	SeqAppend	NumMod	False	Passed	Model Under Test Equivalent Model
0258a9f92c4ae5c43baa5b1dca77214dd69d532b	Apalache	SeqAppend	NumPow	True	Passed	Model Under Test Equivalent Model
00c579dc779af4e8f9d937a07e00e63fd2b27cdf	Apalache	SeqAppend	NumPow	False	Passed	Model Under Test Equivalent Model
617dd5622eb8e7f88095b02ca9ef0cbac3fc15e3	Apalache	SeqAppend	NumGt	True	Passed	Model Under Test Equivalent Model
2a8699f50e64a8f0184de68e1f34e265fd03e030	Apalache	SeqAppend	NumGt	False	Passed	Model Under Test Equivalent Model
21976a7f94d1a43d758635d8e0737ead5a4cd3d6	Apalache	SeqAppend	NumGe	True	Passed	Model Under Test Equivalent Model
4d4bade0969c76a6ad681b3a7c65813ae00cd4df	Apalache	SeqAppend	NumGe	False	Passed	Model Under Test Equivalent Model
02996a835390a17dd3a822c83bccdb21eded7420	Apalache	SeqAppend	NumLt	True	Passed	Model Under Test Equivalent Model
baf2c6a5ddf3d0221ba44e932c6cafcd8c6b2820	Apalache	SeqAppend	NumLt	False	Passed	Model Under Test Equivalent Model
3d2940c488b8a764cd5e4c64e660224550f31c56	Apalache	SeqAppend	NumLe	True	Passed	Model Under Test Equivalent Model
592237afd1347cc02a776fbb3ef674f623ef10c2	Apalache	SeqAppend	NumLe	False	Passed	Model Under Test Equivalent Model
7b538d48d905091dae75540b2e947eb4e8cc60b4	Apalache	SeqAppend	DefFun	True	Passed	Model Under Test Equivalent Model
d79f6c6d9e13f89b4cf98af8d17d26dfb0b83887	Apalache	SeqAppend	DefFun	False	Passed	Model Under Test Equivalent Model
75bc6bad36a3001fabd6cc95db8da19561f86b36	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqAppend	LetDefFun	True	Passed	Model Under Test Equivalent Model
4064b59c9303afeb8a0e05da6bcbd7b290a032f3	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqAppend	LetDefFun	False	Passed	Model Under Test Equivalent Model
4488cfd857ee1a10619f32dfe51a5837b277650b	Apalache	SeqAppend	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
4ebbacab4dc600c3cddd3bd9c0896d3833dadb94	Apalache	SeqAppend	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
8bf8cf1c01684f5ff5a778b45bc50ea386c579d7	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqAppend	LetDefFunRecursive	True	Passed	Model Under Test Equivalent Model
bde9698a46254d64e9fc6fa07af1b8093c6cf98b	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqAppend	LetDefFunRecursive	False	Passed	Model Under Test Equivalent Model
bae20536397e4fe0aec022e9ffe1422a622b6ddd	Apalache	SeqAppend	Def0	True	Passed	Model Under Test Equivalent Model
e97863d45bd071a5258871a3ba52a57485c17d22	Apalache	SeqAppend	Def0	False	Passed	Model Under Test Equivalent Model
b7d8da2b5a75b6f984f432a685fa9803696ea596	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqAppend	LetDef0	True	Passed	Model Under Test Equivalent Model
3c0af8b97444caaf4f1a1eb1d0a2a73bc9ca9a95	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqAppend	LetDef0	False	Passed	Model Under Test Equivalent Model
c6de1ef2bcdd48bd3637a01580c75c831f08068d	Apalache	SeqAppend	Def1	True	Passed	Model Under Test Equivalent Model
f5adec961eb02aa86d0efc23da6807813c7df1a3	Apalache	SeqAppend	Def1	False	Passed	Model Under Test Equivalent Model
423ed142123b4b909e0e5a17e89eedbcddfa0b66	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqAppend	LetDef1	True	Passed	Model Under Test Equivalent Model
97487f60a8635f0256a2a3c60129f7e568c4686b	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqAppend	LetDef1	False	Passed	Model Under Test Equivalent Model
dd6817bb25f008609b2fd2c345546c2dbcef1de6	Apalache	SeqAppend	Def2	True	Passed	Model Under Test Equivalent Model
1be1c58b17eeb3e221dd314901f0d64ae4b10eaa	Apalache	SeqAppend	Def2	False	Passed	Model Under Test Equivalent Model
18050490986a9670a188ba6d98e901c134eb37aa	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqAppend	LetDef2	True	Passed	Model Under Test Equivalent Model
550a9998932a896a1314f7ba9a68bf200debb525	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqAppend	LetDef2	False	Passed	Model Under Test Equivalent Model
2e03cf4b2d5a804b924c6b1b38a12480454de019	Apalache	SeqAppend	Def1Recursive	True	Passed	Model Under Test Equivalent Model
eff4828a022ad3cc35029bbefd64ec0eed3e02e1	Apalache	SeqAppend	Def1Recursive	False	Passed	Model Under Test Equivalent Model
75221bc6d4cf69554b4751d566a7f916137c16e0	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqAppend	LetDef1Recursive	True	Passed	Model Under Test Equivalent Model
e4ea2f7e2c579a12c4ffcdb51769df4f4ecce223	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqAppend	LetDef1Recursive	False	Passed	Model Under Test Equivalent Model
47c5bf199cba955df25cf6de2b0146a85e65a666	Apalache	SeqAppend	Extends	True	Passed	Model Under Test Equivalent Model
6015397de20adb63929ea20b6d054cce32c7f2cc	Apalache	SeqAppend	Extends	False	Passed	Model Under Test Equivalent Model
dfa116825a5529a249f53b7e5234376a6b2cc138	Apalache	SeqAppend	ExtendsInDifferentFolder	True	Passed	Model Under Test Equivalent Model
47e2fa9978cfa07ddd0acf701e18e8bc0d457c74	Apalache	SeqAppend	ExtendsInDifferentFolder	False	Passed	Model Under Test Equivalent Model
a4010c147670a24b7184c8ccf180ec2799ca64f0	Apalache	SeqAppend	Variable	True	Passed	Model Under Test Equivalent Model
b24eace9f38bd2759e269db541adca8f8b66806d	Apalache	SeqAppend	Variable	False	Passed	Model Under Test Equivalent Model
2c915dc20df141cbfe0b18a9a94f97579c19bfe1	Apalache	SeqAppend	Constant	True	Passed	Model Under Test Equivalent Model
2f6d841d1fe7d05eacedc5592990cf90757313e0	Apalache	SeqAppend	Constant	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
59df4c6287e4ab003d7ede2ae47a4b62a7ddd0c8	Apalache	SeqAppend	Instance	True	Passed	Model Under Test Equivalent Model
e68e7a509fdcae23c23cfa45463486c116d05f02	Apalache	SeqAppend	Instance	False	Passed	Model Under Test Equivalent Model
95eb5df79e0591d0622a7fd1b6510c7de86c0e3a	Apalache	SeqAppend	InstanceWith	True	Passed	Model Under Test Equivalent Model
e88943812422068689b7903d414ad68fbd869653	Apalache	SeqAppend	InstanceWith	False	Passed	Model Under Test Equivalent Model
fdcc38e5e9d39d044cf53ef1a344f43585efedd2	Apalache	SeqAppend	InstanceNamed	True	Passed	Model Under Test Equivalent Model
0c148643f1acee98fcb618f78e29bae8f38ecf3b	Apalache	SeqAppend	InstanceNamed	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
04c5abc9152993163815302e1bad30984bb794a9	Apalache	SeqAppend	InstanceInFolder	True	Passed	Model Under Test Equivalent Model
12497bc2437989b9edb361763121ba46d6b7df4c	Apalache	SeqAppend	InstanceInFolder	False	Passed	Model Under Test Equivalent Model
67856c0703e0ab2fc641adada5880154e0b9b1a3	Apalache	SeqAppend	InstanceWithInFolder	True	Passed	Model Under Test Equivalent Model
fee0a51119e964f102714e99dc59959b7242eb5d	Apalache	SeqAppend	InstanceWithInFolder	False	Passed	Model Under Test Equivalent Model
063471d83e77fa5c5a0bb0815d9779f7bf46bc41	Apalache	SeqAppend	InstanceNamedInFolder	True	Passed	Model Under Test Equivalent Model
25c9eef6e26e70fd0c0bd69c570c389cfaa11ee1	Apalache	SeqAppend	InstanceNamedInFolder	False	Passed	Model Under Test Equivalent Model
3e7df518834483b7edfe25cc485ff24f29e4769c	Apalache	SeqAppend	InstanceNamedWithInFolder	True	Passed	Model Under Test Equivalent Model
3883fcd70c564fc2edf7b0fd3bf6fa8ef26ae1ca	Apalache	SeqAppend	InstanceNamedWithInFolder	False	Passed	Model Under Test Equivalent Model
fe5ce7c94ed5fbbf520b4e43f611232feeb04a9c	Apalache	SeqAppend	Enabled	True	Passed	Model Under Test Equivalent Model
12f772a5ca5b4130787e8073d7dd53dbeb7f0559	Apalache	SeqAppend	Enabled	False	Passed	Model Under Test Equivalent Model
015087e5a2aee1c9c4ccb8e0baf90b39182e191a	Apalache	SeqAppend	Cross2	True	Passed	Model Under Test Equivalent Model
9758e55a96d950da3cdf57f4d5040a8a49de08a0	Apalache	SeqAppend	Cross2	False	Passed	Model Under Test Equivalent Model
9ae63f69b3e7b4360f5144f627baaac8aca088c0	Apalache	SeqAppend	Cross3	True	Passed	Model Under Test Equivalent Model
6d5f48799d838c4d88456358910b3b7d1bc8a35d	Apalache	SeqAppend	Cross3	False	Passed	Model Under Test Equivalent Model
8edbb874173e4579ccaa934a3aadf4555c40a945	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))	SeqAppend	FunSet	True	Passed	Model Under Test Equivalent Model
8f9f4574a771447fbb8cda992c782360f5ca521e	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))	SeqAppend	FunSet	False	Passed	Model Under Test Equivalent Model
a6826e444a95253f4432f8ad9ac3e3f0943bd892	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)	SeqAppend	RecordSet	True	Passed	Model Under Test Equivalent Model
8a30120485ee747cd6bd80ddd75660b101b5e230	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)	SeqAppend	RecordSet	False	Passed	Model Under Test Equivalent Model
8f0701d3782d4a8f4ae11527709e6d8359035f7e	Apalache	SeqAppend	SetDiff	True	Passed	Model Under Test Equivalent Model
6bc32e62711a2241abad375564f3b23b265d1e24	Apalache	SeqAppend	SetDiff	False	Passed	Model Under Test Equivalent Model
db8d6ed6476a15368ba147c622c1c72b6f998710	Apalache	SeqAppend	SetUnion	True	Passed	Model Under Test Equivalent Model
8fc3f89385d49f778666f3eae06303b28650f700	Apalache	SeqAppend	SetUnion	False	Passed	Model Under Test Equivalent Model
ec912a9cafc6fe4c5c44a4f1ff75df568150670e	Apalache	SeqAppend	SetIntersect	True	Passed	Model Under Test Equivalent Model
36559ccb19b8a3456bc250985190e39bd61b30a7	Apalache	SeqAppend	SetIntersect	False	Passed	Model Under Test Equivalent Model
2c9cbf345e9f8639af53c41f94937ce759e1a8dc	Apalache	SeqAppend	SubsetEq	True	Passed	Model Under Test Equivalent Model
8500e801f0a0a9898ea59b91df4cc0a0a47bad5b	Apalache	SeqAppend	SubsetEq	False	Passed	Model Under Test Equivalent Model
bb49e8c6ffabc3feb7836216f1593bb61a486344	Apalache	SeqAppend	IfCond	True	Passed	Model Under Test Equivalent Model
8f68d3ab810605f52164141e202c9ae3f9eebf2a	Apalache	SeqAppend	IfCond	False	Passed	Model Under Test Equivalent Model
e8f23e03577f0d79bbc6fd8d5f397297170d3ab3	Apalache	SeqAppend	IfThen	True	Passed	Model Under Test Equivalent Model
5a872583c9aaf11c0c350cba82e6514fe21d1257	Apalache	SeqAppend	IfThen	False	Passed	Model Under Test Equivalent Model
7a0c11df98e4375afdf630d3ee9146e71c3e8888	Apalache	SeqAppend	IfElse	True	Passed	Model Under Test Equivalent Model
dc311a8fce0e12827b3c77ec392ad40bd20731e5	Apalache	SeqAppend	IfElse	False	Passed	Model Under Test Equivalent Model
cd38c1f2eabba978362c7adf4ce4e48674b53526	Apalache	SeqAppend	Subset	True	Passed	Model Under Test Equivalent Model
43970ecc14a15dda98c167b85598b4de709d2604	Apalache	SeqAppend	Subset	False	Passed	Model Under Test Equivalent Model
612ef64f6e11fcaae61698293db0eb3ecdb89332	Apalache	SeqAppend	Domain	True	Passed	Model Under Test Equivalent Model
ca4ea3ec42b35c1adc0b80154c123c11e482ac08	Apalache	SeqAppend	Domain	False	Passed	Model Under Test Equivalent Model
9074fcd745ca56ddf8f2cbb17f05304b304a1d4a	Apalache	SeqAppend	Union	True	Passed	Model Under Test Equivalent Model
c219e32f26669d5b407a5179d6cb2cbab771f83c	Apalache	SeqAppend	Union	False	Passed	Model Under Test Equivalent Model
d8b684b84cdcdd2821c5050bd0c72264be841542	Apalache	SeqAppend	Unchanged	True	Passed	Model Under Test Equivalent Model
107eada58d72f9d19dda5a11e0487809a18d3e6c	Apalache	SeqAppend	Unchanged	False	Passed	Model Under Test Equivalent Model
52504ead642a38c06ac078422bcf8156663a642a	Apalache	SeqAppend	Equivalence	True	Passed	Model Under Test Equivalent Model
47238f18f2ca6f188cdf23e4209c922e4f8e21d5	Apalache	SeqAppend	Equivalence	False	Passed	Model Under Test Equivalent Model
da913c80923c71eb244e929d5caab7716b3e92c5	Apalache	SeqAppend	StringEmpty	True	Passed	Model Under Test Equivalent Model
b8aa06e383c591fdab7b2623176db3f60dea3ac1	Apalache	SeqAppend	StringEmpty	False	Passed	Model Under Test Equivalent Model
300eede17a3775d435e18d5c369fe3309704e704	Apalache	SeqAppend	String	True	Passed	Model Under Test Equivalent Model
c7014431c147ad927bc45bd5364df95b7abe2a71	Apalache	SeqAppend	String	False	Passed	Model Under Test Equivalent Model
f994d0ce9e0a9da3cca480171476e89e736e641d	Apalache	SeqAppend	SeqLen	True	Passed	Model Under Test Equivalent Model
44eae72946dc3b266db4e865a9f68b40a07a222a	Apalache	SeqAppend	SeqLen	False	Passed	Model Under Test Equivalent Model
9d4d64b481e21bdbeca536b5cf46b379b46b1d0e	Apalache	SeqAppend	SeqConcat	True	Passed	Model Under Test Equivalent Model
97ac351f5ca5a9d04fe2e267d66f77dcd1739176	Apalache	SeqAppend	SeqConcat	False	Passed	Model Under Test Equivalent Model
9f6f0b6ad5da2a94debf6dce8c468464169c5f4f	Apalache	SeqAppend	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
26cc42d7ab8cf0c888a451e9898a5751dc4e055a	Apalache	SeqAppend	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
913cc61f0485ec624082be9a225574d40b9de3b0	Apalache	SeqAppend	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
156fe49aa6134a566f949a9fb467ea89f7a0bcf0	Apalache	SeqAppend	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
18bd6f12307c3152851e27fe88480f902150a3e5	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	SeqAppend	NumRange	True	Passed	Model Under Test Equivalent Model
cd425b1b7d03d1b2ea939d575128aa651b666c5e	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	SeqAppend	NumRange	False	Passed	Model Under Test Equivalent Model
cc4f43b75e13afb910d6b18af71ccc178cef8584	TLC with reduction strategy: Plug Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	SeqAppend	TlcSingletonFun	True	Passed	Model Under Test Equivalent Model
a6694a38d399c9a213156aed7359e05f760f3c1a	TLC with reduction strategy: Plug Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	SeqAppend	TlcSingletonFun	False	Passed	Model Under Test Equivalent Model
bf459686ec4bfe15b2f2d03e5569e6e28ceb8b61	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]]	SeqAppend	TlcExtendFun	True	Passed	Model Under Test Equivalent Model
32564d813fa07265b4af32bcd83f25c01a50b5a2	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]]	SeqAppend	TlcExtendFun	False	Passed	Model Under Test Equivalent Model
a5d4f040d6d9ad59f37dbf387ff24e8e36dc2131	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	SeqAppend	TlcPermuteFun	True	Passed	Model Under Test Equivalent Model
e296811f9ed83df9e19757e6abb39eb9d92f8190	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	SeqAppend	TlcPermuteFun	False	Passed	Model Under Test Equivalent Model
28075a2677a076dce35ec4ad7c61b8d68cc615dd	TLC with reduction strategy: Plug Feature: SortSeq(S) is reduced to equivalent sort implementation	SeqAppend	TlcSortSeq	True	Passed	Model Under Test Equivalent Model
b31a944cef21ef074959e6b8d33dabfff3ae1849	TLC with reduction strategy: Plug Feature: SortSeq(S) is reduced to equivalent sort implementation	SeqAppend	TlcSortSeq	False	Passed	Model Under Test Equivalent Model
6ebe99d533bbf589a6fd818056fd31e7b2fbfc8f	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	SeqAppend	TlcEval	True	Passed	Model Under Test Equivalent Model
981d3595ae9a4751d0d5769cb3c408f8197c02c2	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	SeqAppend	TlcEval	False	Passed	Model Under Test Equivalent Model
b4347febee14a2a35a53bfe16f52db9312cebb70	Apalache	SeqAppend	BagBagToSet	True	Passed	Model Under Test Equivalent Model
df52c47a7a7850e6471c342e03b7aff6a4dd0329	Apalache	SeqAppend	BagBagToSet	False	Passed	Model Under Test Equivalent Model
fea4ed739d49b1df29035b9c280c1885f0a36806	Apalache	SeqAppend	BagSetToBag	True	Passed	Model Under Test Equivalent Model
dfe015d5efbe070e375350944dc1d4c0e4060321	Apalache	SeqAppend	BagSetToBag	False	Passed	Model Under Test Equivalent Model
36a84b3ac66079f91c79330109f109e8481d5113	Apalache	SeqAppend	BagBagIn	True	Passed	Model Under Test Equivalent Model
85f3c2d3867a56897c99027ef430e522abaa324e	Apalache	SeqAppend	BagBagIn	False	Passed	Model Under Test Equivalent Model
e56eb7ab473fc275b7374839e95a07d84927841a	Apalache	SeqAppend	BagEmptyBag	True	Passed	Model Under Test Equivalent Model
e2aefe0e97e025cf33232a40deb898302e657f47	Apalache	SeqAppend	BagEmptyBag	False	Passed	Model Under Test Equivalent Model
10f0a9fbab58139d5099325c9bb87b51e330e269	Apalache	SeqAppend	BagAddBag	True	Passed	Model Under Test Equivalent Model
3398c2ce7e5325f10eabff09a05af23fac690954	Apalache	SeqAppend	BagAddBag	False	Passed	Model Under Test Equivalent Model
2c97657fd24d0f83a3d3e341c7bc4117e3efc220	Apalache	SeqAppend	BagBagSub	True	Passed	Model Under Test Equivalent Model
c47a8474c16360839682035abc3107ee11ff891c	Apalache	SeqAppend	BagBagSub	False	Passed	Model Under Test Equivalent Model
99d5eff4a4cbb8622aad56d88dc33431af500482	Apalache	SeqAppend	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
3f3bc4449993b88c0b423a6bb7f1108dc1eff338	Apalache	SeqAppend	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
ff70427904d767adf81146e351ea73b713fbfa6f	Apalache	SeqAppend	BagSubsetEqBag	True	Passed	Model Under Test Equivalent Model
98f2c6a7ee4c75de30a6fff854202d33583171d7	Apalache	SeqAppend	BagSubsetEqBag	False	Passed	Model Under Test Equivalent Model
c9af470c124f21ec7b8323df718e63b078cd3c81	Apalache	SeqAppend	BagBagUnion	True	Passed	Model Under Test Equivalent Model
03a6dc51e0ccfe28fe43db67239ba318aab66ec0	Apalache	SeqAppend	BagBagUnion	False	Passed	Model Under Test Equivalent Model
3da2152f8b5eb2d13101822fb1ef5115975f3395	Apalache	SeqAppend	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
3047795734e383a4caa3f87b39b7865fde69eb07	Apalache	SeqAppend	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
641db3a3483e029d874852ece52ba014ec2cd19e	Apalache	SeqAppend	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
15e987afc59e64e09ded5e1e17f281bcdac3ebb9	Apalache	SeqAppend	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
6679cfc720b104b9e8a9d2c13e4ff9dcc6083209	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	SeqAppend	BagSubBag	True	Passed	Model Under Test Equivalent Model
5201939700c59346d4c6a0ad0fa464eafd3f1b81	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	SeqAppend	BagSubBag	False	Passed	Model Under Test Equivalent Model
e058605e6019ae7d49b2ac132e16e555ef5d5fc5	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)	SeqAppend	FiniteSetsIsFiniteSet	True	Passed	Model Under Test Equivalent Model
552b82e97664f8a6e4f7458271f26bf5a9cad44e	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)	SeqAppend	FiniteSetsIsFiniteSet	False	Passed	Model Under Test Equivalent Model
1eb00b20b2fb188d318b3f4c50a6a59bd9bd58f1	Apalache	SeqAppend	FiniteSetsCardinality	True	Passed	Model Under Test Equivalent Model
59ec7d20fe5f88f3297125c652b0d6b8bce07ede	Apalache	SeqAppend	FiniteSetsCardinality	False	Passed	Model Under Test Equivalent Model
35f1191034d89f028b0c36321eec7e4d827b2a50	Apalache	SeqAppend	SeqHead	True	Passed	Model Under Test Equivalent Model
71c065eb44c5ed27602c52533665dfcb46e69962	Apalache	SeqAppend	SeqHead	False	Passed	Model Under Test Equivalent Model
c4c49339754f16cbb5824a429d57f4e89eff6ad1	Apalache	SeqAppend	SeqTail	True	Passed	Model Under Test Equivalent Model
8772c595232d31651255d9b362d65305384418c0	Apalache	SeqAppend	SeqTail	False	Passed	Model Under Test Equivalent Model
8a5895c4351cbe183dc6583e028231f7a986bd48	Apalache	SeqAppend	SeqAppend	True	Passed	Model Under Test Equivalent Model
efe6f83daccc597384eb85dd7134be837f679024	Apalache	SeqAppend	SeqAppend	False	Passed	Model Under Test Equivalent Model

Index

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