File tree Expand file tree Collapse file tree 1 file changed +6
-11
lines changed Expand file tree Collapse file tree 1 file changed +6
-11
lines changed Original file line number Diff line number Diff line change @@ -1474,24 +1474,19 @@ void goto_checkt::add_guarded_claim(
1474
1474
const exprt &src_expr,
1475
1475
const guardt &guard)
1476
1476
{
1477
- exprt simplified_expr (asserted_expr);
1478
-
1479
1477
// first try simplifier on it
1480
- if (enable_simplify)
1481
- simplify (simplified_expr , ns);
1478
+ exprt simplified_expr =
1479
+ enable_simplify ? simplify_expr (asserted_expr , ns) : asserted_expr ;
1482
1480
1483
1481
// throw away trivial properties?
1484
1482
if (!retain_trivial && simplified_expr.is_true ())
1485
1483
return ;
1486
1484
1487
1485
// add the guard
1488
-
1489
- exprt guarded_expr;
1490
-
1491
- if (guard.is_true ())
1492
- guarded_expr.swap (simplified_expr);
1493
- else
1494
- guarded_expr = implies_exprt (guard.as_expr (), std::move (simplified_expr));
1486
+ exprt guarded_expr =
1487
+ guard.is_true ()
1488
+ ? simplified_expr
1489
+ : implies_exprt{guard.as_expr (), std::move (simplified_expr)};
1495
1490
1496
1491
if (assertions.insert (guarded_expr).second )
1497
1492
{
You can’t perform that action at this time.
0 commit comments