Suppose a function A is failing to verify, and it has a callee B.
A new backtracking strategy proposed by @vikramnitin9 is only going back and backtracking if an LLM provides a different specification for B, assuming that specification in verifying A, and seeing whether it verifies or not.
Suppose a function
Ais failing to verify, and it has a calleeB.A new backtracking strategy proposed by @vikramnitin9 is only going back and backtracking if an LLM provides a different specification for
B, assuming that specification in verifyingA, and seeing whether it verifies or not.