在Z3中使用位向量文字

我开始在C++API中使用Z3,我主要感兴趣的是使用它对位向量的支持。

然而,我完全无法弄清楚如何将位向量文字与表达式结合使用。

以下是我试图实现的基本目标:

context z3_ctx;
solver  z3_solver(z3_ctx);
optimize z3_optimizer(z3_ctx);
expr x = z3_ctx.bv_const("x", 256);
z3_solver.add(x == "#x4123"); // Need help here

网上没有例子显示我如何完成这个简单的任务。如果我的位向量只有64位或更少,这不会是问题,但我需要支持更大的位向量长度。