LARA Circuit-Based Synthesis from Regular Specifications See the paper Synthesis for Unbounded Bitvector Arithmetic. Until this page is updated, please contact Andrej Spielmann. Related project: RegSy and Comfusy.