Expected option exception on checkSat(), only thrown on getInterpolant().

[aniemetz]

https://github.com/cvc5/cvc5/commit/fe3256e67ec224da28f2417d1d3262deb0cf49c4 murxla/murxla@a28daf6fe3ae9caa4f21d84421f0878224924187

#include <cvc5/cvc5.h>

using namespace cvc5;
int main(void)
{
Solver solver;
solver.setOption("produce-unsat-assumptions", "true");
solver.setOption("produce-interpolants", "true");
Sort s0 = solver.mkFloatingPointSort(8, 24);
Term t1 = solver.mkConst(s0, "_x0");
Term t2 = solver.mkBitVector(32, "11000101000100111110111101100100", 2);
Sort s3 = t2.getSort();
Term t4 = solver.mkFloatingPoint(8, 24, t2);
Op o5 = solver.mkOp(FLOATINGPOINT_GEQ);
Term t6 = solver.mkTerm(o5, {t1, t4});
Sort s7 = t6.getSort();
solver.checkSat();
Term t8 = solver.getInterpolant(t6);
}

only fails with the below option exception on getInterpolant(), but not on checkSat().

terminate called after throwing an instance of 'cvc5::CVC5ApiOptionException'
  what():  Error in option parsing: sygus not supported with proofs or unsat cores
Aborted (core dumped)

[ajreynol]

In general, this can be expected behavior. getInterpolant requires invoking an SMT solver with support for sygus, whereas checkSat does not. Note the option parsing is not necessarily on the original solver, maybe the error message could be made clearer.

Also, a minor thing that we are doing wrong in this example, produce-unsat-assumptions should not imply (full) proofs are enabled, I will look into this.