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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
cdbe8f1c6ae66cdde9b2aab3b890a350110f00b4	Apalache	Eq	NumMaxInt	True	Passed	Model Under Test Equivalent Model
bceaecbf977d9a64f3c89c51484b7e1dc657ed16	Apalache	Eq	NumMaxInt	False	Passed	Model Under Test Equivalent Model
741d0f2e3c9d7e05825860dd8a0fe33f1c53d1bb	Apalache	Ne	NumMaxInt	True	Passed	Model Under Test Equivalent Model
816bc804dd0e397594e7f182b3421e814096461a	Apalache	Ne	NumMaxInt	False	Passed	Model Under Test Equivalent Model
51e3eba388510a7fc13e867910f78c42f69eeb87	Apalache	Let	NumMaxInt	True	Passed	Model Under Test Equivalent Model
f1c9ac5d012045620d2a74e43309da1177773303	Apalache	Let	NumMaxInt	False	Passed	Model Under Test Equivalent Model
df73aba831a2ffbe3b30b5ff53e7b4eed2d8dbbc	Apalache	Set0	NumMaxInt	True	Passed	Model Under Test Equivalent Model
976c3e554aeacdde82010a03919fcc09fe10d2e3	Apalache	Set0	NumMaxInt	False	Passed	Model Under Test Equivalent Model
bb7641d1b447c3a78e855cf6eb536b3ce3bb3698	Apalache	Set1	NumMaxInt	True	Passed	Model Under Test Equivalent Model
fdfece869844433404eb13629402574e910630c1	Apalache	Set1	NumMaxInt	False	Passed	Model Under Test Equivalent Model
19ecd84495ab8c599fd4aaa5efed5e442dc1b73e	Apalache	Set2	NumMaxInt	True	Passed	Model Under Test Equivalent Model
34e7b535ee83dd4f099d4dd3f741147d0f819717	Apalache	Set2	NumMaxInt	False	Passed	Model Under Test Equivalent Model
7e91291c7b59e0d0b7a428de0918aedca7e48c04	Apalache	Fun	NumMaxInt	True	Passed	Model Under Test Equivalent Model
bc69226075aef8adcb991f6e757597d77f76e9e0	Apalache	Fun	NumMaxInt	False	Passed	Model Under Test Equivalent Model
b6b6df802598b6da9af17ea63e3be7da59f89ea4	Apalache	In	NumMaxInt	True	Passed	Model Under Test Equivalent Model
5c0654444734603d5839b8dc6c0195d61be2da37	Apalache	In	NumMaxInt	False	Passed	Model Under Test Equivalent Model
83e35ae6ab92d34afcd61dc7e75c6448b4162846	Apalache	NotIn	NumMaxInt	True	Passed	Model Under Test Equivalent Model
ec5c033cdd193d2eaaf619271bec9994d7aea0fb	Apalache	NotIn	NumMaxInt	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
b2c57204d18f38a767c6e930b353cac8cd2d601a	Apalache	Tuple	NumMaxInt	True	Passed	Model Under Test Equivalent Model
0a49a52e9af2326e3317daedf8719bee68279ff1	Apalache	Tuple	NumMaxInt	False	Passed	Model Under Test Equivalent Model
f3717938369e21f71b53af3b0e9d565bf6aa9dba	Apalache	FunApp	NumMaxInt	True	Passed	Model Under Test Equivalent Model
4010b10fc635c68c332553049fe1d2ff258976ca	Apalache	FunApp	NumMaxInt	False	Passed	Model Under Test Equivalent Model
cffc639f9f0844873dd8cb06dda26c384f8196d0	Apalache	Except1Fun	NumMaxInt	True	Passed	Model Under Test Equivalent Model
4cd1180faaccbd609bc6b45adb1ae378b2b9a967	Apalache	Except1Fun	NumMaxInt	False	Passed	Model Under Test Equivalent Model
b519d40424e1458de35e1bc05ce69ac89f23f282	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	NumMaxInt	True	Passed	Model Under Test Equivalent Model
44c45137b8a8295b1b249d6a06e9c1638b8c28a7	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	NumMaxInt	False	Passed	Model Under Test Equivalent Model
718910f223d682e9c90cd591cc14dc709f44077a	Apalache	Except1Rec	NumMaxInt	True	Passed	Model Under Test Equivalent Model
67950a08ad632560c22d6c88ed44783e6b1b1b98	Apalache	Except1Rec	NumMaxInt	False	Passed	Model Under Test Equivalent Model
1d8e8cabedcdf3049fdf67bae1d035fc92ecc00e	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	NumMaxInt	True	Passed	Model Under Test Equivalent Model
9080bda1f87ba8c6800e81937dc025772b8cc917	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	NumMaxInt	False	Passed	Model Under Test Equivalent Model
fde425ba57d933fbe464ed4614e4eae0611e487f	Apalache	Except2Fun	NumMaxInt	True	Passed	Model Under Test Equivalent Model
fb9eceb5b5d4607772ecb8de65f9c93e2b468c61	Apalache	Except2Fun	NumMaxInt	False	Passed	Model Under Test Equivalent Model
2ec813f8d56a4c49aac152c233d15341889ec5d1	Apalache	Prime	NumMaxInt	True	Passed	Model Under Test Equivalent Model
ee9d10a61e455fbd8d80cdf5fca3c6e985611c6e	Apalache	Prime	NumMaxInt	False	Passed	Model Under Test Equivalent Model
5c78fb10f2d92e31bd62a3d7d0d63603657f9605	Apalache	NumUnaryMinus	NumMaxInt	True	Passed	Model Under Test Equivalent Model
c8af08c3c222bd1a8695ff26272b1c810ba2b318	Apalache	NumUnaryMinus	NumMaxInt	False	Passed	Model Under Test Equivalent Model
4142febf3f1f73ebb34b120aa12dc0bb2de8b6fd	Apalache	NumPlus	NumMaxInt	True	Failed: TLC internally represents integers as 32 bit numbers and reports an error if the value is overflowed. Apalache is unable to detect overflows	Model Under Test Equivalent Model
1745d72d9d851029e3331ff2327ed2ce209afee8	Apalache	NumPlus	NumMaxInt	False	Failed: TLC internally represents integers as 32 bit numbers and reports an error if the value is overflowed. Apalache is unable to detect overflows	Model Under Test Equivalent Model
8e065bc75cba6088068647e4312ff994cda10fcd	Apalache	NumMinus	NumMaxInt	True	Passed	Model Under Test Equivalent Model
0333f5ac9e0f7fd9f74654b1ad1a958a756cd279	Apalache	NumMinus	NumMaxInt	False	Passed	Model Under Test Equivalent Model
1663ba55031fbe24d8618dc7e85880a019776ced	Apalache	NumMul	NumMaxInt	True	Passed	Model Under Test Equivalent Model
ec1a0923b4026e5b4886e4b2fc6a208bf4a5e20a	Apalache	NumMul	NumMaxInt	False	Passed	Model Under Test Equivalent Model
88aa182c3d9ddffea593eaf85473a94cfbc20722	Apalache	NumDiv	NumMaxInt	True	Passed	Model Under Test Equivalent Model
3e01cbea26ff65309139a93f5e6e49bdee3fa1eb	Apalache	NumDiv	NumMaxInt	False	Passed	Model Under Test Equivalent Model
3fcb6b44cbd8a5f28806cdc3a24d83d0754323a5	Apalache	NumMod	NumMaxInt	True	Passed	Model Under Test Equivalent Model
0b89c400ef8f0712e374d547a782a17e5ee6c73d	Apalache	NumMod	NumMaxInt	False	Passed	Model Under Test Equivalent Model
43aff303ad3271d7c79c418775cbe1b2f2bfe549	Apalache	NumPow	NumMaxInt	True	Passed	Model Under Test Equivalent Model
81480fb85d718e5ccab76dd99e73315fe9ff5f1b	Apalache	NumPow	NumMaxInt	False	Passed	Model Under Test Equivalent Model
a7f24237de0384129fb6746123f8299e6420ef10	Apalache	NumGt	NumMaxInt	True	Passed	Model Under Test Equivalent Model
ac8093f636a81d5227fb2fb3cffe50a6518cba53	Apalache	NumGt	NumMaxInt	False	Passed	Model Under Test Equivalent Model
272137bb0f64ae527008cf2eb6a09879f7a55244	Apalache	NumGe	NumMaxInt	True	Passed	Model Under Test Equivalent Model
1586dcb62b75c013c3d58eca3154f94f8fb43abc	Apalache	NumGe	NumMaxInt	False	Passed	Model Under Test Equivalent Model
7f1e6425936b1c1b8e076a23c0f08c19ff2305d3	Apalache	NumLt	NumMaxInt	True	Passed	Model Under Test Equivalent Model
241b0a995cff962bf93097729c3c67387e2f0efd	Apalache	NumLt	NumMaxInt	False	Passed	Model Under Test Equivalent Model
497e5d2e2715107f95e580a3f6dd11eb1db340d2	Apalache	NumLe	NumMaxInt	True	Passed	Model Under Test Equivalent Model
6980e1f44f1ee396e9095a875688585b13158ce6	Apalache	NumLe	NumMaxInt	False	Passed	Model Under Test Equivalent Model
e2d1e6b56bbbee342450b62c499e92a9b5fefdfc	Apalache	DefFun	NumMaxInt	True	Passed	Model Under Test Equivalent Model
59b5acd76397ecaeffbd0ad2f6169f1895ea24fa	Apalache	DefFun	NumMaxInt	False	Passed	Model Under Test Equivalent Model
c8a758c1e9c187be5ed288af88c8d0e6f8741209	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	NumMaxInt	True	Passed	Model Under Test Equivalent Model
01f030c18546f64c26c216220cf0a3e9a715e1fd	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	NumMaxInt	False	Passed	Model Under Test Equivalent Model
e747ac181b904e794c6deb9babb29a07e5cdd7aa	Apalache	DefFunRecursive	NumMaxInt	True	Passed	Model Under Test Equivalent Model
91e2522fc086c7d12b9953816fd79943ff258bf5	Apalache	DefFunRecursive	NumMaxInt	False	Passed	Model Under Test Equivalent Model
3b2a1688366c7915ea1d762c03b13186d1d9b49d	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	NumMaxInt	True	Passed	Model Under Test Equivalent Model
300d0875eccab917d0a3f83b4f24ed9e14666861	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	NumMaxInt	False	Passed	Model Under Test Equivalent Model
971e86ecf462420feebe2c9cf2dc57c53755b262	Apalache	Def0	NumMaxInt	True	Passed	Model Under Test Equivalent Model
e2f9c5dd276184c3b3a5516ca609df2856a59bd8	Apalache	Def0	NumMaxInt	False	Passed	Model Under Test Equivalent Model
eecd05d6dc142a68e9f3a144ed6e9fb207d272f1	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	NumMaxInt	True	Passed	Model Under Test Equivalent Model
b7085d744184f54559637bf44cef711a7e526194	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	NumMaxInt	False	Passed	Model Under Test Equivalent Model
e13f1e1f0d56550fd80a2745cc8c90159f7b318e	Apalache	Def1	NumMaxInt	True	Passed	Model Under Test Equivalent Model
30b08072f48c5792e5d92df0ebee7d80e25726c4	Apalache	Def1	NumMaxInt	False	Passed	Model Under Test Equivalent Model
b88bb74977d56434caf22660993c1c1b207fcaac	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	NumMaxInt	True	Passed	Model Under Test Equivalent Model
92627e227f6ac5d656d590ff24c43518e3c0132f	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	NumMaxInt	False	Passed	Model Under Test Equivalent Model
505949019f12adb89b9a26a0cedeaf1d476b92c8	Apalache	Def2	NumMaxInt	True	Passed	Model Under Test Equivalent Model
5e080b7b44d703a774316b001d8ba85ea9c0d2dd	Apalache	Def2	NumMaxInt	False	Passed	Model Under Test Equivalent Model
f5240504c1576a222b44aceadf7edb9179d970fd	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	NumMaxInt	True	Passed	Model Under Test Equivalent Model
545035af919b19272a48dd7eec306fbaa207ba16	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	NumMaxInt	False	Passed	Model Under Test Equivalent Model
331b588b9f215cec6eef80e7fe40c07c94a33bff	Apalache	Def1Recursive	NumMaxInt	True	Passed	Model Under Test Equivalent Model
8c173dbcf67600a22505bda8273519d17dcd2dee	Apalache	Def1Recursive	NumMaxInt	False	Passed	Model Under Test Equivalent Model
7a62d4be39ec38ea11ca27de92325548870591ef	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	NumMaxInt	True	Passed	Model Under Test Equivalent Model
38f315392e0ec9fc18a59a0be5be4564dc00b9d8	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	NumMaxInt	False	Passed	Model Under Test Equivalent Model
54c6ce476428484a30d8a5812f0cb07e6dff318f	Apalache	Extends	NumMaxInt	True	Passed	Model Under Test Equivalent Model
ccdb5df595e64803eec146e165c5b73968710a7d	Apalache	Extends	NumMaxInt	False	Passed	Model Under Test Equivalent Model
2e8206bd580ccf39920127e997182ef404b95797	Apalache	ExtendsInDifferentFolder	NumMaxInt	True	Passed	Model Under Test Equivalent Model
29a448b2e63b5494e9b7106a45b48aa275fd69e7	Apalache	ExtendsInDifferentFolder	NumMaxInt	False	Passed	Model Under Test Equivalent Model
f0babe7f8183f1877cfc015a744997de14bc1906	Apalache	Variable	NumMaxInt	True	Passed	Model Under Test Equivalent Model
583af8427d40303f1fc81b753b6e448a13603fc5	Apalache	Variable	NumMaxInt	False	Passed	Model Under Test Equivalent Model
561e8986093b0e00018b0c87822282926dba8d10	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	NumMaxInt	True	Passed	Model Under Test Equivalent Model
45fa45202781630305360f938352d85374faf077	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	NumMaxInt	False	Passed	Model Under Test Equivalent Model
319b308afa835cf3c39e748679c003c3c592343f	Apalache	Constant	NumMaxInt	True	Passed	Model Under Test Equivalent Model
27c55045af821b59b607db790300614edb1a2e79	Apalache	Constant	NumMaxInt	False	Passed	Model Under Test Equivalent Model
d7bf61c07c618f8482a79eb8b0e161a0fa30f924	Apalache	ConstantRank1	NumMaxInt	True	Passed	Model Under Test Equivalent Model
9a1b0740a9085e635efdf0101adba9dbf09cc879	Apalache	ConstantRank1	NumMaxInt	False	Passed	Model Under Test Equivalent Model
4f84f78e106d4086f6eca9fbdff5161b6e624936	Apalache	Instance	NumMaxInt	True	Passed	Model Under Test Equivalent Model
1aa168883e7ff0db285eb5b0d2db8d7b01ef4a3d	Apalache	Instance	NumMaxInt	False	Passed	Model Under Test Equivalent Model
94bc0e70ffe318582a60ce29de4d0321bd4a58a1	Apalache	InstanceWith	NumMaxInt	True	Passed	Model Under Test Equivalent Model
316285f73f38aaf50b46141174f88139eec44a55	Apalache	InstanceWith	NumMaxInt	False	Passed	Model Under Test Equivalent Model
0b63c1a8ddc984764c7b59a1500025908c060bd7	Apalache	InstanceNamed	NumMaxInt	True	Passed	Model Under Test Equivalent Model
ca73cc0d16f3bcd5506032e7490a5b2910682810	Apalache	InstanceNamed	NumMaxInt	False	Passed	Model Under Test Equivalent Model
46261a11c61a167d0d7fc109da609cd14f059b46	Apalache	InstanceNamedWith	NumMaxInt	True	Passed	Model Under Test Equivalent Model
8889d39494b9cef04d0db3038958dfd81fbdcc84	Apalache	InstanceNamedWith	NumMaxInt	False	Passed	Model Under Test Equivalent Model
dffe99cfd67ba83f7b937bd135aa2a0b6c001352	Apalache	InstanceInFolder	NumMaxInt	True	Passed	Model Under Test Equivalent Model
e14fc0292fbdfb1f3dc25c4252506899ebad48cc	Apalache	InstanceInFolder	NumMaxInt	False	Passed	Model Under Test Equivalent Model
824f57e05555b7edd0875aabd7fcb02436eed655	Apalache	InstanceWithInFolder	NumMaxInt	True	Passed	Model Under Test Equivalent Model
67ebb894a7fbbffe7b7caf6726838e04f79b3024	Apalache	InstanceWithInFolder	NumMaxInt	False	Passed	Model Under Test Equivalent Model
aeaac1b995f61546a62c07f4b6f930245c352041	Apalache	InstanceNamedInFolder	NumMaxInt	True	Passed	Model Under Test Equivalent Model
b7679e3ccdf587b7fbf27517fc59471f203d23bf	Apalache	InstanceNamedInFolder	NumMaxInt	False	Passed	Model Under Test Equivalent Model
8a40da5b428e5635113be8d47658dd7f03abba12	Apalache	InstanceNamedWithInFolder	NumMaxInt	True	Passed	Model Under Test Equivalent Model
90e07c44ee90996d4952c09ea9418094f4dcd982	Apalache	InstanceNamedWithInFolder	NumMaxInt	False	Passed	Model Under Test Equivalent Model
c976fccd4d4cf00ae5758a9ce7e8931113ccecfe	Apalache	Lambda	NumMaxInt	True	Passed	Model Under Test Equivalent Model
38c035989d9623ce390c96c280033ff33d650bd2	Apalache	Lambda	NumMaxInt	False	Passed	Model Under Test Equivalent Model
b4d6da9481e99d1ef2d4879765428beed4b8871a	Apalache	IfThen	NumMaxInt	True	Passed	Model Under Test Equivalent Model
a617b7f6a1e7c8c3dc76a4a4d8fb2979edb8bd6a	Apalache	IfThen	NumMaxInt	False	Passed	Model Under Test Equivalent Model
26f03dbd5330d11c59e0137d1598b3b50a0d82cd	Apalache	IfElse	NumMaxInt	True	Passed	Model Under Test Equivalent Model
50866fc851160ecb2ae829a70be5a3d5541ca0e7	Apalache	IfElse	NumMaxInt	False	Passed	Model Under Test Equivalent Model
0d474d9e155934031f2ecde9ea0407be01f33288	Apalache	Unchanged	NumMaxInt	True	Passed	Model Under Test Equivalent Model
020e89bc8fe5d90191df87a358b15ccad688fe1f	Apalache	Unchanged	NumMaxInt	False	Passed	Model Under Test Equivalent Model
77f419d906715a262d36e7d9af1eb2e46acab58c	Apalache	SeqSubSeq	NumMaxInt	True	Passed	Model Under Test Equivalent Model
89020b2a9bb6d995df448e5e034d98a5cae6359b	Apalache	SeqSubSeq	NumMaxInt	False	Passed	Model Under Test Equivalent Model
3d66d888c8c2cb42ad8fd99d3a385e1ea405a5c1	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	NumMaxInt	True	Passed	Model Under Test Equivalent Model
f0352d0ade27f06edf94ece5a71a69e3bedc854b	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	NumMaxInt	False	Passed	Model Under Test Equivalent Model
bd31bb0214b8ede54a4d9ab6b93afe8b4c7fdf50	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	NumMaxInt	True	Passed	Model Under Test Equivalent Model
d0fc5858b4c5c8b8c0e5f677f36a1482202160da	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	NumMaxInt	False	Passed	Model Under Test Equivalent Model
8eba09ae6c89a891535684b0ad8cabcfc677b821	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	NumMaxInt	True	Passed	Model Under Test Equivalent Model
b0cca46d087f0ef80209d676bd62dcda40950270	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	NumMaxInt	False	Passed	Model Under Test Equivalent Model
bc29ed9b60098e21f424eb3564d57a79df8eb23b	Apalache	BagBagIn	NumMaxInt	True	Passed	Model Under Test Equivalent Model
4e7315e5092fe85ae3a3879cc5a0d3557d74c67b	Apalache	BagBagIn	NumMaxInt	False	Passed	Model Under Test Equivalent Model
49129014f18cedd1ac8cd4b99deb533dee50268c	Apalache	BagCopiesIn	NumMaxInt	True	Passed	Model Under Test Equivalent Model
17302d00b1b3ae07cbdf18d852c1efc7dd4eb890	Apalache	BagCopiesIn	NumMaxInt	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

Index

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