title: expr substitution segmentation fault 'type error'
body: <p>I use z3 c++ api. I create a copy from exprs in expr_vector1 and store them in new expr_vector2 and then call</p>
  
  <pre><code>        for(unsigned j = 0; j &lt; exprs_vector1.size();++j){
              expr v = exprs_vector1[j];
              uint32_t size; // it is initialized somehow.
  
              std::stringstream name;
              name &lt;&lt; v &lt;&lt;"_"&lt;&lt; i;
              expr var(ctx);
              if(v.is_bool())
                  var = sctx-&gt;ctx.bool_const(name.str().c_str());
              else if(v.is_bv())
                  var = sctx-&gt;ctx.bv_const(name.str().c_str(), size);
              exprs_vector2.push_back(var);
  
              }    
         formula.substitute( expr_vactor1, expr_vector2); // this line causes error
  </code></pre>
  
  <p>but I get z3 exception with message "type error".
  Note that these two vector have the same size and their expressions correspondingly have the same sort and exprs are kind of bool or bitvector. I can't guess the reason of this event.
  the contents of vector1 :</p>
  
  <p>|popcnt::i!0@1#1_1|</p>
  
  <p>and in vector2 we have : </p>
  
  <p>|\|popcnt::i!0@1#1_1\|_1|</p>
  
  <p>both of above expressions are the sort of bitvector32.</p>
  
  <p>the formula doesn't have any expressions of expr_vector1, can it be the reason of this exception?  </p>