We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent dba7ec9 commit 3c9225cCopy full SHA for 3c9225c
src/cbmc/bv_cbmc.cpp
@@ -23,9 +23,9 @@ bvt bv_cbmct::convert_waitfor(const exprt &expr)
23
const exprt &predicate=expr.op3();
24
const exprt new_cycle = make_free_bv_expr(expr.type());
25
26
- mp_integer bound_value;
27
- bool successful_cast = to_integer(bound, bound_value);
28
- 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();
29
30
{
31
// constraint: new_cycle>=old_cycle
0 commit comments