anchor.diff:           (concrete-actions (or concrete-actions
                                  (smt-concrete-actions (operators-actions operators)
                                                         (facts-objects facts))))
  -         (initial-true (or initial-true (facts-init facts)))
  -         (initial-false (or initial-false
  -                            (set-difference  state-vars initial-true :test #'equal)))
  +         (initial-true (unless initial-state (or initial-true (facts-init facts))))
  +         (initial-false (unless initial-state (or initial-false
  +                                                  (set-difference  state-vars initial-true :test #'equal))))
  +         (initial-state (or initial-state
  +                            `(and ,@initial-true
  +                                  ,@(loop for v in initial-false collect `(not ,v)))))
  +
            (goal (or goal (facts-goal facts))))
       (labels ((rec (steps)
                  (multiple-value-bind (assignments is-sat)
                      (multiple-value-bind (stmts vars)
                          (smt-plan-encode state-vars concrete-actions
  -                                        initial-true initial-false
  +                                        initial-state
                                           goal
                                           steps)
                        (smt-run stmts vars))
  
positive.code: 
  
  (defun plan-automaton (&key operators facts)
    (let* ((operators (load-operators operators))
           (facts (load-facts facts))
           (smt-statements nil)
           (state-vars (create-state-variables (operators-predicates operators)
                                                (facts-objects facts)))
           (controllable-actions (loop for a in (operators-actions operators)
  
negative.code:     (dolist (var false-bits)
        (setf (aref bits (state-vars-index state-vars var))
              0))
      (make-concrete-state :bits bits
                           :exp `(and ,@true-bits
                                      ,@(loop for var in false-bits
                                           collect `(not ,var))))))
  
  (defun concrete-state-translate-exp (exp state-vars)
    "Return a lambda expression that evaluates `EXP'."
  