- Z3 is now always enabled by default, now that it is fully open source. The "z3_non_commercial" option is discontinued. In addition, Z3 should now (again) be invoked by default by Sledgehammer. Let me know if you see anything odd, e.g. odd problems with binaries on Linux or Windows. Jasmin