Set model.user_functions=false in Z3

WatForm / fortress

Fortress: Finite Model Finder for Many-Sorted First-Order Logic

MIT License

5 stars 0 forks source link

Set model.user_functions=false in Z3 #140

Closed ryandancy closed 2 months ago

ryandancy commented 3 months ago

This option tells Z3 not to generate definitions for user-defined (interpreted) functions and constants in response to (get-model). This was causing an issue with the new Portus ExprDefns optimization because Z3 was parrotting very large definitions and causing the SMTLIB parser to choke.

ryandancy commented 2 months ago

I think we should probably merge this as a base for the CVC5 changes? Since we know this is necessary for Z3.