Z3_add_rec_def body is not a macro (confusion regarding the "is_macro" parameter in the C FFI)

[let-def]

A test of my own involving recursive functions started to fail at some point after Z3 v4.8.9.
Unfortunately, I was not able to extract a small, reproducible test case:

• my program is mainly using the C API to query Z3 incrementally
• I could extract an smtlib script, but the bug did not appear when using Z3 CLI

I was able to narrow down the commit that introduced the bug. I think this is enough to fix it, though I don't understand much of Z3 codebase :).

Given it is in the FFI, that would explain the difference between the library and the CLI. Writing a testcase probably involves replicating the smtlib script with some C code.

[NikolajBjorner]

do you have the commit SHA?

[let-def]

Sure, I based my branch on top of it, it's commit 0ba518b avoid perf abyss for macros.