Do not perform SSA sanity checks

Iterating over all expression tress has considerable performance cost,
seemingly accounting for up to 10% of runtime (on SV-COMP benchmarks,
with profiling enabled).

Author: tautschnig

src/goto-symex/goto_symex_state.cpp

@@ -38,6 +38,7 @@ goto_symex_statet::goto_symex_statet()
 
 goto_symex_statet::~goto_symex_statet()=default;
 
+#if 0
 /// write to a variable
 static bool check_renaming(const exprt &expr);
 
@@ -120,10 +121,11 @@ static bool check_renaming(const exprt &expr)
 
   return false;
 }
+#endif
 
 static void assert_l1_renaming(const exprt &expr)
 {
-  #if 1
+  #if 0
   if(check_renaming_l1(expr))
   {
     std::cerr << expr.pretty() << '\n';
@@ -136,7 +138,7 @@ static void assert_l1_renaming(const exprt &expr)
 
 static void assert_l2_renaming(const exprt &expr)
 {
-  #if 1
+  #if 0
   if(check_renaming(expr))
   {
     std::cerr << expr.pretty() << '\n';