Fix invariant warnings

Author: reuk

src/goto-instrument/wmm/data_dp.cpp

@@ -13,6 +13,7 @@ Date: 2012
 
 #include "data_dp.h"
 
+#include <util/invariant.h>
 #include <util/message.h>
 
 #include "abstract_event.h"
@@ -151,7 +152,7 @@ void data_dpt::dp_merge()
       it3->eq_class=to;
 
   /* strictly monotonous => converges */
-  assert(initial_size>data.size());
+  INVARIANT(initial_size>data.size(), "strictly monotonous => converges");
 
   /* repeat until classes are disjunct */
   dp_merge();

src/goto-instrument/wmm/event_graph.h

@@ -20,6 +20,7 @@ Date: 2012
 #include <iosfwd>
 
 #include <util/graph.h>
+#include <util/invariant.h>
 
 #include "abstract_event.h"
 #include "data_dp.h"
@@ -213,7 +214,7 @@ class event_grapht
       {
         critical_cyclet reduced(egraph, id);
         this->hide_internals(reduced);
-        assert(!reduced.data.empty());
+        INVARIANT(!reduced.data.empty(), "reduced must not be empty");
         return print_name(reduced, model);
       }
       else

src/util/numbering.h

@@ -15,6 +15,7 @@ Author: Daniel Kroening, [email protected]
 #include <unordered_map>
 #include <vector>
 
+#include <util/invariant.h>
 
 template <typename T>
 // NOLINTNEXTLINE(readability/identifiers)
@@ -48,7 +49,7 @@ class numbering final
     if(result.second) // inserted?
     {
       data.push_back(a);
-      assert(data.size()==numbers.size());
+      INVARIANT(data.size()==numbers.size(), "vector sizes must match");
     }
 
     return (result.first)->second;

src/util/union_find.h

@@ -238,7 +238,7 @@ class union_find final
     if(n>=uuf.size())
       uuf.resize(numbers.size());
 
-    assert(uuf.size()==numbers.size());
+    INVARIANT(uuf.size()==numbers.size(), "container sizes must match");
 
     return n;
   }