write_btor: support $buf

[georgerennie]

This is treated the same as $pos, passing through transparently

[georgerennie]

One thing to consider is whether $buf should actually be passed through transparently, or whether it should result in separate nodes maintaining the structural connection ordering that $buf gives (similar to the benefit of bufnorm -chain).

I think its probably not too important given btor solvers are treated as blackboxes and I don't believe people expect to do structural analysis where this matters on the btor side of things. This is is consistent with the way btor witnesses work, encoding only inputs/initial state and expecting the caller to reconstruct other signals as required.