use proptest::collection;
use proptest::prelude::*;
use arenavec::rc::{Arena, SliceVec};
use arenavec::ArenaBacking;
const DEFAULT_CAPACITY: usize = 4096 << 16;
#[derive(Clone, Debug)]
enum SliceVecOp {
Push(usize),
Resize(usize, usize),
Reserve(usize),
}
prop_compose! {
fn arb_op() (id in 0..3, size in 0..100, val in 0..std::usize::MAX) -> SliceVecOp {
match id {
0 => SliceVecOp::Push(val),
1 => SliceVecOp::Resize(size as usize, val),
2 => SliceVecOp::Reserve(size as usize),
_ => unreachable!(),
}
}
}
prop_compose! {
fn arb_op_seq(num_vecs: usize, len: usize)
(ids in collection::vec(0..num_vecs, len),
ops in collection::vec(arb_op(), len))
-> Vec<(usize, SliceVecOp)> {
let mut res = Vec::with_capacity(len);
for i in 0..len {
res.push((ids[i], ops[i].clone()));
}
res
}
}
const NUM_VECS: usize = 8;
fn rand_op_seq_inner(mut seq: Vec<(usize, SliceVecOp)>, filter: Option<&[usize]>) {
let arena = Arena::init_capacity(ArenaBacking::SystemAllocation, DEFAULT_CAPACITY).unwrap();
let mut vecs = Vec::with_capacity(NUM_VECS);
let mut slice_vecs = Vec::with_capacity(NUM_VECS);
for _ in 0..NUM_VECS {
vecs.push(Vec::new());
}
for _ in 0..NUM_VECS {
slice_vecs.push(SliceVec::new(arena.inner()));
}
for (v, op) in seq.drain(..) {
if let Some(s) = filter {
if !s.contains(&v) {
continue;
}
}
match op {
SliceVecOp::Push(e) => {
vecs[v].push(e);
slice_vecs[v].push(e);
}
SliceVecOp::Resize(l, e) => {
vecs[v].resize(l, e);
slice_vecs[v].resize(l, e);
}
SliceVecOp::Reserve(l) => {
vecs[v].reserve(l);
slice_vecs[v].reserve(l);
}
}
for i in 0..NUM_VECS {
assert_eq!(&*vecs[i], &*slice_vecs[i]);
}
}
}
#[cfg(not(miri))]
mod prop {
use super::*;
const NUM_OPS: usize = 400;
proptest! {
#[test]
fn rand_op_seq(seq in arb_op_seq(NUM_VECS, NUM_OPS)) {
use std::fs::OpenOptions;
use std::io::Write;
let mut file =
OpenOptions::new().create(true).append(true).open("static").unwrap();
writeln!(file, "{:?}", seq).unwrap();
rand_op_seq_inner(seq, None);
}
}
}
#[test]
fn pre_rand_op_seq1() {
use SliceVecOp::*;
let seq = vec![
(5, Reserve(18)),
(5, Resize(96, 7434532511546272613)),
(6, Resize(55, 11836171166212578863)),
(1, Reserve(73)),
(4, Push(14991789319801324260)),
(7, Resize(28, 12717166742316467252)),
(3, Push(16592071023974211167)),
(0, Resize(86, 16429603189613580378)),
(2, Resize(88, 7793320186926176013)),
(0, Reserve(34)),
(4, Resize(56, 15179050872186518862)),
(6, Reserve(67)),
(1, Reserve(99)),
(7, Reserve(44)),
(1, Reserve(86)),
(3, Resize(28, 14535255266552044782)),
(6, Resize(48, 14105599279454668572)),
(4, Resize(27, 9527322489505289215)),
(1, Reserve(55)),
(4, Resize(54, 13779177552654293536)),
(4, Push(814320020935280048)),
(2, Push(13321971741513898712)),
(1, Resize(24, 18291098732177080589)),
(6, Resize(78, 9148270455281011662)),
(6, Push(8833158480580114405)),
(5, Resize(27, 1274906245410706342)),
(3, Reserve(56)),
(5, Push(12869799416869990094)),
(6, Push(915054377613569407)),
(0, Reserve(12)),
(1, Reserve(67)),
(7, Resize(16, 3789659809604807811)),
(3, Reserve(20)),
(1, Reserve(40)),
(7, Push(6922281658351195093)),
(2, Resize(82, 13539788957650865408)),
(6, Reserve(82)),
(0, Resize(36, 882642177597567028)),
(1, Reserve(42)),
(7, Resize(78, 826798127694797277)),
(1, Push(10990333923729152933)),
(7, Resize(34, 3500577806690379107)),
(4, Reserve(72)),
(1, Resize(68, 11748951353819237183)),
(0, Reserve(43)),
(6, Reserve(85)),
(7, Reserve(8)),
(7, Resize(52, 11073697234124871737)),
(6, Reserve(15)),
(3, Reserve(61)),
(4, Push(1554299979281996185)),
(3, Resize(94, 3486907836119369331)),
(7, Reserve(81)),
(4, Reserve(36)),
(7, Push(13734558101552238331)),
(2, Reserve(30)),
(4, Push(14469684486135786576)),
(4, Resize(42, 12992470109552634917)),
(7, Reserve(20)),
(0, Push(7866590370907767796)),
(3, Resize(18, 6584163843175693599)),
(5, Push(7688937448577411386)),
(0, Reserve(38)),
(3, Resize(2, 2367775010005837822)),
(5, Resize(23, 11821434197020047061)),
(0, Reserve(5)),
(1, Push(8097179394331876406)),
(1, Reserve(46)),
(7, Push(3029851440503049484)),
(2, Resize(18, 11548509876046543326)),
(4, Reserve(12)),
(7, Push(1593774132763176699)),
(4, Push(12399826378467105353)),
(5, Resize(53, 9546063174298787707)),
(0, Push(13985504485696120884)),
(3, Resize(65, 12870527496588722859)),
(7, Reserve(18)),
(6, Resize(15, 2369818071208968029)),
(1, Reserve(22)),
(6, Reserve(2)),
(7, Reserve(35)),
(2, Reserve(59)),
(6, Reserve(6)),
(3, Reserve(77)),
(3, Resize(55, 14399546376740999461)),
(6, Resize(90, 805929507655167903)),
(7, Resize(23, 987129242317969159)),
(0, Reserve(27)),
(3, Resize(93, 17995679049300670256)),
(4, Resize(25, 9652416451722358081)),
(3, Resize(42, 1117105597129765631)),
(3, Push(17071450624198860125)),
(5, Push(15556953558815298799)),
(1, Push(6777489812646189744)),
(0, Push(3420467694587346486)),
(5, Reserve(1)),
(7, Resize(7, 4784347693029963215)),
(5, Push(17581632846449609163)),
(6, Reserve(15)),
(1, Push(16548635869386875967)),
(4, Push(8985473428401699581)),
(2, Reserve(28)),
(5, Resize(66, 13546264137598621127)),
(6, Resize(40, 17253870872849269820)),
(5, Push(10279553803484858365)),
(6, Reserve(78)),
(3, Push(8887485158247156070)),
(7, Push(5419091861778966634)),
(1, Reserve(36)),
(5, Resize(8, 8096136916066598173)),
(5, Reserve(24)),
(5, Push(627254974063755064)),
(5, Push(9035846514407681585)),
(3, Push(8194052711830070641)),
(6, Resize(82, 7651231518029554847)),
(3, Push(15836795116344246968)),
(5, Push(17618535346168238634)),
(4, Reserve(33)),
(1, Reserve(93)),
(2, Resize(60, 13372644315447413471)),
(3, Resize(44, 9430698778940913120)),
(4, Push(1891902720743089149)),
(6, Push(18403865303966597389)),
(4, Reserve(49)),
(5, Reserve(23)),
(3, Resize(52, 789580560073913388)),
(6, Resize(19, 17261691963387684276)),
(2, Reserve(32)),
(3, Resize(68, 3238836699368529878)),
(2, Push(16543570418418538438)),
(2, Resize(34, 4814923162354884313)),
(0, Push(13325533280353813112)),
(4, Push(13864360737784853712)),
(6, Resize(24, 1592605390302100212)),
(6, Reserve(52)),
(5, Reserve(30)),
(7, Resize(47, 1425498795419035517)),
(1, Push(3848451596760165612)),
(3, Push(15089234937428320911)),
(2, Reserve(39)),
(2, Push(5713960296948700510)),
(6, Resize(45, 12100875500011920742)),
(7, Push(12062076374931716414)),
(2, Reserve(45)),
(1, Reserve(38)),
(0, Push(9138762390727573675)),
(3, Resize(12, 7617883756884930449)),
(7, Resize(90, 14512857894682084132)),
(4, Resize(26, 9702020285439726243)),
(1, Resize(20, 17354431448132454830)),
(4, Push(15600115716981553405)),
(3, Resize(82, 4332456343976075177)),
(1, Push(17579533218773998033)),
(7, Push(3861319371437802116)),
(1, Push(4238676302210114556)),
(3, Resize(20, 14728372563112249573)),
(2, Reserve(31)),
(0, Reserve(94)),
(7, Resize(61, 13622545542577143562)),
(3, Reserve(3)),
(3, Resize(71, 10729988071305226681)),
(7, Resize(6, 7426108624556647785)),
(4, Reserve(50)),
(4, Resize(39, 10224587222459554962)),
(4, Resize(44, 570548645906481521)),
(7, Push(9420687631161847908)),
(3, Resize(29, 489925511289468281)),
(2, Resize(37, 1858657781982553873)),
(6, Push(13891528011355657627)),
(4, Reserve(91)),
(7, Resize(66, 6661376383413711898)),
(4, Push(1916598647339775945)),
(6, Reserve(15)),
(5, Push(6956938135864214783)),
(0, Reserve(45)),
(3, Push(11684865107781406689)),
(4, Resize(79, 15196479610394063796)),
(1, Resize(76, 8510470983404048639)),
(2, Resize(18, 8540564175138020844)),
(7, Reserve(36)),
(7, Reserve(7)),
(7, Resize(82, 10369146083588901681)),
(3, Reserve(78)),
(2, Reserve(30)),
(2, Reserve(86)),
(6, Reserve(53)),
(0, Resize(62, 4081661520403283412)),
(1, Push(1732056619466402251)),
(7, Reserve(29)),
(4, Push(6468446417235325484)),
(7, Push(1300512593664612238)),
(5, Push(13803896047621899962)),
(6, Push(10168224645268992510)),
(2, Reserve(2)),
(1, Resize(56, 18381331589099637809)),
(5, Reserve(70)),
(7, Reserve(59)),
(7, Push(8327431407684993266)),
(5, Push(5553637212980114752)),
(6, Push(13729085403743721172)),
(5, Resize(40, 9472983903595113633)),
(6, Push(17533714037682523667)),
(4, Reserve(25)),
(4, Push(13367231127912003528)),
(5, Push(3805442765486049018)),
(6, Reserve(8)),
(4, Reserve(87)),
(0, Reserve(21)),
(5, Resize(89, 10732247370426436277)),
(3, Resize(5, 2020562476612454987)),
(0, Reserve(20)),
(2, Reserve(81)),
(1, Reserve(42)),
(0, Reserve(27)),
(6, Reserve(46)),
(5, Resize(65, 17501060746955555737)),
(3, Push(8477000901703784552)),
(7, Reserve(24)),
(2, Resize(41, 10863320204162507024)),
(6, Push(4776005791173790931)),
(2, Push(12549462382137704871)),
(2, Resize(39, 17561928801683131965)),
(7, Reserve(98)),
(4, Reserve(52)),
(2, Resize(99, 16491524746282208841)),
(7, Push(11466547191694976267)),
(1, Resize(23, 2248955733084774259)),
(2, Push(13976748479160618391)),
(0, Push(9829509661504466993)),
(5, Reserve(65)),
(4, Reserve(88)),
(1, Push(12464862572709632597)),
(7, Push(7958578588217181700)),
(3, Reserve(51)),
(6, Reserve(93)),
(6, Reserve(92)),
(7, Push(13736681831895922008)),
(5, Reserve(56)),
(6, Push(1650707862179895666)),
(1, Push(15449995469481788571)),
(7, Resize(36, 9805349881339365818)),
(5, Push(6404087729724611804)),
(2, Push(15196452833475501888)),
(6, Push(2730470788408704076)),
(2, Reserve(24)),
(1, Resize(5, 3595298397402076354)),
(3, Push(15290799440347688)),
(4, Push(14006473401008893296)),
(5, Resize(3, 10451862953297807063)),
(1, Resize(74, 265309732783932296)),
(0, Reserve(55)),
(0, Reserve(54)),
(2, Reserve(2)),
(1, Reserve(54)),
(2, Reserve(91)),
(7, Resize(99, 15245773801816280978)),
(6, Push(2953136686063730661)),
(2, Resize(43, 6243229630648977189)),
(3, Reserve(75)),
(1, Push(3212425695570232032)),
(6, Reserve(85)),
(0, Push(17717453381519020148)),
(0, Push(12937359446267210119)),
(3, Reserve(3)),
(5, Reserve(36)),
(1, Reserve(75)),
(2, Resize(53, 2845317859068894618)),
(2, Reserve(52)),
(1, Push(15491795612141018262)),
(6, Resize(64, 10251876321685121580)),
(2, Reserve(18)),
(4, Reserve(9)),
(1, Resize(62, 12415563551632339417)),
(7, Resize(72, 2993443444742592288)),
(1, Reserve(27)),
(4, Reserve(54)),
(6, Push(7908828014430241492)),
(5, Reserve(12)),
(7, Push(6852433628287986625)),
(6, Push(9794161938746646723)),
(1, Push(451632942197011340)),
(1, Push(2281780498448241994)),
(2, Resize(12, 17302563519604653656)),
(1, Resize(50, 16079140408200486745)),
(0, Push(3563922921970803189)),
(6, Reserve(95)),
(0, Resize(95, 6328196690094006589)),
(5, Resize(51, 16535457293684301111)),
(3, Resize(72, 18294727691595166965)),
(5, Reserve(67)),
(4, Push(10750347787304408774)),
(7, Resize(13, 4812695112627343575)),
(4, Resize(71, 8873528311297012767)),
(0, Push(17150718072159411663)),
(5, Reserve(0)),
(3, Push(14005157157345397976)),
(3, Push(10236229771925961686)),
(0, Reserve(65)),
(4, Resize(4, 3810045160007715666)),
(1, Reserve(96)),
(6, Reserve(23)),
(7, Resize(87, 5642488162026501146)),
(5, Push(6221691914213430142)),
(1, Reserve(15)),
(4, Reserve(35)),
(0, Resize(90, 6625694300628371279)),
(4, Push(13633972252472168822)),
(0, Push(5913651452064016401)),
(4, Reserve(28)),
(3, Resize(52, 16132288721990023755)),
(7, Push(10951066952073463152)),
(2, Push(17012835433406106620)),
(3, Reserve(49)),
(5, Resize(0, 10757036212954212254)),
(5, Push(17558520471082390717)),
(2, Push(6030951989897128161)),
(5, Push(6192812795771748990)),
(1, Resize(21, 8182847900438242280)),
(2, Reserve(4)),
(4, Push(1912563234267631336)),
(4, Reserve(35)),
(2, Reserve(61)),
(2, Push(4417126518861866896)),
(7, Resize(27, 16586350593895250795)),
(6, Reserve(69)),
(7, Resize(74, 12442472354864680048)),
(1, Reserve(90)),
(5, Reserve(33)),
(1, Reserve(40)),
(7, Reserve(19)),
(5, Resize(16, 15448378381288877643)),
(6, Push(2384921129845462378)),
(4, Push(1013321282484744767)),
(4, Push(13271344473838945078)),
(0, Push(2190931531631436621)),
(0, Resize(75, 1215803094246020623)),
(2, Push(12642696422898771728)),
(4, Resize(16, 9159112165581493102)),
(2, Push(13066839194534133079)),
(3, Resize(72, 3782309607529202990)),
(7, Reserve(0)),
(0, Push(14444802699059598249)),
(4, Resize(52, 3472629142902738772)),
(1, Resize(4, 10850167234350445461)),
(4, Resize(71, 898855096635968587)),
(7, Resize(95, 13200366182641147137)),
(5, Reserve(53)),
(5, Push(11239406290682213077)),
(7, Resize(96, 11271031291738299086)),
(7, Push(13446965229295377341)),
(4, Resize(48, 11716682760119559957)),
(6, Push(9603590962195566523)),
(7, Resize(38, 6235453618755557023)),
(1, Resize(83, 2198020767332768068)),
(6, Reserve(52)),
(7, Resize(74, 5043395211010898773)),
(5, Reserve(83)),
(1, Reserve(47)),
(1, Push(14703457258365147126)),
(3, Reserve(91)),
(5, Resize(30, 15590066610425715599)),
(0, Resize(55, 8853521250954134046)),
(6, Push(16195402152382416595)),
(2, Push(9422096042476496900)),
(2, Reserve(7)),
(5, Push(17805686037271418567)),
(2, Push(5147554562838977248)),
(7, Push(17974847039109331148)),
(3, Reserve(34)),
(7, Resize(76, 18089078196912612808)),
(2, Resize(46, 12459793132713846679)),
(0, Resize(79, 14480165576712101013)),
(5, Resize(21, 15071476447610373821)),
(7, Push(4992448698263760096)),
(1, Push(10020600278138913520)),
(4, Reserve(72)),
(0, Reserve(61)),
(6, Resize(7, 15064964772413805485)),
(0, Reserve(97)),
(4, Resize(34, 7202041726188883415)),
(5, Resize(5, 4750971916391312718)),
(5, Reserve(51)),
(0, Reserve(87)),
(4, Resize(73, 14451155451840320170)),
(1, Resize(58, 4201312026579324206)),
(1, Push(7087037479030288788)),
(3, Reserve(35)),
(7, Reserve(34)),
(1, Push(973573467986414015)),
(3, Resize(33, 17073760823659202543)),
(4, Resize(90, 7002136876418133005)),
(1, Resize(99, 8243106874128009760)),
(4, Reserve(96)),
(5, Push(18139700090506776254)),
(0, Push(17838226851675992773)),
(2, Reserve(40)),
(1, Resize(79, 7324287648850370154)),
(7, Push(2988546105184828028)),
(2, Resize(49, 6555181995891599849)),
(6, Reserve(19)),
];
rand_op_seq_inner(seq, None);
}
#[test]
fn pre_rand_op_seq2() {
use SliceVecOp::*;
let seq = vec![
(6, Push(8571704643031140639)),
(0, Resize(98, 17598300304473862305)),
(2, Push(10673108108330974792)),
(2, Reserve(0)),
(3, Reserve(25)),
(2, Reserve(76)),
(7, Resize(85, 8147346080438701674)),
(2, Resize(83, 964644805778128179)),
(7, Reserve(94)),
(2, Reserve(30)),
(4, Resize(19, 15160805831113754163)),
(4, Resize(44, 1502254100891562158)),
(5, Reserve(80)),
(1, Resize(35, 11531738861786119800)),
(0, Push(3664415400661013128)),
(4, Push(16911168056797407744)),
(3, Resize(62, 15284348711435874451)),
(3, Reserve(55)),
(0, Reserve(58)),
(3, Reserve(72)),
(7, Reserve(0)),
(3, Resize(80, 13364769953759628791)),
(1, Reserve(19)),
(4, Resize(70, 9857562065498559959)),
(5, Reserve(34)),
(4, Resize(27, 10211445460498058801)),
(5, Push(15094763455739304238)),
(6, Reserve(47)),
(2, Push(10442044456551944993)),
(0, Resize(34, 1812854062588894737)),
(7, Resize(79, 17565298827834421763)),
(6, Resize(42, 13521913155721089079)),
(0, Resize(13, 701208137330599767)),
(4, Reserve(54)),
(6, Resize(91, 10311663382213544238)),
(4, Resize(65, 8473632458421022773)),
(3, Push(6448923683892002613)),
(0, Push(4985722735428100225)),
(2, Reserve(30)),
(1, Reserve(34)),
(4, Reserve(23)),
(4, Push(6604452905770361145)),
(4, Reserve(31)),
(3, Push(3665268368356514533)),
(1, Push(13491316185381568805)),
(0, Resize(77, 14985355469545938484)),
(1, Resize(76, 9794777480629469760)),
(6, Push(8486083127508768000)),
(5, Push(3579000517743526593)),
(2, Resize(65, 5097567639574804681)),
(4, Reserve(50)),
(7, Push(9076403318192407882)),
(4, Push(228001952269633685)),
(4, Reserve(93)),
(4, Resize(73, 6117577782634335007)),
(1, Reserve(49)),
(3, Resize(42, 1274811717647677032)),
(4, Resize(29, 5794915859890527824)),
(2, Reserve(55)),
(1, Resize(71, 227201394442576538)),
(6, Reserve(72)),
(3, Resize(0, 6289667211629638856)),
(1, Reserve(18)),
(3, Push(13834230432887299611)),
(0, Push(9820546493818449427)),
(0, Push(13211181115898970904)),
(0, Push(10966940377309801532)),
(7, Resize(20, 16290344738375090040)),
(6, Push(8376557472076204755)),
(5, Push(7075107822081082475)),
(4, Push(13688906561890343957)),
(6, Push(18397397298154655122)),
(1, Push(12241272500589537243)),
(3, Push(12647322535621493448)),
(4, Reserve(52)),
(6, Push(16708086432963643365)),
(0, Resize(59, 11616400252456090558)),
(0, Push(11933557546634591469)),
(2, Push(4465138436592395375)),
(1, Reserve(91)),
(0, Resize(99, 6582327297630873598)),
(0, Push(2917645691347360867)),
(2, Push(13540072504010523105)),
(3, Reserve(17)),
(2, Reserve(16)),
(0, Reserve(2)),
(3, Push(752321737674337719)),
(7, Reserve(32)),
(0, Reserve(71)),
(2, Push(9081992076940592004)),
(1, Resize(43, 7684511904390755849)),
(5, Push(17569856771915805365)),
(4, Push(5548408350015950457)),
(1, Resize(75, 4915642915733658997)),
(0, Push(987102234284290876)),
(6, Reserve(82)),
(6, Push(10293356557352555457)),
(1, Push(1300257579199677867)),
(4, Push(12889788053091681020)),
(3, Push(822814087742694605)),
(7, Reserve(25)),
(1, Reserve(79)),
(6, Resize(89, 2257550051579926048)),
(6, Reserve(16)),
(2, Resize(9, 13488887023827776204)),
(2, Resize(69, 12839521478462225630)),
(6, Push(9205953369572398835)),
(1, Push(9243504304607826725)),
(7, Push(429236702686864935)),
(4, Resize(41, 15488999146079567718)),
(0, Push(14851820478376629590)),
(4, Push(15896539374520472181)),
(3, Resize(27, 5692976620089907557)),
(6, Resize(52, 14377327576084841497)),
(5, Push(3306479383112047596)),
(6, Push(441983513269468745)),
(0, Reserve(43)),
(1, Resize(57, 5487696609942702356)),
(2, Push(344299554771332129)),
(7, Reserve(49)),
(5, Reserve(5)),
(4, Reserve(67)),
(1, Resize(96, 6398700515314304433)),
(2, Resize(19, 16068163172971061627)),
(3, Reserve(59)),
(6, Resize(46, 7556766827689372214)),
(0, Resize(69, 13270043707243941141)),
(3, Resize(80, 15435745910835209784)),
(0, Resize(23, 17678716989182847050)),
(7, Reserve(57)),
(6, Push(18232981473844706499)),
(3, Resize(7, 5774591707393533770)),
(1, Push(12046682489383942907)),
(3, Resize(41, 5224387578766817303)),
(5, Reserve(97)),
(3, Resize(78, 2679295251457757521)),
(7, Reserve(1)),
(6, Reserve(45)),
(3, Push(16509358460557708371)),
(4, Reserve(31)),
(7, Reserve(94)),
(0, Push(3937217562061589671)),
(1, Push(5906037351812797474)),
(3, Reserve(36)),
(1, Push(15178821695834095251)),
(7, Resize(91, 9794502638203248100)),
(6, Resize(42, 9613929237883037624)),
(1, Push(4599326753355542128)),
(1, Reserve(24)),
(2, Reserve(3)),
(6, Push(17488390456372991652)),
(1, Resize(35, 10413538906329710191)),
(3, Resize(63, 7089861612598655412)),
(7, Resize(73, 2503708897832437533)),
(5, Push(4640814851723099506)),
(0, Push(6996082249668953711)),
(6, Resize(86, 15227194503105842076)),
(3, Reserve(63)),
(6, Push(3196056850873317527)),
(4, Push(399836781972870995)),
(5, Resize(43, 14825103139336093147)),
(5, Reserve(6)),
(1, Resize(76, 4892475064355782827)),
(6, Push(12390075741166097247)),
(4, Resize(90, 18436285272951707514)),
(1, Resize(21, 2918140766224845648)),
(5, Reserve(88)),
(5, Push(3335204913117583534)),
(0, Push(15743747858747785255)),
(5, Resize(31, 10267170282093158614)),
(3, Resize(49, 14231167602682777350)),
(3, Reserve(84)),
(7, Reserve(85)),
(0, Push(5019514301157935629)),
(5, Resize(17, 5883624102454575456)),
(3, Reserve(94)),
(5, Reserve(51)),
(6, Push(9217450148175425243)),
(7, Resize(59, 9633693270724072726)),
(7, Reserve(10)),
(1, Reserve(5)),
(2, Resize(81, 4649551299926023161)),
(3, Push(7611674631818278927)),
(7, Reserve(71)),
(1, Reserve(1)),
(1, Reserve(38)),
(4, Resize(81, 15783501365382499737)),
(5, Reserve(73)),
(1, Push(3337285622280602938)),
(1, Resize(32, 561682769353209217)),
(2, Push(7477863033752468939)),
(1, Resize(18, 15076461858634126137)),
(2, Resize(26, 6756497160158165109)),
(3, Push(14531825449056867231)),
(2, Reserve(42)),
(0, Reserve(59)),
(6, Reserve(99)),
(3, Push(16582187338810011513)),
(0, Reserve(7)),
(7, Reserve(49)),
(7, Reserve(83)),
(7, Push(16440204891268282632)),
(4, Resize(82, 16570023916659548634)),
(4, Push(12683962471258754451)),
(5, Push(5791973939458236569)),
(6, Push(13213510239406200528)),
(3, Reserve(79)),
(6, Push(15151307855246737024)),
(5, Push(18110379106169373794)),
(6, Resize(70, 16265517345271633039)),
(3, Reserve(24)),
(7, Reserve(88)),
(5, Resize(25, 941960336346673535)),
(1, Resize(63, 10216767809765890372)),
(3, Push(13304940051244382601)),
(2, Push(14882904976297793409)),
(2, Push(11569588926909486508)),
(3, Push(5528621615841482224)),
(1, Reserve(59)),
(0, Push(12857827069239766853)),
(5, Resize(13, 15867530733364759125)),
(5, Resize(79, 7083622966161660992)),
(6, Resize(73, 17745503955733160843)),
(5, Reserve(17)),
(1, Reserve(15)),
(2, Push(16159478224118658921)),
(2, Resize(83, 6143385470724018223)),
(2, Push(2861412736163086968)),
(5, Reserve(9)),
(2, Resize(49, 2597859128867577171)),
(7, Resize(8, 8691095441763065170)),
(3, Resize(85, 14749237194408553888)),
(1, Push(12613456404160136228)),
(6, Reserve(62)),
(0, Resize(9, 13445206803119276873)),
(1, Reserve(99)),
(7, Reserve(29)),
(2, Resize(59, 14780250818751707961)),
(4, Push(18230048853166366343)),
(1, Reserve(82)),
(2, Push(18262091739584071212)),
(6, Push(12340500320916417079)),
(0, Push(16718706910633256492)),
(5, Push(10022904588350819343)),
(1, Push(14513473731490793527)),
(1, Push(13321333111082934834)),
(3, Resize(57, 16035774627986749941)),
(2, Resize(79, 7516080677271412287)),
(0, Resize(84, 3275081912479550278)),
(1, Push(9335943052069771717)),
(3, Resize(90, 741665365317424548)),
(7, Push(4784516684947081405)),
(7, Resize(33, 11931793047609001431)),
(2, Resize(4, 18270819633106215317)),
(2, Push(1800214047186378173)),
(4, Resize(86, 2500544818230093706)),
(7, Resize(29, 4676717314521769775)),
(3, Push(1032059459069719847)),
(3, Resize(9, 10330166000581011355)),
(3, Resize(8, 2751967310522721445)),
(7, Push(4781601218464691600)),
(0, Resize(34, 4678438393402615100)),
(3, Resize(19, 15674867404793608550)),
(1, Push(6137232626642763037)),
(0, Push(18439788688585119739)),
(3, Resize(79, 10186791813373670715)),
(0, Resize(9, 4381079811306291212)),
(6, Reserve(58)),
(3, Push(2590056937737970261)),
(5, Reserve(95)),
(7, Reserve(80)),
(4, Reserve(64)),
(1, Push(10783417499695203044)),
(3, Resize(9, 14468736489993925518)),
(7, Resize(5, 16128883050309857162)),
(0, Reserve(2)),
(5, Push(12785926325014837615)),
(2, Resize(99, 15878487414784161903)),
(4, Resize(32, 11436782439796538255)),
(0, Resize(72, 1570104243660315982)),
(0, Push(13714353127567045290)),
(7, Reserve(35)),
(7, Reserve(36)),
(1, Resize(20, 4254330562542153936)),
(4, Reserve(21)),
(6, Reserve(1)),
(6, Push(15723119482315723397)),
(6, Reserve(68)),
(1, Reserve(39)),
(3, Push(13925026279088168711)),
(1, Push(12512371844331225703)),
(3, Push(17491843885563059621)),
(5, Push(15640843850412469565)),
(4, Resize(6, 5495866525514215352)),
(0, Resize(78, 376812290890297982)),
(4, Push(3119804732190693274)),
(0, Push(10649693029762344711)),
(4, Resize(0, 2805787139708530871)),
(1, Push(5799739932524152048)),
(2, Reserve(74)),
(3, Resize(20, 3819612525069790771)),
(2, Resize(41, 10102602867279941121)),
(7, Resize(85, 17495981587299947726)),
(7, Push(17110771282840114449)),
(1, Reserve(85)),
(5, Reserve(21)),
(3, Reserve(6)),
(7, Push(8335952026385400474)),
(6, Push(11596903061863365962)),
(4, Push(964814673025398563)),
(7, Reserve(82)),
(0, Reserve(33)),
(6, Reserve(46)),
(6, Reserve(60)),
(4, Reserve(22)),
(7, Resize(71, 9806261207981417408)),
(4, Push(5819104801120654773)),
(7, Push(16107863213855999050)),
(7, Push(2702720670289344196)),
(7, Push(16049741483323875487)),
(5, Reserve(5)),
(0, Resize(67, 3016723081177068981)),
(0, Resize(87, 6290252406291272204)),
(4, Resize(63, 1509437710969278911)),
(0, Reserve(46)),
(2, Resize(35, 12695478531576903684)),
(1, Push(1919515398301307586)),
(6, Reserve(15)),
(0, Resize(49, 9334302579832564788)),
(1, Reserve(95)),
(6, Push(3205104346745568223)),
(7, Reserve(21)),
(5, Push(13994165259637534467)),
(6, Reserve(33)),
(3, Resize(78, 568884156863163741)),
(1, Resize(4, 1578751576855810311)),
(3, Push(612827329542074034)),
(6, Reserve(65)),
(5, Resize(91, 11597552787912730251)),
(6, Resize(70, 16794745016355576351)),
(6, Resize(22, 8010685806294072765)),
(5, Resize(50, 16501264971956211474)),
(5, Reserve(19)),
(4, Reserve(16)),
(0, Resize(88, 9056857703603157841)),
(6, Push(10387213449934502296)),
(4, Resize(81, 11181275113404847846)),
(3, Push(18293768560649599640)),
(1, Resize(39, 7325648604548967540)),
(0, Push(3204513896835787907)),
(5, Push(4785596010931471935)),
(2, Resize(28, 1915217858803857846)),
(7, Push(14013567789228732649)),
(3, Push(8717620574923877051)),
(0, Push(6180107370417069911)),
(4, Reserve(99)),
(7, Push(4937820000918431608)),
(0, Resize(17, 11028864438573721116)),
(4, Push(14526351704074105667)),
(3, Push(14698974792005445501)),
(4, Push(13473872864183283796)),
(4, Reserve(97)),
(2, Push(11565790739491550656)),
(6, Push(12867301537842065675)),
(3, Resize(57, 18395334540803284173)),
(7, Push(10669324893310290347)),
(2, Reserve(93)),
(4, Push(7302556619043146732)),
(4, Push(16059879797872393380)),
(1, Resize(80, 15707822832450654573)),
(4, Resize(67, 17322616832252248336)),
(3, Resize(89, 15664268963544292746)),
(6, Push(10224960836742423014)),
(7, Resize(46, 1535430416666820101)),
(2, Reserve(19)),
(4, Reserve(23)),
(3, Push(16165956669883332935)),
(1, Reserve(46)),
(3, Reserve(91)),
(4, Reserve(86)),
(6, Reserve(33)),
(0, Push(8383723510733348605)),
(2, Resize(62, 5050263965764670933)),
(2, Resize(60, 13414652522662030188)),
(0, Push(2163545114686344084)),
(0, Push(8159566120606897744)),
(2, Reserve(81)),
(2, Push(65198384152091738)),
(6, Push(13063063387541250953)),
(6, Push(8263764888341946834)),
(3, Resize(81, 11361146613014776609)),
(7, Push(6777904842678076726)),
(4, Resize(28, 16747455473350839104)),
(1, Push(1022572818789219642)),
(4, Resize(65, 10438872822855775470)),
(3, Resize(82, 3728010992530822830)),
(1, Reserve(46)),
(1, Resize(6, 3074843612257847349)),
(5, Resize(73, 8276561271062403640)),
(3, Reserve(10)),
];
rand_op_seq_inner(seq, None);
}