title: Z3,C++ API, How to convert bool sort to int sort
body: <p>I am using Z3 in C++, and I have some bool-sort exprs. </p>
  
  <p>What I want to do is to count the number of true-value exprs. </p>
  
  <p>A very simple way is to convert those expr into int-sort and then add them up.</p>
  
  <p>However I don't know how to convert bool to int.</p>
  
  <p>Thanks!</p>
  
  <hr>
  
  <p>SOLUTION:</p>
  
  <p>As the cpp example file shows(function ite_example2()):</p>
  
  <pre><code>expr b = c.bool_const("x");
  expr x = c.int_val(1);
  expr y = c.int_val(0);
  expr conj = ite(b,x,y);
  </code></pre>