Z3 naming let bindings in API

I am using Z3 from the API and I'm looking for a way to debug my constraints. My code compiles and Z3 runs on my constraints, but something is wrong with my constraints. I'm hoping to look at the constraints that I gave to Z3 to determine what is wrong or missing, but I'm not 开发者_如何学Csure how to do this in a way that is very readable. The problem is that using facilities like SMTLIB_DUMP_ASSERTIONS does not provide meaningful names in any let bound variables. Since I have many reuses of the same expressions, nearly everything is let-bound with a generated variable.

Is there any way to dump a file of the input constraints, where let-bound variables have a name that I have assigned? I don't particularly care what the format is, but SMTLIB 1 or 2 would be nice.

---

No, you cannot provide names to let variables automatically created by Z3 AST printers. One possible solution is to write your own AST printer. In the Z3 distribution, we have an example application examples/c/test_capi.c. It contains the function:

void display_ast(Z3_context c, FILE * out, Z3_ast v) 

It shows how to implement a simple AST printer. This example is very simple, but it is a starting point.