@@ -2295,20 +2295,27 @@ simplify_exprt::simplify_overflow_unary(const unary_overflow_exprt &expr)
2295
2295
return false_exprt{};
2296
2296
}
2297
2297
2298
- bool simplify_exprt::simplify_node_preorder (exprt & expr)
2298
+ simplify_exprt::resultt<> simplify_exprt::simplify_node_preorder (exprt expr)
2299
2299
{
2300
- bool result=true ;
2301
-
2302
2300
// The ifs below could one day be replaced by a switch()
2303
2301
2304
2302
if (expr.id ()==ID_address_of)
2305
2303
{
2306
2304
// the argument of this expression needs special treatment
2305
+ return unchanged (expr);
2307
2306
}
2308
2307
else if (expr.id ()==ID_if)
2309
- result=simplify_if_preorder (to_if_expr (expr));
2308
+ {
2309
+ bool no_change = simplify_if_preorder (to_if_expr (expr));
2310
+ if (no_change)
2311
+ return unchanged (expr);
2312
+ else
2313
+ return expr;
2314
+ }
2310
2315
else
2311
2316
{
2317
+ bool has_changed = false ;
2318
+
2312
2319
if (expr.has_operands ())
2313
2320
{
2314
2321
Forall_operands (it, expr)
@@ -2317,13 +2324,18 @@ bool simplify_exprt::simplify_node_preorder(exprt &expr)
2317
2324
if (r_it.has_changed ())
2318
2325
{
2319
2326
*it = r_it.expr ;
2320
- result= false ;
2327
+ has_changed = true ;
2321
2328
}
2322
2329
}
2323
2330
}
2331
+
2332
+ if (has_changed)
2333
+ return expr;
2334
+ else
2335
+ return unchanged (expr);
2324
2336
}
2325
2337
2326
- return result ;
2338
+ return unchanged (expr) ;
2327
2339
}
2328
2340
2329
2341
simplify_exprt::resultt<> simplify_exprt::simplify_node (exprt node)
@@ -2604,17 +2616,19 @@ simplify_exprt::resultt<> simplify_exprt::simplify_rec(const exprt &expr)
2604
2616
}
2605
2617
#endif
2606
2618
2607
- // We work on a copy to prevent unnecessary destruction of sharing.
2608
- exprt tmp=expr;
2609
- bool no_change = simplify_node_preorder (tmp);
2619
+ bool no_change = true ;
2610
2620
2611
- auto simplify_node_result = simplify_node (tmp);
2621
+ auto preorder_result = simplify_node_preorder (expr);
2622
+
2623
+ if (preorder_result.has_changed ())
2624
+ no_change = false ;
2625
+
2626
+ auto simplify_node_result = simplify_node (preorder_result.expr );
2612
2627
2613
2628
if (simplify_node_result.has_changed ())
2614
- {
2615
2629
no_change = false ;
2616
- tmp = simplify_node_result. expr ;
2617
- }
2630
+
2631
+ exprt tmp = simplify_node_result. expr ;
2618
2632
2619
2633
#ifdef USE_LOCAL_REPLACE_MAP
2620
2634
#if 1
0 commit comments