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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
795e68f5b970461c16eade8af033fbbc93d2986d	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Record	OneLineComment	True	Passed	Model Under Test Equivalent Model
8f58e06d9e06fc470307f406a0e498d2f1c0b443	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Record	OneLineComment	False	Passed	Model Under Test Equivalent Model
612bec9ac3ce4c8f0084d30523c305079bd7ba73	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Record	MultiLineComment	True	Passed	Model Under Test Equivalent Model
715e3ba2f365c2e58d78e21e99dbecb6a9c4c4e0	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Record	MultiLineComment	False	Passed	Model Under Test Equivalent Model
c4e1f3c660ca96300d1f5ffddaf880ad16924b3f	Apalache	Record	BoolTrue	True	Passed	Model Under Test Equivalent Model
c8800b6589fba759fc3fa262f475d0fc357fe13c	Apalache	Record	BoolTrue	False	Passed	Model Under Test Equivalent Model
234b830e0329c6922930656f0f25e4a5ab4bf4eb	Apalache	Record	BoolFalse	True	Passed	Model Under Test Equivalent Model
9f3581360a6c6b0ab7aa585b1ace93b4c9048cb7	Apalache	Record	BoolFalse	False	Passed	Model Under Test Equivalent Model
870627c805b52251adf6fbc1e6bb14343a5c7549	Apalache	Record	BoolSet	True	Passed	Model Under Test Equivalent Model
e5765c5c65893f7116cc133d5b333c861245d33f	Apalache	Record	BoolSet	False	Passed	Model Under Test Equivalent Model
9f4499a6de4cca8631a60a9037cde4c839baaf17	Apalache	Record	And	True	Passed	Model Under Test Equivalent Model
428e21c7e9ac79e2db5d59ea94aa42e9017e6454	Apalache	Record	And	False	Passed	Model Under Test Equivalent Model
83fd1741fceacbd0fbc8b5b9077cef406b044048	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	Record	AndMultiLine	True	Passed	Model Under Test Equivalent Model
031946ddf099a0103086caad2a614e1120740bd5	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	Record	AndMultiLine	False	Passed	Model Under Test Equivalent Model
c60217e1d77b9059652d2e842d7663ed5ad088b5	Apalache	Record	Imply	True	Passed	Model Under Test Equivalent Model
556b932b43b03a9570ac5bcc7955312dae438463	Apalache	Record	Imply	False	Passed	Model Under Test Equivalent Model
3fa73ca397661e5e35bdd4d53c6064db2bd6f57b	Apalache	Record	Not	True	Passed	Model Under Test Equivalent Model
725db4bdbcd3568800d0757616d00e2edca19aa9	Apalache	Record	Not	False	Passed	Model Under Test Equivalent Model
1e323f28649776e9fb1d27ab98221d5dd2e850a3	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	Record	Or	True	Passed	Model Under Test Equivalent Model
6a70e56b7bfbd31ab62f23a4ec224134ad7912ba	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	Record	Or	False	Passed	Model Under Test Equivalent Model
ac213bc95678032bb27041b302733783529abd3e	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	Record	OrMultiLine	True	Passed	Model Under Test Equivalent Model
a3338af9a3b046e8c65e9bcdfab524c8fa912045	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	Record	OrMultiLine	False	Passed	Model Under Test Equivalent Model
38009ac7e116ccfa1c01ae825f7396f13ca133a7	Apalache	Record	Eq	True	Passed	Model Under Test Equivalent Model
b8be198509c2107baf800e5e919a82cc091c2d0e	Apalache	Record	Eq	False	Passed	Model Under Test Equivalent Model
549f0c88be79aa5b93f30413998d6de8a4f0e3ea	Apalache	Record	Ne	True	Passed	Model Under Test Equivalent Model
c51920f4b836f505fbede4a5b71d4df791ef18f8	Apalache	Record	Ne	False	Passed	Model Under Test Equivalent Model
272c9e9e5af40291e866b6dffe5a0819e4cd9e46	Apalache	Record	Let	True	Passed	Model Under Test Equivalent Model
babbd6b3336d63bef568069764a3b128fbfa76d3	Apalache	Record	Let	False	Passed	Model Under Test Equivalent Model
e0a29517fcc0d1f34ed8b58d05b9c54820f72908	Apalache	Record	SetEmpty	True	Passed	Model Under Test Equivalent Model
0c4868f13dd67a7ed91755c00f101918e6958f67	Apalache	Record	SetEmpty	False	Passed	Model Under Test Equivalent Model
a0aa8de41ba3d17af97d3b78ad58fa35dd730177	Apalache	Record	Set0	True	Passed	Model Under Test Equivalent Model
9e9d4be7eb08651c77771d3644825106523aaf98	Apalache	Record	Set0	False	Passed	Model Under Test Equivalent Model
4a67c526a94a3e8852d6c8eab5b65eba679e57a8	Apalache	Record	Set1	True	Passed	Model Under Test Equivalent Model
8aa70ba8d1110e3d674cc1810eebea98b2d9044a	Apalache	Record	Set1	False	Passed	Model Under Test Equivalent Model
9282ccc70d1f9f6f2b303457776de018f2322d6b	Apalache	Record	Set2	True	Passed	Model Under Test Equivalent Model
a8b595a443f2b3199702955e35c0ab2b90f2da93	Apalache	Record	Set2	False	Passed	Model Under Test Equivalent Model
9e56f0ad389b7c4b68e2cc6d40fe0b14bd0b3632	Apalache	Record	Fun	True	Passed	Model Under Test Equivalent Model
40aaee352319893e83a2585849bc66ac34a2ac0c	Apalache	Record	Fun	False	Passed	Model Under Test Equivalent Model
ef04c07e4ae6183d8cf048356622b21ea27569cd	Apalache	Record	In	True	Passed	Model Under Test Equivalent Model
1b0bd6e7ba997e3271e1730b0ff8c325af4caf36	Apalache	Record	In	False	Passed	Model Under Test Equivalent Model
0b12d02e052cd1f8cae27a42d4f745edb26758f2	Apalache	Record	NotIn	True	Passed	Model Under Test Equivalent Model
74b0e20374ffa4931501f22e63935f22f77c0101	Apalache	Record	NotIn	False	Passed	Model Under Test Equivalent Model
c4e8022de588ee00970518649bb7b6cf1d70ff14	Apalache	Record	Exists	True	Passed	Model Under Test Equivalent Model
50e28fca077176eec1a3f925b38bac43ed4a0b0f	Apalache	Record	Exists	False	Passed	Model Under Test Equivalent Model
a1725a9cc92d33bb5fd9a6b9e692da80b532c759	Apalache	Record	Forall	True	Passed	Model Under Test Equivalent Model
55fc3e98a33299dec9b519dfccaee62f33ecd807	Apalache	Record	Forall	False	Passed	Model Under Test Equivalent Model
337b2ba81682281f6f3780d1cac11aac88ae8352	Apalache	Record	Choose	True	Passed	Model Under Test Equivalent Model
0470c3850643baf576765e494219a9cc52ae0ca4	Apalache	Record	Choose	False	Passed	Model Under Test Equivalent Model
3e848ba94cae723b5ecf2e790b7cc1627ecee079	Apalache	Record	Record	True	Passed	Model Under Test Equivalent Model
213ad5b59c28a31ae988994e10d7b80fa69dd20f	Apalache	Record	Record	False	Passed	Model Under Test Equivalent Model
c3bddc2e87a1668b4baad84f34631de9a9857604	Apalache	Record	Tuple	True	Passed	Model Under Test Equivalent Model
4ba9204f45a4ca8a9e42b6c1ff0cee9ee80fb402	Apalache	Record	Tuple	False	Passed	Model Under Test Equivalent Model
5d1927e8e06e9155ce839317f0d8275624e648e7	Apalache	Record	TupleEmpty	True	Passed	Model Under Test Equivalent Model
1b9c7a4807d03b5b96931a787370bff7c37a5b11	Apalache	Record	TupleEmpty	False	Passed	Model Under Test Equivalent Model
3a89e1c6f54d52364a6a206ac49eb3a17c58cc0c	Apalache	Record	FunApp	True	Passed	Model Under Test Equivalent Model
18d8809d3e388d5c4c13fac278e0c9a14f9c25cc	Apalache	Record	FunApp	False	Passed	Model Under Test Equivalent Model
4913276bf159fafc2ba6936db5fd30d1f2044cc8	Apalache	Record	Prime	True	Passed	Model Under Test Equivalent Model
4443ebba1b0d803978c4ed227521016168ed0b51	Apalache	Record	Prime	False	Passed	Model Under Test Equivalent Model
2130653de461e84dad1d91a4903081fa234d09a2	Apalache	Record	NumZero	True	Passed	Model Under Test Equivalent Model
ef618bfdcc8a3681c4bbc3f33497c3697795cbce	Apalache	Record	NumZero	False	Passed	Model Under Test Equivalent Model
ff178d0283755def8465b7c841bd15315f41d1fd	Apalache	Record	NumOne	True	Passed	Model Under Test Equivalent Model
5c75fd9d4c35bf83e342a2b7643171effbf548e8	Apalache	Record	NumOne	False	Passed	Model Under Test Equivalent Model
58d1042ea88a3e755392b1e4751ecf7cd1f1899f	Apalache	Record	NumMaxInt	True	Passed	Model Under Test Equivalent Model
20fa63fff93159b4b04c14dedd99ed53c2e103fb	Apalache	Record	NumMaxInt	False	Passed	Model Under Test Equivalent Model
5f46ddd84fb283d22b84f0b817428b146ca3cbe8	Apalache	Record	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
c9f1a1929e8c34996d3559aa5c1ea491493c9b92	Apalache	Record	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
006d96d4a24fd02968bfcb70864179156d909558	Apalache	Record	NumPlus	True	Passed	Model Under Test Equivalent Model
0239023002f1469eaf9ebcd511a9ab5fbf436b70	Apalache	Record	NumPlus	False	Passed	Model Under Test Equivalent Model
b98e85873adee1f90dc5f4db155db4380683a622	Apalache	Record	NumMinus	True	Passed	Model Under Test Equivalent Model
42fd0408e639f5880c25300b20aaae903f966716	Apalache	Record	NumMinus	False	Passed	Model Under Test Equivalent Model
58a702722f7fa7fe745aada7ac1112681f1055f4	Apalache	Record	NumMul	True	Passed	Model Under Test Equivalent Model
16e4422287f48a69954ddb41760e2c380b1f2d6a	Apalache	Record	NumMul	False	Passed	Model Under Test Equivalent Model
2255fcb8ff26b94c4aa4380e626020fceb280e92	Apalache	Record	NumDiv	True	Passed	Model Under Test Equivalent Model
40608ae15532ad71dac043f310274e5b6c45bc7b	Apalache	Record	NumDiv	False	Passed	Model Under Test Equivalent Model
dbf97a6e4363cfa1c9fceecaad8bb7235c8e18d7	Apalache	Record	NumMod	True	Passed	Model Under Test Equivalent Model
66081fffbea2e9e7427f64820eb2294aa50df84a	Apalache	Record	NumMod	False	Passed	Model Under Test Equivalent Model
8f514848fdb2569cdef2d7f377faa5ca4fd840a4	Apalache	Record	NumPow	True	Passed	Model Under Test Equivalent Model
a697303a1ffa0691864b6bc7e0ade990870a2f56	Apalache	Record	NumPow	False	Passed	Model Under Test Equivalent Model
dd857f2ba584f8d456e8c7e921eaaedc23280b00	Apalache	Record	NumGt	True	Passed	Model Under Test Equivalent Model
1edfa34d60f58cb6e13027dcaf1ee58755e0e23f	Apalache	Record	NumGt	False	Passed	Model Under Test Equivalent Model
361b3f2e4c269fa5693f8debd27a5e9dd0637cb6	Apalache	Record	NumGe	True	Passed	Model Under Test Equivalent Model
5668b23c522e3167ab5ef53f3bcf4d15ba3757e4	Apalache	Record	NumGe	False	Passed	Model Under Test Equivalent Model
809b63927e68661a5bcf8fcf971900906dfd9f52	Apalache	Record	NumLt	True	Passed	Model Under Test Equivalent Model
8ee6f9a95cf73216c3e4423f27c8d31c2b66ed19	Apalache	Record	NumLt	False	Passed	Model Under Test Equivalent Model
1333615049a34d36af58e1ea9abb9514692fe5ee	Apalache	Record	NumLe	True	Passed	Model Under Test Equivalent Model
5c24a738c8c3b3f30abb66313541724bcdd0cadd	Apalache	Record	NumLe	False	Passed	Model Under Test Equivalent Model
7256c462ad9a743577d4d62d6a506a5e4171046e	Apalache	Record	DefFun	True	Passed	Model Under Test Equivalent Model
787ec98c3041e2ce885813b836e6f5f9d272fb2a	Apalache	Record	DefFun	False	Passed	Model Under Test Equivalent Model
e700b917c7b726120686ae9e571079646efffe5f	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Record	LetDefFun	True	Passed	Model Under Test Equivalent Model
52d89fa79b039ded8fcfb507bad0f1b02d912725	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Record	LetDefFun	False	Passed	Model Under Test Equivalent Model
fea252f99362b8e2c9b583e20f31437533026ec1	Apalache	Record	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
c41f46236b9a0deab6a0ab75046b911103aa2a0a	Apalache	Record	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
adbea9fba37d645fdc836555a11ea8c0b6b9039b	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Record	LetDefFunRecursive	True	Passed	Model Under Test Equivalent Model
5bdeabf80bc776e7fb5a34457972274d4fa3f135	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Record	LetDefFunRecursive	False	Passed	Model Under Test Equivalent Model
cfdf1cd41666f4aa271a1738c4de15ca025025c4	Apalache	Record	Def0	True	Passed	Model Under Test Equivalent Model
321c56fdb0c9965550d01b630645cb1e949377d2	Apalache	Record	Def0	False	Passed	Model Under Test Equivalent Model
03cc5cc13745bc542199ff6940a42b1660caa7c6	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Record	LetDef0	True	Passed	Model Under Test Equivalent Model
62117a7c70c72a2c52bd831705a314db9ae4fb11	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Record	LetDef0	False	Passed	Model Under Test Equivalent Model
a1f05f858015536db1fc3ba1db51b8e71cde92b7	Apalache	Record	Def1	True	Passed	Model Under Test Equivalent Model
97e2091916951acb9ab11d5625975a1dac795b35	Apalache	Record	Def1	False	Passed	Model Under Test Equivalent Model
13b55413fb4513b027260db0b8624a18909a00d3	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Record	LetDef1	True	Passed	Model Under Test Equivalent Model
28e3fa34bdbdad2adf2b12ea96eda17fb46db2cd	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Record	LetDef1	False	Passed	Model Under Test Equivalent Model
bee1db56ef48265793131d5aec92b39e093ffe28	Apalache	Record	Def2	True	Passed	Model Under Test Equivalent Model
3f976ce0089c4e5dca2da301184ab590d6830bb2	Apalache	Record	Def2	False	Passed	Model Under Test Equivalent Model
ed686bb4e242b53e7aa7dbb2d3ffa66339140916	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Record	LetDef2	True	Passed	Model Under Test Equivalent Model
cb95f968d4911e327a0dec44c60f36041f599287	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Record	LetDef2	False	Passed	Model Under Test Equivalent Model
e5bb025ef8c852811fe6546b9630609c267284aa	Apalache	Record	Def1Recursive	True	Passed	Model Under Test Equivalent Model
5c77da7195cf87874ea9fa70c7cabee377f6ad6b	Apalache	Record	Def1Recursive	False	Passed	Model Under Test Equivalent Model
a1e7cba252081615f70c921688e1c4b2f8902cd3	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Record	LetDef1Recursive	True	Passed	Model Under Test Equivalent Model
4383fce64cdad43ec016dc383f6f99456d36ea0a	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Record	LetDef1Recursive	False	Passed	Model Under Test Equivalent Model
c96597a1c9615e1b28c36299001893e6c444ef64	Apalache	Record	Extends	True	Passed	Model Under Test Equivalent Model
4ee4699c5b0941da095b4e61b879f3e6303beb28	Apalache	Record	Extends	False	Passed	Model Under Test Equivalent Model
129e2bb4ec6d15c928b3f03af2beccb78a2c0cc1	Apalache	Record	ExtendsInDifferentFolder	True	Passed	Model Under Test Equivalent Model
cc81282f75f4b03ed296af89968182414daf83bc	Apalache	Record	ExtendsInDifferentFolder	False	Passed	Model Under Test Equivalent Model
47c643a5054c6754ec5ae6c0afbaa0b9e6de4a49	Apalache	Record	Variable	True	Passed	Model Under Test Equivalent Model
bbb26f1eda787685d3b7ce9380d41106cba7b9c2	Apalache	Record	Variable	False	Passed	Model Under Test Equivalent Model
23352b711b2c896b9be035d415efbf74849dbf2c	Apalache	Record	Constant	True	Passed	Model Under Test Equivalent Model
2a5a0d3c1124f93b706f3679e4db02293b9af908	Apalache	Record	Constant	False	Passed	Model Under Test Equivalent Model
aa0a7f104ab6e61ca52480ff769a41c8591b714c	Apalache	Record	ConstantModelValue	True	Passed	Model Under Test Equivalent Model
a5cf0fdf9650f0c0b2cc78956e25658431bfe8eb	Apalache	Record	ConstantModelValue	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
a59c41a960b634cdf0b6c21f8a4dd64aaa7d7263	Apalache	Record	Instance	True	Passed	Model Under Test Equivalent Model
84550f2af0a9dd6e1a0aa46ef5c2f77175b189bc	Apalache	Record	Instance	False	Passed	Model Under Test Equivalent Model
f86dab7486ace9da7f84f0ebf733c163b97a21e7	Apalache	Record	InstanceWith	True	Passed	Model Under Test Equivalent Model
2755b9a12cc8342967955f18285caad5d64edb89	Apalache	Record	InstanceWith	False	Passed	Model Under Test Equivalent Model
7f19ce0407ece47c913aa6e38df7e3c675b88413	Apalache	Record	InstanceNamed	True	Passed	Model Under Test Equivalent Model
7109cc989490a6c99be48e1856240ab3e7bb2323	Apalache	Record	InstanceNamed	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
55bd623d226885db57350d02c7ee8bc159057973	Apalache	Record	InstanceInFolder	True	Passed	Model Under Test Equivalent Model
527d057a580f1521b317a3aad7be6920199faf19	Apalache	Record	InstanceInFolder	False	Passed	Model Under Test Equivalent Model
8b38d8f087a39543a4fb8727fdf00517a74ef7c7	Apalache	Record	InstanceWithInFolder	True	Passed	Model Under Test Equivalent Model
ba7692f92ed91831b42627b8530f0b0b67244aae	Apalache	Record	InstanceWithInFolder	False	Passed	Model Under Test Equivalent Model
9a76550e37d4474d1ceb1a20427a47d0b65a9164	Apalache	Record	InstanceNamedInFolder	True	Passed	Model Under Test Equivalent Model
eea5c1f4b0c5828c86234e73512a4634fc44a492	Apalache	Record	InstanceNamedInFolder	False	Passed	Model Under Test Equivalent Model
b8ce34bc8634ae70e5aa90fef8cf9bd9c68e3105	Apalache	Record	InstanceNamedWithInFolder	True	Passed	Model Under Test Equivalent Model
731b9c4336a5e3e75bb9bc8d3a63c58c7119d32d	Apalache	Record	InstanceNamedWithInFolder	False	Passed	Model Under Test Equivalent Model
b0b4d9a9654f421a0d65ff52d36f3b88d63ef38d	Apalache	Record	Enabled	True	Passed	Model Under Test Equivalent Model
5d4e3253356d53d565e39ee95f554a950017a5be	Apalache	Record	Enabled	False	Passed	Model Under Test Equivalent Model
fe09de3dad08e69a6d0912d0df3c887010c9f22d	Apalache	Record	Cross2	True	Passed	Model Under Test Equivalent Model
1beda44657277a46883946e1b1ca40eb5b85d7b7	Apalache	Record	Cross2	False	Passed	Model Under Test Equivalent Model
2dd9c8403891a2d1464ec8503f6bbfe3ee8ef831	Apalache	Record	Cross3	True	Passed	Model Under Test Equivalent Model
4b3592e76943fc72f55e1b3235ac5ce7ae92513a	Apalache	Record	Cross3	False	Passed	Model Under Test Equivalent Model
49582b49ef293cf5ce13c22e8ed87f29cfac1fc1	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))	Record	FunSet	True	Passed	Model Under Test Equivalent Model
07e6cc212b3ac6cc3fbd869f453e19465707fb85	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))	Record	FunSet	False	Passed	Model Under Test Equivalent Model
9814b53cf79b684082eea719417d9173f604d179	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)	Record	RecordSet	True	Passed	Model Under Test Equivalent Model
c580f033b4b0f943ddb3ba63ce16c042493f8381	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)	Record	RecordSet	False	Passed	Model Under Test Equivalent Model
166c5ed1def9b2dadb3c34795bf809adab9a2945	Apalache	Record	SetDiff	True	Passed	Model Under Test Equivalent Model
9f53695b37b7e61e10ddfbd5f01dde136f34f525	Apalache	Record	SetDiff	False	Passed	Model Under Test Equivalent Model
37228fa77e8dee7d2f9c60a1b7b1beda097d4ae1	Apalache	Record	SetUnion	True	Passed	Model Under Test Equivalent Model
255b0c1353c89399b938e8383c120192dba390c7	Apalache	Record	SetUnion	False	Passed	Model Under Test Equivalent Model
da48d56e3aa4b5dfc1271a2a282944352d471388	Apalache	Record	SetIntersect	True	Passed	Model Under Test Equivalent Model
8b0c6e29a5b53dd00a7306ec854926a859f55228	Apalache	Record	SetIntersect	False	Passed	Model Under Test Equivalent Model
7d5d2fb640c48b003cc86759c20589f2e9151687	Apalache	Record	SubsetEq	True	Passed	Model Under Test Equivalent Model
cb18bb6bd8ee0a649d9f0ecf47bd952b81d1aa29	Apalache	Record	SubsetEq	False	Passed	Model Under Test Equivalent Model
1d6d08faca220fbe8f1a6761cca1d83c3a545ff1	Apalache	Record	IfCond	True	Passed	Model Under Test Equivalent Model
e0f0c210a222335dee21e62dc9e713ea576c5da9	Apalache	Record	IfCond	False	Passed	Model Under Test Equivalent Model
e766b024125fb911f9160e24e0dec1bb74e15041	Apalache	Record	IfThen	True	Passed	Model Under Test Equivalent Model
64eb29ffc71f867463b1f82428e4d92b68dcd222	Apalache	Record	IfThen	False	Passed	Model Under Test Equivalent Model
cc11710d9acb6c19a2c953050550658eb7a1ff94	Apalache	Record	IfElse	True	Passed	Model Under Test Equivalent Model
c6befcc1e6510ee9139cca5986f8ad68d1a328de	Apalache	Record	IfElse	False	Passed	Model Under Test Equivalent Model
5f386267a713b9d20b139082412e1dc3a02544df	Apalache	Record	Subset	True	Passed	Model Under Test Equivalent Model
c28e7560929637ab489aab97ef06165345fecc88	Apalache	Record	Subset	False	Passed	Model Under Test Equivalent Model
178badaca50d3d59aa84379825802d90e1f29350	Apalache	Record	Domain	True	Passed	Model Under Test Equivalent Model
945aec7a6e32e265252eef7319cce315d20ae589	Apalache	Record	Domain	False	Passed	Model Under Test Equivalent Model
7d4b60595c73cbcd9f0fa5d63395161ce23be98b	Apalache	Record	Union	True	Passed	Model Under Test Equivalent Model
b9bec69ead4544eb7b431b35e1cceed82ab21de7	Apalache	Record	Union	False	Passed	Model Under Test Equivalent Model
55cbd84b509d87ee037b90058bf907f7b2102cc8	Apalache	Record	Unchanged	True	Passed	Model Under Test Equivalent Model
3a5489ae8db0b34caeebad5f05780059bd3b1b50	Apalache	Record	Unchanged	False	Passed	Model Under Test Equivalent Model
5a5f408c0923470bb66b5a2402ad8c62fb0ca45a	Apalache	Record	Equivalence	True	Passed	Model Under Test Equivalent Model
b9ef92711e61f97c403fdd0f69c8301b889ba255	Apalache	Record	Equivalence	False	Passed	Model Under Test Equivalent Model
a2782784e3c4b54a3f4b5b87e6db2c2fad01356c	Apalache	Record	StringEmpty	True	Passed	Model Under Test Equivalent Model
e263a259be1255cf7c847ec8528450c4a054d947	Apalache	Record	StringEmpty	False	Passed	Model Under Test Equivalent Model
c798c14896583188bdfd3400d0c173380a3dd0d4	Apalache	Record	String	True	Passed	Model Under Test Equivalent Model
090d90501c00e8111dfafdf28a60e326dd5464bb	Apalache	Record	String	False	Passed	Model Under Test Equivalent Model
27a7b0c09ae36a567e1f1c9091b431c79c52640b	Apalache	Record	SeqLen	True	Passed	Model Under Test Equivalent Model
092af55a50d9a6f43813e866b3860c1d7f8b6ac6	Apalache	Record	SeqLen	False	Passed	Model Under Test Equivalent Model
bc63bd58a0fa0d2abf3bf3ba8a9c55fdd042b5bb	Apalache	Record	SeqConcat	True	Passed	Model Under Test Equivalent Model
c2a2016350127051ad240b3c310c90f62fc9894f	Apalache	Record	SeqConcat	False	Passed	Model Under Test Equivalent Model
ca01f5266f1ce3eba37df0ae49afab127a3de75c	Apalache	Record	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
efba664b33757c127b9c6e78f5b69020772907cc	Apalache	Record	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
69cd19b75f57e0c276be9b878175023b684bf7d6	Apalache	Record	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
a00bb5049304921220985fd311669f5489db4d4a	Apalache	Record	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
c9bffc700b7af20f979fc3ad718f2c47446ea665	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	Record	NumRange	True	Passed	Model Under Test Equivalent Model
07e281d4d1553ed5d0dbca20adbe865ffa308438	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	Record	NumRange	False	Passed	Model Under Test Equivalent Model
4e13a5415db7c602230532e489e1e2f899523d80	TLC with reduction strategy: Plug Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	Record	TlcSingletonFun	True	Passed	Model Under Test Equivalent Model
f84f48d7c6e0a77620a3d04d0c01e805c7ebac21	TLC with reduction strategy: Plug Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	Record	TlcSingletonFun	False	Passed	Model Under Test Equivalent Model
fc777027b3cbdfb56e62e04526f21d7ce9b97b46	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]]	Record	TlcExtendFun	True	Passed	Model Under Test Equivalent Model
a425ba0671c01f2148d6b0169743f64d533b153b	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]]	Record	TlcExtendFun	False	Passed	Model Under Test Equivalent Model
61c20715759f2dc4aef9a2f7f501aa1827b72f26	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	Record	TlcPermuteFun	True	Passed	Model Under Test Equivalent Model
716fc49be478ecd3852fefd7dda0c5438bb522fe	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	Record	TlcPermuteFun	False	Passed	Model Under Test Equivalent Model
d0bd402d0661b2ff771e50a4a0aacdc305cf2a6f	TLC with reduction strategy: Plug Feature: SortSeq(S) is reduced to equivalent sort implementation	Record	TlcSortSeq	True	Passed	Model Under Test Equivalent Model
47b89b2ef8d2b3cb29a04837171b7e2c279bbc3c	TLC with reduction strategy: Plug Feature: SortSeq(S) is reduced to equivalent sort implementation	Record	TlcSortSeq	False	Passed	Model Under Test Equivalent Model
75fa8c254de6772d38a5edba12e3a760c8af6888	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	Record	TlcEval	True	Passed	Model Under Test Equivalent Model
835f09529359e3c91014584a25a145f9390a203e	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	Record	TlcEval	False	Passed	Model Under Test Equivalent Model
ad7de9898e0cef251b9d91e252029e3c7a86b988	Apalache	Record	BagBagToSet	True	Passed	Model Under Test Equivalent Model
ed459bd022331e4c60bb01580ee583eb3a0b5128	Apalache	Record	BagBagToSet	False	Passed	Model Under Test Equivalent Model
46fb5e2f02603931708836513ab01541ac4c8e8e	Apalache	Record	BagSetToBag	True	Passed	Model Under Test Equivalent Model
1fc802416ba7694ece3cc1d4397dddda58f22e88	Apalache	Record	BagSetToBag	False	Passed	Model Under Test Equivalent Model
a4af553dda768e78a818ce3e236eff4769796d79	Apalache	Record	BagBagIn	True	Passed	Model Under Test Equivalent Model
00f0c4ced4d83213ef27f2b60842e87df5c6884d	Apalache	Record	BagBagIn	False	Passed	Model Under Test Equivalent Model
28c61816ed25dc75de860bc8bf37368ef6ef6e52	Apalache	Record	BagEmptyBag	True	Passed	Model Under Test Equivalent Model
3e11ffd91deb8cebc425525c517b981801809c08	Apalache	Record	BagEmptyBag	False	Passed	Model Under Test Equivalent Model
257506345a5c1e89d2e6905959aabc7738dcf01a	Apalache	Record	BagAddBag	True	Passed	Model Under Test Equivalent Model
fada54d7040c7c92a79835e0ee6c798851f1401d	Apalache	Record	BagAddBag	False	Passed	Model Under Test Equivalent Model
bc95e979dcd6e95aa7ccc116af35723ad4bea8a3	Apalache	Record	BagBagSub	True	Passed	Model Under Test Equivalent Model
c2d3782fae9986a8b0871b2966ff23f3ce8d9d8b	Apalache	Record	BagBagSub	False	Passed	Model Under Test Equivalent Model
fd52c919c075b6290c469206ebfbaf27b2e4a960	Apalache	Record	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
b7be877b02803d1fe79ecb85f327f74b2d763709	Apalache	Record	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
a2de2467e5abe2dc3dc4d32d9000ebcfd9a6fbdf	Apalache	Record	BagSubsetEqBag	True	Passed	Model Under Test Equivalent Model
38b676019f1ac676f51ca85f5f184c088335ef25	Apalache	Record	BagSubsetEqBag	False	Passed	Model Under Test Equivalent Model
0459517802ea5a3add21c728c90e3cf50c17eb8f	Apalache	Record	BagBagUnion	True	Passed	Model Under Test Equivalent Model
12cb1a69306c2ce7e1c4564901150efafad76f9c	Apalache	Record	BagBagUnion	False	Passed	Model Under Test Equivalent Model
2d733567f63c274693dcbc943c6f5228c24ac703	Apalache	Record	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
589fb971ad004f577e0418a56bfd387a8bbb0631	Apalache	Record	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
45ab57444a590d5672149cf556e10b00ff01eb79	Apalache	Record	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
524284894d3c2dcae99690e9467b0b4e648909b8	Apalache	Record	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
8bfc85707e1ddb0090468a2a857b1fb9f2cc5a7f	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	Record	BagSubBag	True	Passed	Model Under Test Equivalent Model
76c2dae1c45f66544e59cc0c8f2c7ea9999b998d	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	Record	BagSubBag	False	Passed	Model Under Test Equivalent Model
6180c39ae857d434b13682d35b2bbcdf89a2b026	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)	Record	FiniteSetsIsFiniteSet	True	Passed	Model Under Test Equivalent Model
97eca99ce6dd24545c82b39232faf778e7a3036e	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)	Record	FiniteSetsIsFiniteSet	False	Passed	Model Under Test Equivalent Model
b27b04ed6a2173339b8cf459b7a4b4432ba944ba	Apalache	Record	FiniteSetsCardinality	True	Passed	Model Under Test Equivalent Model
0dd9104e344f15b86dd76c19b962c81d38d4a137	Apalache	Record	FiniteSetsCardinality	False	Passed	Model Under Test Equivalent Model
4c533603977cd5ba01ff747dc37e75f8717a7dcc	Apalache	Record	SeqHead	True	Passed	Model Under Test Equivalent Model
691a7dd5994921372739d395b11752528a6cad29	Apalache	Record	SeqHead	False	Passed	Model Under Test Equivalent Model
4bbba3803e3b308f0730b715a5c0ec6f43983bda	Apalache	Record	SeqTail	True	Passed	Model Under Test Equivalent Model
9480281110f8df3b98c52b3ff1322c08aaf56d1d	Apalache	Record	SeqTail	False	Passed	Model Under Test Equivalent Model
2878769febd379ed363b34e6f20aa9b1c4cd9b97	Apalache	Record	SeqAppend	True	Passed	Model Under Test Equivalent Model
eff7fac0be2feba9f099786ff3b2ca837c0c5ea5	Apalache	Record	SeqAppend	False	Passed	Model Under Test Equivalent Model

Index

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