Add directly within the constraint system data structure the status Forall/Exists. Then remove the constraint system Exists from one side if there is no constraint system Forall of the other side. It should speed up the procedure.
Moreover we could add an information on the constraint system indicating wether we know that they have distinct solutions (for instance constraint system obtained by the same conditional but with different branch). In such a case, as soon as we obtain one of these constraint system in solve form, we can automatically delete the other constraint system (avoid calculus of mgs).
Add directly within the constraint system data structure the status Forall/Exists. Then remove the constraint system Exists from one side if there is no constraint system Forall of the other side. It should speed up the procedure.
Moreover we could add an information on the constraint system indicating wether we know that they have distinct solutions (for instance constraint system obtained by the same conditional but with different branch). In such a case, as soon as we obtain one of these constraint system in solve form, we can automatically delete the other constraint system (avoid calculus of mgs).