Our approach to synthesis is however
conceptually different from other SyGuS-based methods, such
as [1]}, [2]}, [3]}: rather than iteratively
refining both the input and the solution space of synthesized programs, we take
polynomial relations describing a potentially infinite set of input values and
precisely capture not just one loop, but the set of all loops (i) whose invariant is given by
our input polynomial and (ii) whose variables induce C-finite number
sequences.
Any instance of this set therefore yields a loop that is
partially correct by construction and only implements affine computations. Figures REF -REF  depict two solutions of our loop synthesis task for the
invariant \({c=n^3 \wedge k=3n^2+3n+1 \wedge m=6n+6}\) .
