z3 solver check call hangs when solver is created with smt tactic about z3 HOT 1 CLOSED

1. This does not reproduce. Maybe your old version of z3 suffered from a non-termination bug for some cases of integers.
2. You could try the QF_LIA tactic, or you could use tactics that include pre-processing. When you run the default solver it uses equality and constant propagation. You compose tactics using "then". Tactics are documented here https://microsoft.github.io/z3guide/docs/strategies/tactics/ and here https://microsoft.github.io/z3guide/docs/strategies/summary
3. the default solver is all-round what most applications should use. I tune for default solver behavior. Tactics should be overkill for most cases, or indicate that default solver behavior could be improved.

from z3.