assumptions causing spurious candidate solutions from synthesis engine

[polgreen]

This example takes 1 iteration:

int EXPRESSION();
int nondet_int();

int main()
{
   int y=nondet_int();
 __CPROVER_assert(EXPRESSION()==10, "equality");
  return 0;
}

This example takes two iterations and the first solution produced by the synthesis engine is "return 8", which is clearly not right.

I think what is happening is we are finding solutions that work because the assumptions are incompatible with the inputs and so all paths to the final assertion are blocked.

int EXPRESSION();
int nondet_int();

int main()
{
   int y=nondet_int();
  __CPROVER_assume(y==2);
 __CPROVER_assert(EXPRESSION()==10, "equality");
  return 0;
}

More complicated examples that use assumptions will cause "No Progress" errors