use proptest::collection;
use proptest::prelude::*;

use arenavec::region::{Arena, SliceVec};
use arenavec::ArenaBacking;

const DEFAULT_CAPACITY: usize = 4096 << 16;

#[derive(Clone, Debug)]
enum SliceVecOp {
    Push(usize),
    Resize(usize, usize),
    Reserve(usize),
    Delete,
    Clone(usize),
}

prop_compose! {
    fn arb_op(num_vecs: usize)
        (id in 0..5,
         size in 0..100,
         val in 0..std::usize::MAX,
         index in 0..num_vecs)
        -> SliceVecOp
    {
        match id {
             0 => SliceVecOp::Push(val),
             1 => SliceVecOp::Resize(size as usize, val),
             2 => SliceVecOp::Reserve(size as usize),
             3 => SliceVecOp::Delete,
             4 => SliceVecOp::Clone(index),
             _ => 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(num_vecs), 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 = 16;

fn rand_op_seq_inner(mut seq: Vec<(usize, SliceVecOp)>, filter: Option<&[usize]>) {
    let arena = Arena::init_capacity(ArenaBacking::SystemAllocation, DEFAULT_CAPACITY).unwrap();
    let token = arena.generation_token().unwrap();

    let mut vecs: Vec<Option<Vec<usize>>> = vec![None; NUM_VECS];
    let mut slice_vecs: Vec<Option<SliceVec<usize>>> = vec![None; NUM_VECS];

    for (v, op) in seq.drain(..) {
        if let Some(s) = filter {
            if !s.contains(&v) {
                continue;
            }
        }

        match op {
            SliceVecOp::Push(e) => {
                if let (&mut Some(ref mut r), &mut Some(ref mut r2)) =
                    (&mut vecs[v], &mut slice_vecs[v])
                {
                    r.push(e);
                    r2.push(e);
                } else {
                    let mut vec = Vec::new();
                    let mut slice_vec = SliceVec::new(token.weak());

                    vec.push(e);
                    slice_vec.push(e);

                    vecs[v] = Some(vec);
                    slice_vecs[v] = Some(slice_vec);
                }
            }
            SliceVecOp::Resize(l, e) => {
                if let (&mut Some(ref mut r), &mut Some(ref mut r2)) =
                    (&mut vecs[v], &mut slice_vecs[v])
                {
                    r.resize(l, e);
                    r2.resize(l, e);
                } else {
                    let mut vec = Vec::new();
                    let mut slice_vec = SliceVec::new(token.weak());

                    vec.resize(l, e);
                    slice_vec.resize(l, e);

                    vecs[v] = Some(vec);
                    slice_vecs[v] = Some(slice_vec);
                }
            }
            SliceVecOp::Reserve(l) => {
                if let (&mut Some(ref mut r), &mut Some(ref mut r2)) =
                    (&mut vecs[v], &mut slice_vecs[v])
                {
                    r.reserve(l);
                    r2.reserve(l);
                } else {
                    let mut vec = Vec::new();
                    let mut slice_vec = SliceVec::new(token.weak());

                    vec.reserve(l);
                    slice_vec.reserve(l);

                    vecs[v] = Some(vec);
                    slice_vecs[v] = Some(slice_vec);
                }
            }
            SliceVecOp::Delete => {
                vecs[v] = None;
                slice_vecs[v] = None;
            }
            SliceVecOp::Clone(i) => {
                vecs[v] = vecs[i].clone();
                slice_vecs[v] = slice_vecs[i].clone();
            }
        }

        for i in 0..NUM_VECS {
            if let (&Some(ref r), &Some(ref r2)) = (&vecs[i], &slice_vecs[i]) {
                assert_eq!(**r, **r2);
            } else if vecs[i].is_some() || slice_vecs[i].is_some() {
                panic!("missing vec");
            }
        }
    }
}

#[cfg(not(miri))]
mod prop {
    use super::*;
    const NUM_OPS: usize = 800;

    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("dynamic").unwrap();
            writeln!(file, "{:?}", seq).unwrap();
            rand_op_seq_inner(seq, None);
        }
    }
}

#[test]
fn pre_rand_op_seq1() {
    use SliceVecOp::*;

    let seq = vec![
        (3, Reserve(55)),
        (6, Delete),
        (6, Delete),
        (11, Clone(12)),
        (14, Resize(2, 9181993184925740557)),
        (5, Clone(7)),
        (0, Push(15919843562413822883)),
        (2, Delete),
        (1, Delete),
        (4, Push(9914124670724256873)),
        (6, Delete),
        (4, Reserve(15)),
        (0, Delete),
        (5, Reserve(62)),
        (15, Reserve(97)),
        (0, Push(17760445529334174111)),
        (14, Clone(10)),
        (12, Clone(9)),
        (15, Push(3581819063424083254)),
        (2, Reserve(91)),
        (15, Clone(10)),
        (2, Reserve(78)),
        (6, Push(547912647476391223)),
        (12, Resize(2, 11665879098205780775)),
        (10, Clone(0)),
        (12, Delete),
        (4, Clone(3)),
        (10, Resize(31, 5645937981469876588)),
        (15, Push(510150692187035013)),
        (8, Push(12014721245451062718)),
        (12, Push(8744903044368885281)),
        (3, Clone(13)),
        (0, Clone(0)),
        (13, Push(5608643173010791991)),
        (15, Push(799198662165967016)),
        (15, Clone(14)),
        (4, Resize(89, 9888984187087414676)),
        (9, Push(17674360336369971772)),
        (11, Clone(0)),
        (14, Delete),
        (1, Delete),
        (0, Resize(88, 10378184979890930361)),
        (2, Resize(19, 10504046708792733143)),
        (14, Delete),
        (11, Resize(98, 9352612750929433706)),
        (1, Resize(66, 11074594545764839005)),
        (15, Clone(12)),
        (8, Push(1981579861464125147)),
        (8, Clone(14)),
        (1, Delete),
        (6, Clone(7)),
        (8, Delete),
        (8, Delete),
        (14, Push(924998657106645384)),
        (3, Delete),
        (0, Clone(10)),
        (2, Clone(3)),
        (15, Clone(12)),
        (11, Delete),
        (14, Reserve(4)),
        (14, Push(14447318976041117510)),
        (4, Push(2143289694681391746)),
        (10, Clone(11)),
        (5, Reserve(37)),
        (11, Resize(63, 4472406788999386228)),
        (7, Clone(9)),
        (11, Delete),
        (3, Resize(49, 7440578493354731240)),
        (8, Resize(70, 12739778289680150598)),
        (1, Resize(34, 12450521508988733452)),
        (11, Reserve(29)),
        (1, Clone(8)),
        (6, Resize(26, 2276746818609489529)),
        (7, Clone(8)),
        (8, Clone(6)),
        (9, Delete),
        (15, Push(13021226814418244904)),
        (9, Clone(3)),
        (11, Delete),
        (1, Reserve(30)),
        (10, Reserve(99)),
        (12, Push(3516443519934813697)),
        (1, Clone(15)),
        (1, Reserve(73)),
        (12, Reserve(13)),
        (1, Push(158343935436872664)),
        (0, Reserve(80)),
        (5, Reserve(44)),
        (13, Delete),
        (1, Resize(13, 7644480859250035280)),
        (5, Push(15020480398127936975)),
        (0, Reserve(42)),
        (11, Delete),
        (10, Clone(14)),
        (15, Resize(83, 15209155815080207069)),
        (3, Push(15950510069561915833)),
        (7, Resize(81, 13763136299127400336)),
        (10, Delete),
        (13, Clone(3)),
        (14, Resize(9, 8131723649722137367)),
        (11, Clone(4)),
        (2, Reserve(31)),
        (13, Reserve(91)),
        (3, Clone(1)),
        (9, Resize(86, 8696974401563944681)),
        (0, Reserve(38)),
        (14, Reserve(99)),
        (5, Delete),
        (3, Push(5121446013148128013)),
        (12, Push(4329537422540865920)),
        (2, Resize(68, 11214877473821444136)),
        (1, Reserve(62)),
        (5, Clone(9)),
        (0, Delete),
        (7, Clone(0)),
        (6, Push(11413698659255763737)),
        (14, Resize(63, 321367078517683617)),
        (8, Delete),
        (4, Reserve(93)),
        (11, Clone(4)),
        (7, Delete),
        (6, Clone(1)),
        (5, Delete),
        (15, Reserve(60)),
        (14, Resize(27, 13794855111558696277)),
        (11, Push(3280182800071324128)),
        (11, Reserve(87)),
        (6, Reserve(43)),
        (1, Delete),
        (15, Clone(0)),
        (4, Delete),
        (9, Resize(46, 6760770662726765323)),
        (2, Resize(76, 9957708435082698331)),
        (3, Clone(8)),
        (7, Push(12332036708962085655)),
        (8, Resize(29, 4894435262059075594)),
        (2, Delete),
        (13, Push(6286843531593641487)),
        (12, Delete),
        (4, Reserve(3)),
        (13, Push(11437546260089131405)),
        (15, Resize(12, 17575700331483463663)),
        (10, Resize(98, 13107335384344923642)),
        (9, Resize(24, 2590665981091132743)),
        (13, Reserve(37)),
        (12, Delete),
        (15, Push(17695069646768687545)),
        (0, Clone(15)),
        (15, Delete),
        (6, Resize(77, 5375867269089044845)),
        (9, Resize(16, 10240988741184104069)),
        (7, Resize(56, 10348415685404012920)),
        (15, Reserve(39)),
        (13, Resize(36, 7959804177109318256)),
        (12, Clone(11)),
        (8, Push(2371129037566180605)),
        (12, Resize(37, 8731978314432239103)),
        (3, Clone(13)),
        (0, Push(2390960560404725163)),
        (7, Clone(6)),
        (12, Reserve(1)),
        (9, Push(853290400667496984)),
        (0, Reserve(82)),
        (9, Resize(66, 3011911157500707730)),
        (0, Push(13664977678290632164)),
        (6, Delete),
        (5, Reserve(83)),
        (14, Push(11528933400714123656)),
        (1, Clone(5)),
        (4, Delete),
        (3, Push(15258902163540527833)),
        (8, Clone(10)),
        (3, Push(2856582773279891167)),
        (4, Resize(48, 10937144296519606263)),
        (5, Resize(59, 7874739369683613757)),
        (14, Reserve(15)),
        (5, Reserve(94)),
        (7, Delete),
        (4, Push(96682023318699636)),
        (3, Clone(6)),
        (6, Delete),
        (8, Reserve(17)),
        (7, Delete),
        (3, Reserve(37)),
        (1, Clone(11)),
        (5, Push(10373042326422333449)),
        (3, Clone(7)),
        (1, Clone(8)),
        (8, Push(8920768289946442564)),
        (14, Reserve(31)),
        (14, Delete),
        (7, Clone(14)),
        (3, Reserve(75)),
        (8, Push(6201779546824799226)),
        (0, Resize(33, 320703945681475855)),
        (8, Delete),
        (12, Clone(0)),
        (13, Push(13248668313980984681)),
        (6, Push(2135333570642880765)),
        (7, Resize(75, 3569571901013613901)),
        (15, Push(6355679103294584459)),
        (8, Clone(10)),
        (14, Resize(61, 4440297850203530805)),
        (15, Reserve(9)),
        (13, Push(15232474028054891559)),
        (14, Resize(22, 6003970840550370421)),
        (10, Delete),
        (4, Push(8647684243552655330)),
        (12, Reserve(59)),
        (8, Push(8467165057973842159)),
        (7, Push(184069879120486346)),
        (15, Resize(30, 15323649527069414864)),
        (15, Push(6197218063424935893)),
        (2, Delete),
        (15, Push(6798034692589694115)),
        (7, Clone(6)),
        (0, Push(10882411174140544149)),
        (1, Push(3036188248926166446)),
        (5, Resize(56, 12724156124979085483)),
        (0, Delete),
        (12, Delete),
        (1, Push(2561410546067280154)),
        (14, Push(7700268032066407929)),
        (10, Resize(16, 13303473728354040491)),
        (3, Delete),
        (0, Reserve(48)),
        (10, Delete),
        (10, Delete),
        (11, Clone(5)),
        (5, Resize(69, 13093594591472695334)),
        (11, Push(7148887356064205290)),
        (3, Push(1397635886341542457)),
        (2, Clone(6)),
        (6, Push(13553921681205461901)),
        (2, Delete),
        (0, Push(3396420297232994328)),
        (10, Delete),
        (14, Clone(0)),
        (10, Clone(7)),
        (4, Delete),
        (15, Push(2668745464404037919)),
        (15, Clone(1)),
        (5, Resize(14, 7856649775565334672)),
        (7, Delete),
        (7, Clone(4)),
        (6, Reserve(98)),
        (8, Delete),
        (9, Push(11636296564826611125)),
        (4, Reserve(70)),
        (8, Clone(3)),
        (14, Clone(8)),
        (10, Reserve(24)),
        (0, Push(12135974883370736446)),
        (0, Clone(9)),
        (0, Reserve(96)),
        (15, Clone(12)),
        (1, Delete),
        (11, Push(6270388043910333986)),
        (15, Reserve(90)),
        (13, Push(10721657545784302738)),
        (9, Resize(61, 1027893909673767251)),
        (11, Delete),
        (12, Delete),
        (9, Delete),
        (3, Clone(6)),
        (2, Reserve(53)),
        (14, Reserve(0)),
        (0, Clone(12)),
        (6, Resize(58, 5526308978524795915)),
        (4, Push(15110697512312219883)),
        (10, Reserve(30)),
        (5, Delete),
        (9, Delete),
        (6, Resize(41, 15620245461611686326)),
        (3, Reserve(2)),
        (10, Push(10665300645855081812)),
        (13, Resize(24, 14113110661956051873)),
        (9, Reserve(83)),
        (0, Resize(30, 18444532863587105918)),
        (11, Reserve(90)),
        (1, Resize(77, 17486104945713059802)),
        (2, Reserve(33)),
        (6, Push(2914660377430711691)),
        (15, Reserve(40)),
        (6, Delete),
        (4, Reserve(28)),
        (13, Reserve(19)),
        (7, Reserve(90)),
        (1, Clone(1)),
        (6, Push(15719332401043031158)),
        (12, Push(15927131359584427030)),
        (14, Delete),
        (11, Clone(7)),
        (15, Push(10828173622187565063)),
        (1, Delete),
        (1, Push(9660138156222434978)),
        (15, Push(12811627347852557139)),
        (1, Push(11599694355497791364)),
        (4, Resize(91, 12047418642007310550)),
        (4, Reserve(10)),
        (9, Push(15474194830515731445)),
        (7, Clone(13)),
        (7, Resize(8, 18391955169689383904)),
        (0, Push(8099693322767031229)),
        (3, Push(13039487520172332499)),
        (12, Reserve(99)),
        (8, Reserve(36)),
        (0, Reserve(18)),
        (14, Clone(14)),
        (14, Reserve(8)),
        (11, Reserve(72)),
        (12, Clone(15)),
        (1, Resize(11, 11235794988330384999)),
        (6, Delete),
        (11, Clone(14)),
        (10, Clone(13)),
        (8, Reserve(1)),
        (8, Push(17695553558114134918)),
        (14, Resize(60, 2724013127639216256)),
        (2, Reserve(63)),
        (15, Resize(34, 4377782161344628252)),
        (1, Push(6642628471663747240)),
        (9, Delete),
        (15, Reserve(8)),
        (4, Push(16039751976977441951)),
        (1, Resize(56, 11082581028142055934)),
        (5, Delete),
        (10, Clone(5)),
        (8, Push(1710176479087341789)),
        (1, Delete),
        (2, Push(13064546283145797957)),
        (12, Reserve(12)),
        (4, Reserve(12)),
        (8, Push(4632777438848244713)),
        (15, Clone(10)),
        (14, Reserve(36)),
        (10, Delete),
        (12, Resize(8, 6313553747720661791)),
        (11, Delete),
        (15, Resize(96, 2871082347950632412)),
        (1, Reserve(98)),
        (1, Reserve(44)),
        (3, Push(10125848888979637471)),
        (6, Resize(55, 5198632007033356725)),
        (8, Clone(15)),
        (8, Delete),
        (2, Push(12569468444285000290)),
        (9, Push(14715812815230639425)),
        (14, Reserve(21)),
        (2, Reserve(96)),
        (5, Delete),
        (5, Reserve(68)),
        (14, Reserve(94)),
        (15, Push(7731637077653262569)),
        (10, Resize(60, 5407478343169882329)),
        (6, Push(4661254407631391157)),
        (10, Clone(5)),
        (6, Reserve(5)),
        (8, Delete),
        (10, Delete),
        (10, Reserve(13)),
        (9, Reserve(8)),
        (12, Push(18046866104761954958)),
        (14, Clone(5)),
        (3, Clone(7)),
        (8, Delete),
        (11, Reserve(65)),
        (5, Push(13401052122352721147)),
        (1, Delete),
        (4, Resize(82, 14699307571557200419)),
        (3, Reserve(93)),
        (7, Clone(14)),
        (14, Clone(3)),
        (10, Delete),
        (4, Reserve(33)),
        (0, Reserve(65)),
        (13, Reserve(50)),
        (11, Push(17112356469118082349)),
        (1, Reserve(68)),
        (15, Reserve(31)),
        (13, Clone(14)),
        (14, Reserve(75)),
        (4, Clone(11)),
        (2, Reserve(88)),
        (2, Delete),
        (7, Reserve(16)),
        (10, Push(7964419327283317707)),
        (5, Resize(97, 8140876208351341376)),
        (10, Reserve(75)),
        (12, Push(12612329517189218742)),
        (3, Resize(43, 5938902263435041987)),
        (5, Resize(15, 16327741175170675794)),
        (15, Reserve(43)),
        (3, Delete),
        (13, Delete),
        (6, Resize(77, 18333231746669737739)),
        (0, Delete),
        (7, Resize(47, 9974346952012998876)),
        (10, Delete),
        (9, Reserve(84)),
        (14, Resize(30, 17856428448802793678)),
        (11, Clone(8)),
        (11, Clone(6)),
        (4, Clone(4)),
        (12, Reserve(37)),
        (10, Delete),
        (1, Reserve(46)),
        (1, Reserve(50)),
        (1, Clone(4)),
        (2, Reserve(27)),
        (9, Clone(10)),
        (3, Reserve(99)),
        (5, Reserve(37)),
        (13, Delete),
        (1, Push(2474543140547976700)),
        (10, Reserve(71)),
        (11, Resize(29, 6336955706014035003)),
        (1, Push(5191676920508331440)),
        (3, Push(3959686532702870684)),
        (1, Push(12757412093069411819)),
        (4, Push(3618709367206262463)),
        (0, Resize(6, 2902237554203182817)),
        (2, Clone(7)),
        (12, Reserve(90)),
        (3, Resize(95, 3615060844328178420)),
        (6, Resize(16, 15510455931990274786)),
        (4, Push(6726887419972882410)),
        (12, Clone(6)),
        (2, Resize(53, 11170496714486590860)),
        (15, Clone(11)),
        (10, Resize(95, 12964813814690368573)),
        (3, Reserve(5)),
        (1, Delete),
        (4, Push(11223713596238757756)),
        (0, Clone(5)),
        (12, Delete),
        (9, Resize(97, 15153123251183991406)),
        (1, Resize(6, 13647840168581848176)),
        (13, Delete),
        (7, Resize(26, 8978381703281773190)),
        (4, Delete),
        (3, Reserve(25)),
        (9, Push(4408352192206950537)),
        (5, Resize(12, 11080776107267454358)),
        (8, Resize(44, 6577883378112600156)),
        (13, Push(4353873035812619503)),
        (3, Reserve(98)),
        (5, Resize(28, 4376305969070463055)),
        (11, Resize(83, 7204426792059660124)),
        (14, Resize(46, 3312729852019959808)),
        (9, Reserve(12)),
        (0, Push(4541894469658247636)),
        (7, Push(8199663174758225594)),
        (9, Delete),
        (12, Delete),
        (12, Push(16283647497759403632)),
        (11, Clone(11)),
        (1, Resize(22, 6195947238172734193)),
        (9, Delete),
        (6, Reserve(73)),
        (6, Delete),
        (6, Resize(51, 15536624630625698243)),
        (11, Push(12514575626897823622)),
        (0, Clone(10)),
        (6, Delete),
        (3, Push(129272047846892387)),
        (13, Clone(6)),
        (8, Resize(62, 13366978213480125396)),
        (5, Delete),
        (0, Delete),
        (5, Clone(11)),
        (5, Delete),
        (12, Resize(87, 3567626413837123105)),
        (14, Reserve(21)),
        (5, Push(13354147640050485739)),
        (15, Clone(13)),
        (0, Delete),
        (1, Reserve(27)),
        (10, Push(17126715403919846495)),
        (2, Delete),
        (13, Resize(53, 8810719453609799769)),
        (8, Clone(14)),
        (9, Delete),
        (3, Reserve(4)),
        (3, Reserve(14)),
        (6, Push(17076965640637140044)),
        (14, Reserve(15)),
        (4, Delete),
        (11, Delete),
        (1, Delete),
        (4, Reserve(61)),
        (7, Reserve(60)),
        (9, Resize(32, 4695100641956111160)),
        (0, Reserve(18)),
        (11, Resize(55, 16148431711066523961)),
        (2, Resize(75, 16049491549088778199)),
        (12, Push(10166699799951678313)),
        (10, Delete),
        (11, Reserve(78)),
        (13, Clone(13)),
        (15, Delete),
        (11, Clone(6)),
        (8, Resize(74, 3334269167065671418)),
        (12, Push(14702597994541843967)),
        (2, Delete),
        (8, Reserve(29)),
        (12, Reserve(27)),
        (1, Resize(36, 1084475432692882502)),
        (11, Reserve(22)),
        (2, Resize(60, 17591812941533033042)),
        (0, Delete),
        (0, Delete),
        (3, Delete),
        (1, Clone(12)),
        (0, Reserve(37)),
        (14, Resize(10, 13360692699194996883)),
        (14, Push(13667691162508421195)),
        (4, Push(6987553133451894185)),
        (8, Clone(8)),
        (11, Resize(50, 12212590250776093899)),
        (11, Push(16783449861203380667)),
        (1, Clone(9)),
        (6, Push(5246365745158249543)),
        (1, Resize(49, 5944598282816521192)),
        (12, Delete),
        (6, Push(15586286765145595454)),
        (4, Clone(7)),
        (7, Reserve(5)),
        (12, Reserve(31)),
        (13, Delete),
        (5, Reserve(2)),
        (5, Reserve(49)),
        (0, Resize(35, 3953173403552741728)),
        (5, Resize(43, 10937395669062772261)),
        (3, Push(13791204624100870320)),
        (8, Resize(42, 11666661773193676947)),
        (11, Reserve(72)),
        (0, Resize(60, 10319735218069240569)),
        (7, Delete),
        (9, Reserve(14)),
        (1, Reserve(44)),
        (10, Reserve(60)),
        (5, Reserve(3)),
        (8, Delete),
        (4, Push(6570845830570580962)),
        (2, Delete),
        (0, Reserve(15)),
        (5, Reserve(86)),
        (5, Delete),
        (10, Push(2985620121644481644)),
        (12, Reserve(36)),
        (5, Push(5858339458011945594)),
        (0, Delete),
        (14, Delete),
        (14, Resize(16, 9197817085651009351)),
        (10, Reserve(40)),
        (4, Push(5148370360673310035)),
        (13, Push(11384145534081484566)),
        (8, Clone(3)),
        (8, Resize(58, 9801012182487672931)),
        (5, Reserve(40)),
        (14, Push(3478132030186033225)),
        (10, Push(232116650054545882)),
        (7, Resize(92, 15155939559839928187)),
        (13, Clone(6)),
        (1, Resize(17, 3631018861574665552)),
        (14, Clone(1)),
        (14, Push(8493300277813666423)),
        (0, Push(15129056169923660067)),
        (1, Clone(6)),
        (6, Resize(61, 4216590587403191843)),
        (0, Resize(45, 13567268194935247551)),
        (9, Delete),
        (1, Clone(12)),
        (8, Delete),
        (7, Push(16915960524371525228)),
        (6, Clone(9)),
        (13, Resize(61, 883713671468785578)),
        (12, Push(14267790492635852431)),
        (0, Resize(13, 18306053923598948581)),
        (2, Push(10805350640940842649)),
        (4, Push(6054423930100695817)),
        (8, Resize(5, 17901180604064304275)),
        (4, Delete),
        (10, Push(14994723216754780512)),
        (6, Reserve(65)),
        (0, Resize(13, 4273288529571917330)),
        (12, Clone(8)),
        (2, Delete),
        (3, Resize(27, 6966634420736255684)),
        (13, Reserve(78)),
        (14, Resize(72, 16557589231765597349)),
        (4, Push(205029504079470458)),
        (3, Push(18117362063666301933)),
        (10, Delete),
        (1, Resize(66, 6466571824413052814)),
        (2, Resize(61, 9404648006461021122)),
        (5, Clone(2)),
        (8, Reserve(88)),
        (14, Delete),
        (11, Clone(13)),
        (1, Push(17185371352663328420)),
        (11, Push(2622362610430855524)),
        (10, Resize(72, 10643609083231842380)),
        (1, Resize(11, 2142063448974672506)),
        (13, Reserve(9)),
        (3, Push(7682524984297163044)),
        (7, Push(4392756746682471841)),
        (10, Resize(15, 9420960665991174748)),
        (13, Clone(6)),
        (9, Delete),
        (6, Reserve(38)),
        (5, Delete),
        (5, Clone(3)),
        (6, Clone(3)),
        (9, Delete),
        (15, Push(2736314285263143180)),
        (6, Reserve(77)),
        (10, Clone(3)),
        (13, Reserve(30)),
        (12, Delete),
        (3, Delete),
        (1, Push(11152465421934513759)),
        (8, Delete),
        (14, Delete),
        (9, Reserve(73)),
        (1, Delete),
        (14, Delete),
        (15, Push(3012309411395418875)),
        (1, Clone(11)),
        (10, Resize(72, 8199077075826938900)),
        (1, Push(18305457841488521379)),
        (12, Resize(38, 15107966440460768432)),
        (5, Resize(27, 6760726122492490237)),
        (1, Resize(22, 13860396241720714842)),
        (4, Push(2923106895027045224)),
        (15, Reserve(70)),
        (15, Push(13103570382812154806)),
        (7, Resize(51, 5271739666533136672)),
        (0, Push(11847441018306778217)),
        (9, Push(323664574755184881)),
        (6, Resize(66, 4128707520200225845)),
        (15, Resize(70, 3561364195635090181)),
        (7, Reserve(82)),
        (7, Delete),
        (4, Clone(13)),
        (7, Reserve(51)),
        (11, Push(12513381760032636345)),
        (8, Delete),
        (4, Reserve(57)),
        (9, Delete),
        (14, Delete),
        (11, Delete),
        (0, Delete),
        (8, Reserve(12)),
        (9, Delete),
        (12, Delete),
        (15, Reserve(79)),
        (2, Push(1413493617594690371)),
        (5, Resize(22, 17020552305805010657)),
        (11, Resize(68, 5497527091125783004)),
        (9, Resize(54, 16110795327020332314)),
        (13, Delete),
        (12, Clone(10)),
        (4, Delete),
        (10, Push(13259090806087329830)),
        (9, Clone(14)),
        (4, Clone(1)),
        (15, Delete),
        (6, Resize(83, 7423620524230419130)),
        (4, Push(6376207667979302551)),
        (0, Clone(7)),
        (1, Clone(15)),
        (10, Clone(7)),
        (5, Push(12603759662866108322)),
        (0, Delete),
        (0, Reserve(98)),
        (4, Clone(2)),
        (13, Delete),
        (12, Resize(69, 10134324205586588923)),
        (1, Resize(73, 15214828044589917245)),
        (10, Push(1109696536742761584)),
        (1, Clone(6)),
        (5, Resize(70, 2916982105454529168)),
        (10, Resize(1, 11965745865739463466)),
        (10, Push(17510261854531419314)),
        (0, Push(6213292663251938787)),
        (9, Delete),
        (13, Clone(11)),
        (5, Delete),
        (8, Resize(60, 2909768966767375808)),
        (10, Push(18216821088985205346)),
        (14, Push(15006013824998230473)),
        (1, Delete),
        (13, Clone(9)),
        (14, Push(16655351069419300560)),
        (14, Delete),
        (7, Reserve(75)),
        (7, Reserve(30)),
        (12, Clone(13)),
        (4, Clone(12)),
        (0, Resize(22, 4355438798172179232)),
        (6, Clone(12)),
        (0, Push(15913629395110252303)),
        (12, Clone(3)),
        (5, Clone(13)),
        (10, Delete),
        (15, Delete),
        (10, Resize(87, 15667478156107885113)),
        (7, Reserve(68)),
        (13, Delete),
        (4, Clone(4)),
        (6, Resize(6, 10215906878806388056)),
        (5, Reserve(85)),
        (0, Reserve(1)),
        (8, Reserve(94)),
        (7, Push(3591443853401580409)),
        (10, Reserve(71)),
        (12, Delete),
        (13, Clone(5)),
        (8, Clone(8)),
        (4, Push(8245763814154560620)),
        (6, Delete),
        (2, Resize(86, 13417993361496483730)),
        (2, Delete),
        (3, Push(7081057433724302263)),
        (3, Push(10784959560917395378)),
        (14, Push(11609484217832868867)),
        (15, Clone(14)),
        (1, Resize(88, 11798249978156585761)),
        (12, Delete),
        (7, Resize(49, 4748418655213668696)),
        (14, Push(15437466690359738867)),
        (12, Reserve(84)),
        (9, Delete),
        (6, Push(8663017601009673241)),
        (8, Delete),
        (12, Push(7745018098865148015)),
        (2, Clone(4)),
        (0, Clone(2)),
        (3, Resize(49, 17557567982898507049)),
        (2, Push(7147835882537064218)),
        (12, Clone(5)),
        (5, Resize(9, 4120668921447977215)),
        (10, Push(4496280079788938614)),
        (7, Reserve(22)),
        (0, Resize(46, 15001214878467342258)),
        (6, Resize(93, 4455510829346237032)),
        (2, Clone(11)),
        (7, Push(11546473013499475068)),
        (13, Resize(20, 13844320205102466114)),
        (7, Reserve(30)),
        (14, Reserve(92)),
        (6, Clone(5)),
        (5, Clone(11)),
        (15, Resize(84, 5590720091305169564)),
        (14, Push(4139927891283407852)),
        (15, Resize(13, 18201205879598353462)),
        (0, Push(13659865569384669802)),
        (7, Delete),
        (4, Push(16175036331324087934)),
        (14, Push(17849787141253456711)),
        (15, Reserve(2)),
        (8, Push(12085864335044615185)),
        (1, Resize(60, 9155019104733809553)),
        (9, Clone(10)),
        (15, Delete),
        (0, Clone(15)),
        (5, Clone(15)),
        (4, Clone(1)),
        (15, Push(174924925915074525)),
        (2, Delete),
        (15, Reserve(38)),
        (1, Reserve(49)),
        (3, Delete),
        (2, Reserve(60)),
        (15, Push(13754080712417487138)),
        (13, Resize(71, 15549770938478102778)),
        (6, Reserve(5)),
        (14, Reserve(45)),
        (12, Clone(15)),
        (15, Push(2705173810456840328)),
        (13, Clone(3)),
        (14, Delete),
        (2, Push(9275004763672425495)),
        (4, Push(10770864047420094231)),
        (12, Push(18058391865553253194)),
        (0, Resize(66, 1056249739313670154)),
        (14, Reserve(2)),
        (1, Delete),
        (11, Delete),
        (5, Delete),
        (5, Push(11903383895693220755)),
        (0, Reserve(2)),
        (7, Clone(9)),
        (7, Push(1321113028828608352)),
        (13, Delete),
        (2, Clone(3)),
        (3, Delete),
        (4, Clone(13)),
    ];
    rand_op_seq_inner(seq, None);
}

#[test]
fn pre_rand_op_seq2() {
    use SliceVecOp::*;

    let seq = vec![
        (12, Delete),
        (6, Delete),
        (11, Resize(2, 15135295948867733961)),
        (12, Push(3429178973554612332)),
        (7, Clone(14)),
        (15, Push(807635815477921814)),
        (10, Push(15679985414229696799)),
        (10, Reserve(35)),
        (13, Resize(62, 17362526620214442077)),
        (0, Delete),
        (8, Reserve(27)),
        (1, Push(16504692895295540552)),
        (8, Reserve(38)),
        (7, Clone(13)),
        (1, Push(14403067622847586238)),
        (0, Push(5485601966064679676)),
        (10, Resize(55, 11383283965270597527)),
        (9, Delete),
        (9, Clone(14)),
        (4, Delete),
        (8, Resize(82, 8894109803684733036)),
        (11, Resize(2, 11195470625154206134)),
        (0, Clone(7)),
        (5, Clone(0)),
        (7, Clone(13)),
        (1, Delete),
        (11, Clone(11)),
        (10, Resize(28, 2605556281884650243)),
        (10, Resize(76, 479213999064836890)),
        (15, Push(12144634755678239852)),
        (15, Clone(5)),
        (5, Push(8575552838856676714)),
        (3, Push(11723218463906620893)),
        (8, Delete),
        (5, Resize(86, 5611527186201775080)),
        (1, Delete),
        (0, Clone(10)),
        (14, Resize(8, 14516447580114817083)),
        (3, Resize(84, 515869332870952611)),
        (5, Delete),
        (5, Reserve(70)),
        (0, Clone(6)),
        (2, Delete),
        (8, Delete),
        (4, Push(6008814625108276641)),
        (1, Reserve(72)),
        (5, Resize(2, 12860423200392070663)),
        (9, Resize(18, 17318872461949385719)),
        (4, Resize(46, 16837012545339440543)),
        (9, Resize(16, 16779071973516973346)),
        (8, Push(10261254088961743289)),
        (9, Clone(6)),
        (14, Reserve(21)),
        (3, Reserve(91)),
        (6, Reserve(55)),
        (15, Resize(8, 4746412816811002797)),
        (9, Push(6442232304992044901)),
        (12, Reserve(32)),
        (10, Reserve(31)),
        (3, Resize(2, 2400773149554713789)),
        (10, Push(12627234434932522407)),
        (13, Resize(35, 12622968101102974672)),
        (4, Clone(14)),
        (8, Reserve(97)),
        (15, Reserve(28)),
        (11, Delete),
        (13, Clone(10)),
        (9, Clone(14)),
        (13, Reserve(69)),
        (4, Reserve(39)),
        (13, Delete),
        (15, Delete),
        (13, Reserve(40)),
        (5, Delete),
        (8, Resize(79, 10922506688078496228)),
        (10, Resize(29, 5319366770186573459)),
        (8, Reserve(81)),
        (7, Push(17353183449964460277)),
        (10, Push(224493906566545821)),
        (1, Delete),
        (10, Resize(2, 2394008019151684323)),
        (14, Push(4105538610498431680)),
        (14, Resize(8, 17577983976177592239)),
        (2, Push(9842787526346703250)),
        (5, Push(9149616933788171264)),
        (0, Push(12915436391228677759)),
        (10, Resize(17, 2957049013060012642)),
        (6, Delete),
        (12, Push(16871724786340681768)),
        (10, Push(7695291178628965195)),
        (8, Reserve(8)),
        (13, Push(2161742069208388786)),
        (11, Resize(12, 9066595408114166689)),
        (15, Delete),
        (7, Reserve(48)),
        (2, Clone(6)),
        (1, Clone(3)),
        (2, Push(9335534483790641057)),
        (2, Delete),
        (14, Push(3718188661413467313)),
        (1, Delete),
        (0, Resize(95, 5825623360426598096)),
        (4, Resize(17, 2448800975171212410)),
        (10, Delete),
        (4, Clone(2)),
        (11, Delete),
        (8, Delete),
        (8, Resize(43, 7415149314006282772)),
        (8, Delete),
        (3, Clone(11)),
        (7, Clone(6)),
        (11, Resize(32, 3582380486135964821)),
        (13, Resize(28, 3725636962142724573)),
        (5, Resize(8, 4237374045867851871)),
        (14, Reserve(32)),
        (10, Delete),
        (10, Resize(65, 14263757251958425367)),
        (1, Push(225248509753515027)),
        (12, Clone(3)),
        (6, Resize(72, 4515871947838460375)),
        (4, Delete),
        (11, Reserve(97)),
        (4, Push(3674339437849061914)),
        (14, Delete),
        (1, Reserve(25)),
        (0, Push(1509324165705291066)),
        (0, Clone(15)),
        (7, Clone(14)),
        (2, Delete),
        (7, Reserve(81)),
        (13, Resize(68, 3308525274254620348)),
        (1, Push(13093900911909720996)),
        (6, Push(8919531195595665354)),
        (1, Reserve(92)),
        (6, Push(14312702528967597701)),
        (11, Reserve(46)),
        (4, Push(6310396959379258044)),
        (12, Resize(12, 3828146402436558210)),
        (15, Clone(14)),
        (13, Delete),
        (12, Clone(12)),
        (3, Delete),
        (5, Push(7947760054669610904)),
        (6, Resize(30, 6795878799468144760)),
        (2, Resize(76, 3907076331063547195)),
        (7, Push(4628797161938917935)),
        (13, Clone(9)),
        (8, Resize(24, 8014644937998156619)),
        (12, Resize(13, 8120529529037875462)),
        (15, Reserve(79)),
        (13, Resize(14, 15854375442307482317)),
        (6, Push(15697167709013533477)),
        (4, Delete),
        (3, Clone(13)),
        (9, Clone(4)),
        (4, Delete),
        (6, Push(6904010300053726869)),
        (3, Reserve(73)),
        (7, Clone(7)),
        (11, Reserve(5)),
        (0, Clone(1)),
        (3, Reserve(35)),
        (6, Push(6813733674615100908)),
        (10, Delete),
        (3, Delete),
        (13, Clone(9)),
        (2, Clone(2)),
        (5, Clone(4)),
        (4, Push(8742435089913659460)),
        (0, Resize(67, 6247685813725168115)),
        (15, Resize(79, 17886126470757154342)),
        (15, Resize(22, 16283801123260057502)),
        (13, Resize(14, 830691867711149608)),
        (10, Resize(83, 13714389569421794352)),
        (5, Push(4611483424996732595)),
        (3, Resize(45, 4302872429924608121)),
        (7, Reserve(80)),
        (1, Delete),
        (9, Resize(94, 10633638728440086413)),
        (13, Clone(7)),
        (9, Delete),
        (15, Reserve(96)),
        (8, Delete),
        (13, Clone(3)),
        (3, Resize(34, 9869309594981802727)),
        (8, Resize(79, 9713608122978205703)),
        (3, Delete),
        (12, Delete),
        (4, Clone(7)),
        (12, Clone(8)),
        (1, Resize(27, 4806014085923082194)),
        (0, Delete),
        (14, Reserve(92)),
        (15, Delete),
        (2, Reserve(78)),
        (14, Reserve(57)),
        (8, Delete),
        (8, Delete),
        (1, Resize(54, 15044043962042578658)),
        (7, Reserve(27)),
        (15, Reserve(74)),
        (14, Push(16139908561032989360)),
        (8, Resize(9, 16843518173379585475)),
        (8, Resize(21, 9992443064582314485)),
        (4, Reserve(39)),
        (0, Clone(7)),
        (12, Resize(11, 5097375509118499925)),
        (14, Reserve(72)),
        (13, Push(2764612434185106013)),
        (0, Resize(28, 7193145741048986102)),
        (6, Resize(92, 923506472582099951)),
        (7, Resize(70, 779882283965442084)),
        (0, Clone(9)),
        (15, Resize(62, 7184299133108799596)),
        (2, Clone(12)),
        (13, Delete),
        (12, Push(7295073665907086380)),
        (5, Reserve(54)),
        (15, Resize(66, 4480585429251778207)),
        (3, Push(9453526612581067247)),
        (11, Clone(15)),
        (6, Push(18343524921260056221)),
        (7, Delete),
        (11, Delete),
        (8, Reserve(24)),
        (13, Clone(11)),
        (4, Delete),
        (11, Resize(58, 6138878928295333432)),
        (11, Resize(49, 12275145529313947630)),
        (12, Reserve(60)),
        (0, Push(3905496006888639853)),
        (13, Reserve(87)),
        (13, Clone(4)),
        (15, Reserve(49)),
        (13, Clone(8)),
        (6, Reserve(76)),
        (11, Reserve(88)),
        (10, Push(2322077192098496286)),
        (11, Clone(13)),
        (7, Resize(97, 15188334462282163330)),
        (2, Resize(27, 18238521126691760663)),
        (14, Clone(0)),
        (8, Clone(0)),
        (2, Delete),
        (5, Clone(8)),
        (10, Delete),
        (2, Clone(15)),
        (10, Push(16930566427071097624)),
        (7, Push(12588902404283935490)),
        (8, Resize(6, 14047087496994038391)),
        (15, Delete),
        (9, Reserve(38)),
        (3, Reserve(54)),
        (6, Push(8089636407830984524)),
        (12, Delete),
        (0, Reserve(48)),
        (12, Clone(14)),
        (4, Resize(15, 9485656056118820546)),
        (4, Reserve(78)),
        (12, Push(5482791625663832187)),
        (9, Clone(6)),
        (3, Reserve(91)),
        (6, Delete),
        (4, Reserve(47)),
        (10, Reserve(90)),
        (10, Delete),
        (6, Resize(45, 2757675282194991383)),
        (4, Clone(12)),
        (5, Resize(39, 8588166565337823274)),
        (14, Delete),
        (8, Clone(12)),
        (6, Reserve(60)),
        (7, Resize(32, 6088954269776718588)),
        (7, Clone(9)),
        (3, Resize(54, 16989974675672370756)),
        (7, Reserve(37)),
        (0, Push(5167962521960987313)),
        (3, Resize(92, 1328629731126291213)),
        (6, Reserve(33)),
        (12, Reserve(94)),
        (2, Reserve(21)),
        (0, Reserve(27)),
        (3, Resize(35, 6669705783967932286)),
        (4, Resize(99, 16207505457004639600)),
        (9, Resize(75, 18442139303035374761)),
        (9, Resize(40, 10344780414135275642)),
        (10, Reserve(66)),
        (2, Clone(4)),
        (7, Delete),
        (14, Delete),
        (0, Clone(11)),
        (1, Reserve(76)),
        (1, Clone(7)),
        (14, Reserve(93)),
        (3, Resize(34, 16233312539425662023)),
        (2, Clone(10)),
        (6, Delete),
        (15, Resize(15, 10381808731711445405)),
        (0, Reserve(37)),
        (9, Push(1471022456004301555)),
        (8, Reserve(75)),
        (8, Push(14509854339851711738)),
        (4, Push(4250594553014377560)),
        (15, Resize(98, 3088933500730104320)),
        (3, Delete),
        (0, Resize(3, 3529606804866144626)),
        (7, Reserve(63)),
        (10, Delete),
        (5, Clone(6)),
        (1, Push(11905708864025781531)),
        (10, Clone(15)),
        (6, Clone(14)),
        (6, Delete),
        (6, Clone(15)),
        (15, Delete),
        (13, Reserve(15)),
        (12, Resize(96, 3938123026849470543)),
        (13, Delete),
        (2, Delete),
        (4, Resize(32, 6835444227822587093)),
        (1, Push(18041283321838192218)),
        (13, Clone(13)),
        (15, Clone(10)),
        (4, Delete),
        (6, Reserve(32)),
        (7, Resize(59, 3075495835736316663)),
        (7, Clone(9)),
        (13, Delete),
        (9, Push(10857928512569804968)),
        (0, Push(12913611567652247616)),
        (14, Resize(10, 8199345158097276773)),
        (12, Resize(41, 12133421477623798912)),
        (11, Clone(1)),
        (0, Push(15804493927766695605)),
        (6, Resize(56, 8417622624160498923)),
        (14, Clone(7)),
        (1, Resize(76, 13489898779562537263)),
        (15, Resize(74, 13183750541466505320)),
        (12, Push(14635341722588481549)),
        (11, Delete),
        (12, Resize(89, 304646683510894770)),
        (15, Resize(69, 8875047105330463189)),
        (15, Delete),
        (3, Clone(9)),
        (8, Reserve(75)),
        (14, Clone(2)),
        (6, Delete),
        (15, Resize(65, 16909835457492490587)),
        (11, Clone(14)),
        (0, Clone(1)),
        (0, Resize(5, 13306587503741294754)),
        (3, Push(3523331032826640970)),
        (4, Reserve(17)),
        (12, Clone(15)),
        (12, Clone(8)),
        (9, Clone(9)),
        (5, Clone(9)),
        (2, Clone(4)),
        (9, Reserve(79)),
        (1, Resize(60, 6286595798066754233)),
        (12, Clone(9)),
        (6, Reserve(12)),
        (3, Resize(5, 14772682942007301387)),
        (10, Clone(8)),
        (12, Push(13991592265642177255)),
        (12, Push(9694852775229264741)),
        (8, Push(8336894077736919678)),
        (5, Resize(4, 18014443594192036220)),
        (7, Reserve(74)),
        (6, Resize(40, 15707007716218660562)),
        (12, Delete),
        (15, Reserve(29)),
        (2, Reserve(90)),
        (8, Resize(99, 17791901069777502831)),
        (3, Delete),
        (5, Delete),
        (13, Delete),
        (3, Push(10149188429780328496)),
        (5, Reserve(65)),
        (15, Delete),
        (8, Delete),
        (12, Push(12992190152951119377)),
        (7, Reserve(3)),
        (8, Delete),
        (13, Resize(6, 7902689719357524519)),
        (2, Clone(12)),
        (5, Reserve(39)),
        (11, Push(14500535438725194115)),
        (9, Clone(7)),
        (8, Push(107959421461136594)),
        (13, Push(13950532451912570392)),
        (6, Resize(88, 9983602160735340236)),
        (15, Push(6649756617859701254)),
        (14, Push(6944999572723386656)),
        (14, Reserve(60)),
        (6, Push(17806608067683726302)),
        (6, Reserve(51)),
        (4, Delete),
        (12, Push(4004348275630388876)),
        (1, Reserve(61)),
        (12, Push(1498361358734956611)),
        (0, Resize(9, 7811237704209259380)),
        (12, Delete),
        (15, Resize(65, 3847651091716910209)),
        (10, Reserve(81)),
        (1, Clone(15)),
        (10, Delete),
        (1, Clone(5)),
        (13, Resize(14, 6535428652457078666)),
        (1, Push(4436983607368856241)),
        (6, Resize(54, 16527827240646041231)),
        (10, Resize(61, 5720486117649466558)),
        (6, Delete),
        (10, Reserve(7)),
        (6, Push(17479173953456910912)),
        (1, Clone(5)),
        (8, Reserve(79)),
        (7, Clone(13)),
        (11, Clone(15)),
        (12, Clone(6)),
        (11, Reserve(65)),
        (12, Delete),
        (0, Resize(26, 7931382661147830502)),
        (1, Clone(6)),
        (10, Delete),
        (0, Resize(47, 16559132149078946626)),
        (14, Push(1439776395374865974)),
        (8, Delete),
        (0, Delete),
        (0, Resize(57, 9533940919185571304)),
        (0, Reserve(37)),
        (9, Reserve(55)),
        (10, Reserve(67)),
        (8, Delete),
        (13, Reserve(49)),
        (10, Resize(72, 17538058309919370657)),
        (5, Push(3908756463430007514)),
        (12, Clone(13)),
        (5, Reserve(81)),
        (0, Resize(77, 2676576520258376717)),
        (10, Delete),
        (3, Delete),
        (8, Clone(7)),
        (11, Resize(80, 10000685205068136556)),
        (1, Clone(2)),
        (6, Delete),
        (14, Delete),
        (15, Push(10053759544885827150)),
        (3, Delete),
        (3, Reserve(54)),
        (10, Resize(65, 15994332470539207734)),
        (5, Resize(33, 15332397716082519156)),
        (7, Clone(8)),
        (6, Delete),
        (10, Push(13502416912705641271)),
        (11, Reserve(19)),
        (14, Delete),
        (8, Reserve(89)),
        (12, Delete),
        (10, Clone(10)),
        (8, Resize(76, 13632010671585244187)),
        (0, Reserve(93)),
        (11, Push(6418115506678749805)),
        (10, Delete),
        (6, Delete),
        (5, Reserve(2)),
        (9, Resize(66, 3828084445250841480)),
        (3, Resize(44, 14239641642974796963)),
        (10, Reserve(65)),
        (8, Delete),
        (6, Resize(86, 4371356290937974760)),
        (9, Reserve(29)),
        (8, Resize(22, 17774593038634906998)),
        (10, Resize(68, 16542101837094968488)),
        (0, Reserve(40)),
        (12, Reserve(63)),
        (5, Resize(94, 8610674986295374586)),
        (3, Clone(6)),
        (0, Push(16810243824572601580)),
        (11, Reserve(26)),
        (13, Clone(6)),
        (9, Push(15567114957826901413)),
        (2, Reserve(56)),
        (15, Push(7520878254713741693)),
        (14, Delete),
        (9, Delete),
        (3, Delete),
        (3, Clone(13)),
        (7, Reserve(38)),
        (7, Reserve(93)),
        (8, Delete),
        (8, Delete),
        (6, Reserve(68)),
        (13, Reserve(16)),
        (8, Delete),
        (0, Resize(52, 14061624734666342947)),
        (7, Resize(67, 5782837434442813618)),
        (0, Clone(4)),
        (14, Clone(10)),
        (9, Resize(75, 14965092750113977597)),
        (1, Delete),
        (10, Reserve(79)),
        (11, Clone(10)),
        (0, Delete),
        (9, Clone(5)),
        (7, Reserve(42)),
        (4, Resize(97, 10747872944387448980)),
        (0, Resize(57, 13570903293681993717)),
        (1, Reserve(19)),
        (6, Delete),
        (0, Clone(6)),
        (3, Resize(23, 14770116415348403982)),
        (13, Reserve(28)),
        (15, Delete),
        (15, Clone(11)),
        (14, Resize(83, 13850695708641000238)),
        (11, Delete),
        (9, Delete),
        (6, Delete),
        (12, Push(1289627795762085506)),
        (5, Clone(0)),
        (11, Resize(2, 7598941441323296749)),
        (0, Reserve(22)),
        (9, Clone(8)),
        (2, Reserve(99)),
        (0, Resize(79, 4208631791030061914)),
        (2, Clone(12)),
        (5, Push(13003502398034147088)),
        (6, Reserve(53)),
        (12, Resize(36, 10687895361368441296)),
        (6, Push(3268344881426863458)),
        (7, Resize(46, 6115199747176589600)),
        (8, Push(7516259074695957415)),
        (10, Clone(5)),
        (9, Clone(2)),
        (8, Reserve(14)),
        (11, Push(2535384553763363331)),
        (13, Push(9819763810956347654)),
        (8, Clone(6)),
        (2, Push(5494329100118930351)),
        (10, Resize(12, 9034330727496950683)),
        (12, Reserve(70)),
        (4, Delete),
        (15, Clone(14)),
        (6, Reserve(63)),
        (9, Delete),
        (2, Delete),
        (8, Delete),
        (5, Delete),
        (6, Clone(8)),
        (10, Reserve(27)),
        (3, Resize(70, 4719905000317361236)),
        (3, Resize(60, 17929459758415168147)),
        (3, Delete),
        (3, Reserve(63)),
        (8, Resize(49, 15555029443193652192)),
        (11, Delete),
        (13, Delete),
        (3, Clone(5)),
        (13, Resize(29, 7748100920455889203)),
        (2, Reserve(90)),
        (14, Push(15701523292370264387)),
        (13, Push(7369091640477344772)),
        (7, Delete),
        (12, Push(14365237216603446730)),
        (9, Delete),
        (11, Push(970746898747055332)),
        (10, Push(3026974275020306799)),
        (5, Delete),
        (14, Clone(14)),
        (4, Reserve(5)),
        (6, Push(10349054423217947743)),
        (6, Resize(56, 6651048908912302637)),
        (0, Resize(18, 11767532070349460329)),
        (14, Push(9904836397841960779)),
        (4, Clone(6)),
        (0, Reserve(4)),
        (12, Reserve(88)),
        (1, Clone(10)),
        (13, Delete),
        (15, Delete),
        (6, Delete),
        (10, Reserve(81)),
        (0, Resize(65, 15793498804661589216)),
        (11, Reserve(11)),
        (11, Delete),
        (0, Push(15106199871120915034)),
        (12, Resize(91, 5962336054991826734)),
        (3, Clone(4)),
        (9, Push(10601860704219246948)),
        (7, Clone(14)),
        (9, Reserve(98)),
        (14, Resize(46, 2057047163267829276)),
        (14, Clone(6)),
        (14, Clone(10)),
        (5, Reserve(78)),
        (5, Delete),
        (7, Clone(15)),
        (6, Resize(79, 10220056845078702544)),
        (7, Resize(44, 13538656163909026178)),
        (13, Clone(9)),
        (13, Reserve(85)),
        (5, Resize(53, 9011553229340911773)),
        (2, Push(13714574654982808108)),
        (1, Push(2033673054718863474)),
        (8, Push(17150806818172057881)),
        (11, Reserve(5)),
        (0, Reserve(3)),
        (1, Clone(7)),
        (14, Reserve(38)),
        (13, Reserve(62)),
        (11, Clone(15)),
        (5, Resize(92, 9049941025305325294)),
        (5, Clone(9)),
        (10, Reserve(33)),
        (4, Push(16593073585760353702)),
        (3, Push(5607928126534166044)),
        (11, Delete),
        (4, Clone(3)),
        (10, Clone(1)),
        (9, Resize(92, 10495021841638989890)),
        (11, Delete),
        (2, Reserve(97)),
        (0, Delete),
        (14, Reserve(94)),
        (10, Reserve(39)),
        (15, Push(7217406332167871152)),
        (4, Push(5624223369024110671)),
        (13, Reserve(77)),
        (10, Clone(5)),
        (0, Delete),
        (3, Clone(14)),
        (15, Delete),
        (8, Reserve(12)),
        (11, Push(11612372335995019528)),
        (1, Reserve(75)),
        (9, Push(350697313831985324)),
        (3, Clone(13)),
        (12, Reserve(1)),
        (3, Clone(0)),
        (4, Push(12707924117714330848)),
        (5, Push(17921423227846253113)),
        (3, Delete),
        (0, Clone(6)),
        (4, Reserve(31)),
        (13, Push(10642740198955269184)),
        (6, Resize(1, 10027188363892935889)),
        (3, Resize(67, 16023742445806894065)),
        (1, Resize(53, 13814965564799140896)),
        (7, Delete),
        (5, Resize(71, 8648490113132204439)),
        (6, Resize(60, 13446322347041053931)),
        (13, Push(1858810689262931711)),
        (10, Clone(15)),
        (0, Push(9770458579555334612)),
        (5, Resize(21, 6555720957923688554)),
        (0, Resize(99, 2410566794334942964)),
        (11, Clone(4)),
        (11, Delete),
        (2, Clone(11)),
        (14, Reserve(60)),
        (14, Reserve(33)),
        (1, Push(15210147863955193448)),
        (14, Resize(94, 9176814767454249494)),
        (5, Delete),
        (0, Resize(85, 15924542516975190622)),
        (9, Reserve(70)),
        (2, Clone(9)),
        (4, Reserve(24)),
        (9, Reserve(32)),
        (3, Reserve(68)),
        (5, Clone(12)),
        (0, Clone(5)),
        (1, Reserve(54)),
        (11, Push(8505682426275625605)),
        (10, Clone(4)),
        (4, Resize(21, 16013505221605244384)),
        (1, Delete),
        (11, Push(7742475759440089559)),
        (4, Clone(4)),
        (8, Reserve(67)),
        (2, Resize(92, 556243838889681219)),
        (10, Delete),
        (11, Delete),
        (6, Clone(7)),
        (7, Clone(5)),
        (13, Delete),
        (7, Resize(83, 16522774684017429086)),
        (9, Delete),
        (12, Delete),
        (15, Reserve(13)),
        (3, Delete),
        (10, Resize(56, 8070877884364491318)),
        (8, Clone(1)),
        (12, Push(15347937983631689221)),
        (13, Reserve(69)),
        (2, Clone(8)),
        (6, Delete),
        (6, Push(5034519913333244655)),
        (3, Reserve(9)),
        (4, Resize(93, 5445369943890247033)),
        (0, Push(17023593647044649502)),
        (3, Resize(9, 17774479241564684170)),
        (7, Resize(72, 18407695063865882296)),
        (14, Delete),
        (13, Delete),
        (10, Resize(74, 11898708138122413820)),
        (9, Clone(13)),
        (14, Clone(2)),
        (15, Push(4067541407354431036)),
        (10, Reserve(94)),
        (14, Clone(4)),
        (15, Clone(15)),
        (6, Push(16195243627449635319)),
        (9, Delete),
        (1, Resize(97, 15373516578227225587)),
        (11, Clone(7)),
        (15, Clone(7)),
        (10, Push(14972925203467802078)),
        (10, Clone(13)),
        (0, Resize(2, 3177135457074965433)),
        (4, Delete),
        (15, Reserve(7)),
        (2, Reserve(13)),
        (2, Clone(14)),
        (11, Delete),
        (5, Clone(1)),
        (10, Resize(88, 10536697259299608024)),
        (10, Reserve(1)),
        (13, Push(18278693230831742053)),
        (14, Push(14300998486744637794)),
        (9, Resize(54, 13755137328224773400)),
        (4, Delete),
        (2, Reserve(60)),
        (4, Reserve(90)),
        (10, Delete),
        (5, Reserve(62)),
        (3, Resize(73, 6142101422829298489)),
        (1, Push(13680234029722763964)),
        (11, Reserve(98)),
        (11, Resize(28, 5440402956881647104)),
        (15, Push(15985673956226243550)),
        (3, Push(2159558598949659380)),
        (1, Delete),
        (3, Reserve(6)),
        (15, Clone(11)),
        (11, Delete),
        (1, Resize(34, 5764929149052461213)),
        (3, Clone(8)),
        (1, Clone(7)),
        (0, Delete),
        (4, Delete),
        (0, Clone(15)),
        (10, Delete),
        (2, Resize(80, 5154796327111883408)),
        (4, Push(4170725385241150659)),
        (5, Reserve(11)),
        (6, Clone(11)),
        (2, Push(6973495995711418444)),
        (7, Reserve(34)),
        (0, Resize(42, 15394305031332186914)),
        (15, Resize(14, 14954491715701802708)),
        (6, Reserve(75)),
        (6, Push(8775073385255599863)),
        (2, Push(5507872285882580903)),
        (3, Resize(11, 3190173039088119938)),
        (8, Resize(47, 3367981164217960537)),
        (3, Resize(33, 14830867446613375029)),
        (3, Reserve(61)),
        (7, Push(3064658784107342820)),
        (15, Clone(15)),
        (8, Resize(99, 11182695511351145286)),
        (14, Push(11590095205140352119)),
        (9, Delete),
        (9, Delete),
        (0, Delete),
        (14, Reserve(52)),
        (13, Push(6868029560373433730)),
        (9, Resize(69, 8004361793246875227)),
        (1, Delete),
        (8, Resize(13, 15177204734353228624)),
        (1, Push(12669582834685271211)),
        (15, Push(8437237855330753332)),
        (3, Resize(70, 5834686850989683087)),
        (2, Clone(13)),
        (8, Delete),
        (10, Reserve(55)),
        (3, Reserve(26)),
        (2, Clone(10)),
        (8, Reserve(68)),
        (13, Resize(63, 14888498609891116385)),
        (12, Push(6558189421400768640)),
        (7, Push(4355870057028313051)),
        (15, Resize(35, 4409674738688470479)),
        (2, Resize(44, 11450761590678539197)),
        (0, Delete),
        (7, Resize(74, 4232912305902271640)),
        (13, Resize(81, 13733668580851191664)),
        (4, Delete),
        (15, Reserve(32)),
    ];
    rand_op_seq_inner(seq, None);
}