public double setIncreaseFactor(double x) { if (x < 0) return bdd_error(BDD_RANGE); double old = increasefactor; increasefactor = x; return old; }
public double setIncreaseFactor(double x) { return bdd_setincreasefactor(x); }
    public double setIncreaseFactor(double x) {        if (x < 0)            return bdd_error(BDD_RANGE);        double old = increasefactor;        increasefactor = x;        return old;    }