Generalization for sygus verify utility (#8586)
This is in preparation for synthesis modulo oracles (SyMO), where the verification loop may run multiple times for a given solution. In a follow up PR, the loop introduced in this PR may run multiple times when oracles are present, since oracle invocations in the subsolver may trigger further simplifications to the rewritten form of the specification.
It also makes it so that candidate models are generated for "unknown" results for subsolvers, which is required for SyMO.
projects / cvc5.git / commit