Skip to content

Commit beddcaf

Browse files
Simplify boolbvt::set_to
1 parent 5f815a7 commit beddcaf

File tree

1 file changed

+4
-15
lines changed

1 file changed

+4
-15
lines changed

src/solvers/flattening/boolbv.cpp

Lines changed: 4 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -630,22 +630,11 @@ bool boolbvt::boolbv_set_equality_to_true(const equal_exprt &expr)
630630

631631
void boolbvt::set_to(const exprt &expr, bool value)
632632
{
633-
if(expr.type().id()!=ID_bool)
634-
{
635-
error() << "boolbvt::set_to got non-boolean operand: "
636-
<< expr.pretty() << eom;
637-
throw 0;
638-
}
639-
640-
if(value)
641-
{
642-
if(expr.id()==ID_equal)
643-
{
644-
if(!boolbv_set_equality_to_true(to_equal_expr(expr)))
645-
return;
646-
}
647-
}
633+
PRECONDITION(expr.type().id() == ID_bool);
648634

635+
const auto equal_expr = expr_try_dynamic_cast<equal_exprt>(expr);
636+
if(value && equal_expr && !boolbv_set_equality_to_true(*equal_expr))
637+
return;
649638
return SUB::set_to(expr, value);
650639
}
651640

0 commit comments

Comments
 (0)