sat-solver.c

        // Get a pointer to the literal that needs assignment, if one exists
        if ((lp = is_unitclause(form->clauses[i], assigned, vals)) != NULL) {
            // COPY THE LITERAL POINTER
            lp1 = (literal*) malloc(sizeof(literal));
            memcpy(lp1, lp, sizeof(literal));

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

            // COPY THE STACK ITEM
            sip = (stack_item*) malloc(sizeof(stack_item));
            memcpy(sip, &si, sizeof(stack_item));

            push_stack(&s, sip);
        }
        
        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++;
        }