DEBUGGING

Author: tautschnig

src/util/simplify_expr.cpp

@@ -29,10 +29,10 @@ Author: Daniel Kroening, [email protected]
 
 // #define DEBUGX
 
-#ifdef DEBUGX
+//#ifdef DEBUGX
 #include "format_expr.h"
 #include <iostream>
-#endif
+//#endif
 
 #include "simplify_expr_class.h"
 
@@ -2312,7 +2312,27 @@ bool simplify_exprt::simplify_rec(exprt &expr)
 
   if(!result)
   {
-    POSTCONDITION(type_eq(tmp.type(), expr.type(), ns));
+#if 0
+    if(tmp.type().id() == ID_pointer && expr.type().id() == ID_pointer)
+    {
+      const pointer_typet &old_type = to_pointer_type(expr.type());
+      const pointer_typet &new_type = to_pointer_type(tmp.type());
+      POSTCONDITION(old_type.get_width() == new_type.get_width());
+      POSTCONDITION(type_eq(old_type.subtype(), new_type.subtype(), ns));
+    }
+    else
+    {
+#endif
+      if(tmp.type() != expr.type())
+      {
+        std::cerr << "expr=" << expr.pretty() << std::endl;
+        std::cerr << "tmp=" << tmp.pretty() << std::endl;
+        std::cerr << "AFTER SIMP: " << expr.id() << " to " << tmp.id() << std::endl;
+      }
+      POSTCONDITION(type_eq(tmp.type(), expr.type(), ns));
+      POSTCONDITION(tmp.type() == expr.type());
+    //}
+    //POSTCONDITION(type_eq(tmp.type(), expr.type(), ns));
     expr.swap(tmp);
 
     #ifdef USE_CACHE