Z3 hangs on formula with define-funs-rec #4263
Description
Hi,
For this case, Z3 master branch hangs on it while z3-4.8.7 answers it quickly:
[619] % time z3-4.8.7 small.smt2
sat
real 0m0.053s
user 0m0.014s
sys 0m0.003s
[620] % timeout -s 9 30 z3release small.smt2
Killed
[621] %
[621] % cat small.smt2
(define-funs-rec ((a ((b Int)) Int) (c ((d Int)) Int)) ((a 0) (c 0)))
(assert (= (a 0) 0))
(check-sat)
[622] %
OS: Ubuntu 18.04
Commit: 6c72f39