We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 017c1b0 commit f06cbeaCopy full SHA for f06cbea
src/cbmc/bv_cbmc.cpp
@@ -24,9 +24,9 @@ bvt bv_cbmct::convert_waitfor(const exprt &expr)
24
const exprt &predicate=expr.op3();
25
const exprt new_cycle = make_free_bv_expr(expr.type());
26
27
- mp_integer bound_value;
28
- bool successful_cast = to_integer(bound, bound_value);
29
- INVARIANT(successful_cast, "waitfor bound must be a constant");
+ optionalt<mp_integer> bound_converted = numeric_cast<mp_integer>(bound);
+ INVARIANT(bound_converted.has_value(), "waitfor bound must be a constant");
+ mp_integer bound_value = bound_converted.value();
30
31
{
32
// constraint: new_cycle>=old_cycle
0 commit comments