Current C to gates synthesis tools do not support programs that make non-trivial use of dynamically-allocated heap (e.g. linked-list C programs that call malloc and free). The problem is that its difficult to determine an a priori bound on the amount of heap used during the program’s execution, if a bound even exists. In this paper we develop a new method of synthesizing symbolic bounds expressed over generic parameters, thus leading to a C to gates synthesis fow for programs using dynamic allocation and deallocation.