title: z3 tutorial: why does this return UNSAT?
body: <p>I am new to Z3 (and SMT solvers in general), and I've been going through the <a href="https://rise4fun.com/Z3/tutorial/guide" rel="nofollow noreferrer">Z3 tutorial</a>. In the section on quantifiers, it has me run the following code:</p>
  
  <pre><code>(declare-fun f (Int) Int)
  (declare-fun g (Int) Int)
  (declare-const a Int)
  (declare-const b Int)
  (declare-const c Int)
  
  (assert (forall ((x Int))
                  (! (= (f (g x)) x))))
  (assert (= (g a) c))
  (assert (= (g b) c))
  (assert (not (= a b)))
  (check-sat)
  </code></pre>
  
  <p>And running this returns UNSAT. But this seems satisfiable: just take a = 1, b = 2, c = 1, f(x) = 1 - x, and g(x) = 0 if x = 0, otherwise 1. Then a != b, g(a) = g(b) = 1, and we have no fixed points, since f(g(x)) maps everything to 0 except for 0 itself, which gets mapped to 1.</p>
  
  <p>Where am I going wrong here?</p>