anchor.diff:                                       (1+ i))))
         ;; check-sat
         (smt-plan-check cx :max-steps max-steps))))
  +
  +(defun smt-plan-other (cx &key (max-steps 10))
  +  "Try to find an alternate plan, recursively."
  +  (let ((values (smt-plan-result cx)))
  +    ;; Invalidate the current plan
  +    ;; TODO: maybe we just need the true actions?
  +    (let ((exp (smt-not (apply #'smt-and
  +                               (loop for (variable truth) in values
  +                                  collect (ecase truth
  +                                            ((true |true|)
  +                                             variable)
  +                                            ((false |false|)
  +                                             (smt-not variable))))))))
  +      (smt-eval (smt-plan-context-smt cx)
  +                (smt-assert exp)))
  +    ;; Get another plan
  +    (smt-plan-check cx :max-steps max-steps)))
  +
  +(defun smt-plan-next (cx &key (max-steps 10))
  +  "Find the next valid plan."
  +  (if (smt-plan-context-values cx)
  +      (smt-plan-other cx :max-steps max-steps)
  +      (smt-plan-step cx :max-steps max-steps)))
   
   (defun smt-plan-result (cx)
     "Retrive action variable assignments from SMT solver."
  
positive.code:                              :goal goal
                               :step 0))))
  
  (defun smt-plan-other (cx &key (max-steps 10))
    "Try to find an alternate plan, recursively."
    (let ((values (smt-plan-result cx)))
      ;; Invalidate the current plan
      ;; TODO: maybe we just need the true actions?
      (let ((exp (smt-not (apply #'smt-and
                                 (loop for (variable truth) in values
                                    collect (ecase truth
                                              ((true |true|)
                                               variable)
                                              ((false |false|)
                                               (smt-not variable))))))))
        (smt-eval (smt-plan-context-smt cx)
                  (smt-assert exp)))
      ;; Get another plan
      (smt-plan-check cx :max-steps max-steps)))
  
  
  (defun smt-plan ( &key
  
negative.code:   ground-actions
    goal
    step
    values
    )
  
  (defun smt-plan-check (cx &key max-steps)
  