To the best of our knowledge, existing synthesis approaches are restricted to linear
invariants, see e.g. [1]}, whereas our work supports
loop synthesis from non-linear polynomial properties. We note that many
interesting program
properties can be best expressed using non-linear arithmetic, for
example programs implementing powers (see
e.g. Figure REF ), square roots and/or Euclidean
divison require non-linear invariants.
