Well, I have did the same:
if (is_dot_node(line)): node_id = str_between(line, 'Node', ' [shape=record') label = get_label(line) label = (label.replace('\\"', '"').replace('\\\\', '\\') ...
I believe this is the correct behavior. What I have pointed out is the opposite: when we have a unicode character we have to escape it, so it would be that \\\\ case. Rewrite that to '\\' is cool and safe.
You *have to* remove backslashes, because sometimes we have \\\\ so two of them packed together. Then when you remove it, it will be only one (\\ ), which is handled by JSON properly. Sadly it is very strict and cannot predict two should not be a problem.