let backtrack_incomplete (state: state) (retract: choice_point) : unit =
  if
    State.choice_point_equal (State.root_choice_point state) retract
    ||
    State.choice_point_equal State.valid_choice_point retract
  then begin
    raise UNSATISFIABLE
  end;
  invalidate state retract;

  (* remove invalidated context literals. *)
  State.backtrack_literal_info state