title: using square root objects in Z3 c++
body: <p>I am using Z3 with the C++ APIs. I have to solve a system of equations that include square root terms. how can I use square root in Z3 C++?
  temporarily, I replace something like this:</p>
  
  <blockquote>
    <p>s.add(x == sqrt(4));</p>
  </blockquote>
  
  <p>with this:</p>
  
  <blockquote>
    <p>s.add(x*x == 4);</p>
  </blockquote>
  
  <p>but in some cases, it doesn't give the right results, so I am asking is there a way to do the sqrt directly?</p>