Function check_synth_next 

pub unsafe extern "C" fn check_synth_next(
    cvc5: *mut Solver,
) -> SynthResult

Try to find a next solution for the synthesis conjecture corresponding to the current list of functions-to-synthesize, universal variables and constraints. Must be called immediately after a successful call to check-synth or check-synth-next.

@note Requires incremental mode.

SyGuS v2:

\verbatim embed:rst:leading-asterisk .. code:: smtlib

(check-synth-next)

\endverbatim

@param cvc5 The solver instance. @return The result of the check, which is “solution” if the check found a solution in which case solutions are available via getSynthSolutions, “no solution” if it was determined there is no solution, or “unknown” otherwise.