title: Why does introducing this existential quantifier cause non-termination?
body: <p>I am just starting to play with Z3 on my own and I thought one interesting experiment would be to construct a 3-element field.</p>
  
  <p>So I declared my field S to be a scalar enumeration of three elements, A, B, C, and started gradually adding field axioms, asking Z3 for a model after each step, just to see what is going on.  All goes well until I assert the possibility of subtraction, ∀ab.(∃x.a+x=b): </p>
  
  <pre><code>(declare-datatypes () ((S A B C)))
  
  ; there exist three distinct elements in S
  (declare-const someA S)
  (declare-const someB S)
  (declare-const someC S)
  (assert (distinct someA someB someC))
  
  (declare-fun ADD (S S) S)
  (declare-fun MUL (S S) S)
  
  ; commutative
  (assert (forall ((x S) (y S)) (= (ADD x y) (ADD y x))))
  (assert (forall ((x S) (y S)) (= (MUL x y) (MUL y x))))
  
  ; associative
  (assert (forall ((x S) (y S) (z S)) (= (ADD x (ADD y z)) (ADD (ADD x y) z))))
  (assert (forall ((x S) (y S) (z S)) (= (MUL x (MUL y z)) (MUL (MUL x y) z))))
  
  ; subtractivity
  (assert (forall ((a S) (b S)) (exists ((x S)) (= (ADD a x) b))))
  
  (check-sat)
  (get-model)
  </code></pre>
  
  <p>This results in Z3 looping forever.  I am surprised.  I mean yes, I understand why FOL is in general undecidable, but I'd think this would be one of those "easy" cases because the space of all possible values for a, b and ADD is finite (and in this case even very small)?  Why does it loop?  and what is the correct way to express the subtractability axiom preferably in a way that doesn't lose being perceivable as its intended intuitive meaning?</p>