Avatar-to-proverif generates an unvalid proverif specification because invalid guards for proverif are not detected
For instance, (a==b) != false generates a faulty proverif specification
For instance, (a==b) != false generates a faulty proverif specification