title: How to use Z3py and Sympy together
body: <p>I am trying to perform some symbolic calculation on matrices (with symbols as an entries of matrices), and after that I will have a number of possible solution. My goal is to select solutions/ solution based upon constraints. </p>
  
  <p>for example, <code>M</code> is a matrix which have one element as a <code>symbol</code>.
  This matrix will have 2 eigenvalues one is positive an one is negative. Using z3 I am trying to find out only negative value, but I am unable to do so as a is defined as a symbol and I cannot write it as a constraint unless I convert it to a real value. </p>
  
  <p>what should I do? is there any way to convert a (symbol) in to real or integer so that I can use it as a constraint <code>s.add(a&gt;0)</code></p>
  
  <pre><code>from sympy import* 
  from z3 import* 
  from math import*
  
  a=Symbol('a')
  
  M=Matrix([[a,2],[3,4]]) m=M.eigenvals();
  
  s=Solver()
  
  s.add(m&lt;0)
  print(s.check())
  model = s.model() print(model)
  </code></pre>