'sat)))

      ;; Then, outside of Z3, we can do something with the result.  Here, we

      ;; check that a solution can be found.

        ;; If we find one, we ask one to Z3 and we get a nice association list

        ;; as a result.

        (let ((solution (z3-eval context '((get-value (x y))))))