  We describe an integration of program synthesis into Uclid5, a formal
modelling and verification tool. To the best of our knowledge, the new version
of Uclid5 is the only tool that supports program synthesis with bounded model
checking, k-induction, sequential program verification, and hyperproperty
verification. We use the integration to generate 25 program synthesis
benchmarks with simple, known solutions that are out of reach of current
synthesis engines, and we release the benchmarks to the community.
