From 96a70142f3f5cc9a5eee1e4e3240921ea2b48041 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 22 Jun 2018 12:26:15 +0100
Subject: [PATCH] Explicit type cast to avoid signed/unsigned warning

---
 jbmc/src/java_bytecode/object_factory_parameters.h | 3 ++-
 src/solvers/sat/satcheck_minisat2.cpp              | 5 ++++-
 2 files changed, 6 insertions(+), 2 deletions(-)

diff --git a/jbmc/src/java_bytecode/object_factory_parameters.h b/jbmc/src/java_bytecode/object_factory_parameters.h
index 13eb09bf030..50491a12156 100644
--- a/jbmc/src/java_bytecode/object_factory_parameters.h
+++ b/jbmc/src/java_bytecode/object_factory_parameters.h
@@ -15,7 +15,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/irep.h>
 
 #define MAX_NONDET_ARRAY_LENGTH_DEFAULT 5
-#define MAX_NONDET_STRING_LENGTH std::numeric_limits<std::int32_t>::max()
+#define MAX_NONDET_STRING_LENGTH \
+  static_cast<std::size_t>(std::numeric_limits<std::int32_t>::max())
 #define MAX_NONDET_TREE_DEPTH 5
 #define MAX_NONNULL_TREE_DEPTH 0
 
diff --git a/src/solvers/sat/satcheck_minisat2.cpp b/src/solvers/sat/satcheck_minisat2.cpp
index 43e41ce163d..59c48d517f3 100644
--- a/src/solvers/sat/satcheck_minisat2.cpp
+++ b/src/solvers/sat/satcheck_minisat2.cpp
@@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <unistd.h>
 #endif
 
+#include <limits>
 #include <stack>
 
 #include <util/invariant.h>
@@ -28,7 +29,9 @@ Author: Daniel Kroening, kroening@kroening.com
 
 void convert(const bvt &bv, Minisat::vec<Minisat::Lit> &dest)
 {
-  dest.capacity(bv.size());
+  PRECONDITION(
+    bv.size() <= static_cast<std::size_t>(std::numeric_limits<int>::max()));
+  dest.capacity(static_cast<int>(bv.size()));
 
   forall_literals(it, bv)
     if(!it->is_false())