diff --git a/src/analyses/invariant_set.cpp b/src/analyses/invariant_set.cpp index ce745f27fad..b6afe7d34ff 100644 --- a/src/analyses/invariant_set.cpp +++ b/src/analyses/invariant_set.cpp @@ -752,9 +752,8 @@ void invariant_sett::nnf(exprt &expr, bool negate) typecast_expr.op().type().id() == ID_unsignedbv || typecast_expr.op().type().id() == ID_signedbv) { - equal_exprt tmp; - tmp.lhs() = typecast_expr.op(); - tmp.rhs() = from_integer(0, typecast_expr.op().type()); + equal_exprt tmp( + typecast_expr.op(), from_integer(0, typecast_expr.op().type())); nnf(tmp, !negate); expr.swap(tmp); } @@ -1053,9 +1052,7 @@ void invariant_sett::assignment( const exprt &lhs, const exprt &rhs) { - equal_exprt equality; - equality.lhs()=lhs; - equality.rhs()=rhs; + equal_exprt equality(lhs, rhs); // first evaluate RHS simplify(equality.rhs()); diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index 3180bba4d29..b61bdb83f74 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -2540,8 +2540,8 @@ exprt c_typecheck_baset::do_special_functions( throw 0; } - equal_exprt equality_expr; - equality_expr.operands()=expr.arguments(); + equal_exprt equality_expr( + expr.arguments().front(), expr.arguments().back()); equality_expr.add_source_location()=source_location; if(!base_type_eq(equality_expr.lhs().type(), diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index 179370fa560..9e8f50f1c35 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/src/goto-programs/goto_convert.cpp @@ -1156,9 +1156,7 @@ exprt goto_convertt::case_guard( forall_expr(it, case_op) { - equal_exprt eq_expr; - eq_expr.lhs() = value; - eq_expr.rhs() = *it; + equal_exprt eq_expr(value, *it); dest.move_to_operands(eq_expr); } INVARIANT( diff --git a/src/solvers/flattening/boolbv_byte_extract.cpp b/src/solvers/flattening/boolbv_byte_extract.cpp index f9e7749d928..695edc75890 100644 --- a/src/solvers/flattening/boolbv_byte_extract.cpp +++ b/src/solvers/flattening/boolbv_byte_extract.cpp @@ -143,9 +143,6 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr) // add implications - equal_exprt equality; - equality.lhs() = expr.offset(); // index operand - // type of index operand const typet &constant_type = expr.offset().type(); @@ -154,8 +151,6 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr) for(std::size_t i=0; i(offset + j)]); - prop.l_set_to_true( - prop.limplies(convert(index_equality), prop.land(equal_bv))); + prop.l_set_to_true(prop.limplies( + convert(equal_exprt(index, from_integer(i, index.type()))), + prop.land(equal_bv))); } } else { bv.resize(width); - equal_exprt equality; - equality.lhs()=index; // index operand - #ifdef COMPACT_EQUAL_CONST bv_utils.equal_const_register(convert_bv(index)); // Definitely #endif @@ -247,9 +229,8 @@ bvt boolbvt::convert_index(const index_exprt &expr) for(mp_integer i=0; i