omega counterexample with no goal constraints: goal was not parsed

On Lean v4.35, when omega cannot use the goal (for example a goal with a True conjunct, as simp only [Prod.mk.injEq] leaves behind for identical tuple components), it does not say so. It tries to refute the hypotheses alone and prints 'a possible counterexample may satisfy the constraints' listing only facts from hypotheses. Check: if no constraint in the counterexample corresponds to the goal, rewrite the goal first. For True conjuncts, simp only [true_and, and_true] (both are needed: true_and does not remove a trailing ∧ True). True ∨ P goals and True inside hypotheses are fine.