Skip to content

Commit 371cb09

Browse files
committed
Fix assert to limit array size
CBMC has changed the representation of numerical values in constant_expr (at least for array sizes) - instead of base 2, it now uses base 16. We have to fix this in our assertion that limits the size of arrays in competition mode due to solver unsoundness that appears for arrays of size >=50000.
1 parent 2c857ee commit 371cb09

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/2ls/preprocessing_util.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -674,7 +674,7 @@ void twols_parse_optionst::limit_array_bounds(goto_modelt &goto_model)
674674
if(size_expr.id()==ID_constant)
675675
{
676676
int size=std::stoi(
677-
id2string(to_constant_expr(size_expr).get_value()), nullptr, 2);
677+
id2string(to_constant_expr(size_expr).get_value()), nullptr, 16);
678678
// @TODO temporary solution - there seems to be a bug in the solver
679679
assert(size<=50000);
680680
}

0 commit comments

Comments
 (0)