[Consolidated] issues affecting tactic.default_tactic=smt sat.euf=true

Hi, for the following formula,
z3 af5c6e43b91aad0a2ae16
~~~~
(declare-sort A)
(declare-fun f (A) A)
(assert (forall ((x A)) (forall ((y A)) (and (= x (f (f x))) (= x y)))))
(check-sat)
~~~~
~~~~
unexpected SAT
ASSERTION VIOLATION
File: ../src/sat/smt/sat_dual_solver.cpp
Line: 149
UNEXPECTED CODE WAS REACHED.
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
~~~~