title: How to compare two expression in z3?
body: <p>I am wondering how to compare two expressions in C++ z3. The following code generates two equal expressions, but the result shows they do not share the same id, which is different from <a href="https://stackoverflow.com/questions/26069496/z3-check-whether-two-expressions-are-the-same">this post</a>. A way to do this is to simplify before checking but the speed is slow due to the simplify overhead. Is there an efficient way to solve it?</p>
  <pre><code>z3::context c;
  z3::expr z1 = c.bool_const(&quot;z1&quot;);
  z3::expr z2 = c.bool_const(&quot;z2&quot;);
  z3::expr z11 = z1 &amp;&amp; z2;
  z3::expr z22 = z2 &amp;&amp; z1;
  auto res = Z3_is_eq_ast(c, z11, z22);
  </code></pre>