diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index 711bade9e97..b27daf59570 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -1067,7 +1067,7 @@ bool simplify_exprt::simplify_if_preorder(if_exprt &expr) result=false; } - #if 0 +#ifdef USE_LOCAL_REPLACE_MAP replace_mapt map_before(local_replace_map); // a ? b : c --> a ? b[a/true] : c @@ -1109,10 +1109,10 @@ bool simplify_exprt::simplify_if_preorder(if_exprt &expr) result=simplify_rec(falsevalue) && result; local_replace_map.swap(map_before); - #else +#else result=simplify_rec(truevalue) && result; result=simplify_rec(falsevalue) && result; - #endif +#endif } else { @@ -2382,6 +2382,7 @@ bool simplify_exprt::simplify_rec(exprt &expr) if(!simplify_node(tmp)) result=false; +#ifdef USE_LOCAL_REPLACE_MAP #if 1 replace_mapt::const_iterator it=local_replace_map.find(tmp); if(it!=local_replace_map.end()) @@ -2397,6 +2398,7 @@ bool simplify_exprt::simplify_rec(exprt &expr) result=false; } #endif +#endif if(!result) { diff --git a/src/util/simplify_expr_class.h b/src/util/simplify_expr_class.h index 3bcda0ac352..a89134433b2 100644 --- a/src/util/simplify_expr_class.h +++ b/src/util/simplify_expr_class.h @@ -19,7 +19,10 @@ Author: Daniel Kroening, kroening@kroening.com #include "type.h" #include "mp_arith.h" +// #define USE_LOCAL_REPLACE_MAP +#ifdef USE_LOCAL_REPLACE_MAP #include "replace_expr.h" +#endif class bswap_exprt; class byte_extract_exprt; @@ -154,7 +157,9 @@ class simplify_exprt #ifdef DEBUG_ON_DEMAND bool debug_on; #endif +#ifdef USE_LOCAL_REPLACE_MAP replace_mapt local_replace_map; +#endif }; #endif // CPROVER_UTIL_SIMPLIFY_EXPR_CLASS_H