Каждый узел BDD, на который нет ссылки, подлежит удалению любой операцией Cudd.Если вы хотите убедиться, что все узлы, хранящиеся в вашем массиве, остаются действительными, вам нужно Cudd_Ref их сразу после того, как они возвращены CUDD.Следовательно, вам нужно исправить свой код следующим образом:
for(k=0;k<N;k++)
{
x[k] = Cudd_bddNewVar(gbm);
Cudd_Ref(x[k]);
nx[k] = Cudd_Not(x[k]);
Cudd_Ref(nx[k]);
y[k] = Cudd_bddNewVar(gbm);
Cudd_Ref(y[k]);
ny[k] = Cudd_Not(y[k]);
Cudd_Ref(yn[k]);
}
Перед отменой освобождения менеджера Cudd вам необходимо разыменовать узлы:
for(k=0;k<N;k++)
{
Cudd_RecursiveDeref(gbm,x[k]);
Cudd_RecursiveDeref(gbm,nx[k]);
Cudd_RecursiveDeref(gbm,y[k]);
Cudd_RecursiveDeref(gbm,ny[k]);
}
Обратите внимание, что тот факт, что ваш код работаетпри выделении большего количества переменных не видно, что ссылки не нужны.Возможно, вы просто не используете достаточно узлов для запуска сборщика мусора, и до этого проблема не обнаруживается.