Skip to content

Commit 30dcd9a

Browse files
Simplify boolbvt::set_to
1 parent 597a5b0 commit 30dcd9a

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
@@ -631,22 +631,11 @@ bool boolbvt::boolbv_set_equality_to_true(const equal_exprt &expr)
631631

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

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

0 commit comments

Comments
 (0)