diff --git a/src/goto-programs/json_expr.cpp b/src/goto-programs/json_expr.cpp index d3473b9d65d..b7f13081e39 100644 --- a/src/goto-programs/json_expr.cpp +++ b/src/goto-programs/json_expr.cpp @@ -51,9 +51,7 @@ static exprt simplify_json_expr(const exprt &src) // simplify expressions of the form &member(object, @class_identifier) return simplify_json_expr(object); } - else if( - object.id() == ID_index && to_index_expr(object).index().is_constant() && - to_constant_expr(to_index_expr(object).index()).value_is_zero_string()) + else if(object.id() == ID_index && to_index_expr(object).index() == 0) { // simplify expressions of the form &array[0] return simplify_json_expr(to_index_expr(object).array()); diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp index 2cb21826d6f..f789bfdfb37 100644 --- a/src/util/simplify_expr_int.cpp +++ b/src/util/simplify_expr_int.cpp @@ -782,7 +782,7 @@ simplify_exprt::simplify_bitwise(const multi_ary_exprt &expr) } else if( it->is_constant() && it->type().id() == ID_bv && - to_constant_expr(*it).value_is_zero_string() && + *it == to_bv_type(it->type()).all_zeros_expr() && new_expr.operands().size() > 1) { it = new_expr.operands().erase(it); diff --git a/src/util/std_expr.h b/src/util/std_expr.h index 8ca02d50de1..4cf659779f8 100644 --- a/src/util/std_expr.h +++ b/src/util/std_expr.h @@ -3133,8 +3133,6 @@ class constant_exprt : public nullary_exprt set(ID_value, value); } - bool value_is_zero_string() const; - /// Returns true if \p expr has a pointer type and a value NULL; it also /// returns true when \p expr has value zero and NULL_is_zero is true; returns /// false in all other cases. @@ -3166,6 +3164,9 @@ class constant_exprt : public nullary_exprt { check(expr, vm); } + +protected: + bool value_is_zero_string() const; }; template <> diff --git a/unit/goto-symex/goto_symex_state.cpp b/unit/goto-symex/goto_symex_state.cpp index 999fadf374c..9042248686e 100644 --- a/unit/goto-symex/goto_symex_state.cpp +++ b/unit/goto-symex/goto_symex_state.cpp @@ -173,8 +173,7 @@ SCENARIO( const symbol_exprt object_symbol = to_symbol_expr(object_descriptor->object()); REQUIRE(object_symbol.get_identifier() == "int_value!0"); - REQUIRE(to_constant_expr(object_descriptor->offset()) - .value_is_zero_string()); + REQUIRE(object_descriptor->offset() == 0); } THEN("The target equations are unchanged") {