ASSUME Assume_Domains

ASSUME a2 a3

INVARIANT i1

INVARIANT i2 i3