public int setNodeTableSize(int size) { int old = bddnodesize; doResize(true, old, size); return old; }
public int setNodeTableSize(int size) { return bdd_setallocnum(size); }
    public int setNodeTableSize(int size) {        int old = bddnodesize;        doResize(true, old, size);        return old;    }