Open georgerennie opened 2 weeks ago
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.
This is treated the same as
$pos
, passing through transparently