sat-solver-failing.c

        // Get a pointer to the literal that needs assignment, if one exists
        if ((lp = is_unitclause(form->clauses[i], assigned, vals)) != NULL) 
        {

            assert_literal(lp, vals, assigned);
            stack_item si = {lp, i, 0};

            push_stack(&s, &si);
        }
        
        void push_stack(stack *sp, stack_item *item)
        {
            if (DEBUG)
                printf("push (ID) %d (S) %d (G) %d (CI) %d\n", item->lp->id, item->lp->sign, item->guess, item->ci);
            sp->top++;
            sp->items[sp->top] = item;
            sp->size++;
        }