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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
b4227716d4f6085350c6d6d6be5b5fdad2ce7b65	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Exists	OneLineComment	True	Passed	Model Under Test Equivalent Model
8140ae37b1c30084ae5e2604349f3bc1cd4dccea	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Exists	OneLineComment	False	Passed	Model Under Test Equivalent Model
b2a6ecf0c9c2b86d52b6cc1d49f6c3d122360540	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Exists	MultiLineComment	True	Passed	Model Under Test Equivalent Model
65595d7d1d893a6aff5b40eba9f63a132884388d	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Exists	MultiLineComment	False	Passed	Model Under Test Equivalent Model
53dc8ead63bf1c4509df8d87225b349e254c1700	Apalache	Exists	BoolTrue	True	Passed	Model Under Test Equivalent Model
5747a4215238c2b8f70f293df80a8b3279ca42f6	Apalache	Exists	BoolTrue	False	Passed	Model Under Test Equivalent Model
935d74d83c98c4d11211c89f0203b8ded3cbc310	Apalache	Exists	BoolFalse	True	Passed	Model Under Test Equivalent Model
156c890d66f192fa1b2ec431b1514dba876741b3	Apalache	Exists	BoolFalse	False	Passed	Model Under Test Equivalent Model
5332141224a2d3fc948c1be832a3c6aa96666574	Apalache	Exists	And	True	Passed	Model Under Test Equivalent Model
56f02cf1d0802de9f601dacb7b5ebab4a6ad3fd5	Apalache	Exists	And	False	Passed	Model Under Test Equivalent Model
8636c774642e823c7b946d8fd70cbb84a97bbd00	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	Exists	AndMultiLine	True	Passed	Model Under Test Equivalent Model
1766e75b122742fdd1bef416c53f3f6dc014d52c	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	Exists	AndMultiLine	False	Passed	Model Under Test Equivalent Model
f86c676b49b6daceb3590912de2d68de7beba028	Apalache	Exists	Imply	True	Passed	Model Under Test Equivalent Model
3447f92bd9737cdc1755511b8808994e0d05af43	Apalache	Exists	Imply	False	Passed	Model Under Test Equivalent Model
328de057e68d8059306b85730850a298641410c1	Apalache	Exists	Not	True	Passed	Model Under Test Equivalent Model
6b9f597b80bd75c11a3077126df645393e3d51b9	Apalache	Exists	Not	False	Passed	Model Under Test Equivalent Model
cc0f90d95a246a7c8c55ce28c4b02ff3b6139308	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	Exists	Or	True	Passed	Model Under Test Equivalent Model
0ad62d05ed9820dd33f66ac76446808ac69b9f5d	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	Exists	Or	False	Passed	Model Under Test Equivalent Model
24bbb675bb5fc1caf511376925c4fc5304577e62	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	Exists	OrMultiLine	True	Passed	Model Under Test Equivalent Model
e1bb3645fde4bca23ecbd92444368d545021ff85	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	Exists	OrMultiLine	False	Passed	Model Under Test Equivalent Model
688ac68ae5f77aa869aadfc6e0d602a994919ae6	Apalache	Exists	Eq	True	Passed	Model Under Test Equivalent Model
8ce1670fc48d4e2fecd49597607e8941f078c190	Apalache	Exists	Eq	False	Passed	Model Under Test Equivalent Model
a7860d94284a772f1757fd879d00da9e005be967	Apalache	Exists	Ne	True	Passed	Model Under Test Equivalent Model
9a50172b37b783885e1562931b97c021bf55678e	Apalache	Exists	Ne	False	Passed	Model Under Test Equivalent Model
5b2a3533162dff034d56036fffed406db9ba9967	Apalache	Exists	Let	True	Passed	Model Under Test Equivalent Model
3fa5ab0ba7bbc76f27a0607426319584f48b628a	Apalache	Exists	Let	False	Passed	Model Under Test Equivalent Model
ca671148bca3af9e5b425b0f4cb3f8c23fc449d4	Apalache	Exists	In	True	Passed	Model Under Test Equivalent Model
d31001880926a1e6aa491e29ea925f2ae2485247	Apalache	Exists	In	False	Passed	Model Under Test Equivalent Model
38f82774379bc72569da49066f02992f0465e87f	Apalache	Exists	NotIn	True	Passed	Model Under Test Equivalent Model
c53868d21b28a0f3401076648fda4a2bf79db959	Apalache	Exists	NotIn	False	Passed	Model Under Test Equivalent Model
05f0c757ef74c3548f82af4f943646d7b0a0a0a1	Apalache	Exists	Exists	True	Passed	Model Under Test Equivalent Model
167b4a9e00643baf9424f1a445f5252904dcde18	Apalache	Exists	Exists	False	Passed	Model Under Test Equivalent Model
d6df8c6837cc711146c2d6d7c2e24ff2a94d0a97	Apalache	Exists	Forall	True	Passed	Model Under Test Equivalent Model
4c7aea0c82e48014ace4c36e7d1e1162727caa27	Apalache	Exists	Forall	False	Passed	Model Under Test Equivalent Model
8e8233774b3b90bc20f5698c693cb15bf40eb2ae	Apalache	Exists	Choose	True	Passed	Model Under Test Equivalent Model
2c339cbf924a5eef0f764c72b45e2ab0d6fb29e5	Apalache	Exists	Choose	False	Passed	Model Under Test Equivalent Model
1afe202b8279350f0e888eceb1cadbdb80690cf4	Apalache	Exists	FunApp	True	Passed	Model Under Test Equivalent Model
3d9808f9c8b886d0fc71ea37fd4d9695c4f147d9	Apalache	Exists	FunApp	False	Passed	Model Under Test Equivalent Model
253234aab29f13790e177e8572cb9593093c253d	Apalache	Exists	Prime	True	Passed	Model Under Test Equivalent Model
7fbdcd7abf96ffb5ae7fb46f96aa25a958b9296e	Apalache	Exists	Prime	False	Passed	Model Under Test Equivalent Model
73cae06e4a70be8784fbd804f0053391473bdd70	Apalache	Exists	NumGt	True	Passed	Model Under Test Equivalent Model
9fd5293680005520e9a6d96baee4bf13b7de63ac	Apalache	Exists	NumGt	False	Passed	Model Under Test Equivalent Model
e35e6a60ea2e92e4d4bf3ed68816e773d37865c7	Apalache	Exists	NumGe	True	Passed	Model Under Test Equivalent Model
159f0a3318be44990ba1c97da08984e95ee2f687	Apalache	Exists	NumGe	False	Passed	Model Under Test Equivalent Model
d9e6c2419e17befe5cde1219bdc69d68543f93e9	Apalache	Exists	NumLt	True	Passed	Model Under Test Equivalent Model
b3a724c3da44c5814b219578f7c42d1bc00b0b61	Apalache	Exists	NumLt	False	Passed	Model Under Test Equivalent Model
e0b7429fb1701c90407f170ac70902cce8aea6fa	Apalache	Exists	NumLe	True	Passed	Model Under Test Equivalent Model
7c9f5def29b95d03454b01ea9a2fc876d75ddccc	Apalache	Exists	NumLe	False	Passed	Model Under Test Equivalent Model
ae1eceb90a58ea4bc1ec2c6d4ec635acc64bf411	Apalache	Exists	Def0	True	Passed	Model Under Test Equivalent Model
b4bca5e75340e5384d4905eca52c2ec36b2cdd68	Apalache	Exists	Def0	False	Passed	Model Under Test Equivalent Model
a6d584f4791c3566826ae3bd5237a136a1e0e342	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Exists	LetDef0	True	Passed	Model Under Test Equivalent Model
17a520bcf3cae1e08efcdc6348a49ceabb4d9e1a	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Exists	LetDef0	False	Passed	Model Under Test Equivalent Model
cd3a64e17c9c981a743626fbd7e48bbc16df6138	Apalache	Exists	Def1	True	Passed	Model Under Test Equivalent Model
3c722091382a378fdd91cbcb8094de7e10e69215	Apalache	Exists	Def1	False	Passed	Model Under Test Equivalent Model
871331f1b4c05021ee31002982cb99034f20c1bf	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Exists	LetDef1	True	Passed	Model Under Test Equivalent Model
d04818f8a5dbb1d64b8b2db37ce11748dca4140a	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Exists	LetDef1	False	Passed	Model Under Test Equivalent Model
85543fd52d0f7c1090c89f03ed7dbf00d81e11d0	Apalache	Exists	Def2	True	Passed	Model Under Test Equivalent Model
a717a6c24356db1fdd31e4b40c734fed474dd7ac	Apalache	Exists	Def2	False	Passed	Model Under Test Equivalent Model
6dc24a161919e3c6367b81e8180de9e21bdf7512	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Exists	LetDef2	True	Passed	Model Under Test Equivalent Model
da26503ee0a3e3acece8234314dc2bfbc931d9cf	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Exists	LetDef2	False	Passed	Model Under Test Equivalent Model
7ff9232fc49e7439f93746a16ecc2298d50f9e7b	Apalache	Exists	Def1Recursive	True	Passed	Model Under Test Equivalent Model
f5ae8b2cf7ba4e3f0b242ca845743a82da53575e	Apalache	Exists	Def1Recursive	False	Passed	Model Under Test Equivalent Model
e66a77b14d21bed3817ff2dd8a71e1d5659415b5	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Exists	LetDef1Recursive	True	Passed	Model Under Test Equivalent Model
1a2b9109ef68cd1f8ab20d75369055a62dea0bca	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Exists	LetDef1Recursive	False	Passed	Model Under Test Equivalent Model
c5a44c3485e874507261eec8f7b2a24b1c5be4d3	Apalache	Exists	Extends	True	Passed	Model Under Test Equivalent Model
dd57e437e7a69bc6dc200b753bc7625d2b4ed886	Apalache	Exists	Extends	False	Passed	Model Under Test Equivalent Model
29d4c7a72b2eaec1910705593709d1c34120a386	Apalache	Exists	ExtendsInDifferentFolder	True	Passed	Model Under Test Equivalent Model
34c0d758fd2905abf0f5b39916e375ab81b93766	Apalache	Exists	ExtendsInDifferentFolder	False	Passed	Model Under Test Equivalent Model
efd45114c1f72007e3f78226825fef24daef53eb	Apalache	Exists	Variable	True	Passed	Model Under Test Equivalent Model
7f0a9dc36d66113bbfb23a2ea743b5d26bb42315	Apalache	Exists	Variable	False	Passed	Model Under Test Equivalent Model
2c3145216ad21e6cd743576dc48f17b67028ebb1	Apalache	Exists	Constant	True	Passed	Model Under Test Equivalent Model
5e992921269c5391abcc879a7ae029cc589dc944	Apalache	Exists	Constant	False	Passed	Model Under Test Equivalent Model
d4c0e3d0f6cb5bc488111f25fa16607e88b54e88	Apalache	Exists	ConstantRank1	True	Passed	Model Under Test Equivalent Model
2da2951fa4e7196827aeea4494f5b3e00e58b317	Apalache	Exists	ConstantRank1	False	Passed	Model Under Test Equivalent Model
a7cc1d5f22b31ef71af6b28db1d78a18badd5407	Apalache	Exists	Instance	True	Passed	Model Under Test Equivalent Model
4770a8762008f7c0024dfc0bbd1743b94cd688c9	Apalache	Exists	Instance	False	Passed	Model Under Test Equivalent Model
44e10088791c0264a72924ccbca6fd6523071dee	Apalache	Exists	InstanceWith	True	Passed	Model Under Test Equivalent Model
2fbcb2229245f20efa43c4c7b9e255687dc3ad6d	Apalache	Exists	InstanceWith	False	Passed	Model Under Test Equivalent Model
341a1df8ba3e4f85539ac6e5fd8f8864327d69db	Apalache	Exists	InstanceNamed	True	Passed	Model Under Test Equivalent Model
f419e4eedfb0709cd1bcf40aab83afc29997e82d	Apalache	Exists	InstanceNamed	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
4c749db7c56bac76445be1770a8216a695f8db40	Apalache	Exists	InstanceInFolder	True	Passed	Model Under Test Equivalent Model
fa41514bf04a8fc38ef1e86524cfcf7625b37a33	Apalache	Exists	InstanceInFolder	False	Passed	Model Under Test Equivalent Model
61df5851a5b61ef31271390b72c750d182f491e9	Apalache	Exists	InstanceWithInFolder	True	Passed	Model Under Test Equivalent Model
684a2ff71e741d2d04dd5d091b74a49800e7c03d	Apalache	Exists	InstanceWithInFolder	False	Passed	Model Under Test Equivalent Model
a52c9a7136b164fa9507b07a97a613c9d2311d7b	Apalache	Exists	InstanceNamedInFolder	True	Passed	Model Under Test Equivalent Model
a2ca75617130a0d4784c7788cb8c890742e05a31	Apalache	Exists	InstanceNamedInFolder	False	Passed	Model Under Test Equivalent Model
26186d7c39d260e1ebb11d07a35077ba3b62f4b1	Apalache	Exists	InstanceNamedWithInFolder	True	Passed	Model Under Test Equivalent Model
30be5ae6d2881e0e0faebe4b0ebce721aa2d637c	Apalache	Exists	InstanceNamedWithInFolder	False	Passed	Model Under Test Equivalent Model
820985ec5d4a1b834361483f91072b181db23333	Apalache	Exists	Enabled	True	Passed	Model Under Test Equivalent Model
b080300d3bedd92760638d514969b90e90bd7a55	Apalache	Exists	Enabled	False	Passed	Model Under Test Equivalent Model
75a4a11f4d1a8bb9b9bd497066e058a52f364de2	Apalache	Exists	SubsetEq	True	Passed	Model Under Test Equivalent Model
258744b787bbc7f7506ceef1751d2b556268050b	Apalache	Exists	SubsetEq	False	Passed	Model Under Test Equivalent Model
62a5248e4b3606d94a4d0e2ce917d2b098a5e062	Apalache	Exists	IfCond	True	Passed	Model Under Test Equivalent Model
253a342b74a8e96fafe2769cbda8ef368f31abd0	Apalache	Exists	IfCond	False	Passed	Model Under Test Equivalent Model
cffcdea3282830f2444ef8822fab1aeb2dc4a525	Apalache	Exists	IfThen	True	Passed	Model Under Test Equivalent Model
e8799b282f9b6b3a88b00c773da59125bfeba06d	Apalache	Exists	IfThen	False	Passed	Model Under Test Equivalent Model
634a11501090b257098922a4349c9f4374f51d5a	Apalache	Exists	IfElse	True	Passed	Model Under Test Equivalent Model
a7bbb96492536c009102373e790b5ba31edd3d3b	Apalache	Exists	IfElse	False	Passed	Model Under Test Equivalent Model
0659312890300a44ca36e4835956884bf7ca77c1	Apalache	Exists	Unchanged	True	Passed	Model Under Test Equivalent Model
5221ac322273caea196c8760d043c0e48f7d5497	Apalache	Exists	Unchanged	False	Passed	Model Under Test Equivalent Model
c680a9cf2a7390c138d71a776011496986d9ccb2	Apalache	Exists	Equivalence	True	Passed	Model Under Test Equivalent Model
345141e00fa3e8e258678086771a009f691006b3	Apalache	Exists	Equivalence	False	Passed	Model Under Test Equivalent Model
83937cdcfd170ba3cece247ef9e8ffe565d25945	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	Exists	TlcEval	True	Passed	Model Under Test Equivalent Model
2377837f19a8d6e252f2fe256e5d20078e2e739d	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	Exists	TlcEval	False	Passed	Model Under Test Equivalent Model
52ac2555ada96addccc00de61adc58e84c93f32a	Apalache	Exists	BagBagIn	True	Passed	Model Under Test Equivalent Model
dc308f74c1774fac273865287ccd880e7464d968	Apalache	Exists	BagBagIn	False	Passed	Model Under Test Equivalent Model
4e851d9d4136f6e254a0ad7403a12a8be7e96fcd	Apalache	Exists	BagSubsetEqBag	True	Passed	Model Under Test Equivalent Model
22f3f8ecd0efc2f32ad3c43f061da2cfb4fab75d	Apalache	Exists	BagSubsetEqBag	False	Passed	Model Under Test Equivalent Model
8878d85203d0fe50df20d9848bfdebaae190004c	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)	Exists	FiniteSetsIsFiniteSet	True	Passed	Model Under Test Equivalent Model
f7df3c47d734ffc6963ab341bcb6e91eabe76900	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)	Exists	FiniteSetsIsFiniteSet	False	Passed	Model Under Test Equivalent Model
f7df349975c76f4644791da923dd9a637f9b9c9b	Apalache	Exists	SeqHead	True	Passed	Model Under Test Equivalent Model
d396c936081195a136c435204ff48529c427fa07	Apalache	Exists	SeqHead	False	Passed	Model Under Test Equivalent Model

Index

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