title: Error adding containts to solver in z3
body: <pre><code>assign wfwe = wb_acc &amp; (adr_i == 2'b10) &amp; ack_o &amp;  we_i;
  </code></pre>
  
  <p>For the above assign statement which is in verilog, i getting error while implememting it in z3</p>
  
  <p>My code: </p>
  
  <pre><code>BitVecExpr[] wfwe = new BitVecExpr[1];
  BitVecExpr[] wb_acc = new BitVecExpr[1];
  BitVecExpr[] adr_i = new BitVecExpr[1];
  BitVecExpr[] ack_o = new BitVecExpr[1];
  BitVecExpr[] we_i = new BitVecExpr[1];
  
  wfwe[0] = ctx.mkBVConst("wfwe",1);
  wb_acc[0] = ctx.mkBVConst("wb_acc",1);
  adr_i[0] = ctx.mkBVConst("adr_i",2);
  ack_o[0] = ctx.mkBVConst("ack_o",1);
  we_i[0] = ctx.mkBVConst("we_i",1);
  
  Solver s = ctx.mkSolver();
  
  s.add(ctx.mkBVAND(wb_acc[0],ctx.mkEq(adr_i[0],ctx.mkNumeral("2",2)),ack_o[0],we_i[0]));
  </code></pre>
  
  <p>I am getting error in above add statement:
  error: method mkBVAND in class Context cannot be applied to given types;
  required: BitVecExpr,BitVecExpr
  found: BitVecExpr,BoolExpr</p>
  
  <p>Which is true. Can anyone suggest me workaround. Am i implementing it incorrectly please let me know. </p>