Skip to content

Commit 4365c28

Browse files
Simplify boolbvt::set_to
1 parent b18109f commit 4365c28

File tree

1 file changed

+5
-16
lines changed

1 file changed

+5
-16
lines changed

src/solvers/flattening/boolbv.cpp

Lines changed: 5 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -631,23 +631,12 @@ 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

650-
return SUB::set_to(expr, value);
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;
639+
SUB::set_to(expr, value);
651640
}
652641

653642
exprt boolbvt::make_bv_expr(const typet &type, const bvt &bv)

0 commit comments

Comments
 (0)