title: Z3Py Constants with user defined sorts different by default
body: <p>I have an uninterpreted sort Dataset:</p>
  <pre><code>Dataset = z3.DeclareSort(&quot;Dataset&quot;)
  </code></pre>
  <p>When I create constants from this sort:</p>
  <pre><code>d = z3.FreshConst(ZDataset)
  d2 = z3.FreshConst(ZDataset)
  </code></pre>
  <p>I want the solver to see them as different, so <code>d == d2</code> should be unsat.</p>
  <p>Is there any way to do this by default, so every time I create a constant, it is different from all others already made?</p>
  <p>The most straightforward solution I can see is to create a mock uninterpreted function like:</p>
  <pre><code>mock = Function(
      &quot;mock&quot;, ZDataset, z3.IntSort()
  )
  </code></pre>
  <p>and each time I create a constant, add a constraint to the solver:</p>
  <pre><code>solver.add(mock(d) == 0)
  </code></pre>
  <p>using a Python variable that is incremented each time.</p>
  <p>Although it is not the cleanest solution, it makes the solver see them as different.</p>