As described in Section ,
loop synthesis in Absynth is reduced to solving PCPs. These PCPs
are currently
expressed in the quantifier-free fragment of non-linear real arithmetic
(QF_NRA). We used Absynth in conjunction with the SMT solvers Yices [1]} (version 2.6.1)
and Z3 [2]} (version 4.8.6) for solving the PCPs and
therefore synthesizing loops.
For instance, Figures REF -REF  and Example REF  are synthesized automatically using Absynth.
