1. A method comprising: modifying program code by inserting one or more dynamic annotations having unsolved variables, the unsolved variables being in the form of arguments of the dynamic annotations; generating one or more constraints on the unsolved variables based on the one or more dynamic annotations using a verifier, the generated constraints relating the unsolved variables to program variables; statically solving the one or more generated constraints in terms of variables of the program code to determine values for the unsolved variables; and modifying the program code by inserting a dynamic annotation with a determined variable value in place of an annotation of the one or more annotations having unsolved variables, the dynamic annotation having a dynamic call executable during run time.