[dnautics]

> For example if after one branch you don't converge, but after two you do, do you accept that?

you should refactor so that it's representable.

> Add dynamically sized values (e.g. arrays) and loops/recursion and now you also need to simulate a possibly unbounded number of iterations.

regions are hard. You kinda have to reject regions that are not uniform. loops you can find a fixpoint for.