Merge pull request #32 from tautschnig/merge_irept-loses-comments

merge_irept should not destroy comments (but it may ignore differences)

Author: kroening

src/util/merge_irep.cpp

@@ -200,6 +200,17 @@ const irept& merge_irept::merged(const irept &irep)
     dest_named_sub[it->first]=merged(it->second); // recursive call
     #endif
 
+  const irept::named_subt &src_comments=irep.get_comments();
+  irept::named_subt &dest_comments=new_irep.get_comments();
+
+  forall_named_irep(it, src_comments)
+    #ifdef SUB_IS_LIST
+    dest_comments.push_back(
+      std::make_pair(it->first, merged(it->second))); // recursive call
+    #else
+    dest_comments[it->first]=merged(it->second); // recursive call
+    #endif
+
   return *irep_store.insert(new_irep).first;
 }