In Figure REF , we show a few illustrative examples used in our experiments from
Table REF , using the Absynth input language. As mentioned in
Section REF , we considered
loops annotated with their invariants from the invariant generation
literature [1]}, [2]}.
For each
example in Figures REF -REF , we first
list such a loop (Original loop).
We then give the first loop synthesized by our
work (Absynth loop) in
combination with Yices and Z3, respectivelyIn
Figure REF , Absynth with Yices failed
to synthesize a loop, as indicated in Table REF .. That is, the
synthesized loops of
Figures REF -REF  are generated
by Absynth from the loop invariants
of [1]}, [2]}.
Observe that in most cases Absynth work was able to derive the
loop as [1]}, [2]}.
<FIGURE>