muZ3: Non-deterministic recursive call

Question

Is there a way to perform a recursive call non-deterministically in a muZ3 relation specification? Specifically, I want to translate a function like the following:

int foo(int x) {
    ...
    if (*) y = foo(y);
    ...
}

to the muZ3 rule format.

Answer 1

You can have a separate rule for the two cases:

  (declare-fun foo (Int Int) Bool)

   (assert (forall ((x Int) (y Int) (z Int))  (=> (and ... (foo x y) ...) (foo x z)))

   (assert (forall ((x Int) (y Int) (z Int))  (=> (and ... true ...) (foo x z)))