Once the analysis is complete, it should be possible to print an overview of the state transitions in the abstract analysis. This will allow a meta-interpreter which implements the selection rule to keep track of where it is with respect to the abstract analysis, so that it can shift certain conjuncts to a multi abstraction. That, in turn, should allow a meta-interpreter specialization which is identical to the synthesized program.
Once the analysis is complete, it should be possible to print an overview of the state transitions in the abstract analysis. This will allow a meta-interpreter which implements the selection rule to keep track of where it is with respect to the abstract analysis, so that it can shift certain conjuncts to a multi abstraction. That, in turn, should allow a meta-interpreter specialization which is identical to the synthesized program.