Make sygus refinement step more robust to unevaluatable counterexamples (#5102)

Make sygus refinement step more robust to unevaluatable counterexamples (#5102)

Currently, the CEGIS refinement loop of the sygus solver may terminate with "unknown" when a duplicate counterexample is generated. This is caused by a candidate t for a conjecture exists f. forall x. G[f, x] such that:

(1) G[t, c] evaluates to a non-constant expression,
(2) ~G[t, k] is satisfiable with model k = c.

Notice this exclusively limited to theories with incomplete functions, e.g. (non-linear) division.

In this case, we know that t is an incorrect solution, but the counterexample we found was not new.

Currently, we abort with "unknown" since the counterexample was not new. After this PR, we exclude t and continue, which is uncontroversially the correct behavior.

This PR moves the resposibility for lemma from synth engine to synth conjecture, which simplifies the behavior of the main check conjecture method.