title: Is it possible to force a Z3 model to evaluate boolean expressions involving arrays?
body: <p>Sometimes, evaluating a boolean expression in a model doesn't return a concrete boolean value even when the expression clearly has a concrete value.  I've been able to reduce this to cases involving array expressions such as <a href="http://rise4fun.com/Z3Py/K5FB" rel="nofollow">this test case</a>:</p>
  
  <pre><code>from z3 import *
  
  x = K(IntSort(), 0)
  s = Solver()
  s.check()
  m = s.model()
  print m.evaluate(x == Store(x, 0, 1), model_completion=True)
  </code></pre>
  
  <p>I would expect this to print <code>False</code>, but instead it prints <code>K(Int, 0) == Store(K(Int, 0), 0, 1)</code>.  Other examples produce similar results.  Replacing the first line with <code>x = Array('x', IntSort(), IntSort())</code> gives the same result (though that's up to the default interpretation).  Interestingly, replacing the first line with <code>x = Store(K(IntSort(), 0), 0, 1)</code> causes the example to print <code>True</code>.</p>
  
  <p>Is there a way to force Z3 to evaluate such expressions to concrete values?</p>