I'm using Python Z3 to try and satisfy a large number of clauses containing variables and integers. When I run one of my Z3 scripts though, the Python shell hangs. The script is supposed to return SAT or UNSAT, but it does neither. It just hangs. The formula is very long, but I have run scripts with longer formulas and I haven't had any problem with those, so I'm not convinced that I'm encountering some kind of size limit. The only thing that I thought might be causing a problem is how Z3 treats clauses that contain both Int and Bool variables.
My scripts are very long, so I've uploaded them to this Github Issues Page as text files.
I found a similar thread where someone's issue stemmed from using String variables. The fix for this problem was to add a Z3 context to the variables and checker, but that solution hasn't worked for me.