- if (check_visited(new, visited, init->vars.varset) == 0){
- if (check_goal(new, g->bdd, init->vars.varset) == 0){
- lurd_t *lrd = tmp_state->lrd;
- state_t *new_state = NULL;
- new_state = (state_t*)malloc(sizeof(state_t));
- new_state->bdd = new;
- new_state->vars = init->vars;
- lrd = lappend(lrd, 'l');
- new_state->lrd = lrd;
- state_queue = enq(new_state, state_queue);
- visited = sylvan_or(new, visited);
- }
- else {
- lurd_t *lrd = tmp_state->lrd;
- state_t *new_state = NULL;
- new_state = (state_t*)malloc(sizeof(state_t));
- new_state->bdd = new;
- new_state->vars = init->vars;
- lrd = lappend(lrd, 'l');
- new_state->lrd = lrd;
- return new_state;
+ if (new != sylvan_false && new != tmp_state->bdd){
+ if (check_visited(new, visited, init->vars.varset) == 0){
+ if (check_goal(new, g->bdd, init->vars.varset) == 0){
+ lurd_t *lrd = (lurd_t *)malloc(sizeof(lurd_t));
+ lrd = tmp_state->lrd;
+ state_t *new_state = (state_t *)malloc(sizeof(state_t));
+ new_state->bdd = new;
+ new_state->vars = init->vars;
+ lrd = lappend(lrd, 'l');
+ new_state->lrd = lrd;
+ state_queue = enq(new_state, state_queue);
+ visited = sylvan_or(new, visited);
+ }
+ else {
+ printf("GOAL\n");
+ lurd_t *lrd = tmp_state->lrd;
+ state_t *new_state = NULL;
+ new_state = (state_t*)malloc(sizeof(state_t));
+ new_state->bdd = new;
+ new_state->vars = init->vars;
+ lrd = lappend(lrd, 'l');
+ new_state->lrd = lrd;
+ return new_state;
+ }