Maintain ID_C_expr_simplified

tautschnig · tautschnig · commit 7c9c51393d11 · 2017-06-08T08:06:46.000+01:00
diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h
@@ -131,13 +131,13 @@ class goto_symext
     statet &state,
     const bool write);
 
-  void dereference_rec(
+  bool dereference_rec(
     exprt &expr,
     statet &state,
     guardt &guard,
     const bool write);
 
-  void dereference_rec_address_of(
+  bool dereference_rec_address_of(
     exprt &expr,
     statet &state,
     guardt &guard);
diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp
@@ -436,12 +436,13 @@ void goto_symex_statet::set_ssa_indices(
   }
 }
 
-void goto_symex_statet::rename(
+bool goto_symex_statet::rename(
   exprt &expr,
   const namespacet &ns,
   levelt level)
 {
   // rename all the symbols with their last known value
+  bool result=false;
 
   if(expr.id()==ID_symbol &&
      expr.get_bool(ID_C_SSA_symbol))
@@ -476,7 +477,10 @@ void goto_symex_statet::rename(
           propagation.values.find(ssa.get_identifier());
 
         if(p_it!=propagation.values.end())
+        {
           expr=p_it->second; // already L2
+          result=true;
+        }
         else
           set_ssa_indices(ssa, ns, L2);
       }
@@ -493,16 +497,16 @@ void goto_symex_statet::rename(
         ns,
         level);
 
-      return;
+      return false;
     }
 
     expr=ssa_exprt(expr);
-    rename(expr, ns, level);
+    result=rename(expr, ns, level);
   }
   else if(expr.id()==ID_address_of)
   {
     assert(expr.operands().size()==1);
-    rename_address(expr.op0(), ns, level);
+    result=rename_address(expr.op0(), ns, level);
     assert(expr.type().id()==ID_pointer);
     expr.type().subtype()=expr.op0().type();
   }
@@ -513,7 +517,7 @@ void goto_symex_statet::rename(
 
     // do this recursively
     Forall_operands(it, expr)
-      rename(*it, ns, level);
+      result=rename(*it, ns, level) || result;
 
     // some fixes
     if(expr.id()==ID_with)
@@ -525,6 +529,11 @@ void goto_symex_statet::rename(
       expr.type()=to_if_expr(expr).true_case().type();
     }
   }
+
+  if(result)
+    expr.remove(ID_C_expr_simplified);
+
+  return result;
 }
 
 /// thread encoding
@@ -709,11 +718,13 @@ bool goto_symex_statet::l2_thread_write_encoding(
   return threads.size()>1;
 }
 
