Skip to content

Commit

Permalink
[fix, tmp] Removed assert for constant.
Browse files Browse the repository at this point in the history
  • Loading branch information
S1eGa committed Nov 18, 2023
1 parent c421267 commit a7314d5
Showing 1 changed file with 1 addition and 4 deletions.
5 changes: 1 addition & 4 deletions lib/Solver/BitwuzlaSolver.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -558,8 +558,7 @@ SolverImpl::SolverRunStatus BitwuzlaSolverImpl::handleSolverResponse(
for (const ref<Expr> &offsetExpr : env.usedArrayBytes.at(array)) {
Term arrayElementOffsetExpr =
theSolver.get_value(builder->construct(offsetExpr));
assert(arrayElementOffsetExpr.is_const() &&
"Evaluated size expression has wrong sort");

uint64_t concretizedOffsetValue =
std::stoull(arrayElementOffsetExpr.value<std::string>(10));
offsetValues.insert(concretizedOffsetValue);
Expand All @@ -569,8 +568,6 @@ SolverImpl::SolverRunStatus BitwuzlaSolverImpl::handleSolverResponse(
// We can't use Term here so have to do ref counting manually
Term initial_read = builder->getInitialRead(array, offset);
Term initial_read_expr = theSolver.get_value(initial_read);
assert(initial_read_expr.is_const() &&
"Evaluated expression has wrong sort");

uint64_t arrayElementValue =
std::stoull(initial_read_expr.value<std::string>(10));
Expand Down

0 comments on commit a7314d5

Please sign in to comment.