Skip to content

Commit

Permalink
klee: fixed z3 api
Browse files Browse the repository at this point in the history
Signed-off-by: Vitaly Chipounov <[email protected]>
  • Loading branch information
vitalych committed Apr 20, 2024
1 parent c024c0e commit 07b5bbc
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions klee/lib/Solver/Z3Solver.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -233,8 +233,8 @@ void Z3BaseSolverImpl::extractModel(const ArrayVec &objects, std::vector<std::ve
z3::expr value_ast = model.eval(builder_->getInitialRead(array, offset), true);
unsigned value_num;

Z3_bool conv_result = Z3_get_numeral_uint(context_, value_ast, &value_num);
::check(conv_result == Z3_TRUE, "Could not convert value");
auto conv_result = Z3_get_numeral_uint(context_, value_ast, &value_num);
::check(conv_result, "Could not convert value");
assert(value_num < (1 << 8 * sizeof(unsigned char)) && "Invalid model value");

data.push_back((unsigned char) value_num);
Expand Down

0 comments on commit 07b5bbc

Please sign in to comment.