From 3c23b28353e2fe679bbfdd1b4edb174700312fe9 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 15 Aug 2017 17:04:13 +0100
Subject: [PATCH] Consistently disable simplify_exprt::local_replace_map

This avoids unnecessarily computing the hash of an exprt for an unused map. The
common preprocessor macro now also links together all related bits of code.
---
 src/util/simplify_expr.cpp     | 8 +++++---
 src/util/simplify_expr_class.h | 5 +++++
 2 files changed, 10 insertions(+), 3 deletions(-)

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