left.firstLevel = bddvar2level[lseq[0]]; left.lastLevel = bddvar2level[lseq[leftsize]]; right.firstLevel = bddvar2level[rseq[0]]; right.lastLevel = bddvar2level[rseq[rightsize]];
    void blockdown(BddTree left) {        BddTree right = left.next;        //System.out.println("Swapping "+left.first+".."+left.last+" and "+right.first+".."+right.last);        int n;        int leftsize = left.last - left.first;        int rightsize = right.last - right.first;        int leftstart = bddvar2level[left.seq[0]];        int[] lseq = left.seq;        int[] rseq = right.seq;        /* Move left past right */        while (bddvar2level[lseq[0]] < bddvar2level[rseq[rightsize]]) {            for (n = 0; n < leftsize; n++) {                if (bddvar2level[lseq[n]] + 1 != bddvar2level[lseq[n + 1]]                    && bddvar2level[lseq[n]] < bddvar2level[rseq[rightsize]]) {                    reorder_vardown(lseq[n]);                }            }            if (bddvar2level[lseq[leftsize]] < bddvar2level[rseq[rightsize]]) {                reorder_vardown(lseq[leftsize]);            }        }        /* Move right to where left started */        while (bddvar2level[rseq[0]] > leftstart) {            for (n = rightsize; n > 0; n--) {                if (bddvar2level[rseq[n]] - 1 != bddvar2level[rseq[n - 1]]                    && bddvar2level[rseq[n]] > leftstart) {                    reorder_varup(rseq[n]);                }            }            if (bddvar2level[rseq[0]] > leftstart)                reorder_varup(rseq[0]);        }        /* Swap left and right data in the order */        left.next = right.next;        right.prev = left.prev;        left.prev = right;        right.next = left;        if (right.prev != null)            right.prev.next = right;        if (left.next != null)            left.next.prev = left;        n = left.pos;        left.pos = right.pos;        right.pos = n;                left.interleaved = false;        right.interleaved = false;    }