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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
ea85a75714b02907d998ad5818526102ba5a4238	Apalache	Eq	NumPlus	True	Passed	Model Under Test Equivalent Model
1983b8f9a7e57585404f36213378778c2f4c7ce1	Apalache	Eq	NumPlus	False	Passed	Model Under Test Equivalent Model
90a3081d76a1621090056895be27bbf7269b9f6c	Apalache	Ne	NumPlus	True	Passed	Model Under Test Equivalent Model
e1e6188ef72cf1aac1079ee71674d2eada1dda21	Apalache	Ne	NumPlus	False	Passed	Model Under Test Equivalent Model
cd9d58b53fdf6eadbb842e865a69def8890396f9	Apalache	Let	NumPlus	True	Passed	Model Under Test Equivalent Model
3d9cfbce17f322b8ba1f3c2c1628949b9352375a	Apalache	Let	NumPlus	False	Passed	Model Under Test Equivalent Model
1a2740f26dc14e8331a15c472b54add4efba2a4c	Apalache	Set0	NumPlus	True	Passed	Model Under Test Equivalent Model
8adc4dce77512286969ee636eb6ef19f23cf0dd1	Apalache	Set0	NumPlus	False	Passed	Model Under Test Equivalent Model
2f272dc80c213e54f47ba0d64fcb819da0c953fc	Apalache	Set1	NumPlus	True	Passed	Model Under Test Equivalent Model
b2fb1e4576666494021090509c77206b04a2a5b5	Apalache	Set1	NumPlus	False	Passed	Model Under Test Equivalent Model
5d5b0e7a28ad5d9ca87464bb90086a5af14c8800	Apalache	Set2	NumPlus	True	Passed	Model Under Test Equivalent Model
bfa70f4e4cf690ed1e3916f848c305c20670d5db	Apalache	Set2	NumPlus	False	Passed	Model Under Test Equivalent Model
90f9f752939990a869b0c54a794910ae8fa744cf	Apalache	Fun	NumPlus	True	Passed	Model Under Test Equivalent Model
9cbb8f815ba72d544100aee3d7820a7e01a3f050	Apalache	Fun	NumPlus	False	Passed	Model Under Test Equivalent Model
7c008c140f8a4a51705dbffd099177c15541a2c3	Apalache	In	NumPlus	True	Passed	Model Under Test Equivalent Model
b928b07c5820bce7de2a33d3ebafd30f01b4fae4	Apalache	In	NumPlus	False	Passed	Model Under Test Equivalent Model
16243f75aa18dcb285f600f4da74de9fbb76be86	Apalache	NotIn	NumPlus	True	Passed	Model Under Test Equivalent Model
6d18cee8236e0d0edbe83ad59409d9b8eacaa285	Apalache	NotIn	NumPlus	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
a6b60c3dd223f5a602a6f8a1b27082e80a655312	Apalache	Tuple	NumPlus	True	Passed	Model Under Test Equivalent Model
4939f273c92e847f80f294250ce5ac789be8ecd9	Apalache	Tuple	NumPlus	False	Passed	Model Under Test Equivalent Model
9fa9058f7693d149ec6d2c787afd5e3cea5ed27a	Apalache	FunApp	NumPlus	True	Passed	Model Under Test Equivalent Model
2c97657efa7bc7ac6e2276f85494960df8c8bcf6	Apalache	FunApp	NumPlus	False	Passed	Model Under Test Equivalent Model
a97cba1cc825c722170d48902a63342333f1bdba	Apalache	Except1Fun	NumPlus	True	Passed	Model Under Test Equivalent Model
5182bbe9b6c811e116417dedccb6783d59928410	Apalache	Except1Fun	NumPlus	False	Passed	Model Under Test Equivalent Model
0158f62ead11f23f3e3f0df9f8374435e4cf1c44	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	NumPlus	True	Passed	Model Under Test Equivalent Model
6ec111d2490f07a82b8d8960d557f98d88b17ad1	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	NumPlus	False	Passed	Model Under Test Equivalent Model
7e3c5fa9f422eb02f94c1329f4ee40a382253c91	Apalache	Except1Rec	NumPlus	True	Passed	Model Under Test Equivalent Model
6f876d2acc2239a23e98e747feb86a986975674c	Apalache	Except1Rec	NumPlus	False	Passed	Model Under Test Equivalent Model
6dee216df3120201abaa6b7400ac2e064717e2a2	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	NumPlus	True	Passed	Model Under Test Equivalent Model
8a5437c0fb7c8bc5a73084a2faf6ca4eda2a51af	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	NumPlus	False	Passed	Model Under Test Equivalent Model
810efe13e8895804a9403b62c215c66dcc95951f	Apalache	Except2Fun	NumPlus	True	Passed	Model Under Test Equivalent Model
d4c28b1e76eb4f0e5bbe816c90deb0d852f9171b	Apalache	Except2Fun	NumPlus	False	Passed	Model Under Test Equivalent Model
18399ecbf63d99d1ae692d0d9fee8b4e49cfba02	Apalache	Prime	NumPlus	True	Passed	Model Under Test Equivalent Model
3ee17945cc1c6d4e1a63fdfce36e1ee7878c7405	Apalache	Prime	NumPlus	False	Passed	Model Under Test Equivalent Model
78e2bfb1f5d7523e3a66be18aa42a074348a6192	Apalache	NumUnaryMinus	NumPlus	True	Passed	Model Under Test Equivalent Model
d4b39f2ec46f58e0f95b4e59b656775ea8e54e8f	Apalache	NumUnaryMinus	NumPlus	False	Passed	Model Under Test Equivalent Model
2f6bf3ff975dcfe3c9603070dd60fd313204d74b	Apalache	NumPlus	NumPlus	True	Passed	Model Under Test Equivalent Model
75884a4a7ff760a5f04fb3292796f98eb3f05071	Apalache	NumPlus	NumPlus	False	Passed	Model Under Test Equivalent Model
9c99fc5bc817447607d3de4fc71eafc35408adf3	Apalache	NumMinus	NumPlus	True	Passed	Model Under Test Equivalent Model
69658586b0c52595348f393e7305e79e98f036ca	Apalache	NumMinus	NumPlus	False	Passed	Model Under Test Equivalent Model
5981480cc521b4f4816d29258e1ff9581fa1e32e	Apalache	NumMul	NumPlus	True	Passed	Model Under Test Equivalent Model
a0a9d9b1f710d4737fe604fc6f8197427615704f	Apalache	NumMul	NumPlus	False	Passed	Model Under Test Equivalent Model
bb73c5bc7634056770f7a459e8f1b926cc37dcb2	Apalache	NumDiv	NumPlus	True	Passed	Model Under Test Equivalent Model
ac805ce3e370a768e424f65adceabbe925942ab6	Apalache	NumDiv	NumPlus	False	Passed	Model Under Test Equivalent Model
fcae8c653bace3ef21d9f5946d891f7aaa653631	Apalache	NumMod	NumPlus	True	Passed	Model Under Test Equivalent Model
faf8ffac617060f6c703ed22effe42bbe0c7db7e	Apalache	NumMod	NumPlus	False	Passed	Model Under Test Equivalent Model
3d058bd90baf69a446c8af0937eab57fcaaf7fe4	Apalache	NumPow	NumPlus	True	Passed	Model Under Test Equivalent Model
485b763c11a66d67dc5b9a67b7425b789586fe44	Apalache	NumPow	NumPlus	False	Passed	Model Under Test Equivalent Model
280fb08bdd99f87e7d73aae4a8bcae7c9ba422c4	Apalache	NumGt	NumPlus	True	Passed	Model Under Test Equivalent Model
0654c25b5319b8e27b000e844634c6aa696e6fed	Apalache	NumGt	NumPlus	False	Passed	Model Under Test Equivalent Model
a8119699f75415735d4020d32d39a91e46a4e395	Apalache	NumGe	NumPlus	True	Passed	Model Under Test Equivalent Model
3e81c17e46dd4f87e8b265d928498b9e9153bd23	Apalache	NumGe	NumPlus	False	Passed	Model Under Test Equivalent Model
f2eabcbab825be9326c8b269ddafce3653cad325	Apalache	NumLt	NumPlus	True	Passed	Model Under Test Equivalent Model
43ba74e884276ca53b834a7f37043ca2d2a5416a	Apalache	NumLt	NumPlus	False	Passed	Model Under Test Equivalent Model
b01c5e68c3a3098000b85ee17a6aceab3bcdab9f	Apalache	NumLe	NumPlus	True	Passed	Model Under Test Equivalent Model
3af46a4c9031495f15032e5df69eb71dff53babf	Apalache	NumLe	NumPlus	False	Passed	Model Under Test Equivalent Model
70bdb2f7eda1e75c29d3a3550eed143f21bf29d2	Apalache	DefFun	NumPlus	True	Passed	Model Under Test Equivalent Model
3acf953d34894a48e842b263bccde90b6046ddba	Apalache	DefFun	NumPlus	False	Passed	Model Under Test Equivalent Model
6224a7108e44af9737395a58dfb9a5239d4ba928	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	NumPlus	True	Passed	Model Under Test Equivalent Model
e0204cba09bc49b48bd0d95dcdc504e361b4436f	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	NumPlus	False	Passed	Model Under Test Equivalent Model
6ce32bf136e6d3979b55cefef2e428961b357d80	Apalache	DefFunRecursive	NumPlus	True	Passed	Model Under Test Equivalent Model
9068c4a6c1a5d2e91aee00eed0f0a00fa8def8da	Apalache	DefFunRecursive	NumPlus	False	Passed	Model Under Test Equivalent Model
11b3c4f80b757ff1254daebd8acbedcbd6114eb1	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	NumPlus	True	Passed	Model Under Test Equivalent Model
7635428b7e87ded7734a70f7530950dcbcc5a9dd	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	NumPlus	False	Passed	Model Under Test Equivalent Model
d9bf2f7804167c950652b437622ac1ff91342ddb	Apalache	Def0	NumPlus	True	Passed	Model Under Test Equivalent Model
56d4fff94c5c4fe85440970f220b56c10075109f	Apalache	Def0	NumPlus	False	Passed	Model Under Test Equivalent Model
4f4e42a8e4dff8c749f1454967f42ee58074cbe0	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	NumPlus	True	Passed	Model Under Test Equivalent Model
ba5ef2ef2fe37dd01509ee52b491736f1bb47056	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	NumPlus	False	Passed	Model Under Test Equivalent Model
a8e1db3a345c1e51c32a9621c83405ab965613be	Apalache	Def1	NumPlus	True	Passed	Model Under Test Equivalent Model
ce5728a3262819d0c494cc4df7849bcfe19c293b	Apalache	Def1	NumPlus	False	Passed	Model Under Test Equivalent Model
84ad8d699e5341105a96ff44be37c97d79e3bc6a	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	NumPlus	True	Passed	Model Under Test Equivalent Model
7b14412132c0d1d915f00c5fcc97ce5b9fc9d477	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	NumPlus	False	Passed	Model Under Test Equivalent Model
50821a7152e7633a91ab330796b8c836300d4a22	Apalache	Def2	NumPlus	True	Passed	Model Under Test Equivalent Model
cd5d2e7f3614b2c48b5861c11666edc089aa74b1	Apalache	Def2	NumPlus	False	Passed	Model Under Test Equivalent Model
a9760dffcf70b65816fb215f66dceda79dd65f8d	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	NumPlus	True	Passed	Model Under Test Equivalent Model
8952f51105602fb61ac22fd93995b78dd3f072fb	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	NumPlus	False	Passed	Model Under Test Equivalent Model
a509918dd6f62e22298a444cdba3378d36c83d63	Apalache	Def1Recursive	NumPlus	True	Passed	Model Under Test Equivalent Model
9322fae92e2a132a739d0c68fe2bd29a7175a788	Apalache	Def1Recursive	NumPlus	False	Passed	Model Under Test Equivalent Model
3386b4c6cab4727df8cc437f9981eecd2d6634a7	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	NumPlus	True	Passed	Model Under Test Equivalent Model
12599a834d5237448eff5529cc0053bf98ab81de	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	NumPlus	False	Passed	Model Under Test Equivalent Model
2f04536befc2c16ee7c090d6a696bd139d443ea4	Apalache	Extends	NumPlus	True	Passed	Model Under Test Equivalent Model
14b04bd99c8a5e611e972979e20d3489f7dcbe9f	Apalache	Extends	NumPlus	False	Passed	Model Under Test Equivalent Model
4bdaca8ebc4357c8cba5c32e854b9275a1cd1f32	Apalache	ExtendsInDifferentFolder	NumPlus	True	Passed	Model Under Test Equivalent Model
e9005a3056d49a9301b1f419ff0ac763dbd2a8a1	Apalache	ExtendsInDifferentFolder	NumPlus	False	Passed	Model Under Test Equivalent Model
d2362395b8492e72777fc5dbfb7dcf5d53765d1d	Apalache	Variable	NumPlus	True	Passed	Model Under Test Equivalent Model
415bb74f5124f9c77c487103a0726e2e054d00f9	Apalache	Variable	NumPlus	False	Passed	Model Under Test Equivalent Model
737fb5c76c7007b9d4026445e251773cadb71485	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	NumPlus	True	Passed	Model Under Test Equivalent Model
4b724f47feb7be1e929a380e522dd7441a7df787	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	NumPlus	False	Passed	Model Under Test Equivalent Model
efba448f830594eb31e640fb0bb5b093ad21ebe9	Apalache	Constant	NumPlus	True	Passed	Model Under Test Equivalent Model
564eedb63cdc3c572d7655907b2674a99dd7dbf7	Apalache	Constant	NumPlus	False	Passed	Model Under Test Equivalent Model
a4bea1861376bf7447f0c38e9cfdaeab42791a3c	Apalache	ConstantRank1	NumPlus	True	Passed	Model Under Test Equivalent Model
01fba18cc1909412732039ce239227d5c301707a	Apalache	ConstantRank1	NumPlus	False	Passed	Model Under Test Equivalent Model
031473bb4131678a8bbe8e55780ff57d2732afd5	Apalache	Instance	NumPlus	True	Passed	Model Under Test Equivalent Model
cc1c3832042d70a9ffc1f7f60194d1a358809dd7	Apalache	Instance	NumPlus	False	Passed	Model Under Test Equivalent Model
3091b6993af386c5a97bc7aedbddb4ea1d559142	Apalache	InstanceWith	NumPlus	True	Passed	Model Under Test Equivalent Model
3a2135ff951df7837c138107dde7aa29b13d8768	Apalache	InstanceWith	NumPlus	False	Passed	Model Under Test Equivalent Model
46e53a9d46920f4e790e38b5627af84ff907060a	Apalache	InstanceNamed	NumPlus	True	Passed	Model Under Test Equivalent Model
238edf607efec46e1dd508768e818384abe1d6f4	Apalache	InstanceNamed	NumPlus	False	Passed	Model Under Test Equivalent Model
cb10561f52cb9165303b3eee85786b864f524fa0	Apalache	InstanceNamedWith	NumPlus	True	Passed	Model Under Test Equivalent Model
04918cdb37c04e5314370985e7db99d98104d939	Apalache	InstanceNamedWith	NumPlus	False	Passed	Model Under Test Equivalent Model
dc2f019c275a0ef2da841c72a55f564d76bc4436	Apalache	InstanceInFolder	NumPlus	True	Passed	Model Under Test Equivalent Model
063aeae443d37c23fc89381841010ac4369df203	Apalache	InstanceInFolder	NumPlus	False	Passed	Model Under Test Equivalent Model
6ce78dcd415db39a57ce2ee86fffd0dd27d35cca	Apalache	InstanceWithInFolder	NumPlus	True	Passed	Model Under Test Equivalent Model
73aaef301b8b9056d793a524c87442251be58f72	Apalache	InstanceWithInFolder	NumPlus	False	Passed	Model Under Test Equivalent Model
e5e035b2b9991eb9a4351214df917d656d6045c5	Apalache	InstanceNamedInFolder	NumPlus	True	Passed	Model Under Test Equivalent Model
1f22cbe1f0c0dd30d0cd39c5be8d51cd499f6799	Apalache	InstanceNamedInFolder	NumPlus	False	Passed	Model Under Test Equivalent Model
bd5c2c42ef743580c29de56924b401812b9dfb36	Apalache	InstanceNamedWithInFolder	NumPlus	True	Passed	Model Under Test Equivalent Model
73e582da6004dce69b25c2e8f04fb76f17ffd405	Apalache	InstanceNamedWithInFolder	NumPlus	False	Passed	Model Under Test Equivalent Model
4571513c699248c168df867bf2c4cfc355287f90	Apalache	Lambda	NumPlus	True	Passed	Model Under Test Equivalent Model
fcb8f41d88a7a60e1197bb57358f2a61426a4dda	Apalache	Lambda	NumPlus	False	Passed	Model Under Test Equivalent Model
d1a71f4581cd5d71e5de73e23b33a8cfd4a5b836	Apalache	IfThen	NumPlus	True	Passed	Model Under Test Equivalent Model
9237150795936630b7e431828a7e182dc857ed25	Apalache	IfThen	NumPlus	False	Passed	Model Under Test Equivalent Model
fed3755b18f54cffd27ab492733e6c05b18216da	Apalache	IfElse	NumPlus	True	Passed	Model Under Test Equivalent Model
2064b321b5bc878f51c0a6fb445736500b5d6a04	Apalache	IfElse	NumPlus	False	Passed	Model Under Test Equivalent Model
7eb958e5f683c9f7b761ff8af65045156e9e9aa8	Apalache	Unchanged	NumPlus	True	Passed	Model Under Test Equivalent Model
420e7cb8bab02c43bfa7d11efac5db33bae11437	Apalache	Unchanged	NumPlus	False	Passed	Model Under Test Equivalent Model
c004d0c433ac4626002bb8c2fb45db23a34f6546	Apalache	SeqSubSeq	NumPlus	True	Passed	Model Under Test Equivalent Model
3988fbbf3fe45775e0ca396a293deb4c326a951e	Apalache	SeqSubSeq	NumPlus	False	Passed	Model Under Test Equivalent Model
864b124ae2c1a38394bda5e247700760e4048fb5	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	NumPlus	True	Passed	Model Under Test Equivalent Model
00c3c4264aa77cba8d9a788db9a23de6d38e76f0	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	NumPlus	False	Passed	Model Under Test Equivalent Model
5fc9666eeeec69df80fda3f4ea7285c20fee6820	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	NumPlus	True	Passed	Model Under Test Equivalent Model
0ceb916f36098b5b15e8445c49294f5766e37fe6	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	NumPlus	False	Passed	Model Under Test Equivalent Model
62356cc495be509e7747e6c582117eed868030e5	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	NumPlus	True	Passed	Model Under Test Equivalent Model
9d2e53c213410534282cafb1ce2ad307a436a0c8	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	NumPlus	False	Passed	Model Under Test Equivalent Model
843e1731545f012ef607f1814af94610c5a7bfbc	Apalache	BagBagIn	NumPlus	True	Passed	Model Under Test Equivalent Model
5a7b9864360793947242fed66b983da2b790cbc0	Apalache	BagBagIn	NumPlus	False	Passed	Model Under Test Equivalent Model
dacd59d802b3f01c9b9c91381388f1b303b770d4	Apalache	BagCopiesIn	NumPlus	True	Passed	Model Under Test Equivalent Model
645c9049bff29ea4c502a174ec599dba71d25e6e	Apalache	BagCopiesIn	NumPlus	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

Index

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