Following #1087 I believe the assume_literals function is incorrect: it should call Uf.find_r on all semantic values that appear in the literals.
Semantic values that appear in the literals given to assume are not guaranteed to be in normal form, even though they usually are: during CC(X) resolution I believe it is possible to generate a literal such as x = y then later pick a new representative for y or x. I have seen this happen with bit-vectors; presumably it can also happen with ADTs.
Following #1087 I believe the
assume_literalsfunction is incorrect: it should callUf.find_ron all semantic values that appear in the literals.Semantic values that appear in the literals given to
assumeare not guaranteed to be in normal form, even though they usually are: during CC(X) resolution I believe it is possible to generate a literal such asx = ythen later pick a new representative foryorx. I have seen this happen with bit-vectors; presumably it can also happen with ADTs.(Sorry, I missed it during review!)