From 2c84b3a9c867acab8cefd0011845a252869ce223 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <kroening@cs.ox.ac.uk>
Date: Mon, 19 Jun 2017 20:53:29 +0100
Subject: [PATCH 1/2] add empty() to container-like classes with size()

---
 src/pointer-analysis/value_set_fivr.h     | 17 +++++++++--------
 src/pointer-analysis/value_set_fivrns.cpp |  2 +-
 src/pointer-analysis/value_set_fivrns.h   | 17 +++++++++--------
 3 files changed, 19 insertions(+), 17 deletions(-)

diff --git a/src/pointer-analysis/value_set_fivr.h b/src/pointer-analysis/value_set_fivr.h
index 92c5ab45b37..66adf837394 100644
--- a/src/pointer-analysis/value_set_fivr.h
+++ b/src/pointer-analysis/value_set_fivr.h
@@ -84,12 +84,13 @@ class value_set_fivrt
     typedef objmapt::iterator iterator;
 
     const_iterator find(unsigned k) { return objmap.find(k); }
-    iterator begin(void) { return objmap.begin(); }
-    const_iterator begin(void) const { return objmap.begin(); }
-    iterator end(void) { return objmap.end(); }
-    const_iterator end(void) const { return objmap.end(); }
-    size_t size(void) const { return objmap.size(); }
-    void clear(void) { objmap.clear(); validity_ranges.clear(); }
+    iterator begin() { return objmap.begin(); }
+    const_iterator begin() const { return objmap.begin(); }
+    iterator end() { return objmap.end(); }
+    const_iterator end() const { return objmap.end(); }
+    size_t size() const { return objmap.size(); }
+    bool empty() const { return objmap.empty(); }
+    void clear() { objmap.clear(); validity_ranges.clear(); }
 
     objectt &operator[](unsigned k)
     {
@@ -112,7 +113,7 @@ class value_set_fivrt
       unsigned function;
       unsigned from, to;
 
-      validity_ranget(void):
+      validity_ranget():
         function(0), from(0), to(0)
       {
       }
@@ -318,7 +319,7 @@ class value_set_fivrt
     const exprt &code,
     const namespacet &ns);
 
-  bool handover(void);
+  bool handover();
 
   void assign(
     const exprt &lhs,
diff --git a/src/pointer-analysis/value_set_fivrns.cpp b/src/pointer-analysis/value_set_fivrns.cpp
index 63373e09226..0d10df43d5d 100644
--- a/src/pointer-analysis/value_set_fivrns.cpp
+++ b/src/pointer-analysis/value_set_fivrns.cpp
@@ -1508,7 +1508,7 @@ bool value_set_fivrnst::object_map_dt::is_valid_at(
   return false;
 }
 
-bool value_set_fivrnst::handover(void)
+bool value_set_fivrnst::handover()
 {
   bool changed=false;
 
diff --git a/src/pointer-analysis/value_set_fivrns.h b/src/pointer-analysis/value_set_fivrns.h
index 5ce1d4464c6..e01db014cbd 100644
--- a/src/pointer-analysis/value_set_fivrns.h
+++ b/src/pointer-analysis/value_set_fivrns.h
@@ -85,12 +85,13 @@ class value_set_fivrnst
     typedef objmapt::iterator iterator;
 
     const_iterator find(unsigned k) { return objmap.find(k); }
-    iterator begin(void) { return objmap.begin(); }
-    const_iterator begin(void) const { return objmap.begin(); }
-    iterator end(void) { return objmap.end(); }
-    const_iterator end(void) const { return objmap.end(); }
-    size_t size(void) const { return objmap.size(); }
-    void clear(void) { objmap.clear(); validity_ranges.clear(); }
+    iterator begin() { return objmap.begin(); }
+    const_iterator begin() const { return objmap.begin(); }
+    iterator end() { return objmap.end(); }
+    const_iterator end() const { return objmap.end(); }
+    size_t size() const { return objmap.size(); }
+    bool empty() const { return objmap.empty(); }
+    void clear() { objmap.clear(); validity_ranges.clear(); }
 
     objectt &operator[](unsigned k)
     {
@@ -113,7 +114,7 @@ class value_set_fivrnst
       unsigned function;
       unsigned from, to;
 
-      validity_ranget(void):
+      validity_ranget():
         function(0), from(0), to(0)
       {
       }
@@ -315,7 +316,7 @@ class value_set_fivrnst
     const exprt &code,
     const namespacet &ns);
 
-  bool handover(void);
+  bool handover();
 
   void assign(
     const exprt &lhs,

From 7181e417344afdcae09028027026a2a5ac6b9338 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <kroening@cs.ox.ac.uk>
Date: Mon, 19 Jun 2017 21:33:51 +0100
Subject: [PATCH 2/2] missing header

---
 src/solvers/sat/satcheck_minisat2.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/solvers/sat/satcheck_minisat2.cpp b/src/solvers/sat/satcheck_minisat2.cpp
index fe9ed4527ca..5fa9e44b132 100644
--- a/src/solvers/sat/satcheck_minisat2.cpp
+++ b/src/solvers/sat/satcheck_minisat2.cpp
@@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <stack>
 
 #include <util/threeval.h>
+#include <util/invariant.h>
 
 #include "satcheck_minisat2.h"