Non-terminating code may be synthesised

[JonasAlaif]

Given the following example (with dll defined as in the examples):

{ [x, 3] ** x :-> v ** (x + 1) :-> 0 ** (x + 2) :-> r ** dll(r, a, s) }
void helper (loc r)
{ dll(x, b, {v} ++ s) }

When run with -c 2 SuSLik outputs:

void helper (loc r) {
  if (r == 0) {
  } else {
    let y = *(r + 1);
    *(r + 2) = y;
    *(r + 1) = 0;
    helper(y);
    helper(r);
  }
}

Which, when called with r != 0 will recursively call itself with the same argument forever.
I tried to explore the tree in the online IDE, but am not familiar enough with the rules to figure out why the second recursive call was allowed. Possibly an issue in SuSLik or Cyclist, I'm not sure.

[JonasAlaif]

So I understand the issue a little better now. The spec for this function is essentially folding the predicate, but does not ensure any relationship between the predicate in the precondition and postcondition. A "fix" could be writing the spec as:

{ a0 < a1; [x, 3] ** x :-> v ** (x + 1) :-> 0 ** (x + 2) :-> r ** dll(r, a, s)<a0> }
void helper (loc r)
{ dll(x, b, {v} ++ s)<a1> }

Maybe such an ordering should automatically be applied to any predicates in pre/postconditions? I'm not sure if that would break things?

[ilyasergey]

Thanks for digging into this. I don't think this ordering can be inferred in a general case (as it can be guessed in this example).