Skip to content
This repository has been archived by the owner on Feb 3, 2020. It is now read-only.

Commit

Permalink
Z3Builder: fixed sign extension bug
Browse files Browse the repository at this point in the history
Signed-off-by: Vitaly Chipounov <vitaly@cyberhaven.io>
  • Loading branch information
vitaly-cyberhaven committed Nov 25, 2019
1 parent 818e595 commit 3216200
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion lib/Solver/Z3Builder.cpp
Expand Up @@ -150,7 +150,7 @@ z3::expr Z3Builder::makeExpr(ref<Expr> e) {

z3::expr src = getOrMakeExpr(ce->getSrc());
if (src.is_bool()) {
return z3::to_expr(context_, Z3_mk_ite(context_, src, context_.bv_val(1, ce->getWidth()),
return z3::to_expr(context_, Z3_mk_ite(context_, src, context_.bv_val(-1, ce->getWidth()),
context_.bv_val(0, ce->getWidth())));
} else {
return z3::to_expr(context_, Z3_mk_sign_ext(context_, ce->getWidth() - src.get_sort().bv_size(), src));
Expand Down

0 comments on commit 3216200

Please sign in to comment.