Why is z3 unable to sat check the following?

```
(declare-fun f (Int) Int)
(assert (forall ((a Int) (b Int)) (= (+ (f a) (f b) ) (f (+ a b)))))
(assert (= (f 1) 1))
(check-sat)
(get-model)
```

I would expect a result along the lines of `f(x) = x`

, however z3 seems to consume an increasing amount of ram, and never find a solution.
Is this something uninterpreted functions are not intended for?

I've tried using reals and adding an additional function which I expect is the same as f, like so:

```
(declare-fun f (Real) Real)
(declare-fun g (Real) Real)
(assert (forall ((a Real)) (= (g a) a)))
(assert (forall ((a Real) (b Real)) (= (+ (f a) (f b) ) (f (+ a b)))))
(assert (= (f 1) 1))
(check-sat)
(get-model)
```