def get_shift_bit(char, var):
  """Returns the var argument if char is '1', otherwise (bvnot var).

  Args:
    char: A string, either '0' or '1'
    var: A string, representing a variable we've defined in the smt2 file.

  Returns:
    The value or its inversion.
  """
  if char == "0":
    return f"(bvnot {var})"
  elif char == "1":
    return var
  else:
    raise ValueError("Bit string contained value that wasn't 0 or 1")