When I run z3 with this input, the solver eventually locks up and stops checking for timeout. When I run it with "z3 timeout=1000", the timeout properly happens and interrupts z3. However, when I run it with "z3 timeout=10000", there is no interruption and the solver locks up indefinitely, consuming 100% CPU.

(declare-const a Int)
(declare-const b Int)
(declare-const c Int)
(declare-const n Int)
(assert (>= a 1))
(assert (>= b 1))
(assert (>= c 1))
(assert (= n 3))
(assert (= (+ (^ a n) (^ b n)) (^ c n)))
(check-sat)
(get-model)