Program synthesis with Z3

A deep dive into using Z3, Microsoft Research's automated theorem prover, to synthesize programs for an Advent of Code puzzle involving a jumping robot. The robot must be programmed in a fictional language called SpringScript (up to 15 boolean instructions). Rather than solving manually, the author symbolically executes the program with Z3 by treating all 105 bits of the program as unknown BitVec variables, then asserts correctness constraints based on the map. Z3 finds a valid program automatically. The post also covers minimizing instruction count, handling multiple maps, and generating adversarial maps that require the maximum number of instructions using existential quantifiers.