Most synthesis approaches
exploit counterexample-guided
synthesis [1]}, [2]}, [3]}, [4]} within the
SyGuS framework. These
methods take
input-output examples satisfying a given property and synthesise a
candidate program
that is consistent with the given inputs. Correctness
of the candidate program with respect to the given property is then
checked using formal verification, in particular using SMT-based
reasoning. Whenever verification fails, a counterexample violating the
given property is generated
as an additional input and a new candidate program is generated. Our
work does not use an iterative refinement of the input-output
values satisfying a given property \(p(x)=0\) . Rather, we consider a
precise
characterisation of
the solution space of loops with invariant
\(p(x)=0\)  to describe
all, potentially infinite input-output values of interest.
Similarly to sketches [2]}, [4]}, we consider loop templates restricting the
search for solutions to synthesis. Yet, our templates support non-linear
arithmetic, which is not yet the case
in [4]}, [3]}.
