Equalities need to be transferred into inequalities, so A == B is modeled as A >= B && A <= B. A the moment, the logic to collect facts supports equalities by simplify adding A >= B and A <= B as facts.
You don’t need to handle all possible cases in the initial patch. As for 1. yes that’s true, but there’s a bunch of logic to transfer signed facts to the unsigned system. Facts from equality predicates are added to the unsigned system, so initially it should be fine to just query the unsigned system.
As for 2), I think you should be able to just do CS.isConditionImplied(A >= B) && CS.isConditionImplied(A <=B)?