diff --git a/libyul/backends/evm/ssa/StackShuffler.h b/libyul/backends/evm/ssa/StackShuffler.h index e8028db1afbd..70c381a899dc 100644 --- a/libyul/backends/evm/ssa/StackShuffler.h +++ b/libyul/backends/evm/ssa/StackShuffler.h @@ -792,7 +792,7 @@ class StackShuffler static std::optional allNecessarySlotsReachableOrFinal(Stack const& _stack, detail::State const& _state) { // check that args are either in position or reachable - for (StackOffset const offset: _state.stackArgsRange()) + for (StackOffset offset{_state.target().tailSize}; offset < _state.target().size; ++offset.value) { if (_state.isArgsCompatible(offset, offset)) continue; diff --git a/test/libyul/ssa/stackShuffler/dup_value_into_args_with_grow_1.stack b/test/libyul/ssa/stackShuffler/dup_value_into_args_with_grow_1.stack index 5bbaeb2b4e2d..0b81b635f176 100644 --- a/test/libyul/ssa/stackShuffler/dup_value_into_args_with_grow_1.stack +++ b/test/libyul/ssa/stackShuffler/dup_value_into_args_with_grow_1.stack @@ -11,30 +11,13 @@ targetStackTop: [v2, JUNK, JUNK, JUNK, JUNK, JUNK, JUNK, JUNK, JUNK, JUNK, phi1, // DUP2| v3 * * * * * * * * * phi1 * v1 v2 lit2 v2 // PUSH lit1| v3 * * * * * * * * * phi1 * v1 v2 lit2 v2 lit1 // DUP2| v3 * * * * * * * * * phi1 * v1 v2 lit2 v2 lit1 v2 -// DUP2| v3 * * * * * * * * * phi1 * v1 v2 lit2 v2 lit1 v2 lit1 -// SWAP6| v3 * * * * * * * * * phi1 * lit1 v2 lit2 v2 lit1 v2 v1 -// SWAP1| v3 * * * * * * * * * phi1 * lit1 v2 lit2 v2 lit1 v1 v2 -// SWAP2| v3 * * * * * * * * * phi1 * lit1 v2 lit2 v2 v2 v1 lit1 -// POP| v3 * * * * * * * * * phi1 * lit1 v2 lit2 v2 v2 v1 -// DUP6| v3 * * * * * * * * * phi1 * lit1 v2 lit2 v2 v2 v1 lit1 -// SWAP2| v3 * * * * * * * * * phi1 * lit1 v2 lit2 v2 lit1 v1 v2 -// SWAP2| v3 * * * * * * * * * phi1 * lit1 v2 lit2 v2 v2 v1 lit1 -// POP| v3 * * * * * * * * * phi1 * lit1 v2 lit2 v2 v2 v1 -// DUP6| v3 * * * * * * * * * phi1 * lit1 v2 lit2 v2 v2 v1 lit1 -// SWAP2| v3 * * * * * * * * * phi1 * lit1 v2 lit2 v2 lit1 v1 v2 -// SWAP2| v3 * * * * * * * * * phi1 * lit1 v2 lit2 v2 v2 v1 lit1 -// POP| v3 * * * * * * * * * phi1 * lit1 v2 lit2 v2 v2 v1 -// DUP6| v3 * * * * * * * * * phi1 * lit1 v2 lit2 v2 v2 v1 lit1 -// SWAP2| v3 * * * * * * * * * phi1 * lit1 v2 lit2 v2 lit1 v1 v2 -// SWAP2| v3 * * * * * * * * * phi1 * lit1 v2 lit2 v2 v2 v1 lit1 -// POP| v3 * * * * * * * * * phi1 * lit1 v2 lit2 v2 v2 v1 -// DUP6| v3 * * * * * * * * * phi1 * lit1 v2 lit2 v2 v2 v1 lit1 -// SWAP2| v3 * * * * * * * * * phi1 * lit1 v2 lit2 v2 lit1 v1 v2 -// SWAP2| v3 * * * * * * * * * phi1 * lit1 v2 lit2 v2 v2 v1 lit1 -// POP| v3 * * * * * * * * * phi1 * lit1 v2 lit2 v2 v2 v1 -// DUP6| v3 * * * * * * * * * phi1 * lit1 v2 lit2 v2 v2 v1 lit1 -// SWAP2| v3 * * * * * * * * * phi1 * lit1 v2 lit2 v2 lit1 v1 v2 -// ...| +// SWAP1| v3 * * * * * * * * * phi1 * v1 v2 lit2 v2 v2 lit1 +// POP| v3 * * * * * * * * * phi1 * v1 v2 lit2 v2 v2 +// SWAP16| v2 * * * * * * * * * phi1 * v1 v2 lit2 v2 v3 +// PUSH lit1| v2 * * * * * * * * * phi1 * v1 v2 lit2 v2 v3 lit1 +// SWAP5| v2 * * * * * * * * * phi1 * lit1 v2 lit2 v2 v3 v1 +// DUP6| v2 * * * * * * * * * phi1 * lit1 v2 lit2 v2 v3 v1 lit1 +// SWAP2| v2 * * * * * * * * * phi1 * lit1 v2 lit2 v2 lit1 v1 v3 // +------------------------------------------------------------------------------------------------------------------------------------- // (target)| v2 * * * * * * * * * phi1 * lit1 v2 lit2 v2 lit1 v1 v3 -// Status: MaxIterationsReached +// Status: Admissible diff --git a/test/libyul/ssa/stackShuffler/dup_value_into_tail_and_args.stack b/test/libyul/ssa/stackShuffler/dup_value_into_tail_and_args.stack index 06d2df40340b..287ba86cf2a2 100644 --- a/test/libyul/ssa/stackShuffler/dup_value_into_tail_and_args.stack +++ b/test/libyul/ssa/stackShuffler/dup_value_into_tail_and_args.stack @@ -11,30 +11,13 @@ targetStackTop: [JUNK, JUNK, v2, JUNK, JUNK, JUNK, JUNK, JUNK, JUNK, JUNK, JUNK, // DUP2| * * v3 * * * * * * * * * * * v1 v2 lit2 v2 // PUSH lit3| * * v3 * * * * * * * * * * * v1 v2 lit2 v2 lit3 // DUP2| * * v3 * * * * * * * * * * * v1 v2 lit2 v2 lit3 v2 -// PUSH lit1| * * v3 * * * * * * * * * * * v1 v2 lit2 v2 lit3 v2 lit1 -// SWAP6| * * v3 * * * * * * * * * * * lit1 v2 lit2 v2 lit3 v2 v1 -// SWAP1| * * v3 * * * * * * * * * * * lit1 v2 lit2 v2 lit3 v1 v2 -// SWAP2| * * v3 * * * * * * * * * * * lit1 v2 lit2 v2 v2 v1 lit3 -// POP| * * v3 * * * * * * * * * * * lit1 v2 lit2 v2 v2 v1 -// PUSH lit3| * * v3 * * * * * * * * * * * lit1 v2 lit2 v2 v2 v1 lit3 -// SWAP2| * * v3 * * * * * * * * * * * lit1 v2 lit2 v2 lit3 v1 v2 -// SWAP2| * * v3 * * * * * * * * * * * lit1 v2 lit2 v2 v2 v1 lit3 -// POP| * * v3 * * * * * * * * * * * lit1 v2 lit2 v2 v2 v1 -// PUSH lit3| * * v3 * * * * * * * * * * * lit1 v2 lit2 v2 v2 v1 lit3 -// SWAP2| * * v3 * * * * * * * * * * * lit1 v2 lit2 v2 lit3 v1 v2 -// SWAP2| * * v3 * * * * * * * * * * * lit1 v2 lit2 v2 v2 v1 lit3 -// POP| * * v3 * * * * * * * * * * * lit1 v2 lit2 v2 v2 v1 -// PUSH lit3| * * v3 * * * * * * * * * * * lit1 v2 lit2 v2 v2 v1 lit3 -// SWAP2| * * v3 * * * * * * * * * * * lit1 v2 lit2 v2 lit3 v1 v2 -// SWAP2| * * v3 * * * * * * * * * * * lit1 v2 lit2 v2 v2 v1 lit3 -// POP| * * v3 * * * * * * * * * * * lit1 v2 lit2 v2 v2 v1 -// PUSH lit3| * * v3 * * * * * * * * * * * lit1 v2 lit2 v2 v2 v1 lit3 -// SWAP2| * * v3 * * * * * * * * * * * lit1 v2 lit2 v2 lit3 v1 v2 -// SWAP2| * * v3 * * * * * * * * * * * lit1 v2 lit2 v2 v2 v1 lit3 -// POP| * * v3 * * * * * * * * * * * lit1 v2 lit2 v2 v2 v1 -// PUSH lit3| * * v3 * * * * * * * * * * * lit1 v2 lit2 v2 v2 v1 lit3 -// SWAP2| * * v3 * * * * * * * * * * * lit1 v2 lit2 v2 lit3 v1 v2 -// ...| +// SWAP1| * * v3 * * * * * * * * * * * v1 v2 lit2 v2 v2 lit3 +// POP| * * v3 * * * * * * * * * * * v1 v2 lit2 v2 v2 +// SWAP16| * * v2 * * * * * * * * * * * v1 v2 lit2 v2 v3 +// PUSH lit1| * * v2 * * * * * * * * * * * v1 v2 lit2 v2 v3 lit1 +// SWAP5| * * v2 * * * * * * * * * * * lit1 v2 lit2 v2 v3 v1 +// PUSH lit3| * * v2 * * * * * * * * * * * lit1 v2 lit2 v2 v3 v1 lit3 +// SWAP2| * * v2 * * * * * * * * * * * lit1 v2 lit2 v2 lit3 v1 v3 // +--------------------------------------------------------------------------------------------------------------------------------------------------- // (target)| * * v2 * * * * * * * * * * * lit1 v2 lit2 v2 lit3 v1 v3 -// Status: MaxIterationsReached +// Status: Admissible diff --git a/test/libyul/ssa/stackShuffler/multi_dup_with_phi_in_tail.stack b/test/libyul/ssa/stackShuffler/multi_dup_with_phi_in_tail.stack index a72977f3bde0..aa563e6f9f2b 100644 --- a/test/libyul/ssa/stackShuffler/multi_dup_with_phi_in_tail.stack +++ b/test/libyul/ssa/stackShuffler/multi_dup_with_phi_in_tail.stack @@ -11,30 +11,13 @@ targetStackTop: [JUNK, v5, JUNK, v1, v2, JUNK, JUNK, JUNK, JUNK, phi1, JUNK, v3, // DUP2| * v6 * v1 v2 * * * * phi1 * v3 phi2 v4 v5 lit2 v5 // PUSH lit3| * v6 * v1 v2 * * * * phi1 * v3 phi2 v4 v5 lit2 v5 lit3 // DUP2| * v6 * v1 v2 * * * * phi1 * v3 phi2 v4 v5 lit2 v5 lit3 v5 -// PUSH lit1| * v6 * v1 v2 * * * * phi1 * v3 phi2 v4 v5 lit2 v5 lit3 v5 lit1 -// SWAP6| * v6 * v1 v2 * * * * phi1 * v3 phi2 lit1 v5 lit2 v5 lit3 v5 v4 -// SWAP1| * v6 * v1 v2 * * * * phi1 * v3 phi2 lit1 v5 lit2 v5 lit3 v4 v5 -// SWAP2| * v6 * v1 v2 * * * * phi1 * v3 phi2 lit1 v5 lit2 v5 v5 v4 lit3 -// POP| * v6 * v1 v2 * * * * phi1 * v3 phi2 lit1 v5 lit2 v5 v5 v4 -// PUSH lit3| * v6 * v1 v2 * * * * phi1 * v3 phi2 lit1 v5 lit2 v5 v5 v4 lit3 -// SWAP2| * v6 * v1 v2 * * * * phi1 * v3 phi2 lit1 v5 lit2 v5 lit3 v4 v5 -// SWAP2| * v6 * v1 v2 * * * * phi1 * v3 phi2 lit1 v5 lit2 v5 v5 v4 lit3 -// POP| * v6 * v1 v2 * * * * phi1 * v3 phi2 lit1 v5 lit2 v5 v5 v4 -// PUSH lit3| * v6 * v1 v2 * * * * phi1 * v3 phi2 lit1 v5 lit2 v5 v5 v4 lit3 -// SWAP2| * v6 * v1 v2 * * * * phi1 * v3 phi2 lit1 v5 lit2 v5 lit3 v4 v5 -// SWAP2| * v6 * v1 v2 * * * * phi1 * v3 phi2 lit1 v5 lit2 v5 v5 v4 lit3 -// POP| * v6 * v1 v2 * * * * phi1 * v3 phi2 lit1 v5 lit2 v5 v5 v4 -// PUSH lit3| * v6 * v1 v2 * * * * phi1 * v3 phi2 lit1 v5 lit2 v5 v5 v4 lit3 -// SWAP2| * v6 * v1 v2 * * * * phi1 * v3 phi2 lit1 v5 lit2 v5 lit3 v4 v5 -// SWAP2| * v6 * v1 v2 * * * * phi1 * v3 phi2 lit1 v5 lit2 v5 v5 v4 lit3 -// POP| * v6 * v1 v2 * * * * phi1 * v3 phi2 lit1 v5 lit2 v5 v5 v4 -// PUSH lit3| * v6 * v1 v2 * * * * phi1 * v3 phi2 lit1 v5 lit2 v5 v5 v4 lit3 -// SWAP2| * v6 * v1 v2 * * * * phi1 * v3 phi2 lit1 v5 lit2 v5 lit3 v4 v5 -// SWAP2| * v6 * v1 v2 * * * * phi1 * v3 phi2 lit1 v5 lit2 v5 v5 v4 lit3 -// POP| * v6 * v1 v2 * * * * phi1 * v3 phi2 lit1 v5 lit2 v5 v5 v4 -// PUSH lit3| * v6 * v1 v2 * * * * phi1 * v3 phi2 lit1 v5 lit2 v5 v5 v4 lit3 -// SWAP2| * v6 * v1 v2 * * * * phi1 * v3 phi2 lit1 v5 lit2 v5 lit3 v4 v5 -// ...| +// SWAP1| * v6 * v1 v2 * * * * phi1 * v3 phi2 v4 v5 lit2 v5 v5 lit3 +// POP| * v6 * v1 v2 * * * * phi1 * v3 phi2 v4 v5 lit2 v5 v5 +// SWAP16| * v5 * v1 v2 * * * * phi1 * v3 phi2 v4 v5 lit2 v5 v6 +// PUSH lit1| * v5 * v1 v2 * * * * phi1 * v3 phi2 v4 v5 lit2 v5 v6 lit1 +// SWAP5| * v5 * v1 v2 * * * * phi1 * v3 phi2 lit1 v5 lit2 v5 v6 v4 +// PUSH lit3| * v5 * v1 v2 * * * * phi1 * v3 phi2 lit1 v5 lit2 v5 v6 v4 lit3 +// SWAP2| * v5 * v1 v2 * * * * phi1 * v3 phi2 lit1 v5 lit2 v5 lit3 v4 v6 // +-------------------------------------------------------------------------------------------------------------------------------------------- // (target)| * v5 * v1 v2 * * * * phi1 * v3 phi2 lit1 v5 lit2 v5 lit3 v4 v6 -// Status: MaxIterationsReached +// Status: Admissible diff --git a/test/libyul/ssa/stackShuffler/return_label_with_dup_and_grow.stack b/test/libyul/ssa/stackShuffler/return_label_with_dup_and_grow.stack index 7c22e8f52dc3..571ed4a24269 100644 --- a/test/libyul/ssa/stackShuffler/return_label_with_dup_and_grow.stack +++ b/test/libyul/ssa/stackShuffler/return_label_with_dup_and_grow.stack @@ -22,19 +22,13 @@ targetStackTop: [ReturnLabel[1], JUNK, JUNK, v2, JUNK, JUNK, JUNK, JUNK, JUNK, J // DUP2| ReturnLabel[1] * * v3 * * * * * * * * * * * v1 v2 lit2 v2 // PUSH lit1| ReturnLabel[1] * * v3 * * * * * * * * * * * v1 v2 lit2 v2 lit1 // DUP2| ReturnLabel[1] * * v3 * * * * * * * * * * * v1 v2 lit2 v2 lit1 v2 -// DUP2| ReturnLabel[1] * * v3 * * * * * * * * * * * v1 v2 lit2 v2 lit1 v2 lit1 -// SWAP6| ReturnLabel[1] * * v3 * * * * * * * * * * * lit1 v2 lit2 v2 lit1 v2 v1 -// SWAP1| ReturnLabel[1] * * v3 * * * * * * * * * * * lit1 v2 lit2 v2 lit1 v1 v2 -// SWAP2| ReturnLabel[1] * * v3 * * * * * * * * * * * lit1 v2 lit2 v2 v2 v1 lit1 -// POP| ReturnLabel[1] * * v3 * * * * * * * * * * * lit1 v2 lit2 v2 v2 v1 -// DUP6| ReturnLabel[1] * * v3 * * * * * * * * * * * lit1 v2 lit2 v2 v2 v1 lit1 -// SWAP2| ReturnLabel[1] * * v3 * * * * * * * * * * * lit1 v2 lit2 v2 lit1 v1 v2 -// SWAP2| ReturnLabel[1] * * v3 * * * * * * * * * * * lit1 v2 lit2 v2 v2 v1 lit1 -// POP| ReturnLabel[1] * * v3 * * * * * * * * * * * lit1 v2 lit2 v2 v2 v1 -// DUP6| ReturnLabel[1] * * v3 * * * * * * * * * * * lit1 v2 lit2 v2 v2 v1 lit1 -// SWAP2| ReturnLabel[1] * * v3 * * * * * * * * * * * lit1 v2 lit2 v2 lit1 v1 v2 -// SWAP2| ReturnLabel[1] * * v3 * * * * * * * * * * * lit1 v2 lit2 v2 v2 v1 lit1 -// ...| +// SWAP1| ReturnLabel[1] * * v3 * * * * * * * * * * * v1 v2 lit2 v2 v2 lit1 +// POP| ReturnLabel[1] * * v3 * * * * * * * * * * * v1 v2 lit2 v2 v2 +// SWAP16| ReturnLabel[1] * * v2 * * * * * * * * * * * v1 v2 lit2 v2 v3 +// PUSH lit1| ReturnLabel[1] * * v2 * * * * * * * * * * * v1 v2 lit2 v2 v3 lit1 +// SWAP5| ReturnLabel[1] * * v2 * * * * * * * * * * * lit1 v2 lit2 v2 v3 v1 +// DUP6| ReturnLabel[1] * * v2 * * * * * * * * * * * lit1 v2 lit2 v2 v3 v1 lit1 +// SWAP2| ReturnLabel[1] * * v2 * * * * * * * * * * * lit1 v2 lit2 v2 lit1 v1 v3 // +------------------------------------------------------------------------------------------------------------------------------------------------------------------ +------- // (target)| ReturnLabel[1] * * v2 * * * * * * * * * * * lit1 v2 lit2 v2 lit1 v1 v3 | -// Status: MaxIterationsReached +// Status: Admissible diff --git a/test/libyul/ssa/stackShuffler/triple_dup_no_phi.stack b/test/libyul/ssa/stackShuffler/triple_dup_no_phi.stack index 438ab16fbddb..845095016f9d 100644 --- a/test/libyul/ssa/stackShuffler/triple_dup_no_phi.stack +++ b/test/libyul/ssa/stackShuffler/triple_dup_no_phi.stack @@ -11,30 +11,13 @@ targetStackTop: [JUNK, v2, JUNK, JUNK, JUNK, JUNK, JUNK, JUNK, JUNK, JUNK, JUNK, // DUP2| * v3 * * * * * * * * * * * v1 v2 lit2 v2 // PUSH lit3| * v3 * * * * * * * * * * * v1 v2 lit2 v2 lit3 // DUP2| * v3 * * * * * * * * * * * v1 v2 lit2 v2 lit3 v2 -// PUSH lit1| * v3 * * * * * * * * * * * v1 v2 lit2 v2 lit3 v2 lit1 -// SWAP6| * v3 * * * * * * * * * * * lit1 v2 lit2 v2 lit3 v2 v1 -// SWAP1| * v3 * * * * * * * * * * * lit1 v2 lit2 v2 lit3 v1 v2 -// SWAP2| * v3 * * * * * * * * * * * lit1 v2 lit2 v2 v2 v1 lit3 -// POP| * v3 * * * * * * * * * * * lit1 v2 lit2 v2 v2 v1 -// PUSH lit3| * v3 * * * * * * * * * * * lit1 v2 lit2 v2 v2 v1 lit3 -// SWAP2| * v3 * * * * * * * * * * * lit1 v2 lit2 v2 lit3 v1 v2 -// SWAP2| * v3 * * * * * * * * * * * lit1 v2 lit2 v2 v2 v1 lit3 -// POP| * v3 * * * * * * * * * * * lit1 v2 lit2 v2 v2 v1 -// PUSH lit3| * v3 * * * * * * * * * * * lit1 v2 lit2 v2 v2 v1 lit3 -// SWAP2| * v3 * * * * * * * * * * * lit1 v2 lit2 v2 lit3 v1 v2 -// SWAP2| * v3 * * * * * * * * * * * lit1 v2 lit2 v2 v2 v1 lit3 -// POP| * v3 * * * * * * * * * * * lit1 v2 lit2 v2 v2 v1 -// PUSH lit3| * v3 * * * * * * * * * * * lit1 v2 lit2 v2 v2 v1 lit3 -// SWAP2| * v3 * * * * * * * * * * * lit1 v2 lit2 v2 lit3 v1 v2 -// SWAP2| * v3 * * * * * * * * * * * lit1 v2 lit2 v2 v2 v1 lit3 -// POP| * v3 * * * * * * * * * * * lit1 v2 lit2 v2 v2 v1 -// PUSH lit3| * v3 * * * * * * * * * * * lit1 v2 lit2 v2 v2 v1 lit3 -// SWAP2| * v3 * * * * * * * * * * * lit1 v2 lit2 v2 lit3 v1 v2 -// SWAP2| * v3 * * * * * * * * * * * lit1 v2 lit2 v2 v2 v1 lit3 -// POP| * v3 * * * * * * * * * * * lit1 v2 lit2 v2 v2 v1 -// PUSH lit3| * v3 * * * * * * * * * * * lit1 v2 lit2 v2 v2 v1 lit3 -// SWAP2| * v3 * * * * * * * * * * * lit1 v2 lit2 v2 lit3 v1 v2 -// ...| +// SWAP1| * v3 * * * * * * * * * * * v1 v2 lit2 v2 v2 lit3 +// POP| * v3 * * * * * * * * * * * v1 v2 lit2 v2 v2 +// SWAP16| * v2 * * * * * * * * * * * v1 v2 lit2 v2 v3 +// PUSH lit1| * v2 * * * * * * * * * * * v1 v2 lit2 v2 v3 lit1 +// SWAP5| * v2 * * * * * * * * * * * lit1 v2 lit2 v2 v3 v1 +// PUSH lit3| * v2 * * * * * * * * * * * lit1 v2 lit2 v2 v3 v1 lit3 +// SWAP2| * v2 * * * * * * * * * * * lit1 v2 lit2 v2 lit3 v1 v3 // +-------------------------------------------------------------------------------------------------------------------------------------------- // (target)| * v2 * * * * * * * * * * * lit1 v2 lit2 v2 lit3 v1 v3 -// Status: MaxIterationsReached +// Status: Admissible diff --git a/test/libyul/ssa/stackShuffler/triple_dup_with_phi.stack b/test/libyul/ssa/stackShuffler/triple_dup_with_phi.stack index 0d3e5f867e95..3d28212bd91f 100644 --- a/test/libyul/ssa/stackShuffler/triple_dup_with_phi.stack +++ b/test/libyul/ssa/stackShuffler/triple_dup_with_phi.stack @@ -11,30 +11,13 @@ targetStackTop: [JUNK, v2, JUNK, JUNK, JUNK, JUNK, JUNK, JUNK, phi1, JUNK, JUNK, // DUP2| * v3 * * * * * * phi1 * * * * v1 v2 lit2 v2 // PUSH lit3| * v3 * * * * * * phi1 * * * * v1 v2 lit2 v2 lit3 // DUP2| * v3 * * * * * * phi1 * * * * v1 v2 lit2 v2 lit3 v2 -// PUSH lit1| * v3 * * * * * * phi1 * * * * v1 v2 lit2 v2 lit3 v2 lit1 -// SWAP6| * v3 * * * * * * phi1 * * * * lit1 v2 lit2 v2 lit3 v2 v1 -// SWAP1| * v3 * * * * * * phi1 * * * * lit1 v2 lit2 v2 lit3 v1 v2 -// SWAP2| * v3 * * * * * * phi1 * * * * lit1 v2 lit2 v2 v2 v1 lit3 -// POP| * v3 * * * * * * phi1 * * * * lit1 v2 lit2 v2 v2 v1 -// PUSH lit3| * v3 * * * * * * phi1 * * * * lit1 v2 lit2 v2 v2 v1 lit3 -// SWAP2| * v3 * * * * * * phi1 * * * * lit1 v2 lit2 v2 lit3 v1 v2 -// SWAP2| * v3 * * * * * * phi1 * * * * lit1 v2 lit2 v2 v2 v1 lit3 -// POP| * v3 * * * * * * phi1 * * * * lit1 v2 lit2 v2 v2 v1 -// PUSH lit3| * v3 * * * * * * phi1 * * * * lit1 v2 lit2 v2 v2 v1 lit3 -// SWAP2| * v3 * * * * * * phi1 * * * * lit1 v2 lit2 v2 lit3 v1 v2 -// SWAP2| * v3 * * * * * * phi1 * * * * lit1 v2 lit2 v2 v2 v1 lit3 -// POP| * v3 * * * * * * phi1 * * * * lit1 v2 lit2 v2 v2 v1 -// PUSH lit3| * v3 * * * * * * phi1 * * * * lit1 v2 lit2 v2 v2 v1 lit3 -// SWAP2| * v3 * * * * * * phi1 * * * * lit1 v2 lit2 v2 lit3 v1 v2 -// SWAP2| * v3 * * * * * * phi1 * * * * lit1 v2 lit2 v2 v2 v1 lit3 -// POP| * v3 * * * * * * phi1 * * * * lit1 v2 lit2 v2 v2 v1 -// PUSH lit3| * v3 * * * * * * phi1 * * * * lit1 v2 lit2 v2 v2 v1 lit3 -// SWAP2| * v3 * * * * * * phi1 * * * * lit1 v2 lit2 v2 lit3 v1 v2 -// SWAP2| * v3 * * * * * * phi1 * * * * lit1 v2 lit2 v2 v2 v1 lit3 -// POP| * v3 * * * * * * phi1 * * * * lit1 v2 lit2 v2 v2 v1 -// PUSH lit3| * v3 * * * * * * phi1 * * * * lit1 v2 lit2 v2 v2 v1 lit3 -// SWAP2| * v3 * * * * * * phi1 * * * * lit1 v2 lit2 v2 lit3 v1 v2 -// ...| +// SWAP1| * v3 * * * * * * phi1 * * * * v1 v2 lit2 v2 v2 lit3 +// POP| * v3 * * * * * * phi1 * * * * v1 v2 lit2 v2 v2 +// SWAP16| * v2 * * * * * * phi1 * * * * v1 v2 lit2 v2 v3 +// PUSH lit1| * v2 * * * * * * phi1 * * * * v1 v2 lit2 v2 v3 lit1 +// SWAP5| * v2 * * * * * * phi1 * * * * lit1 v2 lit2 v2 v3 v1 +// PUSH lit3| * v2 * * * * * * phi1 * * * * lit1 v2 lit2 v2 v3 v1 lit3 +// SWAP2| * v2 * * * * * * phi1 * * * * lit1 v2 lit2 v2 lit3 v1 v3 // +-------------------------------------------------------------------------------------------------------------------------------------------- // (target)| * v2 * * * * * * phi1 * * * * lit1 v2 lit2 v2 lit3 v1 v3 -// Status: MaxIterationsReached +// Status: Admissible