1. A method comprising: modifying program code by inserting one or more dynamic annotations having unsolved variables; generating one or more constraints based on the one or more dynamic annotations using a verifier; solving the one or more generated constraints; and modifying the program code by inserting a dynamic annotation in place of an annotation containing an unsolved variable.