throw new BDDException("Reordering triggered");
throw new ReorderException();
    int bdd_makenode(int level, int low, int high) {        int hash2;        int res;        if (CACHESTATS > 0) cachestats.uniqueAccess++;        /* check whether childs are equal */        if (low == high) return low;        /* Try to find an existing node of this kind */        hash2 = NODEHASH(level, low, high);        res = HASH(hash2);        if (res != 0) {            int m1 = (level << LEV_LPOS) | low;            int m2 = ((level << (LEV_HPOS-LEV_LBITS)) & LEV_HMASK) | high;            do {                if (bddnodes[res*__node_size + offset__low] == m1 &&                    bddnodes[res*__node_size + offset__high] == m2) {                    if (CACHESTATS > 0) cachestats.uniqueHit++;                    return res;                }                res = NEXT(res);                if (CACHESTATS > 0) cachestats.uniqueChain++;            } while (res != 0);        }        /* No existing node => build one */        if (CACHESTATS > 0) cachestats.uniqueMiss++;        /* Any free nodes to use ? */        if (bddfreepos == 0) {            if (bdderrorcond != 0) return 0;            /* Try to allocate more nodes */            bdd_gbc();            if ((bddnodesize-bddfreenum) >= usednodes_nextreorder &&                bdd_reorder_ready()) {                throw new BDDException("Reordering triggered");            }            if ((bddfreenum * 100) / bddnodesize <= minfreenodes) {                bdd_noderesize(true);                hash2 = NODEHASH(level, low, high);            }            /* Panic if that is not possible */            if (bddfreepos == 0) {                bdderrorcond = Math.abs(BDD_NODENUM);                bdd_error(BDD_NODENUM);                return 0;            }        }        /* Build new node */        res = bddfreepos;        bddfreepos = NEXT(bddfreepos);        bddfreenum--;        bddproduced++;        INIT_NODE(res, level, low, high, HASH(hash2));        SETHASH(hash2, res);        return res;    }