def parse_smt_command(command):
    """Breaks the given SMT command "(CMD ARG ARG ARG)" into tuple (CMD, [ARG]),
    where ARG again can be a (non-parsed) command"""
    command = command.strip()
    if command[0] != '(':
        return command, []
    command = command[1:-1].split(maxsplit=1)
    if len(command) == 1:
        return command[0], []
    command, arguments = command
    args = ['']
    paren = 0
    while len(arguments) > 0:
        c = arguments[0]
        arguments = arguments[1:]
        if c == '(':
            paren += 1
        elif c == ')':
            paren -= 1
            if paren < 0:
                raise RuntimeError('Unmatched closing brace in SMT output')
        elif c == ' ':
            if paren == 0:
                arguments = arguments.strip()
                args.append('')
                continue
        args[-1] += c
    if not args[-1]:
        args = args[:-1]
    return command, args
