Format of Preconditions #8
Description
Hi! Thanks for this amazing project!
The original paper mentions using BabyAdd as a precondition to improve verification scalability. How can I specify this in the implementation? I also want to do the something for IsZero and Num2Bits.