-void goto_symex_statet::rename_address(
+bool goto_symex_statet::rename_address(
   exprt &expr,
   const namespacet &ns,
   levelt level)
 {
+  bool result=false;
+
   if(expr.id()==ID_symbol &&
      expr.get_bool(ID_C_SSA_symbol))
   {
@@ -728,36 +739,36 @@ void goto_symex_statet::rename_address(
   else if(expr.id()==ID_symbol)
   {
     expr=ssa_exprt(expr);
-    rename_address(expr, ns, level);
+    result=rename_address(expr, ns, level);
   }
   else
   {
     if(expr.id()==ID_index)
     {
       index_exprt &index_expr=to_index_expr(expr);
 
-      rename_address(index_expr.array(), ns, level);
+      result=rename_address(index_expr.array(), ns, level);
       assert(index_expr.array().type().id()==ID_array);
       expr.type()=index_expr.array().type().subtype();
 
       // the index is not an address
-      rename(index_expr.index(), ns, level);
+      result=rename(index_expr.index(), ns, level) || result;
     }
     else if(expr.id()==ID_if)
     {
       // the condition is not an address
       if_exprt &if_expr=to_if_expr(expr);
-      rename(if_expr.cond(), ns, level);
-      rename_address(if_expr.true_case(), ns, level);
-      rename_address(if_expr.false_case(), ns, level);
+      result=rename(if_expr.cond(), ns, level);
+      result=rename_address(if_expr.true_case(), ns, level) || result;
+      result=rename_address(if_expr.false_case(), ns, level) || result;
 
       if_expr.type()=if_expr.true_case().type();
     }
     else if(expr.id()==ID_member)
     {
       member_exprt &member_expr=to_member_expr(expr);
 
-      rename_address(member_expr.struct_op(), ns, level);
+      result=rename_address(member_expr.struct_op(), ns, level);
 
       // type might not have been renamed in case of nesting of
       // structs and pointers/arrays
@@ -781,9 +792,14 @@ void goto_symex_statet::rename_address(
       // do this recursively; we assume here
       // that all the operands are addresses
       Forall_operands(it, expr)
-        rename_address(*it, ns, level);
+        result=rename_address(*it, ns, level) || result;
     }
   }
+
+  if(result)
+    expr.remove(ID_C_expr_simplified);
+
+  return result;
 }
 
 void goto_symex_statet::rename(
diff --git a/src/goto-symex/goto_symex_state.h b/src/goto-symex/goto_symex_state.h
@@ -148,7 +148,7 @@ class goto_symex_statet
   enum levelt { L0=0, L1=1, L2=2 };
 
   // performs renaming _up to_ the given level
-  void rename(exprt &expr, const namespacet &ns, levelt level=L2);
+  bool rename(exprt &expr, const namespacet &ns, levelt level=L2);
   void rename(
     typet &type,
     const irep_idt &l1_identifier,
@@ -170,7 +170,7 @@ class goto_symex_statet
   void get_original_name(exprt &expr) const;
   void get_original_name(typet &type) const;
 protected:
-  void rename_address(exprt &expr, const namespacet &ns, levelt level);
+  bool rename_address(exprt &expr, const namespacet &ns, levelt level);
 
   void set_ssa_indices(ssa_exprt &expr, const namespacet &ns, levelt level=L2);
   // only required for value_set.assign
diff --git a/src/goto-symex/symex_dereference.cpp b/src/goto-symex/symex_dereference.cpp
@@ -23,44 +23,48 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "goto_symex.h"
 #include "symex_dereference_state.h"
 
-void goto_symext::dereference_rec_address_of(
+bool goto_symext::dereference_rec_address_of(
   exprt &expr,
   statet &state,
   guardt &guard)
 {
+  bool result=false;
+
   // Could be member, could be if, could be index.
 
   if(expr.id()==ID_member)
-    dereference_rec_address_of(
+    result=dereference_rec_address_of(
       to_member_expr(expr).struct_op(), state, guard);
   else if(expr.id()==ID_if)
   {
     // the condition is not an address
-    dereference_rec(
+    result=dereference_rec(
       to_if_expr(expr).cond(), state, guard, false);
 
     // add to guard?
-    dereference_rec_address_of(
-      to_if_expr(expr).true_case(), state, guard);
-    dereference_rec_address_of(
-      to_if_expr(expr).false_case(), state, guard);
+    result=dereference_rec_address_of(
+      to_if_expr(expr).true_case(), state, guard) || result;
+    result=dereference_rec_address_of(
+      to_if_expr(expr).false_case(), state, guard) || result;
   }
   else if(expr.id()==ID_index)
   {
     // the index is not an address
-    dereference_rec(
+    result=dereference_rec(
       to_index_expr(expr).index(), state, guard, false);
 
     // the array _is_ an address
-    dereference_rec_address_of(
-      to_index_expr(expr).array(), state, guard);
+    result=dereference_rec_address_of(
+      to_index_expr(expr).array(), state, guard) || result;
   }
   else
   {
     // give up and dereference
 
-    dereference_rec(expr, state, guard, false);
+    result=dereference_rec(expr, state, guard, false);
   }
+
+  return result;
 }
 
 bool goto_symext::is_index_member_symbol_if(const exprt &expr)
@@ -226,12 +230,14 @@ exprt goto_symext::address_arithmetic(
   return result;
 }
 
-void goto_symext::dereference_rec(
+bool goto_symext::dereference_rec(
   exprt &expr,
   statet &state,
   guardt &guard,
   const bool write)
 {
+  bool result=false;
+
   if(expr.id()==ID_dereference)
   {
     if(expr.operands().size()!=1)
@@ -267,6 +273,8 @@ void goto_symext::dereference_rec(
 
     // this may yield a new auto-object
     trigger_auto_object(expr, state);
+
+    result=true;
   }
   else if(expr.id()==ID_index &&
           to_index_expr(expr).array().id()==ID_member &&
@@ -291,6 +299,8 @@ void goto_symext::dereference_rec(
     dereference_rec(tmp, state, guard, write);
 
     expr.swap(tmp);
+
+    result=true;
   }
   else if(expr.id()==ID_index &&
           to_index_expr(expr).array().type().id()==ID_pointer)
@@ -307,6 +317,8 @@ void goto_symext::dereference_rec(
     const typet &expr_type=ns.follow(expr.type());
     expr=address_arithmetic(object, state, guard,
                             expr_type.subtype().id()==ID_array);
+
+    result=true;
   }
   else if(expr.id()==ID_typecast)
   {
@@ -327,17 +339,24 @@ void goto_symext::dereference_rec(
             from_integer(0, index_type())));
 
       dereference_rec(expr, state, guard, write);
+
+      result=true;
     }
     else
     {
-      dereference_rec(tc_op, state, guard, write);
+      result=dereference_rec(tc_op, state, guard, write) || result;
     }
   }
   else
   {
     Forall_operands(it, expr)
-      dereference_rec(*it, state, guard, write);
+      result=dereference_rec(*it, state, guard, write) || result;
   }
+
+  if(result)
+    expr.remove(ID_C_expr_simplified);
+
+  return result;
 }
 
 void goto_symext::dereference(
diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def
@@ -810,6 +810,7 @@ IREP_ID_ONE(cprover_string_to_upper_case_func)
 IREP_ID_ONE(cprover_string_trim_func)
 IREP_ID_ONE(cprover_string_value_of_func)
 IREP_ID_ONE(array_replace)
+IREP_ID_TWO(C_expr_simplified, #expr_simplified)
 
 #undef IREP_ID_ONE
 #undef IREP_ID_TWO
diff --git a/src/util/replace_expr.cpp b/src/util/replace_expr.cpp
@@ -22,6 +22,9 @@ bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
   Forall_operands(it, dest)
     result=replace_expr(what, by, *it) && result;
 
+  if(!result)
+    dest.remove(ID_C_expr_simplified);
+
   return result;
 }
 
@@ -42,5 +45,8 @@ bool replace_expr(const replace_mapt &what, exprt &dest)
   Forall_operands(it, dest)
     result=replace_expr(what, *it) && result;
 
+  if(!result)
+    dest.remove(ID_C_expr_simplified);
+
   return result;
 }
diff --git a/src/util/replace_symbol.cpp b/src/util/replace_symbol.cpp
@@ -70,6 +70,9 @@ bool replace_symbolt::replace(exprt &dest) const
      !replace(static_cast<typet&>(dest.add(ID_C_va_arg_type))))
     result=false;
 
+  if(!result)
+    dest.remove(ID_C_expr_simplified);
+
   return result;
 }
 
@@ -162,6 +165,9 @@ bool replace_symbolt::replace(typet &dest) const
       result=false;
   }
 
+  if(!result)
+    dest.remove(ID_C_expr_simplified);
+
   return result;
 }
 

Original file line number	Diff line number	Diff line change
`@@ -436,12 +436,13 @@ void goto_symex_statet::set_ssa_indices(`
`436`	`436`	`}`
`437`	`437`	`}`
`438`	`438`
`439`		`-void goto_symex_statet::rename(`
	`439`	`+bool goto_symex_statet::rename(`
`440`	`440`	`exprt &expr,`
`441`	`441`	`const namespacet &ns,`
`442`	`442`	`levelt level)`
`443`	`443`	`{`
`444`	`444`	`// rename all the symbols with their last known value`
	`445`	`+ bool result=false;`
`445`	`446`
`446`	`447`	`if(expr.id()==ID_symbol &&`
`447`	`448`	`expr.get_bool(ID_C_SSA_symbol))`
`@@ -476,7 +477,10 @@ void goto_symex_statet::rename(`
`476`	`477`	`propagation.values.find(ssa.get_identifier());`
`477`	`478`
`478`	`479`	`if(p_it!=propagation.values.end())`
	`480`	`+ {`
`479`	`481`	`expr=p_it->second; // already L2`
	`482`	`+ result=true;`
	`483`	`+ }`
`480`	`484`	`else`
`481`	`485`	`set_ssa_indices(ssa, ns, L2);`
`482`	`486`	`}`
`@@ -493,16 +497,16 @@ void goto_symex_statet::rename(`
`493`	`497`	`ns,`
`494`	`498`	`level);`
`495`	`499`
`496`		`- return;`
	`500`	`+ return false;`
`497`	`501`	`}`
`498`	`502`
`499`	`503`	`expr=ssa_exprt(expr);`
`500`		`- rename(expr, ns, level);`
	`504`	`+ result=rename(expr, ns, level);`
`501`	`505`	`}`
`502`	`506`	`else if(expr.id()==ID_address_of)`
`503`	`507`	`{`
`504`	`508`	`assert(expr.operands().size()==1);`
`505`		`- rename_address(expr.op0(), ns, level);`
	`509`	`+ result=rename_address(expr.op0(), ns, level);`
`506`	`510`	`assert(expr.type().id()==ID_pointer);`
`507`	`511`	`expr.type().subtype()=expr.op0().type();`
`508`	`512`	`}`
`@@ -513,7 +517,7 @@ void goto_symex_statet::rename(`
`513`	`517`
`514`	`518`	`// do this recursively`
`515`	`519`	`Forall_operands(it, expr)`
`516`		`- rename(*it, ns, level);`
	`520`	`+ result=rename(*it, ns, level) \|\| result;`
`517`	`521`
`518`	`522`	`// some fixes`
`519`	`523`	`if(expr.id()==ID_with)`
`@@ -525,6 +529,11 @@ void goto_symex_statet::rename(`
`525`	`529`	`expr.type()=to_if_expr(expr).true_case().type();`
`526`	`530`	`}`
`527`	`531`	`}`
	`532`	`+`
	`533`	`+ if(result)`
	`534`	`+ expr.remove(ID_C_expr_simplified);`
	`535`	`+`
	`536`	`+ return result;`
`528`	`537`	`}`
`529`	`538`
`530`	`539`	`/// thread encoding`
`@@ -709,11 +718,13 @@ bool goto_symex_statet::l2_thread_write_encoding(`
`709`	`718`	`return threads.size()>1;`
`710`	`719`	`}`
`711`	`720`
`712`		`-void goto_symex_statet::rename_address(`
	`721`	`+bool goto_symex_statet::rename_address(`
`713`	`722`	`exprt &expr,`
`714`	`723`	`const namespacet &ns,`
`715`	`724`	`levelt level)`
`716`	`725`	`{`
	`726`	`+ bool result=false;`
	`727`	`+`
`717`	`728`	`if(expr.id()==ID_symbol &&`
`718`	`729`	`expr.get_bool(ID_C_SSA_symbol))`
`719`	`730`	`{`
`@@ -728,36 +739,36 @@ void goto_symex_statet::rename_address(`
`728`	`739`	`else if(expr.id()==ID_symbol)`
`729`	`740`	`{`
`730`	`741`	`expr=ssa_exprt(expr);`
`731`		`- rename_address(expr, ns, level);`
	`742`	`+ result=rename_address(expr, ns, level);`
`732`	`743`	`}`
`733`	`744`	`else`
`734`	`745`	`{`
`735`	`746`	`if(expr.id()==ID_index)`
`736`	`747`	`{`
`737`	`748`	`index_exprt &index_expr=to_index_expr(expr);`
`738`	`749`
`739`		`- rename_address(index_expr.array(), ns, level);`
	`750`	`+ result=rename_address(index_expr.array(), ns, level);`
`740`	`751`	`assert(index_expr.array().type().id()==ID_array);`
`741`	`752`	`expr.type()=index_expr.array().type().subtype();`
`742`	`753`
`743`	`754`	`// the index is not an address`
`744`		`- rename(index_expr.index(), ns, level);`
	`755`	`+ result=rename(index_expr.index(), ns, level) \|\| result;`
`745`	`756`	`}`
`746`	`757`	`else if(expr.id()==ID_if)`
`747`	`758`	`{`
`748`	`759`	`// the condition is not an address`
`749`	`760`	`if_exprt &if_expr=to_if_expr(expr);`
`750`		`- rename(if_expr.cond(), ns, level);`
`751`		`- rename_address(if_expr.true_case(), ns, level);`
`752`		`- rename_address(if_expr.false_case(), ns, level);`
	`761`	`+ result=rename(if_expr.cond(), ns, level);`
	`762`	`+ result=rename_address(if_expr.true_case(), ns, level) \|\| result;`
	`763`	`+ result=rename_address(if_expr.false_case(), ns, level) \|\| result;`
`753`	`764`
`754`	`765`	`if_expr.type()=if_expr.true_case().type();`
`755`	`766`	`}`
`756`	`767`	`else if(expr.id()==ID_member)`
`757`	`768`	`{`
`758`	`769`	`member_exprt &member_expr=to_member_expr(expr);`
`759`	`770`
`760`		`- rename_address(member_expr.struct_op(), ns, level);`
	`771`	`+ result=rename_address(member_expr.struct_op(), ns, level);`
`761`	`772`
`762`	`773`	`// type might not have been renamed in case of nesting of`
`763`	`774`	`// structs and pointers/arrays`
`@@ -781,9 +792,14 @@ void goto_symex_statet::rename_address(`
`781`	`792`	`// do this recursively; we assume here`
`782`	`793`	`// that all the operands are addresses`
`783`	`794`	`Forall_operands(it, expr)`
`784`		`- rename_address(*it, ns, level);`
	`795`	`+ result=rename_address(*it, ns, level) \|\| result;`
`785`	`796`	`}`
`786`	`797`	`}`
	`798`	`+`
	`799`	`+ if(result)`
	`800`	`+ expr.remove(ID_C_expr_simplified);`
	`801`	`+`
	`802`	`+ return result;`
`787`	`803`	`}`
`788`	`804`
`789`	`805`	`void goto_symex_statet::rename(`
Original file line number	Diff line number	Diff line change
`@@ -23,44 +23,48 @@ Author: Daniel Kroening, [email protected]`
`23`	`23`	`#include "goto_symex.h"`
`24`	`24`	`#include "symex_dereference_state.h"`
`25`	`25`
`26`		`-void goto_symext::dereference_rec_address_of(`
	`26`	`+bool goto_symext::dereference_rec_address_of(`
`27`	`27`	`exprt &expr,`
`28`	`28`	`statet &state,`
`29`	`29`	`guardt &guard)`
`30`	`30`	`{`
	`31`	`+ bool result=false;`
	`32`	`+`
`31`	`33`	`// Could be member, could be if, could be index.`
`32`	`34`
`33`	`35`	`if(expr.id()==ID_member)`
`34`		`- dereference_rec_address_of(`
	`36`	`+ result=dereference_rec_address_of(`
`35`	`37`	`to_member_expr(expr).struct_op(), state, guard);`
`36`	`38`	`else if(expr.id()==ID_if)`
`37`	`39`	`{`
`38`	`40`	`// the condition is not an address`
`39`		`- dereference_rec(`
	`41`	`+ result=dereference_rec(`
`40`	`42`	`to_if_expr(expr).cond(), state, guard, false);`
`41`	`43`
`42`	`44`	`// add to guard?`
`43`		`- dereference_rec_address_of(`
`44`		`- to_if_expr(expr).true_case(), state, guard);`
`45`		`- dereference_rec_address_of(`
`46`		`- to_if_expr(expr).false_case(), state, guard);`
	`45`	`+ result=dereference_rec_address_of(`
	`46`	`+ to_if_expr(expr).true_case(), state, guard) \|\| result;`
	`47`	`+ result=dereference_rec_address_of(`
	`48`	`+ to_if_expr(expr).false_case(), state, guard) \|\| result;`
`47`	`49`	`}`
`48`	`50`	`else if(expr.id()==ID_index)`
`49`	`51`	`{`
`50`	`52`	`// the index is not an address`
`51`		`- dereference_rec(`
	`53`	`+ result=dereference_rec(`
`52`	`54`	`to_index_expr(expr).index(), state, guard, false);`
`53`	`55`
`54`	`56`	`// the array _is_ an address`
`55`		`- dereference_rec_address_of(`
`56`		`- to_index_expr(expr).array(), state, guard);`
	`57`	`+ result=dereference_rec_address_of(`
	`58`	`+ to_index_expr(expr).array(), state, guard) \|\| result;`
`57`	`59`	`}`
`58`	`60`	`else`
`59`	`61`	`{`
`60`	`62`	`// give up and dereference`
`61`	`63`
`62`		`- dereference_rec(expr, state, guard, false);`
	`64`	`+ result=dereference_rec(expr, state, guard, false);`
`63`	`65`	`}`
	`66`	`+`
	`67`	`+ return result;`
`64`	`68`	`}`
`65`	`69`
`66`	`70`	`bool goto_symext::is_index_member_symbol_if(const exprt &expr)`
`@@ -226,12 +230,14 @@ exprt goto_symext::address_arithmetic(`
`226`	`230`	`return result;`
`227`	`231`	`}`
`228`	`232`
`229`		`-void goto_symext::dereference_rec(`
	`233`	`+bool goto_symext::dereference_rec(`
`230`	`234`	`exprt &expr,`
`231`	`235`	`statet &state,`
`232`	`236`	`guardt &guard,`
`233`	`237`	`const bool write)`
`234`	`238`	`{`
	`239`	`+ bool result=false;`
	`240`	`+`
`235`	`241`	`if(expr.id()==ID_dereference)`
`236`	`242`	`{`
`237`	`243`	`if(expr.operands().size()!=1)`
`@@ -267,6 +273,8 @@ void goto_symext::dereference_rec(`
`267`	`273`
`268`	`274`	`// this may yield a new auto-object`
`269`	`275`	`trigger_auto_object(expr, state);`
	`276`	`+`
	`277`	`+ result=true;`
`270`	`278`	`}`
`271`	`279`	`else if(expr.id()==ID_index &&`
`272`	`280`	`to_index_expr(expr).array().id()==ID_member &&`
`@@ -291,6 +299,8 @@ void goto_symext::dereference_rec(`
`291`	`299`	`dereference_rec(tmp, state, guard, write);`
`292`	`300`
`293`	`301`	`expr.swap(tmp);`
	`302`	`+`
	`303`	`+ result=true;`
`294`	`304`	`}`
`295`	`305`	`else if(expr.id()==ID_index &&`
`296`	`306`	`to_index_expr(expr).array().type().id()==ID_pointer)`
`@@ -307,6 +317,8 @@ void goto_symext::dereference_rec(`
`307`	`317`	`const typet &expr_type=ns.follow(expr.type());`
`308`	`318`	`expr=address_arithmetic(object, state, guard,`
`309`	`319`	`expr_type.subtype().id()==ID_array);`
	`320`	`+`
	`321`	`+ result=true;`
`310`	`322`	`}`
`311`	`323`	`else if(expr.id()==ID_typecast)`
`312`	`324`	`{`
`@@ -327,17 +339,24 @@ void goto_symext::dereference_rec(`
`327`	`339`	`from_integer(0, index_type())));`
`328`	`340`
`329`	`341`	`dereference_rec(expr, state, guard, write);`
	`342`	`+`
	`343`	`+ result=true;`
`330`	`344`	`}`
`331`	`345`	`else`
`332`	`346`	`{`
`333`		`- dereference_rec(tc_op, state, guard, write);`
	`347`	`+ result=dereference_rec(tc_op, state, guard, write) \|\| result;`
`334`	`348`	`}`
`335`	`349`	`}`
`336`	`350`	`else`
`337`	`351`	`{`
`338`	`352`	`Forall_operands(it, expr)`
`339`		`- dereference_rec(*it, state, guard, write);`
	`353`	`+ result=dereference_rec(*it, state, guard, write) \|\| result;`
`340`	`354`	`}`
	`355`	`+`
	`356`	`+ if(result)`
	`357`	`+ expr.remove(ID_C_expr_simplified);`
	`358`	`+`
	`359`	`+ return result;`
`341`	`360`	`}`
`342`	`361`
`343`	`362`	`void goto_symext::dereference(`
Original file line number	Diff line number	Diff line change
`@@ -70,6 +70,9 @@ bool replace_symbolt::replace(exprt &dest) const`
`70`	`70`	`!replace(static_cast<typet&>(dest.add(ID_C_va_arg_type))))`
`71`	`71`	`result=false;`
`72`	`72`
	`73`	`+ if(!result)`
	`74`	`+ dest.remove(ID_C_expr_simplified);`
	`75`	`+`
`73`	`76`	`return result;`
`74`	`77`	`}`
`75`	`78`
`@@ -162,6 +165,9 @@ bool replace_symbolt::replace(typet &dest) const`
`162`	`165`	`result=false;`
`163`	`166`	`}`
`164`	`167`
	`168`	`+ if(!result)`
	`169`	`+ dest.remove(ID_C_expr_simplified);`
	`170`	`+`
`165`	`171`	`return result;`
`166`	`172`	`}`
`167`	`173`