if (satPolarity == BDDONE) {
if (satPolarity) {
    int satoneset_rec(int r, int var) {        if (ISCONST(r) && ISCONST(var))            return r;        if (LEVEL(r) < LEVEL(var)) {            if (ISZERO(LOW(r))) {                int res = satoneset_rec(HIGH(r), var);                int m = bdd_makenode(LEVEL(r), BDDZERO, res);                PUSHREF(m);                return m;            } else {                int res = satoneset_rec(LOW(r), var);                int m = bdd_makenode(LEVEL(r), res, BDDZERO);                PUSHREF(m);                return m;            }        } else if (LEVEL(var) < LEVEL(r)) {            int res = satoneset_rec(r, HIGH(var));            if (satPolarity == BDDONE) {                int m = bdd_makenode(LEVEL(var), BDDZERO, res);                PUSHREF(m);                return m;            } else {                int m = bdd_makenode(LEVEL(var), res, BDDZERO);                PUSHREF(m);                return m;            }        } else /* LEVEL(r) == LEVEL(var) */ {            if (ISZERO(LOW(r))) {                int res = satoneset_rec(HIGH(r), HIGH(var));                int m = bdd_makenode(LEVEL(r), BDDZERO, res);                PUSHREF(m);                return m;            } else {                int res = satoneset_rec(LOW(r), HIGH(var));                int m = bdd_makenode(LEVEL(r), res, BDDZERO);                PUSHREF(m);                return m;            }        }    }