first encoding implementation for bvmult
crazy hack to make everything in cvc4 public