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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
7d16716b10edb275a80f7f331cbe4aa02a004d6a	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Assume	OneLineComment	True	Passed	Model Under Test Equivalent Model
3cf9c4868721dd12e32ab6d6105bd5001c8e11ef	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Assume	OneLineComment	False	Passed	Model Under Test Equivalent Model
fde011fac526463c5e0f777a2e8f226ac3581354	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Assume	MultiLineComment	True	Passed	Model Under Test Equivalent Model
43d8879bbf03686d75d13dc9df0b9196f7f2b468	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Assume	MultiLineComment	False	Passed	Model Under Test Equivalent Model
11147a90621e63c3fe4020d7047ae42169cec33d	Apalache	Assume	BoolTrue	True	Passed	Model Under Test Equivalent Model
9dbd44f2f1c1a214ed7c38f562084529364ad0c0	Apalache	Assume	BoolTrue	False	Passed	Model Under Test Equivalent Model
2a4eddf14b8b28638c031964f594239d9d39d869	Apalache	Assume	BoolFalse	True	Passed	Model Under Test Equivalent Model
be4148cfbd9a57f8456c1235c223377ee61b5f4a	Apalache	Assume	BoolFalse	False	Passed	Model Under Test Equivalent Model
b889191a8d3e9f6beafeff003f75d2caa0c392ee	Apalache	Assume	And	True	Passed	Model Under Test Equivalent Model
42fed1a230c67500cd5a0dbc6d9667e43f95eb62	Apalache	Assume	And	False	Passed	Model Under Test Equivalent Model
825ea29f35db45f630203d753cd025eb5d495ae1	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	Assume	AndMultiLine	True	Passed	Model Under Test Equivalent Model
f80e9519746f84b68b52e7f911a0220fbca1e924	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	Assume	AndMultiLine	False	Passed	Model Under Test Equivalent Model
598cc46b2e06f2eb2ff9f4660f2a5290c9a0d3b9	Apalache	Assume	Imply	True	Passed	Model Under Test Equivalent Model
7372b7042f867bb368b2467b26c688b404519251	Apalache	Assume	Imply	False	Passed	Model Under Test Equivalent Model
c6993462344521884eee0827d1eb34890bac66ea	Apalache	Assume	Not	True	Passed	Model Under Test Equivalent Model
ab1ed1527c6e1d15d04eff06e048d59c2dad1506	Apalache	Assume	Not	False	Passed	Model Under Test Equivalent Model
b513a9e49035f2cd5901bce5c87818bb0a4846f5	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	Assume	Or	True	Passed	Model Under Test Equivalent Model
dd43b4deb41df4c1dbdc688dad04153e885932c6	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	Assume	Or	False	Passed	Model Under Test Equivalent Model
3309262ca11facc33bcef5f3554595b39dd0006c	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	Assume	OrMultiLine	True	Passed	Model Under Test Equivalent Model
0878f5c13d86e7d3b61ad9708996c9ab4303650b	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	Assume	OrMultiLine	False	Passed	Model Under Test Equivalent Model
f5c7f8fbe4822a54911188e408ae2371d0783785	Apalache	Assume	Eq	True	Passed	Model Under Test Equivalent Model
cf155353f4bf4543868f88a8aa0a21987f554f29	Apalache	Assume	Eq	False	Passed	Model Under Test Equivalent Model
5ec61836126644c77de60ce3a1944fc822465812	Apalache	Assume	Ne	True	Passed	Model Under Test Equivalent Model
33bc8bbed4d5ca9e878a70052223e0cc132c4631	Apalache	Assume	Ne	False	Passed	Model Under Test Equivalent Model
af51207f3a842721866d61e8c130eb309e4df84b	Apalache	Assume	Let	True	Passed	Model Under Test Equivalent Model
cb19c183b03f8f7c5283c5d353351815e5a1a71a	Apalache	Assume	Let	False	Passed	Model Under Test Equivalent Model
698f0e719536ac2bed8efd376ca9432b55f31c06	Apalache	Assume	In	True	Passed	Model Under Test Equivalent Model
05c24fc729ea07bea57b84b0865c23bc77ea84eb	Apalache	Assume	In	False	Passed	Model Under Test Equivalent Model
51d55bf898256dce6f782cfcabc4fad5b213cd8c	Apalache	Assume	NotIn	True	Passed	Model Under Test Equivalent Model
c5ef6eec654badfb46954fbd5fc921b7dfdb412e	Apalache	Assume	NotIn	False	Passed	Model Under Test Equivalent Model
4dbffcce3b3329b78ac3f85a9f6d37fad61bc875	Apalache	Assume	Exists	True	Passed	Model Under Test Equivalent Model
f595523a45eb0583dc0c44528d9637c037672828	Apalache	Assume	Exists	False	Passed	Model Under Test Equivalent Model
8f610c4763fb86c80715558a062d8c33f018d3ef	Apalache	Assume	Forall	True	Passed	Model Under Test Equivalent Model
a230c8f3c63aed509630d5dd0905c4b3f3fd2b03	Apalache	Assume	Forall	False	Passed	Model Under Test Equivalent Model
c05196a9329c7177ad6b31c5281e0f26d2287f00	Apalache	Assume	Choose	True	Passed	Model Under Test Equivalent Model
3b04ad5777d68c0c32385956e5e38deced1dcc2b	Apalache	Assume	Choose	False	Passed	Model Under Test Equivalent Model
5bcc00b89787c3fe878e67d2898bdbc850db657c	Apalache	Assume	FunApp	True	Passed	Model Under Test Equivalent Model
22821b66d469783b5f9e59603976b212fe2abcdb	Apalache	Assume	FunApp	False	Passed	Model Under Test Equivalent Model
402af71f13b2e538c15ac6a217e4f57e74be0881	Apalache	Assume	NumGt	True	Passed	Model Under Test Equivalent Model
1f0e1169d050c0ffaf0ef642144657085fc77198	Apalache	Assume	NumGt	False	Passed	Model Under Test Equivalent Model
4a9e811a77a149043c69245ef0bc107d8a9e4248	Apalache	Assume	NumGe	True	Passed	Model Under Test Equivalent Model
e20c72b428a59fa8f9b802c40a8ce7994da1f00d	Apalache	Assume	NumGe	False	Passed	Model Under Test Equivalent Model
f1071c031b4f44f6105d51e8e7ecd8e09e3ddbb6	Apalache	Assume	NumLt	True	Passed	Model Under Test Equivalent Model
65928f3ce77febe2eb9b193cd546b570c7ba5149	Apalache	Assume	NumLt	False	Passed	Model Under Test Equivalent Model
9907a68d07c8e523e66fb81348af0eb32c1cb759	Apalache	Assume	NumLe	True	Passed	Model Under Test Equivalent Model
261c78ee44da22391af12427bcff7c197a652241	Apalache	Assume	NumLe	False	Passed	Model Under Test Equivalent Model
da917272e4ea53b6a4115aa4321e838b007b6148	Apalache	Assume	Def0	True	Passed	Model Under Test Equivalent Model
881c59d8dd7cf0bb069b3e5c14ab004bf3407289	Apalache	Assume	Def0	False	Passed	Model Under Test Equivalent Model
077311c1999faa37a5cf410cc1ed5c817ee48662	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Assume	LetDef0	True	Passed	Model Under Test Equivalent Model
b42a31ebb559dde38e55a797362070a58b1bb126	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Assume	LetDef0	False	Passed	Model Under Test Equivalent Model
b7f2bd019911ce4e06ffe40ea2dd97af9397df6e	Apalache	Assume	Def1	True	Passed	Model Under Test Equivalent Model
a36cd012155c56d6ae23666317628a4441d9c580	Apalache	Assume	Def1	False	Passed	Model Under Test Equivalent Model
9d6969fc073ffb0c68159847d4d390acd38ae5b7	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Assume	LetDef1	True	Passed	Model Under Test Equivalent Model
5934eb707225d137375ea4259f3e0cd5d14fa896	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Assume	LetDef1	False	Passed	Model Under Test Equivalent Model
102fbc98a065890d073b027a591d1aaa72756f14	Apalache	Assume	Def2	True	Passed	Model Under Test Equivalent Model
e0fa808a7c3a757fd3d50fc7d0c0ffb3fd840434	Apalache	Assume	Def2	False	Passed	Model Under Test Equivalent Model
1e6f972dc5f0caabdc52840860a3c9e9f29005af	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Assume	LetDef2	True	Passed	Model Under Test Equivalent Model
e66657e0e2bb8f89c0d8d4b7493f3e0f5c6227a0	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Assume	LetDef2	False	Passed	Model Under Test Equivalent Model
176c667c92d7c4c77ccb2efbda51417006189ea2	Apalache	Assume	Def1Recursive	True	Passed	Model Under Test Equivalent Model
1fde01ccf66764d165d9d0541618fdc0e93d4c2b	Apalache	Assume	Def1Recursive	False	Passed	Model Under Test Equivalent Model
ec877c0f547b9a93b9321a3e5e6e578d139bd37a	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Assume	LetDef1Recursive	True	Passed	Model Under Test Equivalent Model
cfa66d7cf029ec7046a18df703423277117e3cd4	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Assume	LetDef1Recursive	False	Passed	Model Under Test Equivalent Model
485ecfec173c66c843b7307d6106172e487e64d0	Apalache	Assume	Extends	True	Passed	Model Under Test Equivalent Model
94b0d3fd818fadb3ca859817f838524d06a4f545	Apalache	Assume	Extends	False	Passed	Model Under Test Equivalent Model
db4e826185da6fc08da66905a8ce3d3a42d0417c	Apalache	Assume	ExtendsInDifferentFolder	True	Passed	Model Under Test Equivalent Model
454deffac84956b1aa11cc632a6a641a9d4b7938	Apalache	Assume	ExtendsInDifferentFolder	False	Passed	Model Under Test Equivalent Model
2212d5722e3ba11be7fa3bd778f8bcefccc4c238	Apalache	Assume	Constant	True	Passed	Model Under Test Equivalent Model
30fc56d37c1c1b3003277d4889b88169bc981030	Apalache	Assume	Constant	False	Passed	Model Under Test Equivalent Model
f0ef9fc1a561d95b941efc3372a20bd184ac92dd	Apalache	Assume	ConstantRank1	True	Passed	Model Under Test Equivalent Model
1e23a52d63459f10c3ce338256e9959884348313	Apalache	Assume	ConstantRank1	False	Passed	Model Under Test Equivalent Model
d0201764396b58ecda07652722848410bda73431	Apalache	Assume	Instance	True	Passed	Model Under Test Equivalent Model
3859307b43c261d675a23426a3e7ec888d49dc50	Apalache	Assume	Instance	False	Passed	Model Under Test Equivalent Model
54ead1e53a735a239365d925a0dfda87216d37d4	Apalache	Assume	InstanceWith	True	Passed	Model Under Test Equivalent Model
d181f0620b05c7dba72d3aaa0ebf8a9d03c47dda	Apalache	Assume	InstanceWith	False	Passed	Model Under Test Equivalent Model
672ee0f7a8d9f929c6714eb320b97516a4158e3a	Apalache	Assume	InstanceNamed	True	Passed	Model Under Test Equivalent Model
b5011c455f53e2bfe8cdbbe74cf1f90dcbfb2b18	Apalache	Assume	InstanceNamed	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
61d7ac904a416b3aef63155b08e9fce6c5b04de5	Apalache	Assume	InstanceInFolder	True	Passed	Model Under Test Equivalent Model
b2a14f5233d3baf53cf8c2d98b72df2fa89176b4	Apalache	Assume	InstanceInFolder	False	Passed	Model Under Test Equivalent Model
2bc8c9e1117ba8c5ab9af14973e0d7c3ec9b3da8	Apalache	Assume	InstanceWithInFolder	True	Passed	Model Under Test Equivalent Model
52b956f83ec60fad9ebf1544aa6fe88c92287bc9	Apalache	Assume	InstanceWithInFolder	False	Passed	Model Under Test Equivalent Model
478c093cc444db03766bd9683c72c4b37818bfa8	Apalache	Assume	InstanceNamedInFolder	True	Passed	Model Under Test Equivalent Model
d9896e178a3cd3a1372eab5e85a15d49733a3c27	Apalache	Assume	InstanceNamedInFolder	False	Passed	Model Under Test Equivalent Model
c1ce983b9051e8ad53d279cbf840461fede0b36f	Apalache	Assume	InstanceNamedWithInFolder	True	Passed	Model Under Test Equivalent Model
5cf737cb97e02ef4fbc5c00048ce2073a3777305	Apalache	Assume	InstanceNamedWithInFolder	False	Passed	Model Under Test Equivalent Model
45dd31ed60b43a5c79a36332d8e21394d0bda955	Apalache	Assume	SubsetEq	True	Passed	Model Under Test Equivalent Model
89a13a5014ddc948e2be7537746b23a8c0747b47	Apalache	Assume	SubsetEq	False	Passed	Model Under Test Equivalent Model
e25336e6b8a1736390e405d5ed1be3f8c32c19b5	Apalache	Assume	IfCond	True	Passed	Model Under Test Equivalent Model
baa4b34fee31f590342255e1e1abe2123dd1c7a3	Apalache	Assume	IfCond	False	Passed	Model Under Test Equivalent Model
72cebba49dbc4c733e0799d0239d4b6f5f0c56bb	Apalache	Assume	IfThen	True	Passed	Model Under Test Equivalent Model
ceaa8bda28291e69ac68d2a6b4e1e81cef93cd71	Apalache	Assume	IfThen	False	Passed	Model Under Test Equivalent Model
0a9b6e25f11c5fc08f3215232019a787687598cb	Apalache	Assume	IfElse	True	Passed	Model Under Test Equivalent Model
b14104566cfa4a53b860e9a0774c37d9304bc27c	Apalache	Assume	IfElse	False	Passed	Model Under Test Equivalent Model
7b653616ebc284cd2c57db5be8cb83a8acf34de1	Apalache	Assume	Equivalence	True	Passed	Model Under Test Equivalent Model
4512cc5ac3953cf381cda2ef930772e112090c80	Apalache	Assume	Equivalence	False	Passed	Model Under Test Equivalent Model
20319bb79c714c5c4c00b53782996c92273e9cd5	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	Assume	TlcEval	True	Passed	Model Under Test Equivalent Model
d2586b6b7f30d025f24a82d123f4517fbf97a42c	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	Assume	TlcEval	False	Passed	Model Under Test Equivalent Model
63e029213e913466172281e8378b44c16fd7519e	Apalache	Assume	BagBagIn	True	Passed	Model Under Test Equivalent Model
72664287f1a7535210d4d448adb65d675b47366b	Apalache	Assume	BagBagIn	False	Passed	Model Under Test Equivalent Model
a862e5ceb09586301621e9618dbc89da2d3cbdb8	Apalache	Assume	BagSubsetEqBag	True	Passed	Model Under Test Equivalent Model
d4bf314cb195558de5b903ff1ed97f05a4411109	Apalache	Assume	BagSubsetEqBag	False	Passed	Model Under Test Equivalent Model
f9e21eb5fa88931576ec69275ae6a07b6410aa7e	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)	Assume	FiniteSetsIsFiniteSet	True	Passed	Model Under Test Equivalent Model
d0c6f32fea16d309c012bd6727ac6a2a55629d0d	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)	Assume	FiniteSetsIsFiniteSet	False	Passed	Model Under Test Equivalent Model
d7f6ecd8d08e9146513dee334b7fc5fb14efefd9	Apalache	Assume	SeqHead	True	Passed	Model Under Test Equivalent Model
ca0420a0600e7b1d9a5c6bf8657637798f9668d1	Apalache	Assume	SeqHead	False	Passed	Model Under Test Equivalent Model

Index

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