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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
32c862a2d78f9a58254b1b89e9165ba6923fd19e	Apalache	Eq	NumDiv	True	Passed	Model Under Test Equivalent Model
b3826fa6ecc8aec5641dc3c8aef4f91aa4252195	Apalache	Eq	NumDiv	False	Passed	Model Under Test Equivalent Model
b45c1928355b7f99ea37cc5d41ab63ae4136927d	Apalache	Ne	NumDiv	True	Passed	Model Under Test Equivalent Model
014e86c7f6be3c33491e971ff4f1c2a7df601277	Apalache	Ne	NumDiv	False	Passed	Model Under Test Equivalent Model
c56f9709af7d639b852c45c766f572433a6b1e81	Apalache	Let	NumDiv	True	Passed	Model Under Test Equivalent Model
d6666a37b541a3be27bbe34878551c099a73fc7d	Apalache	Let	NumDiv	False	Passed	Model Under Test Equivalent Model
a5eb16aa60c35830145f9fa90c3704dd2fb3c9d2	Apalache	Set0	NumDiv	True	Passed	Model Under Test Equivalent Model
64784fc6bda8b64c27b837b695f7c572d33b5f90	Apalache	Set0	NumDiv	False	Passed	Model Under Test Equivalent Model
abaed169422a1813c1e0c36fbb8b7b8808353d6e	Apalache	Set1	NumDiv	True	Passed	Model Under Test Equivalent Model
43618da2aaeca91bbbf7120152f9b01bf3522539	Apalache	Set1	NumDiv	False	Passed	Model Under Test Equivalent Model
d1e02ca1a81684621627c7f3bde18c888812ea8b	Apalache	Set2	NumDiv	True	Passed	Model Under Test Equivalent Model
207071138e9aa398999b77576cad79e080bf5fa1	Apalache	Set2	NumDiv	False	Passed	Model Under Test Equivalent Model
623cf825de947064759842c8e3304126dfe595e0	Apalache	Fun	NumDiv	True	Passed	Model Under Test Equivalent Model
9f2238204d35db09abfb84630a67f6acc8ab1f68	Apalache	Fun	NumDiv	False	Passed	Model Under Test Equivalent Model
c258317c8a15870d4cc3b523f2bc7578fdc9507a	Apalache	In	NumDiv	True	Passed	Model Under Test Equivalent Model
733ceb722503554718ef98aa2f36e14f089c9ea7	Apalache	In	NumDiv	False	Passed	Model Under Test Equivalent Model
dd41ad801dd946da6aafacfa5a7625bb0b75f7a2	Apalache	NotIn	NumDiv	True	Passed	Model Under Test Equivalent Model
57f004652a55026ebcee6e6c4cee7bcd1d2ec1e6	Apalache	NotIn	NumDiv	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
7c6b9fc9db704c10fccd78ff37c5e59206b42432	Apalache	Tuple	NumDiv	True	Passed	Model Under Test Equivalent Model
593baffc6ec6ce8beeaa8d3596c2976730e15bda	Apalache	Tuple	NumDiv	False	Passed	Model Under Test Equivalent Model
c3cb86fb6a39c5efd2c5979b1826f917ff425589	Apalache	FunApp	NumDiv	True	Passed	Model Under Test Equivalent Model
b2d274f112bca1681ecde16c2e4616cafd98add8	Apalache	FunApp	NumDiv	False	Passed	Model Under Test Equivalent Model
87e344b687410ebb8d2582ef2c4bd6227bc64fa5	Apalache	Except1Fun	NumDiv	True	Passed	Model Under Test Equivalent Model
7691f2323ae838641a7abc9c4a42168dbf69bc1d	Apalache	Except1Fun	NumDiv	False	Passed	Model Under Test Equivalent Model
fecd68b8c73c9f72bd0d9d103146036a05792d7f	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	NumDiv	True	Passed	Model Under Test Equivalent Model
d1ff18f62be9061bad1772a8035a366410e8beaa	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	NumDiv	False	Passed	Model Under Test Equivalent Model
4b4c70be5690844be43a5ea8ff729ce91427159a	Apalache	Except1Rec	NumDiv	True	Passed	Model Under Test Equivalent Model
0c7c5aabc1025dfe567d73e89102315bb0f830db	Apalache	Except1Rec	NumDiv	False	Passed	Model Under Test Equivalent Model
5d3339ae61c6dab5169ed9adaaf29f2b5f099911	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	NumDiv	True	Passed	Model Under Test Equivalent Model
79189fe89501b4e33d77940fc0cffb5e43704024	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	NumDiv	False	Passed	Model Under Test Equivalent Model
739f8cbd4896c9db379bce6a5251a9fb717756e0	Apalache	Except2Fun	NumDiv	True	Passed	Model Under Test Equivalent Model
cc14397e86d4378f0f170c7c8a36687af1a6c07b	Apalache	Except2Fun	NumDiv	False	Passed	Model Under Test Equivalent Model
f70c88c397ffa90213d7bae87880ba6fd744cae8	Apalache	Prime	NumDiv	True	Passed	Model Under Test Equivalent Model
cf8ab6fc1911bf6938b0cadffd54c074111b23f2	Apalache	Prime	NumDiv	False	Passed	Model Under Test Equivalent Model
13f03fb7595dd3b5a73c53116fc4ea2b905d670a	Apalache	NumUnaryMinus	NumDiv	True	Passed	Model Under Test Equivalent Model
b8ab6e54ecf14e54904f56e3d2373cbc2efa95b4	Apalache	NumUnaryMinus	NumDiv	False	Passed	Model Under Test Equivalent Model
4d626714ad223b75130584dc852a1bf9614db943	Apalache	NumPlus	NumDiv	True	Passed	Model Under Test Equivalent Model
3733deeadb031140d786b14d6945d2d667759e5b	Apalache	NumPlus	NumDiv	False	Passed	Model Under Test Equivalent Model
f52e2be645bb297d950b6da7a6ad4281e1bc9a6d	Apalache	NumMinus	NumDiv	True	Passed	Model Under Test Equivalent Model
b4b6c1b18737bd0a8b73115abd1954c0c4b6741a	Apalache	NumMinus	NumDiv	False	Passed	Model Under Test Equivalent Model
251994e7824929055c95ca704c508d96e5941d33	Apalache	NumMul	NumDiv	True	Passed	Model Under Test Equivalent Model
f15b8a46c7220049a8c9051b48b94f275fa7c548	Apalache	NumMul	NumDiv	False	Passed	Model Under Test Equivalent Model
2ab3c5213521b28cc0c62642aaebb94f5c62e1d7	Apalache	NumDiv	NumDiv	True	Passed	Model Under Test Equivalent Model
ba2692ebe60424545aaa5e9c886e3c1497c287dc	Apalache	NumDiv	NumDiv	False	Passed	Model Under Test Equivalent Model
45202268e1d344109964cf2b4e2a8bcea1c39f6c	Apalache	NumMod	NumDiv	True	Passed	Model Under Test Equivalent Model
9bdf1a0a7b7f4ee46e1247ac8606ba3b9e71996d	Apalache	NumMod	NumDiv	False	Passed	Model Under Test Equivalent Model
76776d99e7cffd4127b629889a1b199baf00f6c2	Apalache	NumPow	NumDiv	True	Passed	Model Under Test Equivalent Model
fbcf5765bfe436d9b805a20c9ed3d1c32c6195ed	Apalache	NumPow	NumDiv	False	Passed	Model Under Test Equivalent Model
de805c6465306079a9c16ff63ed66c3e29b2bd00	Apalache	NumGt	NumDiv	True	Passed	Model Under Test Equivalent Model
c086cc9a292aa3fe85ddf9f7c5f23710ff147064	Apalache	NumGt	NumDiv	False	Passed	Model Under Test Equivalent Model
f168b9c72c12e9b228f6b02061210b540d440cbb	Apalache	NumGe	NumDiv	True	Passed	Model Under Test Equivalent Model
093c616ddf936bb39e2285515917b3982eb0847f	Apalache	NumGe	NumDiv	False	Passed	Model Under Test Equivalent Model
07f30319123feea4458302e9bcaab6cc68df616f	Apalache	NumLt	NumDiv	True	Passed	Model Under Test Equivalent Model
3ead2c4f35b7ace7020e84428f069b014cde5f67	Apalache	NumLt	NumDiv	False	Passed	Model Under Test Equivalent Model
8e55b68d748a138ac47b340cbb047966579783f6	Apalache	NumLe	NumDiv	True	Passed	Model Under Test Equivalent Model
99c6223f25e1a6ff555fc98728d345461795b0c1	Apalache	NumLe	NumDiv	False	Passed	Model Under Test Equivalent Model
b1f13a2a7821af669abb809c3b0058a00cb91fb8	Apalache	DefFun	NumDiv	True	Passed	Model Under Test Equivalent Model
c3899ffeca48026ab24fc3a00aeaa682145dd02e	Apalache	DefFun	NumDiv	False	Passed	Model Under Test Equivalent Model
882c224d0d67bb3e2d8052565ec15594bafb95cf	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	NumDiv	True	Passed	Model Under Test Equivalent Model
50b1077991b259fc636297db671012687cd11685	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	NumDiv	False	Passed	Model Under Test Equivalent Model
2e169225355048daa632041b29dbbd2a392ebbe0	Apalache	DefFunRecursive	NumDiv	True	Passed	Model Under Test Equivalent Model
c3c1f3feaf64d41d43fd715cb894eee3c5c0b7dc	Apalache	DefFunRecursive	NumDiv	False	Passed	Model Under Test Equivalent Model
b40de0437f1c3d49ded3efbe4796ee512a223c53	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	NumDiv	True	Passed	Model Under Test Equivalent Model
453bb572611113fc3a0ad2ad8ed662db48020e70	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	NumDiv	False	Passed	Model Under Test Equivalent Model
9c3106fb94eba0bfc52b8c33e821274b48201b6e	Apalache	Def0	NumDiv	True	Passed	Model Under Test Equivalent Model
9ead6fe36949b93a21cc73210683ab2d77e3ad5c	Apalache	Def0	NumDiv	False	Passed	Model Under Test Equivalent Model
c9e2f96cdcdc3ffff3557a9c93e5d3c9a81e2190	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	NumDiv	True	Passed	Model Under Test Equivalent Model
22811d783d9a6f2a1dea34a8b41b2fddf84610a2	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	NumDiv	False	Passed	Model Under Test Equivalent Model
f9c589ac95c4f59cdcbd7ca0f2a90f51567d30f8	Apalache	Def1	NumDiv	True	Passed	Model Under Test Equivalent Model
2f784ea80c6132622b8ba91e9df8c6026d207462	Apalache	Def1	NumDiv	False	Passed	Model Under Test Equivalent Model
96334eb2a6fb817172548c6854abf8f7310e18a3	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	NumDiv	True	Passed	Model Under Test Equivalent Model
25f9c6922b35e630aaa35b3ca038337e473bfd3c	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	NumDiv	False	Passed	Model Under Test Equivalent Model
87f7c5c4d67005ef6631ff1a21555746c3f988b6	Apalache	Def2	NumDiv	True	Passed	Model Under Test Equivalent Model
45e41dbc006133071ecf8244f8830ab61f8c3913	Apalache	Def2	NumDiv	False	Passed	Model Under Test Equivalent Model
f43a7b42cea16b7b1044c643924bedf375acd9c2	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	NumDiv	True	Passed	Model Under Test Equivalent Model
c663781064b7d313539284cea589a140361ed849	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	NumDiv	False	Passed	Model Under Test Equivalent Model
20833862a8282601fc7011f32655cdbdb66db860	Apalache	Def1Recursive	NumDiv	True	Passed	Model Under Test Equivalent Model
83672cb5adca81b1f42a8d4422d6ddf3006640e0	Apalache	Def1Recursive	NumDiv	False	Passed	Model Under Test Equivalent Model
a4cce67713a44ae3febd7180015aec85b5d1d639	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	NumDiv	True	Passed	Model Under Test Equivalent Model
a705691e3ffe0d9fb1b114f5706bf43d682b9ffc	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	NumDiv	False	Passed	Model Under Test Equivalent Model
1de3898ffb58a2baf5a43f3e0cfebbaf892d7172	Apalache	Extends	NumDiv	True	Passed	Model Under Test Equivalent Model
3c91e880f8f6424161cae9342a8def4a0217413c	Apalache	Extends	NumDiv	False	Passed	Model Under Test Equivalent Model
a1eaf8e90aa8f2df6c0ee5f69923a1ec40e3f12e	Apalache	ExtendsInDifferentFolder	NumDiv	True	Passed	Model Under Test Equivalent Model
b3965759e000ac1667f82a88ab6505f96f1ca9d0	Apalache	ExtendsInDifferentFolder	NumDiv	False	Passed	Model Under Test Equivalent Model
59333ecf04add5d25c0fe053b50febb6a014b471	Apalache	Variable	NumDiv	True	Passed	Model Under Test Equivalent Model
4509da9bb30c5deaeefc6427556e524def24bc3e	Apalache	Variable	NumDiv	False	Passed	Model Under Test Equivalent Model
77eba6ba2974bdc3d12561bb89f7a52d6a084e32	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	NumDiv	True	Passed	Model Under Test Equivalent Model
0bcc2724f4c31e8d199a28c11f12928c2ae3aae2	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	NumDiv	False	Passed	Model Under Test Equivalent Model
b42694e42b28426b83fd819f084a3fda693c8a0d	Apalache	Constant	NumDiv	True	Passed	Model Under Test Equivalent Model
644c7c6cc78e5062e28f644510c4a49b0e133ba4	Apalache	Constant	NumDiv	False	Passed	Model Under Test Equivalent Model
5fb6334a29582cf3d373d82d59cd045f1e96921a	Apalache	ConstantRank1	NumDiv	True	Passed	Model Under Test Equivalent Model
725779d1d74849642e06cd0647751a96a0a4784d	Apalache	ConstantRank1	NumDiv	False	Passed	Model Under Test Equivalent Model
aeb3645743a394012dcc814c1879a8e54d5d6d82	Apalache	Instance	NumDiv	True	Passed	Model Under Test Equivalent Model
0ad24805fd7ba91757059733517f394b3e62a1c6	Apalache	Instance	NumDiv	False	Passed	Model Under Test Equivalent Model
9581c81d1251359a52f87573c2235e00b0279ccf	Apalache	InstanceWith	NumDiv	True	Passed	Model Under Test Equivalent Model
85543149acab050bb805f8eff8f1a0fe9adf4052	Apalache	InstanceWith	NumDiv	False	Passed	Model Under Test Equivalent Model
e9e8f33f7018e45015867609677908cac5fda90a	Apalache	InstanceNamed	NumDiv	True	Passed	Model Under Test Equivalent Model
d74035ed8bd7b828d14c17f362b0521c984cda00	Apalache	InstanceNamed	NumDiv	False	Passed	Model Under Test Equivalent Model
199cdca14e8d5e957bc892a47a46ba080c4a5844	Apalache	InstanceNamedWith	NumDiv	True	Passed	Model Under Test Equivalent Model
7b24af00f22b8a73a7b7e3a2f7a0cca0f4fe1dd7	Apalache	InstanceNamedWith	NumDiv	False	Passed	Model Under Test Equivalent Model
b5a1cd51a87e68607bb5657aba3c827aaedb47ea	Apalache	InstanceInFolder	NumDiv	True	Passed	Model Under Test Equivalent Model
9f39fd0d32dae78903f27e759dc7957d9825f34f	Apalache	InstanceInFolder	NumDiv	False	Passed	Model Under Test Equivalent Model
857349f014503ecd78d131d433184f894c66ea37	Apalache	InstanceWithInFolder	NumDiv	True	Passed	Model Under Test Equivalent Model
f3e8ea3b0b79c163d45bb3f16839756e2212c530	Apalache	InstanceWithInFolder	NumDiv	False	Passed	Model Under Test Equivalent Model
153715695cff0df2e5eb4fefeb37beb503afc10c	Apalache	InstanceNamedInFolder	NumDiv	True	Passed	Model Under Test Equivalent Model
4d859860bec09fc9f21d27586aee83dfca1eaf8c	Apalache	InstanceNamedInFolder	NumDiv	False	Passed	Model Under Test Equivalent Model
741b37a71eac2e22cf1b365f107ce8e258198d51	Apalache	InstanceNamedWithInFolder	NumDiv	True	Passed	Model Under Test Equivalent Model
228c8412e4e75df5d81c9218d295aecf2aea2b8b	Apalache	InstanceNamedWithInFolder	NumDiv	False	Passed	Model Under Test Equivalent Model
d5b755a83e33f168695b28ff21b9726e7934bee6	Apalache	Lambda	NumDiv	True	Passed	Model Under Test Equivalent Model
28c4b90b18bb68985e6a31975954bb1ae0190d28	Apalache	Lambda	NumDiv	False	Passed	Model Under Test Equivalent Model
99d0939459f199fef2a31325b5a49caf92c75e9c	Apalache	IfThen	NumDiv	True	Passed	Model Under Test Equivalent Model
3c06e4622f28266db9cd380c08554ea34d3b5a47	Apalache	IfThen	NumDiv	False	Passed	Model Under Test Equivalent Model
d1d35e50f7747e18321f9066756642aa3fb29352	Apalache	IfElse	NumDiv	True	Passed	Model Under Test Equivalent Model
8481ca159537473ad6787214b85f526c7f95ef0b	Apalache	IfElse	NumDiv	False	Passed	Model Under Test Equivalent Model
876a341b56c873345abf803e2d7a2d22c492070f	Apalache	Unchanged	NumDiv	True	Passed	Model Under Test Equivalent Model
1a83ffdf73a413695a23f66355adc4ee987893e9	Apalache	Unchanged	NumDiv	False	Passed	Model Under Test Equivalent Model
4dc4bb2a7a64aa2925dbe0ae5e4faeffa3a68691	Apalache	SeqSubSeq	NumDiv	True	Passed	Model Under Test Equivalent Model
92bd49dbafaa2bb441dcc58dcf2b480dbb38403f	Apalache	SeqSubSeq	NumDiv	False	Passed	Model Under Test Equivalent Model
541cdfdeae6e7e599eff2e8f5203afb290e6a797	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	NumDiv	True	Passed	Model Under Test Equivalent Model
89aebb54c7cdc7424e9fe6e00c693ee03ffa8179	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	NumDiv	False	Passed	Model Under Test Equivalent Model
c1451bdf218935acea24bb95526ce8a2cc4a2d26	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	NumDiv	True	Passed	Model Under Test Equivalent Model
efc2d9340593db27c4be6ea376a5a5444d3641fe	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	NumDiv	False	Passed	Model Under Test Equivalent Model
cd364ab17492e0adf020494d8627c25992a89828	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	NumDiv	True	Passed	Model Under Test Equivalent Model
827a02f4eb181d31cbf39f9290187c44754d54dd	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	NumDiv	False	Passed	Model Under Test Equivalent Model
bddc41a66baab6212f20f8eccd9c3883f8978a97	Apalache	BagBagIn	NumDiv	True	Passed	Model Under Test Equivalent Model
01d1d643779723439023c2fcca9133ac97708157	Apalache	BagBagIn	NumDiv	False	Passed	Model Under Test Equivalent Model
953b369a04a1beae9702a444036d72a575f42e69	Apalache	BagCopiesIn	NumDiv	True	Passed	Model Under Test Equivalent Model
3d13a0d53f50d3722af338b2b03ef215f227033d	Apalache	BagCopiesIn	NumDiv	False	Passed	Model Under Test Equivalent Model
8d38873b30142daa8b22ebb21e1bc4962d0f1073	Apalache	SeqAppend	NumDiv	True	Passed	Model Under Test Equivalent Model
6f3f57a2662bf797847c3e7cfb3404cd979003d0	Apalache	SeqAppend	NumDiv	False	Passed	Model Under Test Equivalent Model

Index

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