DynamicArrays_Medusa_Test.t.sol

// SPDX-License-Identifier: UNLICENSED
pragma solidity ^0.8.13;
import "forge-std/Test.sol";
import "forge-std/console2.sol";
import "../src/DynamicArrays.sol";

contract DynamicArrays_Medusa_Test is Test {
    DynamicArrays target;

    function setUp() public {
        target = new DynamicArrays();
    }
    // Reproduced from: medusa-corpora/corpus-dyn-arr/test_results/1704377304276517000-e15599be-8cab-4d01-8cd7-4cd785554cb6.json
    function test_auto_check_bytesArr_0() public { 
        bytes[] memory input = new bytes[](16);
        input[0] = bytes(hex"45cee200427cbe");
        input[1] = bytes(hex"af6293c1fe6601cae37e176805a8f0455b9279c71d26e4bc");
        input[2] = bytes(hex"8429c8ef56226414b0a78b3254525c8b6222b9fde1341a13d3a00d27d3be779ec6c453a9b2e69691d32ef25f9d526dd67358f61709536179767fcb463e");
        input[3] = bytes(hex"fbd651c645169c07f2d7f6ba8981bd11116a42d3acf60c344692e0b616c2a128aa76fc4fe5f1b988a79b22dfba");
        input[4] = bytes(hex"60e3ccc452ac84e95383b7ccd298c9");
        input[5] = bytes(hex"9f70b3171762ea7823e7d1c561");
        input[6] = bytes(hex"457ec63da2132872dfe38c08fd3db79ac9e64f9940231ac9b01256e3484cc285b3f01025b623e3729e0edd885a61493d34dc70fb552ed9d2bb824438e2fc0ff380c02b31ef9553443794897ed483b2f9bd05aada85a16d47");
        input[7] = bytes(hex"03ed1dce403976611a72aa64b18330316e816ef5bf4c846a3412f48350a41f13f0cbcdf88a962aeb8357c164c736fd5404df831a89db69afa3c01b023cf8cb83a099fd8a2018af4d3909");
        input[8] = bytes(hex"075fdff66e3eb2e9e12e3843d2db17aee114eff54f09658934584e3306560af52067d146cb8141e3f7d60e5aec02102936d1baa411f4a62a54a6072b866e1689a0504f11c3fff7e81b67c5fd3f071b492a744974f1ef7a6d6596");
        input[9] = bytes(hex"f336efa8d4ffd1d743a883799563");
        input[10] = bytes(hex"56b03fa6d69fba21a251704727ce10cf079da40c463a360c0d7b2dbd85ff833e7293b2c934a1655d17eeae428ab63542c16f1bb4d0819ef1ba8cbc0608185bafdcba4959174ec049e1fd05bb85882386225dc1b00c666db417ac5c3df7191811d213");
        input[11] = bytes(hex"07ee1d999aaceac34fef098bb797481ea9488bf531871e849a144e9dd4de00");
        input[12] = bytes(hex"7133ba64d5db70e0d614aecf45a2513d2c318b002a00253896c8a6117c11883f013d4d83038b559a4d3efc4acf5f8b0819fb666cd1");
        input[13] = bytes(hex"177a06df87b48eb029fac004381df3055eb4a5279704df9c4b568e832140d544417ac84055e0d065177f8f6189a51ca2766a706de805e448e5bc2ede94076e7cf64f93aa7009e9748295c803af487d4345002fc7767a6ce86ab7ed8ad8");
        input[14] = bytes(hex"181190d108430b1f4c11aaffa722798e43b548ebc8df13e86197e940c400bf53938ddcba07");
        input[15] = bytes(hex"70d858e348c650a00ed04ccdd960aa62e693e0607857e6884c86149e290a024e4b04e293326a5821eea93516db070ab06e2fbe5add6b0d5b1fc88da321a616e56f8b0a9bfe0361550f713f");

        vm.warp(block.timestamp + 319057);
        vm.roll(block.number + 44673);
        vm.prank(0x0000000000000000000000000000000000020000);
        target.addBytesArr(input);
        
        
        vm.warp(block.timestamp + 4);
        vm.roll(block.number + 2);
        vm.prank(0x0000000000000000000000000000000000010000);
        target.check_bytesArr();
        
    }
    
    // Reproduced from: medusa-corpora/corpus-dyn-arr/test_results/1704377304277060000-e1fe2904-517b-4467-90b5-3af5a6574251.json
    function test_auto_check_bytesArr_1() public { 
        bytes[] memory input = new bytes[](59);
        input[0] = bytes(hex"d7879cbd024fd72433d63401e4b12375e20a1656d130196847da066c794b77093af4a5ba77949331e1b41c76eec0d4ac98635e71443d6c52ec39a5844bd7b65cb9e83679c03bfa86ba8d60");
        input[1] = bytes(hex"8d6ba4b61d97143390afd9ef618fec870209b159b2f9cd0a29fa63a50231ce4ad6690560b9e704b7702510c65c");
        input[2] = bytes(hex"aab2f1d90a89a47276c0f5e82f1bd6ab836106bde2b93f3944ee2f5ee0a4cb6645b70609c614d1ff21f6b446f985e366c5cb876ecbe97d10015ba3");
        input[3] = bytes(hex"83a6");
        input[4] = bytes(hex"9ae5358a49747403d86c37a3970f0818846a033fefb0f5e84f0070170edd0cf1563b78cc9dc957442a2167e133ff54d9c8f586aca5800b428467b2645e64a07ef727cddd6f4c4a7c8d7e480fd13208e18774a6e616f2437c36c17409ec42145650fe");
        input[5] = bytes(hex"d0d796462335a0ec9c39d254a76775d1d4bea295920bd2716f6fcc5c91f58d8452c3e537b675f75398de8b4b360d5deca1");
        input[6] = bytes(hex"90cc79b62a38150290d05b91cf5ddc2be1574766ed34b571040893ccfe9a017f4292796b7944206f77e5e53ecf75428b12e49a177de757945224c024ea510ad5d71cd9c33c55ce9ec1");
        input[7] = bytes(hex"aa19c5aab07c2c5be34f0854159d04aaaa23bf80adb0dc6d48ee5ab5492c08e990857b6aeca3592c7499aad9");
        input[8] = bytes(hex"8c2880690d7b66");
        input[9] = bytes(hex"c63826f559b12731f1e17211625a77");
        input[10] = bytes(hex"bb167d72326671545c1ab5bc60");
        input[11] = bytes(hex"9fbf256f1a63f35cddc7314eb013e5ed");
        input[12] = bytes(hex"35e6afe30e9f5652e33e06fccbd60952");
        input[13] = bytes(hex"d2f4c71b344a9305dbf98a239b1140a42224dd7c304f79b6d88090");
        input[14] = bytes(hex"29abdd59a56d53f1ad364e983d5a486f3e3efe62cd18c1d10f");
        input[15] = bytes(hex"8482f2c35661394314d4c9d282e97e0206cf8afce3ecebc9");
        input[16] = bytes(hex"69f62b13f1691c60f90091cb410175ef5fa2fa901e9a320583dd5c7888e974735a23b1043c8e8dbdb921fd1b5448ccef38c4cfced697b1336a4c08644efef150b19c9473313706da9190edba283c6eea738a");
        input[17] = bytes(hex"e0fd4fbe1de11b2c08914a75cff3deb7064394dbc5c877a9f113ad45751a638d303ddce19a920cdfd631323c270735cee852c1eaba6f4672c21b52dcc3dc74d6");
        input[18] = bytes(hex"c5620d59b6e372118c74eebc4af735e45c8c259b3bf960f4fc49ea4592e0bafaa8e29b0c1dcb28c052bedf0d0b413f683830497af94b78969b7441271817d1da405a399a2fc73e2f287dfec3ae93");
        input[19] = bytes(hex"43d16a386f6f6714ea07ec1669415b1d9ce417f31d7eb970f13a9ef555e71201554b702d5067");
        input[20] = bytes(hex"a09e74cd9f0fd8265649f64f54dcdb9b822583f644348394388726b6");
        input[21] = bytes(hex"3c7bebe3f3089e577242606c05dec951c51ed36dac1bf7f5b8e80cf64e739d8c4b89e0ed4f08fa9f7da5ec94a072ebcfe085ac5069f30ba9728d6e30e1c671bc0d97d31eb9d416b2661a96c916eaa250603b0891a2870d560556ea4b");
        input[22] = bytes(hex"419325fb6747ae1251e87397cd6484ef6dd44ba6ab8a41d7eec1625eb7119e0086d6e19149");
        input[23] = bytes(hex"1aaf");
        input[24] = bytes(hex"118f096bafb3dc2c2c4c2882f4");
        input[25] = bytes(hex"de42bab93b9f4868318925b53c2800b3e340fddc32ec28f2733dde1d97ac110ec7d36001860885a70448ed91f0e6379082605469ac3d2b8fc3fb8e7db649087504f93456553e1464b4");
        input[26] = bytes(hex"198a491ad9c3cf481eb050b51391cf2cb0e187f0a09712328221737216f162462889cf76e4d2c74f064744de681f2af6ecb44f286b");
        input[27] = bytes(hex"94b119dfa69a69d734ea71afcd4d5bd37d67e136acaae52f0707df5e31213b65dd991f65c35414da07e47ebbf8dde0138f540273e7162d58cef5c29523af849baae9e6f6807e030be19494f54adda8ad");
        input[28] = bytes(hex"d7b896e41353ab704268");
        input[29] = bytes(hex"4e4df2842cf286a4d8214c67e878308fe8266a7e0852544ebe86cae92f7566ef2473c816b3626f821d2cbe1e00e2c44b587415ceb53dfb99d6e7e186e737acc5602cb327608a5adfd5f969");
        input[30] = bytes(hex"25529723e1c58fd3f57d30d5f5922c1e8734bb0883544adfbc44a70e39e278b9729abe2e22bb1207");
        input[31] = bytes(hex"8567cf1e3f3aabcefcafe5ca0e77de72daa6bad6d94b5aca250df83dc7941fbf64bb04c210");
        input[32] = bytes(hex"1da32ef4478e51abe7661fcd3ed913a86df97bc592c220bfd81d5a48d78499");
        input[33] = bytes(hex"05b33115cbb4880831d3aefae84ee049775695c173f35f63f700cfc069f123f78bc4092c315e3cfdd228680ba3e235");
        input[34] = bytes(hex"1e9667a2895e14f9ff5a9cbf6b3af89cf58b0f0e2a261d2c4c1b31649dd5dbd80cf5a56af716a54bdc2841a87b105e6ce3ae1e");
        input[35] = bytes(hex"e8");
        input[36] = bytes(hex"6e6d4ac33b88f7bd0b800eb01ccc22a2e3e7d736b522e36138e9ff4a31d3f31980d60738821bd375530c7b31bddb75494133595b79b5a26bdff9b3c96b73d5739872c213b14bd50b7a00");
        input[37] = bytes(hex"7db9f66b36f83dfcf3ccb59273c9d02314ed314087004ef59835474856c4ac2e993206ae99c61602ac366eeeb53c292400ea6e071e35aad995b64ddfcc3b3f56fea26c8fd2a8e061fff2edef18b073");
        input[38] = bytes(hex"9393bfe1ec4a569144272fc77e6aa67c9a06e294c197825aa66dc79e72aef4d871d4e36cd22b2bf0bc2dca20f387");
        input[39] = bytes(hex"600e70c5c9b9feb10f3381d92277fd59fe04f3c2610de2b95352dda6bb5dfd07b447aa6cafa82897355095");
        input[40] = bytes(hex"e91f116e1ce9ef7858a56a868f7a197483aa9ee63e1ce12062d6871e2cf5eafa7040048632766cdd25d6e57ad0647404c994b555a4b95a253e29ad9b7a8c031c32879d4c2f8857ff7e8cff54ad3b58fa");
        input[41] = bytes(hex"446cc25abb5ec62816e10b903260c9e127d7b136b4b62626e9ce3592341f3f484bcbd40fd35037144791c51a934644dbb2413d689d1265a1a60739d9c21247ecab0113b494c7f6f1d035c0d6e74a098515002cd7255b");
        input[42] = bytes(hex"19c321277d8bef5c9b2e9b50c1bf4ed11a408f7e10d8e3fb542e78ded8de6b9b237477ebbf48642a28b283599fd43216b04b3be65c1497e05f48b51196b2ad");
        input[43] = bytes(hex"f3710315301514572c983fd917e034fac352fb528342816c3e28afb0557b9b1123dddf9e8db2bb69b0dbb9ebd30a4bee3e7d5d462a1621256d4e3738b95bd503c362295558590b95fc4db2f8c626");
        input[44] = bytes(hex"5cb37c3b7ec370189440a485fb60b95665ef0ab3b1ee13f592c854bb4ddc7302");
        input[45] = bytes(hex"fced6fa361429d8c1f6f6e25eafdf5c07b559bc1ead0cf83e86eabd9435db4e9f4894fc06dbdac0ce9eefea34507f9e2bc0815f84e0ad899c2");
        input[46] = bytes(hex"5b65bbab6b25d9e24856739f9a790984daf8c90478c5e6353046dcae6e8c9a6142b32cad52ccc36c0c31a56fc92d69d1c6cd88d548bef66d7ea77a55b78f70806fcce734438358");
        input[47] = bytes(hex"17d35198d2aca166de401695bed652a501031bbdb04d7943b8a9668147b537df55479b6d0fba678fa03364acebecc063");
        input[48] = bytes(hex"44030368c592964b72cec71c30954a06c128f2b952d40c5b496785b292d6b7d73fb5d83a61327145d88f18f6fd9a645252dfab90908cf2eacd1905d774f1954b3b0efce3133ae4f365a5");
        input[49] = bytes(hex"8a57a3a01f");
        input[50] = bytes(hex"3e6e8da5f0bcb0");
        input[51] = bytes(hex"e6427f45977cf790f04f485b6ed6963176f9a2eb518cb872aa8603319d43c5e400bc0e765fc0ccbc77d5a81d6df7a1eba73152e3c069048764d8d8d7d3e46bb50e6aa274");
        input[52] = bytes(hex"cf186591cbf67b45a74dfb3f11b0f97ddfe172dd616b4c5998dc5eab4eddbf28c9dacf807f7f4ef027e6db4b037089fb21d82e0373cc6d96305abce2faabbdae46daa96ee1bc30f3336ddb");
        input[53] = bytes(hex"970f816dbb89c0205e6e1bb18df85151c139737f74278e52");
        input[54] = bytes(hex"e1a3f3c89034a612ef67076f895d5d9d6f0aa3ce1bb8027ae4f5540aeacfbc96");
        input[55] = bytes(hex"607facb23df0ffb51d19e89a2a520602380fb37516f31590146969a02c176b15b0307bb96538799d23cbe9705365ac42a8b7663054c9f14c365d60baa0af6fd2dac630");
        input[56] = bytes(hex"b3bdcc2e3f6868833904255d37f126e94ff0704c8d488bbee95941aa4a93985e5721416dcf6a7716cec26b45bcecb33894c0c79fc5e039caff60ebfd8fc0ec0079a13c8db1bad03ba704e3e6956b7f6c717f");
        input[57] = bytes(hex"2bbdeed85b3abce2035d24266757123c621de2807022c2f628d6800385d7add0a2fcd48cb7d62c23263687c4");
        input[58] = bytes(hex"172c0ad19f98");

        vm.warp(block.timestamp + 269053);
        vm.roll(block.number + 23881);
        vm.prank(0x0000000000000000000000000000000000020000);
        target.addBytesArr(input);
        
        
        vm.prank(0x0000000000000000000000000000000000030000);
        target.check_bytesArr();
        
    }
    
    // Reproduced from: medusa-corpora/corpus-dyn-arr/test_results/1704377303350862000-7744abc8-f55a-4ab1-b4fc-43380bd596f8.json
    function test_auto_check_boolArr_2() public { 
        bool[] memory input = new bool[](14);
        input[0] = true;
        input[1] = true;
        input[2] = true;
        input[3] = false;
        input[4] = false;
        input[5] = false;
        input[6] = true;
        input[7] = false;
        input[8] = true;
        input[9] = true;
        input[10] = true;
        input[11] = false;
        input[12] = false;
        input[13] = true;

        vm.warp(block.timestamp + 320182);
        vm.roll(block.number + 23884);
        vm.prank(0x0000000000000000000000000000000000010000);
        target.addBoolArr(input);
        
        
        vm.warp(block.timestamp + 360622);
        vm.roll(block.number + 47114);
        vm.prank(0x0000000000000000000000000000000000010000);
        target.check_boolArr();
        
    }
    
    // Reproduced from: medusa-corpora/corpus-dyn-arr/test_results/1704377305545039000-e0720184-376d-45f2-9a03-673a130654e4.json
    function test_auto_check_strDynArr_3() public { 
        string[] memory input = new string[](85);
        input[0] = unicode"\u00cd";
        input[1] = unicode"\u0074\u00ad\u009f\u0037\u005d";
        input[2] = unicode"\u006a\u00b1\u0070\u00d5\u00a8\u00fb\u0093\u00be\u00b6\u0089\u0015\u0000\u009a\u0094\u0043\u00ff\u0012\u00a5\u004e\u0027\u0082\u0044\u006c\u009e\u002d\u00a6\u003b\u0025\u00f5\u00ef\u0016\u00e8\u0097";
        input[3] = unicode"\u007c\u00fe\u0039\u008d\u001b\u009a\u0041\u0066\u002a\u0024\u00d4\u0087\u004c\u004a\u00d3\u00c2\u0058\u00a0\u0096\u0059\u00a0\u00e2\u00d9\u0013\u009f\u0002\u0022\u00f0\u0035\u0011\u0054\u0094\u00a8\u0093\u008a\u000c\u0060\u00c5\u0032\u00f5\u0058\u00c9\u000a\u003f\u00d8\u00a7\u00b6\u000e\u001a\u00a5\u0027\u001d\u00b6\u005c\u00a0\u005e\u0021\u00d3\u007f\u0007\u004b\u0020\u00df\u005b\u002d\u004f\u00d9\u003c\u004e\u0028\u00d7\u0057\u0091\u00cb\u002a";
        input[4] = unicode"\u00cf\u0028\u00bb\u0047\u0040\u003a\u00db\u00e4\u00c8\u00b9\u00fd\u00ab\u0022\u00b7\u0045\u00c0\u0054\u007f\u00c5\u00e0\u00c3\u00b6\u004c\u0048\u004d\u00a8\u00ec\u00aa\u00db\u00bf\u00aa\u0008\u00ac\u00a3\u0022\u0017\u00ec\u00fb\u0011\u002b\u00f9";
        input[5] = unicode"\u0099\u0022\u0042\u0085";
        input[6] = unicode"\u006e\u00fc\u0013\u009f\u00c1\u00b8\u0020\u00d8\u0025\u00e1";
        input[7] = unicode"\u0026\u0086\u005c\u0079\u0041\u005b\u00c8\u00ad\u0043\u009d\u009a\u007e\u001b\u00eb\u00cd\u0096\u00c0\u002a\u0065\u00e1\u00a7\u0064\u007c\u00db\u0096\u0034\u0074\u00fe\u0092\u0081\u00e0\u008b\u0007\u0009\u0092\u00db\u0073\u0058\u00d0\u00db\u0012\u00db\u005b\u000c\u0031\u0037\u00ef\u00d2\u004d\u0007\u0093\u005d\u0088\u00e7\u0042\u0067\u00b8\u003d\u00a6\u00e0\u00bd\u00a0\u00f7\u0075\u00cc\u00b0\u00e3\u00f6\u00cf\u0033\u006b\u00c5\u0028\u0052\u00ee\u00ea\u00dd\u005e\u0011\u0008\u004b\u0012\u0045\u00fc\u0052\u0089\u0043\u0076\u00ca\u000e\u004a\u008c\u00e6\u0083\u008f\u006a\u007a\u009e\u0035\u00e7";
        input[8] = unicode"\u005b\u0051\u00b1\u0031\u0013\u005f\u0016\u002e\u0095\u0070\u0032\u008b\u00c8\u00c5\u0077\u00e4\u00dd\u006a\u001d\u0032\u007f\u00ff\u0011\u00f8\u0072\u006a\u004a\u00bc\u00aa\u002d\u0038\u00be\u0042\u009d\u0064\u00c1\u006d\u005f\u0054\u003a\u0098\u0094\u00e8\u0022\u0041\u0071\u00b7\u00af\u00f8";
        input[9] = unicode"\u005a\u006f\u00c1\u00c5\u008d\u00d5\u0061\u0089\u00a0\u004a\u0085\u0095\u00b9\u0065\u007a\u0081\u0063\u008a\u00ec\u009a\u00c1\u00c5\u0018\u00b8\u008a\u0044\u00b3\u0093\u006f\u001a\u00f1\u00e5\u0016\u00a7\u002e\u00e1\u00fc\u0090\u000c\u0002\u0087\u00b2\u0039\u0062\u0054\u00a2\u0062\u0088\u0049\u006e\u0037\u004d\u0075\u006c\u0064\u0032\u0085\u00f4\u0087\u00fa\u0064\u00b4\u001e\u0084\u004a\u0004\u0030\u00bd";
        input[10] = unicode"\u0010\u00fa\u0042\u0056\u00bc\u00c6\u00c9\u00a5\u00a5\u00cb\u0077\u009f\u00f3\u0034\u0013\u00f1\u003f\u006c\u00f4\u00f8\u0027\u0098\u006b\u00fc\u007f\u00b2\u0018\u0076\u0074\u0045\u00aa\u002a\u0068\u0040\u00fc\u0074\u00c3\u0081\u005f\u003c\u005f\u002a\u009e\u003a\u0098";
        input[11] = unicode"\u0097\u0087\u001a\u00c1\u00ca\u00b8\u003d\u0091\u003f\u0028\u004e\u00d5\u002b\u00e8\u0038\u00d5\u00e5\u00b0\u0091\u00e4\u002a\u003a\u0069\u000b\u0083\u0071\u002e\u0080\u00f3\u0041\u0064\u0039\u00f0\u0088\u006e\u0009\u00eb";
        input[12] = unicode"\u0012\u00c3\u009e\u00ff\u00bf\u00ee\u006d\u0033\u0088\u0046\u006d\u00a9\u0092\u00b3\u00ca\u00e8\u00f9\u00b1\u0039\u00c6\u00d0\u00c4\u00aa\u00d8\u005d\u002c\u00fe\u00e7\u004c\u0044\u0062\u004d\u00fd\u0084\u00b0\u0054\u0012\u00c5\u0059\u00d4\u002f\u00fe\u008b\u00a6\u0089\u003e\u008c\u00c8\u0049\u0084\u0047\u00fb\u0025\u00e5\u00f1\u00fd\u00fa\u005a\u0093\u008e\u0094\u0073\u009b\u0089\u005e\u00a3\u002b\u002d\u0090\u0010\u0022\u00dd\u0061\u0076\u00a4\u0004\u00c5\u004e\u007c\u009c\u00b9\u0058\u00d7\u00c3\u00b8\u00a1\u0044\u0046\u00bc\u00f5\u00b4\u00d5\u000a\u0073\u0061\u00d7\u00c1\u00d0\u0063\u00c5";
        input[13] = unicode"\u00b0\u001e\u0076\u0009\u0014\u0087\u0078\u00fd\u0058\u00d9\u0055\u00f6\u00b2\u0060\u0026\u0073\u006d\u002a\u0017\u0099\u00b8\u0085\u00bb\u00a4\u005c\u0094\u001c\u00e7\u0025\u007a\u0065\u00c7\u0069\u00fd\u004f";
        input[14] = unicode"\u002a\u0075\u0042\u0034\u0010\u0071\u00de\u00ff\u0008\u000e\u0005\u0074\u007e\u00de\u0072\u0091\u00fe\u0032\u00a6";
        input[15] = unicode"\u00ff\u0074\u00bc\u0040\u0078\u00b2\u007b\u00e2\u0047\u0030\u00be\u001b\u006e\u00d7\u00a4\u0022\u0053\u0070\u00bc\u003c\u006f\u008c\u00d7\u0019\u005c\u00ec";
        input[16] = unicode"\u007e\u00a6\u009d\u0084\u0043\u0072\u0073\u00e7\u00db\u0021\u004f\u0022\u00b9\u006a\u0005\u00a9\u0038\u00ba\u0086\u0063\u0070\u0010\u0020\u006e\u001f\u0061\u00b9\u0037\u00bd\u0006\u002d\u00e6\u00e1\u0006\u00f9\u0007\u00aa\u0049\u00d3\u0028\u0074\u008c\u0052\u0038\u0051\u00a5\u0087\u00c3\u00b6\u0023\u005a\u0097\u00dd\u0058\u003e\u00b8\u00e4\u00ec\u0020\u0046\u00c9\u007a\u0079\u0049\u00e6\u0097\u00a6\u00fb\u0077\u0014\u00c8\u001f\u0036\u004a\u00ee\u00ea\u000c\u0038\u00c8\u0082\u0096\u006b\u0088";
        input[17] = unicode"\u00aa\u0018\u0050\u0057\u0058\u0037\u00fc\u001f\u00ad\u0004\u0028\u0039\u0017\u0053\u00ca\u000d\u0088\u00da\u0080\u00e6\u00d4\u0019\u0010\u0082\u001c\u00ab\u0010\u0010\u00b7";
        input[18] = unicode"\u009c\u00d8\u00c1\u0003\u00d8\u0094\u0061\u00ce\u000e\u00aa\u0014\u00cc\u00c7\u0070\u00bd\u00c4\u00aa\u00c8\u0067\u00fc\u004e\u0078\u0010\u004a\u0066\u0060\u00d6\u00c7\u0035\u0093\u00ed\u0046\u007e\u00f0\u004b\u007e\u00bb\u0056\u00ec\u0059\u0064\u00a2\u00fe\u000c\u003a\u0081\u0009";
        input[19] = unicode"\u00ef\u009c\u0099\u003c\u0055\u00bf\u00dc\u00c9\u0073\u000d\u00fc\u006f\u000a\u00e6\u0008\u009c\u0076\u00a1\u009b\u00c1\u00ef";
        input[20] = unicode"\u00a6\u0052\u0003\u00f1\u0074\u005b\u0016\u004a\u00c9\u00cf\u00c9\u0039\u00be\u00b4\u00c4\u007a\u0051\u002f\u0053\u00c8\u0008\u00d1\u0091\u0050\u00e8\u0000\u0060\u0024\u00ac\u009b\u0061\u0025\u0088\u00ee\u005e\u00d5\u0062\u0088\u00e8\u0044\u00a7\u0088\u0006\u00de\u00b3\u00b2\u00cc\u005b\u006b\u0066\u0075\u0021\u00a7\u0038\u0068\u00bf\u0097\u00d9\u0009\u0039\u0048\u00a8";
        input[21] = unicode"\u0016\u00d9\u00e2\u00a4\u0036\u0055\u00ed\u0066\u0083\u00d0\u0020\u0063\u00ce\u00d6\u0085\u00fc\u00d8\u0023\u0034\u00be\u00c3\u0041\u00ea\u00a7\u009f\u0074\u00c1\u0064\u004e\u00b2\u008a\u009c\u00d1\u00b4\u0059\u008b\u00e6\u00e6\u0042\u0070\u0025\u006f\u0089";
        input[22] = unicode"\u00e0\u00bf\u0072\u003b\u00a8\u0034\u00b1\u0044\u0037\u00c8\u001b\u003f\u00e2\u00ec\u00e8\u008b\u005e\u0066\u00c3\u0010\u00e4\u005d\u000d";
        input[23] = unicode"\u004f\u008f\u0012\u0043\u00d1\u00d0\u003c\u0067\u0055\u0068\u00e5\u0092\u0091\u00e9\u0026\u00cb\u0095\u00ba\u0000\u00cd\u0067\u00c6\u00d6\u0073\u0056\u00ee\u0058\u00ce\u007b\u007b\u0040\u00a4\u00a4\u00a8\u009f\u00b7\u00c3\u0083\u003f\u00f5\u00b5\u003c\u009e\u00bc\u0082\u00ba\u0069\u00e9\u00b9\u00eb\u00d3\u00d4\u0066\u00cc\u008e\u00b4\u005b\u006d\u00b5\u00bf\u0044\u00f7\u00ed\u00af\u00db\u005c\u0033\u0081\u005d\u0096\u00ca\u00c9\u00ec\u008c\u00d9\u00b7\u006c";
        input[24] = unicode"\u0041\u0012\u0010\u004c\u008a\u00c5\u002a\u00ea\u00c5\u00a6\u000f\u0005\u00fc\u000d\u0039\u0069\u0047\u0055\u00a0\u0051\u004e\u0088\u006f\u00d7\u0033\u00bd\u00ed\u0032\u00f8\u00c0\u0033\u0043\u00cb\u006a\u001c\u00b8\u0044\u0063\u00a4\u0035\u00bb\u00e2\u002e\u0041\u003d\u0079\u00a8\u0007\u00ea\u0047\u00ee\u0015\u0042\u00c9\u0021\u00a9\u0084\u0053\u004c\u004f\u00f7\u006b\u009f\u00e1\u00b6\u000b\u008a\u00a4\u004c\u003f\u00d4\u0005\u00a6\u0005\u0070";
        input[25] = unicode"\u0094\u001a\u001a\u00df\u0002\u003d\u0030\u003f\u00df\u0049\u00c3\u0043\u0078\u00e1\u00cf\u002c\u0045\u0003\u00d3\u006b\u0041\u0023\u0053\u00c7\u0072\u0056\u0075\u0014\u00e5\u00a3\u00c2\u00c0\u00c1\u002c\u00e4\u0088\u005c\u00fa\u00d4\u00f3\u00d3\u0006\u00a2\u0027\u0091\u0033\u0016\u0002\u00dd\u003a\u0024\u00d7\u0031\u0080\u00be\u0017\u0054\u00b4\u00e3\u0058\u00f7\u0077\u00ec\u0006\u0090\u00b8\u00f9\u0063\u0008\u0079\u00f0\u002e\u0051\u00a4\u00df\u00b3\u0088\u00e6\u00ca\u00ca\u00ee\u00e6\u008b\u0050\u00cf\u008e\u0074\u00f1\u001c\u0074";
        input[26] = unicode"\u00fd\u00ad\u0092\u0076\u001e\u00fc\u000f\u0041\u0078\u0010\u00a9\u004e\u0093\u0085\u0010\u0052\u00a6\u0083\u00da\u00c2\u00b4\u00d3\u00f9\u00d9\u00d2\u0049\u009b\u0009\u00db\u00aa\u0032\u0050\u0074\u002e\u00f1\u0016\u004f\u000f\u0092\u00de\u005c\u001a\u0092\u002f\u0074";
        input[27] = unicode"\u0034\u0045";
        input[28] = unicode"\u00b5\u004c\u0050\u00f9\u00fb\u003f\u0013\u005c\u003a\u00b0\u004b\u00e5\u00c9\u00f0\u00b4\u00d7\u0082\u000a\u000e\u0046\u0021\u0072\u0028\u0006\u00cd\u00a4\u006d\u0055\u00f3\u00cb\u0056\u00db\u007e\u00de\u006d\u0007\u0008\u0053\u0023\u0029\u007c\u00e8\u009a\u0056\u00c3\u0009\u002f\u009c\u00b9\u00c0\u00f3\u00a4\u00f1\u002d\u0014\u0067";
        input[29] = unicode"\u00ad\u00a1\u0031\u00bb\u0050\u0073\u0024\u003c\u00f0\u00b2\u007a\u00ce\u009b\u004c\u008e\u0098\u001f\u00ac\u00c8\u0075\u003d\u0004\u00ce\u00b7\u00cc\u00be\u00e6\u0078\u00ca\u0067\u0045\u004b\u0020\u00e7\u0092\u00bb\u00cb\u002c\u004a\u00ca\u002e\u0069\u00e2\u0033\u0016\u00d2\u0082\u00b1\u008f\u003b\u0055\u0036\u00c0\u0006\u006c\u001e\u00ea\u00e9\u000a\u006e\u0060\u00a8\u000b\u00ed\u00c7\u0087\u0096\u00d2\u0030\u0026\u00b3\u00ec\u00fd\u00c9\u00ee\u0081\u0086\u0033\u00c3\u005d\u0096\u000b\u00cd\u000f\u000b\u001b";
        input[30] = unicode"\u0084\u008a\u006b\u00c0\u0083\u0091\u00da\u0097\u002c\u009b\u005b\u004e\u0074\u0022\u007c\u004a\u00d2\u000c\u0016\u004e\u000f\u00bb\u00ac\u00a8\u00b7\u00e4";
        input[31] = unicode"\u00b7\u003b\u0044\u0090\u003f\u00bb\u00b2\u00ff\u003c\u004d\u00e1\u004b\u0058\u00ff\u00a2\u004e\u00b2\u00ca\u0056\u00e5\u00fe\u0012\u00c9\u003b\u00c2\u0033\u003a\u005d\u0088\u00e0\u0077\u0090\u0050\u00d8\u00ce\u00e1\u00bf\u0009\u00bc\u0061\u002d\u00ff\u00ca\u0094\u00ea\u0069\u0016\u00d9\u0047\u0077\u00f2\u0022\u00ac\u0094\u0008\u0044\u008e\u00cb\u00d9\u00d2\u00a7\u00cf\u0080\u0095\u0027\u0045\u0024\u0096\u0010\u001c\u00ed\u0054\u0065\u00ad\u00c0\u00f2\u008f";
        input[32] = unicode"\u00ad\u00df\u0038\u0060\u00a3\u00b7\u00ba\u0091\u0042\u000d\u0041\u00c7\u00c7\u00e7\u0070\u008f\u007b\u0084\u00c8\u0065\u007b\u009b\u007a\u0062\u0068\u002c\u0070\u00f5\u000a\u0032\u009d\u009a\u0055\u0026\u00ba\u0083\u005b\u0013\u00dc\u00ae\u008d\u0094\u007b\u0070\u005a\u0021\u0010\u00f4\u00b5\u0033\u003d\u0001\u00d1\u001f\u0012";
        input[33] = unicode"\u0019\u004a\u002e\u00c4\u00d4\u000c\u00de\u008c\u00fe\u008d\u0036\u0016\u00d4\u00d0\u00fa\u0023\u0037\u0008\u00ab\u00ba\u00c8\u0035\u00c0\u0083\u0073\u007f\u00ea\u00ec\u002e\u007f\u00ce\u00b4\u006b";
        input[34] = unicode"\u0055\u0008";
        input[35] = unicode"\u0007\u0072\u002f\u004e\u002d\u00bf\u0078\u0073\u006f\u00d1\u009f\u00ca\u00b7\u008a\u00ec\u007b\u004d\u0047\u00e0\u0057\u0020\u00f6\u00e4\u0002\u001d\u00c4\u002b\u00fc\u0000\u007f\u0001\u0052\u0000\u003b\u0021\u003b\u00be\u001d\u00ba\u00c0\u0031\u003d\u00e6\u00e0\u00e7\u002a\u0053\u002c\u00e1\u00fe\u0095\u0018\u007f\u006a\u0023\u001a\u0026\u00b3\u00b9\u00bc\u007d";
        input[36] = unicode"\u008a\u0015\u00f0\u0026\u0048\u0070\u00c5\u00a4\u00e8\u0080\u0023\u0054\u0001\u007b\u005f\u0067\u00ed\u0097\u00e2\u003f\u005a\u005c\u00fe\u00ba\u0015\u004f\u005a\u004d\u002b\u0049\u00b2\u00cd\u0084\u005d\u0032\u00cd\u0010\u004c\u00e6\u0080\u0005\u00e4\u00e3\u001a\u0050\u001b";
        input[37] = unicode"\u0023\u0093\u00ab\u0042\u00bc\u008b\u00e6\u005a\u00c8\u0073\u0064\u000c\u0058\u00ca\u0034\u0053\u008e\u00cd\u0033\u0065\u002e\u0056\u002e\u00e6\u0046\u0095\u001b\u00a2\u009b\u0061\u0051\u0024\u0037\u0076\u00b7\u006c\u00a9\u006d\u008a\u0076\u003b\u00e3\u0079\u00b6\u0080\u000c\u0066\u0020\u00fe\u00b5\u005a\u0089\u009b\u0073\u0095\u0078\u00b6\u0053\u00e8\u00b9\u00c4";
        input[38] = unicode"\u0096\u00f1\u0002\u00bc\u002e\u006d\u008c\u0069\u0011\u003f\u00c8\u00c1\u00af\u0004\u0064\u0052\u0092\u00c8\u0089\u007f\u00cf\u0004\u00f3\u0011\u00ae\u00aa\u004c\u0008\u0051\u0053\u001e\u0082\u004b\u00b3\u001b\u006c\u00ae\u0054\u0005\u0029\u00e4\u0070\u0029\u007a\u0014\u0072\u0069\u0014\u004a\u00ae\u00df";
        input[39] = unicode"\u005c\u003d\u00f0\u004f\u0062\u008c\u000e\u002f\u00ac\u00cb\u00cf\u00bc\u0031\u00f5\u0096\u00f1\u0026\u0043\u00a5\u00c1\u00d7\u0076\u0058\u00a1\u00bf\u00d2\u0067\u00a0\u007d\u00ad\u00c4\u0089\u0060\u00c7\u00de\u0049\u00bb\u006b\u00f4\u0015\u00ba\u00fe\u0041\u0089\u00f6\u009c\u0049\u0037\u00d8\u0043\u0040\u001c\u00fa\u00c7\u00f3\u00b6\u00f8\u0070\u0072\u0053\u008e\u0031\u00c1\u009f\u001d\u0071\u007d\u00e8";
        input[40] = unicode"\u0075\u00c0\u005f\u00b1\u00c4\u0045\u0066\u006f\u008f\u00f6\u0096\u000c\u0055\u00fa\u0052\u0048\u0082\u0096";
        input[41] = unicode"\u00be\u00f9\u0068\u001e\u0086\u00e9\u006f\u00c2\u0008\u0092\u00d4\u0060\u00cf\u0095\u005b\u0026\u0001\u0048\u0039\u001d\u0072\u0034\u0083\u00dd\u009b\u0015\u0025\u00dc\u004c\u00cf\u00ce\u0066\u00c4\u006a\u0009\u003b\u0051\u0090\u009c\u000d\u0083\u00ef\u00a2\u00c4\u00a7\u005e\u00be\u003d\u007f\u00e3\u0015\u0065\u001f";
        input[42] = unicode"\u00d8\u0083\u00ca\u0073\u0088\u001c\u009d\u00a5\u00a7\u0061\u00e7\u00ec\u004b\u00a8\u0018\u003b\u0081\u005a\u00c3\u0054\u0088\u0088\u0041\u00f8\u007f\u00b1\u00a5\u002e\u0089\u006e\u009a\u0037\u0014\u007f\u00a5\u00c8\u003b\u00c6\u00ad\u0004\u0028\u0083\u0042\u00ce\u009e\u00cc\u002a\u0085\u00e9\u0074\u0002\u00f6\u0081\u00da";
        input[43] = unicode"\u00e5\u0087\u00d5\u00e1\u0076\u002d\u00a0\u0057\u00c8\u004f\u007f\u008f";
        input[44] = unicode"\u00a3\u0061\u002c\u00f6\u00e0\u00e1\u001b\u00b3\u00f9\u0015\u00da\u004c\u008c\u000f\u00a7\u00cb\u0094\u0076\u0045\u004b\u00f8\u00be\u001b\u0086\u004b\u0044\u001d\u00ba\u0065\u0076\u00e2\u0016\u0053\u0022\u007d\u0064\u00e0\u0021\u00bc\u007e\u00d9\u0096\u00b3\u005f\u00ce\u002b\u0063\u00f2\u007f\u00d5\u00c4\u003e\u0022";
        input[45] = unicode"\u00c9\u00e8\u00d0\u0091\u004a\u00fe\u0037\u00e0\u005c\u00e7\u006b\u0002\u001c\u0098\u000c\u001f\u00eb\u00fe\u008f\u00ea\u0081\u00f2\u001a\u0045\u003a\u0046\u005f\u0029\u00a6\u00e6\u0063\u0090\u0010\u003e\u00f7\u0099\u00fa\u00b7\u00ef\u00d3\u00cc\u0050\u00b2\u0046\u00e5\u007f\u00e7\u008d\u0044\u0088\u007c\u0002\u00e9\u00ad\u0062\u0032\u001a";
        input[46] = unicode"\u0058\u00eb\u0019\u00a6\u0073\u00e7\u00c8\u00f7\u00cf\u0008\u006b\u0005\u0029\u0066\u004b\u002a\u009b\u0092\u0060\u00b6\u007f\u00de\u00bf\u0025\u00e6\u0083\u00c6\u00c3\u00d7\u004b\u009f\u00dc\u0006\u0013\u007a\u0016\u006a\u0058\u00db\u00a1\u0013\u001c\u0070\u00c0\u008e\u001c\u0040\u00c2\u00cc\u007b\u001e\u0086\u00c9\u00e0\u006f\u002d\u00e6\u005b\u0042\u00b3";
        input[47] = unicode"\u0035\u002c\u00a6\u002b\u0033\u00c1\u00a5\u0018\u00d6\u0022\u0047\u00c5\u00fe\u009f\u0037\u0090\u0069\u0057\u0008\u00b5\u0061\u007e\u0027\u00aa\u00c5\u0095\u0092\u0009\u0096\u0071\u0021\u0029\u00db\u0026\u0003\u0019\u00ab\u0075\u00dc\u00bb\u00b8\u008f\u005a\u00a9\u007d\u0031\u0081\u0098\u005d\u00d0\u00c7\u0025\u00d2\u004a\u00ec\u005f";
        input[48] = unicode"\u0027\u00ef\u0040\u00eb\u0034\u008f\u0021\u00d6\u005c\u00ba\u003c\u0094\u006e\u0088\u00e0\u0057\u003a\u00d4";
        input[49] = unicode"\u0050\u00be\u0040\u00ba\u007b\u007e\u00ba\u0002\u0098\u0076\u0086\u003e\u00bf\u00a1\u0008\u00ce\u00e0\u00b7\u005b\u0083\u0038\u00ee\u0059\u0056\u004a\u0080\u00e0\u006c\u00aa\u008b\u0038\u008c\u0044\u00b0\u00c8\u00dd\u004f\u00a0\u00f0\u00fc\u004f\u00a9\u0033\u00a3\u0025\u0063\u0060\u0040\u0007\u0002\u005a\u0052\u00d2\u0068\u00eb\u004a\u00ad\u00f8\u0018\u0031\u00f9\u008c\u00df\u009e\u0070\u00c8\u00de\u0016\u00fe\u0085\u0043\u0045\u0062\u005b\u0058\u0061";
        input[50] = unicode"\u00a7\u00e6\u0012\u0075\u0062\u000d\u0011\u005e\u0036";
        input[51] = unicode"\u00dd\u00d6\u0086\u00ae\u00a1\u008f\u0033\u0067\u000a\u0051\u0093\u00cb\u0038\u0076\u009a\u00a5\u00bb\u00c4\u00fe\u0020\u0070\u008f\u00a0\u00ec\u0090\u00e7\u00f1\u00b5\u0086\u009c\u0099\u00d5\u00b2\u0033\u006f\u009b\u00fa\u0012\u00bd\u0000\u0046\u0046\u0052\u001d\u00bc\u0008\u00c5\u0084\u00ce\u00e6\u005d\u006c\u008a\u0005\u00d7\u00f8\u0084\u0029\u00e7\u0088\u0057\u00b4\u0040\u000e\u00ac\u00f3\u006d\u0083\u00af\u003d\u004f\u0009\u0074\u002b\u00ff\u009c\u00df\u00d7\u0097\u004b\u00ec\u00d7\u0083\u00f3\u004d\u00fe\u00af\u0052\u0015";
        input[52] = unicode"\u00ef\u001b\u003a\u00e3\u0025\u000a\u0081\u00fc\u0028\u0055\u003b\u007e\u0053\u00d9\u0075";
        input[53] = unicode"\u0033\u00d6\u0025\u00d9\u0085\u0082\u0004\u0002\u00d0\u00ea\u00dd\u0011\u0080\u00d1\u002b\u00ad\u00e6\u00af\u00bb\u00b6\u0048\u00e7\u009a\u00cd\u006a\u0070\u0072\u0022\u00d4\u00fb\u0049\u0098\u00c0\u0045\u00f5\u0018\u00f2\u00cc\u0069\u00bf\u000f\u00c0\u00b2\u0013\u0009\u00f9\u0089";
        input[54] = unicode"\u002f\u001d\u0021\u00b3\u00da\u006e\u0086\u0084\u0051\u002e\u0084\u00f8\u0095\u0067\u00e8\u0014\u0042\u00b2\u0095\u00f8\u0094\u00a8\u0044\u00be\u0054\u00e0\u000d\u001f\u0012\u0076\u002d\u0041\u0095\u0048\u00cb\u004d\u0003\u0066\u0009\u008e\u00cc\u009e\u0094\u00a7\u00fe\u00af\u005b\u00ff\u00d5\u005c\u0012\u008a\u00e1\u000c\u002b\u004d\u00ee\u0013\u00f0\u00b9\u006b\u00f6\u00d8\u005d\u00cb\u00bc\u0092\u00c9\u006a\u008f\u0098\u002b\u0030\u008c";
        input[55] = unicode"\u00bd\u0029\u000f\u00d9\u0071\u0057\u00ac\u00c1\u00a3\u000d\u009a\u004e\u005a\u00d1\u009d\u0093\u0008\u0099\u0023\u007e\u008c\u0008\u00cd\u0052\u005e\u0027\u00e1\u00ad\u00a2\u00e6\u0068\u00da\u00a6\u0007\u00b4\u007f\u004f\u00e0\u009e\u0041\u00cc\u00f4";
        input[56] = unicode"\u005b\u0018\u00a8\u00e0\u00f1\u0039\u0036\u00f6\u001f\u0016\u0061\u00ba\u00aa\u00ee\u0060\u003f\u00d5\u0036\u0067\u008f\u00c1\u0079\u0069\u0091\u006b\u0024\u0010\u0007\u00bb\u0090\u0088\u0069\u00b1\u0092\u005b\u0004\u0010\u00d3\u00b6\u0052\u0052\u00e0\u00db\u007f\u0040\u0063\u0005\u000a\u0028\u00aa\u00d8\u00b0\u00af\u00d7\u00c2\u00cf\u001f\u003f\u0046";
        input[57] = unicode"\u0044\u00d5\u0066\u00b5\u00de\u006e\u0099\u0074\u00b8\u00db\u0099\u0008\u00b0\u00d9\u000c\u0028\u00e6\u00ac\u00cd\u00a2";
        input[58] = unicode"\u0066\u00ae\u002e\u00b3\u005b\u0063\u003b\u00c3\u004a\u0070";
        input[59] = unicode"\u00f2\u00e9\u0044\u0059\u0021\u0076\u0085\u008f\u00a0\u0027\u008d\u009c\u0073\u0035\u00e5\u00c3\u004b\u005d\u0044\u0057\u000c\u003a\u00ac\u006a\u00e7\u00d8\u000c\u0018\u00cd\u007f\u0095\u0010\u001f\u0092\u0085\u00f5\u006f\u0008\u00c1\u0038\u0087\u0023\u0087\u0020\u00d9\u00a2";
        input[60] = unicode"\u005d\u0039\u006a\u00b4\u0024\u0031\u0017\u00a6\u0008\u00ed\u0017\u004f\u00d7\u0018\u0054\u00e1\u0092\u00bd\u0010\u0040\u0049\u009d\u00e9\u00ed\u004f\u00d3\u009c\u00ef\u00a1\u002d\u0029\u0071\u00bf\u00f4\u007c\u0080\u0025\u002e\u00b8\u009e\u001e\u00cb\u00cd\u00d5\u0080\u0064\u00ab\u0072\u0094\u00de\u006f\u00de\u0037\u0033\u0009\u00fb\u00b7\u0074\u00a6\u0093\u0051\u00d7\u00d1\u0080\u009c\u0002\u0039\u0054\u0098\u0082\u004e\u005a\u0073\u0042\u0060\u00b1\u00a0\u000c\u007f\u00c3\u0013\u0086\u0004\u00b1\u00aa\u0084";
        input[61] = unicode"\u0093\u00d6\u0049\u002f\u00d3\u005e\u0079\u0014\u002f\u007a\u0080\u00a1\u003e\u00c9\u00a8\u005d\u000b\u002f\u0073\u0057\u0070\u00cb\u0034\u0004\u0098\u00e5\u00eb\u0080\u000b\u0068\u0004\u003c\u0049\u005a\u0003\u00ca\u0026\u008f\u00dd\u00ea\u00ce\u00c3\u00d0\u00a3\u00a3\u0038\u008e\u008b\u004f\u00bf\u00cd\u00b8\u009e\u00d5\u00b1\u0042\u00c6\u00d7\u00bd\u0053\u00f3\u0085\u0004\u00ae\u00e1\u0069\u004e\u0011\u00d0\u001e\u00ab\u006e\u0021\u0014\u002f\u0040\u00f1\u0096\u00d5\u00ea\u00c5\u00a7\u00ec\u00cd\u0075\u00ba\u0073\u00f9\u00d6\u0057\u007d\u00b8\u00c3\u005c\u00ed\u0088\u00ed\u0016\u00ea\u0034";
        input[62] = unicode"\u00f0\u00fe\u00fd\u002b\u003f";
        input[63] = unicode"\u00e9\u0076\u0034\u00f0\u0037\u0023\u00f6\u0078";
        input[64] = unicode"\u000d\u0082\u000c\u00bb\u002d\u00f2\u00a6\u00c8\u004a\u0034\u0029\u00fa\u0081\u0017\u001b\u00cb\u0019\u0089\u008d\u002f\u00fd\u0001\u0099\u0015\u003d\u0073\u0058\u008d\u00ba\u005c\u00d7\u00a5\u00b8\u0058\u0093\u00a3\u005b\u00e2\u00ba\u0080\u0045\u00bf\u0069\u0065\u0033";
        input[65] = unicode"\u00c0\u0067\u00d8\u009f";
        input[66] = unicode"\u0095\u003a\u004b\u0096\u0062\u006e\u00a9\u0003\u005b\u0002\u0030\u00e5\u0019\u00bd\u00d3\u00ce\u00f2\u0066\u0063\u00a1\u0036\u0025\u005c\u00e0\u00b3\u0098\u004e\u001b\u00ad\u00dc\u0019\u000d\u00cf\u000e\u001c\u0047\u00aa\u00a2\u00ee\u00c6\u009b\u00e6\u0053\u003f\u002c\u008f\u00e2\u003d\u00b4\u00b4\u00fe\u0071\u005d\u00a1\u00cd\u00e5\u00ab\u0066\u009c\u00c6\u003d\u0067\u00d2\u005c\u004d\u0097\u00f4\u00f1\u0017\u0062\u000c\u006a\u002e\u002a\u00f4\u00c8\u0017\u007d\u00ed\u0055\u008b\u00d9\u00b3";
        input[67] = unicode"\u0067\u007f\u0043\u008d\u00c7\u0027\u00bb\u0064\u00a0\u0027\u00a9\u00d6\u00c9\u00d7\u00a4\u00ac\u0058\u00fc\u0015\u003e\u00b8\u0027\u00ef\u008d\u00f5\u00c0\u0079\u0010\u00c7\u0018\u0046\u0022";
        input[68] = unicode"\u003a\u00f5\u009c\u00d4\u002b\u00c1\u0034\u009c\u0054\u00bb\u0055\u003f\u0090\u00c6\u00a0\u00f8\u0090\u005a\u004f\u00e4\u00a6\u00f6\u00d5\u00e0\u008b\u0088\u0073\u00aa\u00fd\u0002\u000f";
        input[69] = unicode"\u00b8\u0032\u0081\u006e\u0019\u00bc\u0089\u00cd\u0080\u00b5\u0063\u00df\u00ae\u00c1\u00ac\u0070\u00ae\u00dc\u00e4\u00ed\u00e9\u0044\u0080\u0097\u00a9\u00d7\u00fb\u008c\u00fb\u00e4\u008c\u00be\u0084\u00db";
        input[70] = unicode"\u00f3\u0045\u00ee\u0023\u00d1\u006d\u00ca\u00e4\u00e2\u0021\u009e\u005d\u00c3\u00a4\u0014\u0055\u00cd\u00c1\u004a\u0068\u00b8\u0053\u00dd\u0001\u004b\u00ab\u00ca\u0024\u0049\u005a\u0075\u00eb\u006b\u00e2\u000b\u00ac\u0084\u006b\u000f\u0088\u002d\u003c\u00a6\u00dd\u0001\u002c\u00eb\u00ac\u0085";
        input[71] = unicode"\u00ce\u0004\u00c4\u00c9\u0095\u0045\u00bb\u00a8\u0037\u00cb\u00e5\u0085\u0008\u0007\u00eb\u003c\u00c8\u0020\u006d\u006b\u006f\u0095\u0045\u0070\u0038\u00a3\u0052\u005d\u00e3\u00e1\u00e6\u0016\u00b4";
        input[72] = unicode"\u0081\u00f2\u0092\u0012\u007c\u008a\u0090\u007d\u005e\u0064\u00b7\u0049\u00b9\u0021\u00dc\u008e\u005f\u0048\u0062\u00fc\u00eb\u00a0\u002d\u0026\u005d\u00cc\u00eb\u0082\u0031\u0057\u00ce\u007e\u00a6\u009b\u00fe\u00dd\u005a\u009d\u0000\u0045\u0081\u00f4\u00af\u004e\u0042\u0041\u009c\u009b\u00eb\u0070\u00b9\u001c\u00b0\u00de\u0049\u00a0\u0003\u0018\u00ac\u00e8\u0087\u005a\u00eb\u000a\u001b\u00bf\u008e\u00a9\u0043\u0050\u00e6\u007f";
        input[73] = unicode"\u0088\u0084\u0093\u004b\u006e\u00f4\u0031\u00e8\u0096\u002d\u0066\u00f5\u00dc\u002b\u005c\u0021\u0099\u00e0\u00e9\u009e\u0093\u0001\u0083\u00f9\u005d\u0064\u00e5\u00c6\u0080\u0040\u00e9\u006e\u008e\u0067\u005d\u005e\u0091\u0026\u00d1\u0022\u0037\u00fb\u007d\u0085\u00f2\u00fb\u0084\u0022\u001b\u00b9\u0024\u00bd\u0054\u0062\u0039\u00c8\u0064\u00fe";
        input[74] = unicode"\u0018\u009b\u00f7\u00a5\u0047\u0051\u004f\u0010\u00f2\u00cf\u00b3\u0066\u0018\u00be\u00a5\u0058\u0051\u00d6\u0045\u0079\u00cb\u0066\u007a\u00be\u00dd\u0053\u00ed\u00e4\u00a4\u00a5\u004d\u003d\u00ea\u004d\u0094\u000c\u00c3\u00ac\u00f6\u00b0\u00c4\u00de\u00a3\u0071\u00af\u0050\u0099\u00b3\u003a\u0092\u00a2\u00f3\u002a\u008f\u0011\u0012\u005f\u00cf";
        input[75] = unicode"\u00f8\u00a8\u0040\u00b1\u00f0\u0021\u00bd\u007e\u0016\u002b\u0037\u00b9\u00d1\u009a\u0071\u001e\u0041\u00aa\u0041\u00a4\u0042\u00f1\u0016\u006d\u000d\u0058\u00b6\u0035\u0015\u00c9\u005e\u00f8\u005f\u00c7\u0085\u000d\u002a\u00d5\u0021\u0052\u0091\u0011\u0085\u0010\u0018\u004a\u0025\u0079\u003c\u0067\u00ec\u005b\u00c2\u0089\u0080\u002f\u00d5\u00ac\u000e\u00c1\u008a\u00a2\u0028\u00ac\u0020\u007d\u004e\u00dd\u00d3\u0032\u0074\u0056\u0026\u0057\u00f8\u0015\u0072\u00a7\u0019\u0005\u0026\u0070\u0084\u00f7\u003d\u00aa\u00a3\u00c1\u0040\u004f\u00f1\u0005\u00af\u00e8\u0003\u00ea\u00f5\u00a1\u0075\u0022";
        input[76] = unicode"\u000a\u007f\u005a\u00f2\u009f\u008e\u005d\u0001\u00ef\u00a6\u0073\u0052\u0086\u00ab\u0002\u0087\u00bd\u0020\u00e6\u00eb\u003b\u0008\u0095\u0067\u0073\u0098\u00a9\u001d\u00d5\u0002\u0035\u00ac\u00bc\u00c5\u003a";
        input[77] = unicode"\u0021\u00f3\u0099\u0034\u0068\u00ad\u0074\u002a\u008d\u00c2\u0035\u00d6\u0050\u00a1\u00c3\u0002\u005e\u00d9\u002a\u00d9\u001d\u0004\u00e5\u0082\u005c\u006f\u0004\u00f5\u0028\u003a\u00af\u007f\u0001\u00c6\u0074\u0083\u0070\u0007\u0056\u00d8\u00fe\u0064\u0044\u00a7\u008a\u0018\u00ac\u00be\u00a2\u0087\u0089\u0065\u0021\u0001\u0066\u00a7\u005d\u00ff\u00ab\u0023\u00be\u0055\u0023\u0076\u00a6\u005c\u005b\u0050\u00e2\u0058\u007a\u0057\u00c0\u00d1\u0019\u0039\u00fb\u0060\u0013\u00fd\u0002\u0071\u0094\u0032\u004a\u0036\u00eb\u004f\u0070\u00df\u0050\u0095\u002f\u00f6\u00bd\u00d8";
        input[78] = unicode"\u00ea\u00aa\u0094";
        input[79] = unicode"\u0099\u0014\u0019\u00af\u00a4\u00d4\u0067\u003c\u00a6\u0061\u005e\u005b\u00d2\u0048\u0071\u0066\u0094\u0089\u009d\u003c\u00bb";
        input[80] = unicode"\u001e\u00fa\u00e2\u0057\u005c\u00a7\u002b\u00a0\u0015\u00d3\u00c9\u00b9\u006d\u003a\u00c7\u0047\u00b9\u0084\u00f8\u00ad\u006b\u0063\u004c\u0073\u0022\u0089\u003e\u00e6\u006f";
        input[81] = unicode"\u00c8\u0018\u0074\u00c1\u00e3\u00a7\u00ca\u0024\u007a\u00fc\u0060\u00ab\u009c\u00e7\u0071\u00de\u00e2\u00c4";
        input[82] = unicode"\u0053\u009d\u00c5\u00a0\u0091\u0020\u00ab\u008a\u00cd\u0073\u008f\u0048\u00c7\u00fb\u0064\u001b\u00b6\u0033\u00a7\u00aa\u0052";
        input[83] = unicode"\u00f7\u0008\u00b6\u00b9\u00ab\u006c\u0049\u0092\u00ab\u0023\u0072\u0081\u008a\u00e2\u0072\u00bd\u00c7\u0057\u0063\u00c6\u0010\u007e\u000a\u000c\u00b9\u00c9\u006b\u006b\u00fa\u00f1\u00fa\u0034\u00e8\u0033\u00c8\u00a5\u0058\u0064\u00b8\u003b\u003b\u0026\u0073\u0073\u00f0\u000b\u00d0\u0020\u0063\u0028\u0056\u0084\u00da\u00ba\u00e0\u0061\u00b1\u0078\u00d4\u002b\u00e3\u00f0\u0077\u00ae\u0060\u004b\u00b7\u0066\u00a5\u0012\u00a3\u000f\u00d3";
        input[84] = unicode"\u0019\u0037\u0096\u003d\u007a\u0080\u00b8\u0037\u001f\u00f8\u0096\u0011\u009f\u00f0\u006c\u00c6\u00c9\u0050\u0050\u0001\u00a0\u0096\u0063\u00c9\u006e\u003b\u0094\u00fc\u00ec\u0009\u004d\u00da\u007f\u00df\u001b\u002a\u0012\u00bd\u00b3\u005e\u000f\u0035\u0080\u0083\u0080\u009b\u00c6\u0005\u00d6\u0095\u0076\u009c\u00fb\u00f5\u0067\u00cd\u003f\u00c5\u0011\u0076\u0004\u00b0\u0080\u0071\u00e5\u0095\u00b3\u0030";

        vm.warp(block.timestamp + 360604);
        vm.roll(block.number + 23884);
        vm.prank(0x0000000000000000000000000000000000030000);
        target.addStrArr(input);
        
        
        vm.warp(block.timestamp + 1);
        vm.roll(block.number + 0);
        vm.prank(0x0000000000000000000000000000000000020000);
        target.check_strDynArr();
        
    }
    
    // Reproduced from: medusa-corpora/corpus-dyn-arr/test_results/1704377303934867000-b91d964f-2912-4e40-b11c-807b89ad0c27.json
    function test_auto_check_addressDynArr_4() public { 
        address[] memory input = new address[](68);
        input[0] = 0x1CB02a2fd56e000ce64811BfD083a1c134192892;
        input[1] = 0x31cb6dd51AC567B55932D38AC697C589044eb8CF;
        input[2] = 0x47A7828Aace9187707fBF4623F91c284B84E6E39;
        input[3] = 0x9D4B49237B68694ba1e4947358C8e8d04236fE08;
        input[4] = 0x11d9fD97aCa0dE966f326Adc8df7aFb12ac28eF1;
        input[5] = 0x0000000000000000000000000000000000000001;
        input[6] = 0x0000000000000000000000000000000000000005;
        input[7] = 0x8E48c290379c33eDcbE78C8Bd1291e55245ab7f6;
        input[8] = 0x41Ef3a116c989AD341E1279e9374882f0015060B;
        input[9] = 0x888Ce60dF44b7a274B97Cd3135EeE35673DcdA49;
        input[10] = 0x0000000000000000000000000000000000030000;
        input[11] = 0x0000000000000000000000000000000000010000;
        input[12] = 0x84938eD112Ea9Fa3eb6722fa777c0323b06C10f8;
        input[13] = 0x12a62802004AC76b15056C5452d07e24EF158D9d;
        input[14] = 0x0000000000000000000000000000000000000014;
        input[15] = 0x0D88591573572446Bb9DB170d5992301b8876fe4;
        input[16] = 0x0000000000000000000000000000000000030000;
        input[17] = 0xC73BF9C3406bbB73b404c6Ede90B5A0F3251ECa4;
        input[18] = 0xe075133a7e95a3Df6739d16DFd07b44e0eE77F80;
        input[19] = 0x0000000000000000000000000000000000000000;
        input[20] = 0x0000000000000000000000000000000000010000;
        input[21] = 0x0000000000000000000000000000000000000001;
        input[22] = 0x1b27d6318346de44752495eD4bfD7F484B982734;
        input[23] = 0x0000000000000000000000000000000000000000;
        input[24] = 0x0000000000000000000000000000000000000001;
        input[25] = 0x0000000000000000000000000000000000000005;
        input[26] = 0x1559aFB06a978352c900872E5c00c570F2218a6a;
        input[27] = 0x5D20d8deB1Dbfae75a48C0DCAF6BC7E07f32cEc8;
        input[28] = 0xFf8E925702539f849d416bae6cbF228E7DEdB067;
        input[29] = 0x541A6aA296D51B9E1CD554ad04497bB334119990;
        input[30] = 0xaB1D12f2E66bb73592bDa4F82E872237cfbE011D;
        input[31] = 0x1C43505bB9e84094BffE6422C7cB98cC6BD82671;
        input[32] = 0xBdbDD1B8dC555214A3896827b1Aa919029c69E30;
        input[33] = 0x54982095da500AdD17601d3421C493776c0332eB;
        input[34] = 0x0000000000000000000000000000000000000003;
        input[35] = 0x0000000000000000000000000000000000000005;
        input[36] = 0x0000000000000000000000000000000000000002;
        input[37] = 0x0000000000000000000000000000000000000014;
        input[38] = 0xCCCbF0640b634779Af061ea22f8598bc023C538b;
        input[39] = 0x4306334894074c33c0178A785bFA3018FB1e380E;
        input[40] = 0x02cEA5Cca7637da1A1059df2758aC7e18f0F5095;
        input[41] = 0x0000000000000000000000000000000000000004;
        input[42] = 0x0000000000000000000000000000000000000000;
        input[43] = 0x0000000000000000000000000000000000000005;
        input[44] = 0xA647ff3c36cFab592509E13860ab8c4F28781a66;
        input[45] = 0x0000000000000000000000000000000000000002;
        input[46] = 0x0000000000000000000000000000000000030000;
        input[47] = 0x0000000000000000000000000000000000030000;
        input[48] = 0xA647ff3c36cFab592509E13860ab8c4F28781a66;
        input[49] = 0x1304A97fcD0C7B9aC9B072eDEEba12d14eAbD61d;
        input[50] = 0x0000000000000000000000000000000000000001;
        input[51] = 0x0000000000000000000000000000000000030000;
        input[52] = 0x0000000000000000000000000000000000000004;
        input[53] = 0x701554844e0b7b87B1c925B26619f48362F38A7F;
        input[54] = 0x6Bd13221374760eFC3c8E3459105C74e2835b2F4;
        input[55] = 0x0000000000000000000000000000000000000005;
        input[56] = 0x0000000000000000000000000000000000000004;
        input[57] = 0x4717e3a6BE1761B41B205911E635B87c28999398;
        input[58] = 0x544Ed77142F1F75ab681CEadcD9ff55f335dF3ea;
        input[59] = 0x51A1c94043d32a69Dc863164c4dc76Ce6D04C780;
        input[60] = 0x404F524f742D470529d42F2B181272F46b723b1f;
        input[61] = 0x0000000000000000000000000000000000000014;
        input[62] = 0x27a5c17579f3De8c98772E09d393307561F12b34;
        input[63] = 0xa6822d0fED743EA73269Da7F059Da01B64f5B50F;
        input[64] = 0x0000000000000000000000000000000000000005;
        input[65] = 0xB0ddFd138a60EEEe3fc9f361192dAEFd8088e3e0;
        input[66] = 0x0000000000000000000000000000000000000005;
        input[67] = 0x0000000000000000000000000000000000000002;

        vm.warp(block.timestamp + 360623);
        vm.roll(block.number + 3);
        vm.prank(0x0000000000000000000000000000000000020000);
        target.addAddressArr(input);
        
        
        vm.warp(block.timestamp + 475435);
        vm.roll(block.number + 20);
        vm.prank(0x0000000000000000000000000000000000020000);
        target.check_addressDynArr();
        
    }
    
    // Reproduced from: medusa-corpora/corpus-dyn-arr/test_results/1704377304969856000-2f8481da-a733-472e-82b2-98f88ea4e703.json
    function test_auto_check_strDynArr_5() public { 
        string[] memory input = new string[](39);
        input[0] = unicode"\u00f4\u00fb\u000f\u0030\u00af\u0083\u00a2\u00ed\u00eb\u00f4\u008f\u00d5\u00ea\u0086\u00ea\u006f\u00b8\u006f\u00fb\u0031\u004c\u009f\u00dc\u00fe";
        input[1] = unicode"\u0096\u00f3\u00e2\u00e8\u00b3\u002d\u00eb\u0090\u00a5\u0037\u008d\u00d3\u00ee\u0097\u0043\u00d9\u0001\u00f7\u007d\u0021\u00c2\u006b\u006d\u00ed\u0040\u004c\u002c\u0028\u0053\u008f\u0008\u00eb\u0021\u0044\u009c\u006c\u0052\u0049\u00ae\u00f5\u0061\u00fd\u0085\u00f2";
        input[2] = unicode"\u0080\u004c\u003d\u0064\u0060\u00f9\u0053\u0033\u005e\u0047\u00ff\u002a\u0000\u0041\u0063\u00a2\u00a5\u0090\u0063\u009f\u00f0\u0052\u0079\u00e0\u0026\u008e\u0021\u00cb\u008c\u004f\u0017\u0065\u00b8\u00a0\u005a\u006d\u00c0\u0013\u0097\u0011\u00f2\u00db";
        input[3] = unicode"\u00d8\u001c\u0097\u008d\u0005\u00ea\u007c\u001d\u00a5\u001d\u00a0\u0001\u0075\u0006\u00f4\u00d5\u003c\u0096\u0068\u00f2\u0073\u0016\u0057\u0023\u00f5\u007e\u003c\u006e\u006a\u00d7\u00a6\u00ac\u006c\u00c4\u00d4\u00e1\u0079\u0053\u001d\u0008\u00bc\u000c\u00ff\u00e4\u0084\u0091\u0088\u0019\u00f6\u002d\u002f\u0075\u0058\u009f\u007f\u00b8\u0030\u00ed\u0003\u0063\u0014\u0075\u00a1\u006b\u001f\u00ac\u0034\u000b\u0022\u0099\u0046\u00b8\u00b9\u00df\u0097\u0018\u000d";
        input[4] = unicode"\u0091\u0048\u0006\u008c\u005d\u0011\u007e\u00e5\u0027\u0032\u0040\u00e7\u00a8\u00f2\u00b3\u0035\u00ad\u0079\u005e\u00d3\u00f8\u0053\u0025\u0090\u004a\u00ac\u0004\u0004\u00e0\u0071\u0019\u0014\u0054\u00f5\u007a\u0023\u0080\u0020\u00f6\u00aa\u0071\u0073\u002a\u00d8\u009b\u0073\u0079\u0012\u00d4\u00f8\u0056\u00e9\u00d5\u0014\u0047\u00c1\u00dc\u00e3\u0038\u0092\u0071\u000b\u00ed\u00d0\u00dd\u004c\u0025\u00fd\u0054\u00bc\u00b2\u0033";
        input[5] = unicode"\u00de\u0042\u00c1\u0014\u00bd\u005a\u006b\u004e\u00c9\u0082\u005c\u0080\u006a\u009f\u001c\u0073\u001c\u0019\u002e\u0099\u00a1\u00b9\u008c\u0083\u00b2\u00fc\u00c7\u0028\u004f\u0016\u00cf\u0019\u0090\u0067\u000f\u0054\u00ba\u00b5\u0080\u002c\u00d9\u00d9";
        input[6] = unicode"\u006a\u00f0\u00a2\u008f\u0058\u004d\u00b6\u00a5\u00fd\u00c6\u001c\u005c\u0028\u00bd\u004f\u002e\u0003\u0062\u00b7\u0000\u005d\u007a\u0071\u0051\u00b2\u00d3\u0062\u00f8\u00cc\u0022\u001c\u00b5\u00e7\u00be\u0049\u0016\u00e5\u00fc\u002b\u00f9\u0015\u00bb\u00fd\u00e5\u0023\u0021\u00df\u0003\u000f\u0078\u0083\u0055\u00e7\u0049\u0091\u002b\u0019\u0053\u00ce\u0077\u00c2\u00cb\u00ed\u00d6\u009d\u000c\u00c2\u006a\u0041\u00fc\u0054\u00e9\u00ab\u0069\u001a\u0075\u0070\u0049\u00c4\u00cd\u0031\u0004\u00c0\u00eb\u00b9\u005b\u000e\u00df\u0099\u00da\u00f1\u00f2\u001d\u0092\u00ec\u00fa\u001b\u003c\u001a\u007a";
        input[7] = unicode"\u0005\u009d\u0082\u00ab\u0040\u00ba\u0013\u0037\u005f\u0048\u0051\u00e8\u001e\u00c1\u00eb\u00d4\u0095\u0028\u0065\u0075\u00ab\u0025\u006e\u0037\u0053\u0033\u00ef\u000e\u00e1\u000c\u000b\u0008\u0045\u007c\u00e1\u0058\u003e\u000e\u00bb\u0072\u00e4\u0065\u0081\u00da";
        input[8] = unicode"\u007c\u008f\u0068\u000e\u006a\u00b2\u00c2\u00b3\u0053\u00c8\u002e\u00e3\u00ab\u0037\u00de\u0031\u00d5\u00da";
        input[9] = unicode"\u00ff\u00f4\u00f7\u00c1\u00c2\u000e\u0061\u004d\u0028\u00c4\u00f6\u00ed\u00d8\u0083\u0082\u0094\u0045\u00f5\u0048\u000b\u006a\u0079\u0016\u00c0\u0031\u00d6\u0006\u00e3\u0076\u0004\u005a\u00eb";
        input[10] = unicode"\u00c6\u0052\u00df\u006d\u0044\u00da\u0046\u00e0\u0025\u00ff\u0066\u005b\u00a3\u00a1\u00df\u000f\u00d1\u0024\u00bb\u0081\u00f2\u0078\u0017\u0050\u00c0\u0088\u00b3\u00d6\u00c5\u0047\u00dd\u00e5\u00c0\u00d3\u0010\u0021\u00e5\u00cf\u0072\u00bd\u00b7\u007d\u0078\u0024\u0096\u0022\u00ab\u004e\u00b1\u009c\u006e\u00a9\u00b8\u0003\u0012\u005a\u0057\u0085\u0033\u00a7\u00da\u000b\u00d0\u006f\u0055\u0059\u00a8\u0059\u00bc\u0063\u00f5\u00b4\u00de\u00f2\u0097\u0049\u0073\u00b7\u0029\u005b\u000d\u0079\u008c\u00fd\u0060\u00d5\u00d2\u0067\u007c\u0053";
        input[11] = unicode"\u00e0\u00dd\u001c\u006f\u0051\u00e1\u006e\u00de\u0010\u0056\u00b8\u00f5\u0082\u005b\u00f2\u0011\u001d\u00d0\u007f\u0040\u0051\u0069\u001b\u00fe";
        input[12] = unicode"\u0093\u0049\u00f0\u0085\u00b3\u006c\u00fc\u0053\u00d6\u00dc\u0022\u0025\u006d";
        input[13] = unicode"\u00ac\u00fb\u00ef\u00fc\u00f4\u009b\u0037\u006d\u0083\u00c5\u0066\u00a9\u0072\u0022\u0071\u0069\u00c8\u00e7\u00f3";
        input[14] = unicode"\u0069\u007a\u009e\u000b\u00e1\u004e\u00f6";
        input[15] = unicode"\u00be\u00da\u005d\u0008\u00c5\u007d\u0016\u0046\u002e\u009b\u00d7\u00dd\u00f4\u0046\u0028\u0042\u000f\u002f\u00a2\u004a\u0042\u0074\u00b8\u0041\u0047";
        input[16] = unicode"\u006d\u009a\u0096\u00f7\u0009\u0014\u0083\u00eb\u008d\u0033\u007b\u009d\u0014\u001f\u0083\u0081\u00c8\u001a\u0046\u00cb\u005d\u0038\u0002\u00c4\u00a0\u004a\u00a9\u009f\u00f3\u00e6\u00da\u0046\u0090\u0088\u0026\u00f0\u008d\u006d";
        input[17] = unicode"\u006c\u00fc\u0052\u002f\u00b1\u009d\u0082\u00c6\u0033\u00f2\u00b1\u0058\u008e\u00b1\u00a8\u00d4";
        input[18] = unicode"\u00e6\u001a\u0074\u00e4\u00c2\u00cd\u0020\u0087\u00ea\u00c4\u0099\u000f\u009a\u005c\u007b\u0091\u006f\u00c8\u0042\u00b1\u00bb\u008c\u0071\u00cc\u0085\u003c\u0037\u00f1\u009e\u00e4\u0023\u0007\u00f3\u000c\u0016\u0054\u00c9\u0069\u00c1\u0041\u00a2\u00f6\u00cd\u00f4\u00d0\u000d\u007a\u00b7\u005e\u009c\u00f4\u0045\u00a0\u005f\u00b1\u0013\u0052\u009b\u0041\u004a\u00d2\u00d4\u001c\u00b5\u009e\u00f6\u0067\u00b6\u0061\u003d\u0074\u0047\u008c\u00a3\u006b\u009d\u0024\u00f4\u0063\u0010\u0083\u007e\u0009\u00aa\u0007\u00d0\u000b\u0028\u00aa\u00d0";
        input[19] = unicode"\u00c2\u00af\u00d0\u0036\u00b4\u0045\u0071\u0025\u000a\u0081\u0047\u0071\u00fd\u00eb\u00dd\u0066\u00d1\u00a6\u00a5\u00a2\u000a\u00f6\u0085\u00c8\u0090\u006c\u000a\u00c7\u007c\u00bd\u00c4\u00a9\u003f\u00bb\u006a\u003a\u006e\u0010\u00b9\u007a\u00ec\u008d\u0028\u00cd\u00cd\u00f4\u0041\u001b\u0071\u0029\u00cf\u0012\u00ab\u0080";
        input[20] = unicode"\u009e\u0053\u00e9\u0060\u00ce\u00d7\u0038\u000a\u00a7\u00bd\u00b6\u009d\u00e5\u00f8\u00b6\u0011\u00c6\u0098\u006b\u0018\u005c\u0004\u0060\u008c\u0075\u0074\u0063\u009e\u00a0\u00b9\u00fd\u009f\u001d\u006f\u00c6\u0016\u0071\u00cc\u00dc\u00fa\u009b\u0009\u00a2";
        input[21] = unicode"\u00e1\u0008\u0000\u00a9\u0032\u0006\u00d7\u006b\u00c7\u0039\u0001\u0067\u0082\u008a\u00fd\u0036\u00f0\u0053\u00ab\u005f\u0097\u0006\u00bd\u0074\u0057\u00a5\u0096\u00c3\u0044\u000e\u001a\u00e5\u005e\u003c\u0006\u00f3\u00fd\u0096\u00c1\u008d\u00ee\u0051\u0032\u0008\u00e2\u00c3\u008f\u0057\u0030\u0049\u00a9\u00c7\u002d\u0018\u002b\u007d\u0013\u0094\u00b8\u00d6\u0069\u00a5";
        input[22] = unicode"\u003e\u00ba\u0018\u00bc\u0092\u00a9\u0028\u0022\u00fc\u00f2\u00fb\u0006\u0027\u00af\u00d0\u008b\u00c6\u0002\u0025\u000f\u00d7\u006c\u0072\u007e\u002e\u0005\u00a2\u0011\u0008\u00b2\u0085\u002f\u00da\u0078\u000c\u001a\u0075\u0059\u00da\u00dd\u004e\u00f1\u000c\u0041\u00d8\u006e\u0067\u0014\u00bd\u00c3\u0030\u00f7\u0027\u0026\u00f2\u00b3\u0025\u00f7\u0045";
        input[23] = unicode"\u0032\u00b2\u0036\u0059\u009b\u00af\u0082\u008c\u0002\u001d\u006e\u00f9\u00a1\u007b\u0033\u008c\u004a\u0099\u0011";
        input[24] = unicode"\u00fb\u0046\u001d\u0053\u0028\u00c1\u00c7\u008a\u0059\u00f4\u0009\u00e7\u00a3\u00fc\u0060\u0010\u0020\u0015\u0092\u00ee\u00d2\u0014\u0098\u008a\u0085\u008e\u005b\u001c\u00ab\u0086\u007e\u009c\u0096\u00a1\u00b0\u009c\u008e\u00b0\u005f\u00ac\u0025\u0000\u0033\u00ae\u0005\u0098\u00a2\u0081\u0004\u00c2\u0070\u00ae\u00b0\u005b\u00cb\u009a\u00d9\u0017\u00dc\u007e\u008e\u00bb\u002b\u006e\u0031\u0085\u0041\u00c8\u0096\u00b8\u0070\u009f\u0065\u007b\u00dd\u0029\u0092\u009d\u0078\u004e\u0092\u0014\u001f\u0067\u00e0\u006c";
        input[25] = unicode"\u00fc\u00c5\u0044\u0099\u00f1\u0044\u00d4\u00ee\u002f\u0076\u0067\u00f9\u0097\u00c8\u0017\u0098\u00f8\u0058\u002f\u00c9\u0049\u003a\u00b3\u007c\u003c\u009d\u00c4\u00f4\u0018\u00eb\u00ce\u00f2\u0084\u0084\u004d\u00e8\u0081\u0085\u005a\u00b1\u004e\u008c\u00cf\u0046\u0001\u0082\u0006\u00c1\u0039\u00c1\u0002\u0028\u0045\u001b\u00ce\u00bc\u0057\u0079\u0096\u0017\u00e6\u00d9\u008b\u0024\u00eb\u005b\u006a\u005d\u00ec\u00de";
        input[26] = unicode"\u00ed\u00ab\u00ac\u00ce\u0081\u00db\u0006\u002a\u007c\u0084\u0007\u0071\u00e0\u002c\u004f\u001a\u00a7\u00d9\u007d\u0086\u00dc\u0005\u00a8\u00f8\u00a5\u0041\u003d\u00ee\u00b9\u0037\u0000\u00b7\u005c\u0067\u0042\u0030\u004a\u0051\u00b4\u005d\u0009\u002a\u0014\u00eb\u00f5\u00b1\u0003\u0040\u00a1\u009d\u007a\u00f8\u0089\u0032\u0042\u0012\u00e3\u009e\u00f1\u007b\u001d\u00c9\u0069\u00b7\u00fc\u0058\u00ba\u006f\u00b9\u0051\u0079\u0042\u0001\u006c\u004c\u009e\u00ac\u00f2\u0081\u0008\u003f\u0013\u0019\u004d\u004a";
        input[27] = unicode"";
        input[28] = unicode"\u00a1\u00e0\u00b7\u00a9\u0070\u00e4\u00f9\u0050\u00cb\u0000\u008e\u0073\u00bd\u0059\u0078\u00be\u00c1\u00bc\u0089\u0096\u00fe\u00f2\u000f\u000e\u00cc\u0019\u0088\u0088\u0027\u00ab\u00c1\u0032\u0063\u00be\u00a4\u000a\u006c\u0069\u009a\u00db\u0076\u001a\u00b1\u0017\u0059\u001c\u00c0\u0056\u008c\u005c\u0004\u0091\u00c7\u00b5\u005e\u009a\u007b\u0012\u0041\u0086\u0062\u00a4\u00ad\u00e7\u007f\u0009\u00f2\u008f\u0051\u0012\u007b\u00d2\u00a1\u009b\u0060\u00f8";
        input[29] = unicode"\u0003\u005e\u0060\u0094\u0029\u00b3\u0054\u0038\u00fa\u00b7\u0028\u004a\u000a\u00e8\u0016\u00b5\u00e4\u006a\u002a\u00a2\u00c4\u00fe\u00b3\u0072\u0093\u00a0\u00c7\u00f3\u00f8\u0069\u0056\u00e7\u003f\u00ad\u0084\u00fd\u0032\u006a\u001b\u0005\u000a\u006b\u005a\u00ad\u000d\u008e\u0064\u00cf\u0000\u0072\u00af\u0054\u0062\u0002\u0061\u003b\u0002\u00ba\u00bc\u00b5\u0033\u00a6\u00a9\u0052\u0086\u00fd\u00b2\u00aa\u00c9\u0021\u006f\u003a\u00fb\u0056\u0099\u008c\u0044\u0087\u003d\u0018\u0027\u0012\u0076\u0099\u00f1\u00d1\u0072\u00ec\u0057\u003d\u0035\u0059\u003d\u00ff\u0002\u0093";
        input[30] = unicode"\u00ed\u0047\u0020\u0046\u003f\u00ab\u0041\u00f0\u00fd\u00ec\u0039\u00c8\u004c\u0035\u0005\u0002\u003c\u00df\u009a\u00d5\u00e4\u0066\u0043\u000d\u00d9\u00ae\u000a\u005b\u00db\u005f\u00bd\u00b7\u00db\u0033\u0021\u0041\u0049\u0099\u00be\u0053\u002c\u00ac\u00a4\u003c\u0014\u00c3\u0000\u00ed\u00e0\u00fb\u0025\u00a1\u00b0\u0044\u0085\u005a\u003e\u0031\u000f\u0043\u00ac\u00cc\u009a\u0064\u0058\u007d\u003d\u005f\u004f\u00d3\u0031\u00de\u002f\u0046\u003d\u009f\u0053\u00f4\u0070\u0076\u00be\u0024\u0007\u002a\u007d";
        input[31] = unicode"\u003e\u00bd\u0071\u005d\u00f5\u004a\u003f\u00aa\u00d3\u0067\u00eb\u00f3\u00df\u0030\u00ab\u0035\u0088\u0015\u0004\u00d9\u00ae\u009c\u0037\u0056\u000a\u0086\u0021\u00ab\u0014\u00ef\u00d2\u00f6\u0068\u0094\u0016\u0079\u0085\u00f3\u00a8\u00d3\u001b\u0032\u0097\u0024\u0048\u000d\u00ad\u00c0\u009e\u0074\u000e\u00c0\u007f\u00f2\u00c1\u001a\u00fc\u00c9\u0070\u0003\u007f\u001d\u001b\u0011\u00fb\u00bf\u0094\u007d\u009d\u0042\u007e\u0012\u009e\u0077\u002d\u000c\u0018";
        input[32] = unicode"\u00e3\u007f\u003e\u0083\u00db\u0066\u001f\u004d\u0028\u008e\u00dc\u0082\u0044\u0033\u0039\u0011\u000d\u0088\u0098\u008e\u0045\u007f\u00f9\u0077\u0050\u0077\u006e\u009f\u0082\u00b9\u0039\u007e\u00e5\u00a2\u00f8\u006c\u00b4\u00a3\u0087\u00a0\u00a8\u00ea\u005d\u0050\u00bc\u0081\u007d\u0005\u0068\u0073\u0026\u00e1\u0099\u0088\u00d7\u0064\u00df\u006a\u0070\u00c2\u0017\u00c4\u00a0\u0080\u004d\u0032\u00e6\u006c\u00da\u0026\u004e\u0010\u00db\u0000\u0034\u00b6\u00c4\u00ad\u0055\u0050\u008a\u0042\u005c\u0083\u00e6\u008a\u008f\u009e\u00fa\u0014\u001f\u008d\u00c7";
        input[33] = unicode"\u00df\u00d9\u0000\u006c\u0020\u000f\u00b2\u00b8\u0009\u006a\u0048\u0054\u00d2\u0060\u00e8\u004b\u0010\u0010\u00bb\u0005\u0047\u00c4\u00c7\u0058\u00f5\u006b\u0029\u00e8\u002f\u00ca\u009c\u0007\u007f\u00d4\u0046\u002c\u00d0\u0001\u00e5\u00ae\u00c2\u0033\u004d\u00f2\u0074\u008a\u00a5\u0071\u00c1\u00af\u00ec\u0007\u0066\u0039\u0017\u002d\u0056\u0099\u0065\u00c8\u00b2\u003e\u0073\u0081\u0051\u001e\u00dc\u0038\u006c\u0054\u0039";
        input[34] = unicode"\u0080\u00ee\u0006\u0047\u0070\u005e\u004a\u00c9\u00a4\u0083\u00b3\u0019\u0051\u0044\u0004\u0035\u0070\u0073\u00ee\u0048\u000a\u0013\u0051\u00cb\u00b5\u00d5\u0001\u002d\u0061\u0050\u001f\u00cd\u00d5\u00a2\u009d\u00e3\u0028\u0077\u0058\u0067\u001d\u00aa\u00ba\u00db\u005a\u0086\u00a5\u00f7\u00b3\u00fc\u00f2\u009d\u003b\u0068\u00cf\u007c\u0070\u0080\u000c\u0092\u00df\u005c\u0053\u0055\u00ff\u0076\u0088\u0014\u0090\u0062\u009e\u00c1\u00dc\u00f9\u00c3";
        input[35] = unicode"\u002a\u005c\u0013\u0072\u0080\u00e7\u0043\u00f7\u00ed\u00b1\u0009\u00bc\u00e0\u001e\u003d\u0092\u00e3\u0073\u0064\u008a\u00ac\u00bc";
        input[36] = unicode"\u008b\u0075\u00a5\u0057\u000d\u00ba\u007f\u00c4\u0052\u00e4\u00df\u0011\u00bd\u0063\u00f0\u0070\u00be\u00cf\u0023\u00a5\u007f\u0024\u006f\u0091\u00fa\u002e\u00ef\u0016\u00b6\u008b\u0018\u009d\u00df\u0075\u0002\u0071\u00bd\u0033\u000e\u001d\u0065\u0076";
        input[37] = unicode"\u00f8\u008f\u000c\u00ca\u00f3\u0069\u00bf\u0026\u00e1\u0068\u008f\u0035\u003f\u00ae\u0022\u0071\u00f5\u0091\u0069\u00f5\u0072\u00f7\u00c8\u0083\u00e5\u0087\u0006\u001b\u007f\u0054\u006c\u00a9\u0003\u00a3\u00dd\u0017\u0077\u0085\u001c\u003e\u00ae\u0017\u005e\u00ce\u0017\u008a\u00fe\u0068\u0035\u002b\u0086\u00d5\u0036\u00eb\u002e\u00c4\u001e\u00c4\u00cf\u00a6\u00ae\u00e5\u0028\u0041\u00fc\u0003\u002a\u00b5\u00f1\u00a7\u000d\u00f9\u0031\u001c\u0037\u003a\u0086\u003a\u00e7\u0004\u00ce\u004c\u0027\u00fd\u002e\u0057\u00d1\u004f\u0030\u00fe\u005e\u0086\u008c\u00d5\u0059\u0040\u00e6\u003a\u001d\u0065";
        input[38] = unicode"\u00bc\u0011\u0066\u0043\u0082\u009c\u00f8\u0072\u003d\u004f\u0058\u0055\u004f\u00d4\u0049\u0073\u00c5\u0000\u002c\u0018\u00d2\u0092\u0079\u0077\u0091\u00b9\u0044\u00e9\u0068\u002d\u0071\u00b6\u00c4\u0011\u00a4\u000d\u00ae\u001a\u0004\u00ce\u00c3\u002f\u0026\u0020\u0028\u005b\u0032\u00f6\u00b6\u009d\u008e\u005b\u0076\u00e5\u00be\u0091\u006f\u009e\u0041\u0046\u00f4\u00e6\u002d\u0077\u00df\u009d\u0017\u00a3\u0011\u004c\u0077\u00fa\u0076\u00c3\u007b\u0035\u008f\u0085\u005e\u009c\u0023\u0051\u0093\u00ca\u0022\u002f\u002a\u00c1\u0029\u0083\u0066\u00f1\u0095\u0050\u0010\u00a4";

        vm.warp(block.timestamp + 360624);
        vm.roll(block.number + 23885);
        vm.prank(0x0000000000000000000000000000000000020000);
        target.addStrArr(input);
        
        
        vm.warp(block.timestamp + 322526);
        vm.roll(block.number + 0);
        vm.prank(0x0000000000000000000000000000000000020000);
        target.check_strDynArr();
        
    }
    
    // Reproduced from: medusa-corpora/corpus-dyn-arr/test_results/dyn_array_variable_definition.json
    function test_auto_check_boolArr_6() public { 
        bool[] memory input = new bool[](14);
        input[0] = true;
        input[1] = true;
        input[2] = true;
        input[3] = false;
        input[4] = false;
        input[5] = false;
        input[6] = true;
        input[7] = false;
        input[8] = true;
        input[9] = true;
        input[10] = true;
        input[11] = false;
        input[12] = false;
        input[13] = true;

        vm.warp(block.timestamp + 320182);
        vm.roll(block.number + 23884);
        vm.prank(0x0000000000000000000000000000000000010000);
        target.addBoolArr(input);
        
        input = new bool[](14);
        input[0] = true;
        input[1] = true;
        input[2] = true;
        input[3] = false;
        input[4] = false;
        input[5] = false;
        input[6] = true;
        input[7] = false;
        input[8] = true;
        input[9] = true;
        input[10] = true;
        input[11] = false;
        input[12] = false;
        input[13] = true;

        vm.warp(block.timestamp + 320182);
        vm.roll(block.number + 23884);
        vm.prank(0x0000000000000000000000000000000000010000);
        target.addBoolArr(input);
        
        
        vm.warp(block.timestamp + 360622);
        vm.roll(block.number + 47114);
        vm.prank(0x0000000000000000000000000000000000010000);
        target.check_boolArr();
        
    }
    
}