diff --git a/osra.cpp b/osra.cpp
index 65b43507b..08295bd05 100644
--- a/osra.cpp
+++ b/osra.cpp
@@ -592,7 +592,8 @@ void OSRA::handleLogicalOperator(Instruction *I) {
 // TODO: give a better name
 BoundedValue OSRA::mergePredicate(OSR &BaseOp, Predicate P, Constant *ConstOp) {
   const Value *V = BaseOp.boundedValue()->value();
-  bool IsSigned = BaseOp.boundedValue()->isSigned();
+  bool HasSignedness = BaseOp.boundedValue()->hasSignedness();
+  bool IsSigned = HasSignedness ? BaseOp.boundedValue()->isSigned() : false;
   // Solve the equation to obtain the new boundary value
   // x <  1.5 == x <  2 (Ceiling)
   // x <= 1.5 == x <= 1 (Floor)
@@ -633,10 +634,16 @@ BoundedValue OSRA::mergePredicate(OSR &BaseOp, Predicate P, Constant *ConstOp) {
     return BoundedValue::createLE(V, NewBound, IsSigned);
 
   case CmpInst::ICMP_EQ:
-    return BoundedValue::createEQ(V, NewBound, IsSigned);
+    if (HasSignedness)
+      return BoundedValue::createEQ(V, NewBound, IsSigned);
+    else
+      return BoundedValue::createConstant(V, NewBound);
 
   case CmpInst::ICMP_NE:
-    return BoundedValue::createNE(V, NewBound, IsSigned);
+    if (HasSignedness)
+      return BoundedValue::createNE(V, NewBound, IsSigned);
+    else
+      return BoundedValue::createNegatedConstant(V, NewBound);
 
   default:
     llvm_unreachable("Unexpected comparison operator");
@@ -658,22 +665,12 @@ Optional<BoundedValue> OSRA::applyConstraint(Instruction *I,
 
   // Notify the BV about the sign we're going to use, unless it's a comparison
   // of (in)equality
-  bool IsSigned;
-  if (P != CmpInst::ICMP_EQ && P != CmpInst::ICMP_NE) {
-    IsSigned = ICmpInst::isSigned(P);
-    BVs.setSignedness(BB, OriginalBV->value(), IsSigned);
-  } else {
-    // TODO: we don't know what sign to use here, so we ignore it, should we
-    //       switch to AnySignedness?
-    if (!OriginalBV->hasSignedness())
-      return Optional<BoundedValue>();
-
-    IsSigned = OriginalBV->isSigned();
-  }
+  if (P != CmpInst::ICMP_EQ && P != CmpInst::ICMP_NE)
+    BVs.setSignedness(BB, OriginalBV->value(), ICmpInst::isSigned(P));
 
   // If setting the sign we went to bottom or still don't have it (e.g., due to
   // being top), give up
-  if (OriginalBV->isBottom() || !OriginalBV->hasSignedness())
+  if (OriginalBV->isBottom())
     return Optional<BoundedValue>();
 
   BoundedValue Result = mergePredicate(BaseOp, P, ConstOp);
@@ -1711,7 +1708,9 @@ void BoundedValue::describe(formatted_raw_ostream &O) const {
   } else if (!isUninitialized()) {
     for (auto Bound : Bounds) {
       O << ", [";
-      if (!isConstant() && Bound.first == lowerExtreme()) {
+      if (!isConstant()
+          && hasSignedness()
+          && Bound.first == lowerExtreme()) {
         O << "min";
       } else {
         O << Bound.first;
@@ -1719,7 +1718,9 @@ void BoundedValue::describe(formatted_raw_ostream &O) const {
 
       O << ", ";
 
-      if (!isConstant() && Bound.second == upperExtreme()) {
+      if (!isConstant()
+          && hasSignedness()
+          && Bound.second == upperExtreme()) {
         O << "max";
       } else {
         O << Bound.second;
@@ -1775,8 +1776,10 @@ void OSRA::describe(formatted_raw_ostream &O, const Instruction *I) const {
 Constant *OSR::solveEquation(Constant *KnownTerm,
                              bool CeilingRounding,
                              const DataLayout &DL) {
-  // (KnownTerm - Base) udiv Factor
-  bool IsSigned = BV->isSigned();
+  // TODO: we're assuming unsigned if no signedness
+  // (KnownTerm - Base) div Factor
+  bool HasSignedness = BV->hasSignedness();
+  bool IsSigned = HasSignedness ? BV->isSigned() : false;
 
   auto *BaseConst = CI::get(KnownTerm->getType(), Base, IsSigned);
   auto *Numerator = CE::getSub(KnownTerm, BaseConst);
@@ -1784,14 +1787,31 @@ Constant *OSR::solveEquation(Constant *KnownTerm,
 
   Constant *Remainder = nullptr;
   Constant *Division = nullptr;
-  if (IsSigned) {
-    Remainder = CE::getSRem(Numerator, Denominator);
-    Division = CE::getSDiv(Numerator, Denominator);
-  } else {
-    Remainder = CE::getURem(Numerator, Denominator);
-    Division = CE::getUDiv(Numerator, Denominator);
+
+  Constant *SignedRemainder = nullptr;
+  Constant *SignedDivision = nullptr;
+  if (IsSigned or not HasSignedness) {
+    SignedRemainder = CE::getSRem(Numerator, Denominator);
+    SignedDivision = CE::getSDiv(Numerator, Denominator);
+    Remainder = SignedRemainder;
+    Division = SignedDivision;
   }
 
+  Constant *UnsignedRemainder = nullptr;
+  Constant *UnsignedDivision = nullptr;
+  if (not IsSigned or not HasSignedness) {
+    UnsignedRemainder = CE::getURem(Numerator, Denominator);
+    UnsignedDivision = CE::getUDiv(Numerator, Denominator);
+    Remainder = UnsignedRemainder;
+    Division = UnsignedDivision;
+  }
+
+  // If we no signedness but it would produce different results, bail out
+  if (not HasSignedness
+      and (SignedRemainder != UnsignedRemainder
+           or SignedDivision != UnsignedDivision))
+    return UndefValue::get(Division->getType());
+
   if (isa<UndefValue>(Division))
     return Division;
 
@@ -1967,8 +1987,10 @@ void OSRA::mergeLoadReacher(LoadInst *Load) {
     OSR ReachingOSR = P.second;
     if (ReachingOSR != Result) {
       OSR FreeOSR = createOSR(Load, Load->getParent());
-      if (Reachers.size() == RDP.getReachingDefinitionsCount(Load))
-        BVs.forceBV(Load, pathSensitiveMerge(Load));
+      if (Reachers.size() == RDP.getReachingDefinitionsCount(Load)) {
+        BoundedValue NewBVs = pathSensitiveMerge(Load);
+        BVs.forceBV(Load, NewBVs);
+      }
       OSRs.insert({ Load, FreeOSR });
       return;
     }
@@ -2596,10 +2618,13 @@ BoundedValue BoundedValue::mergeImpl(const BoundedValue &Other) const {
 }
 
 template<BoundedValue::MergeType MT>
-bool BoundedValue::merge(const BoundedValue &Other,
+bool BoundedValue::merge(BoundedValue Other,
                          const DataLayout &DL,
                          Type *Int64) {
 
+  if (*this == Other)
+    return false;
+
   if (MT == And) {
     // x & bottom = bottom
     if (Bottom)
@@ -2640,8 +2665,12 @@ bool BoundedValue::merge(const BoundedValue &Other,
   }
 
   if (Sign == AnySignedness || Other.Sign == AnySignedness) {
-    if (Sign == AnySignedness)
+    if (Sign == AnySignedness) {
       Sign = Other.Sign;
+    } else {
+      assert(hasSignedness());
+      Other.setSignedness(Sign == Signed);
+    }
   } else {
     setSignedness(Other.isSigned());
   }
diff --git a/osra.h b/osra.h
index 028a96558..fa1f9e0af 100644
--- a/osra.h
+++ b/osra.h
@@ -122,7 +122,7 @@ public:
 
     /// \brief Merge \p Other using the \p MT policy
     template<MergeType MT=And>
-    bool merge(const BoundedValue &Other,
+    bool merge(BoundedValue Other,
                const llvm::DataLayout &DL,
                llvm::Type *Int64);
 
@@ -146,6 +146,14 @@ public:
         return Bounds[0].second == upperExtreme();
     }
 
+    uint64_t lowerBound() const {
+      assert(isRightOpen());
+      if (Negated)
+        return Bounds[0].second;
+      else
+        return Bounds[0].first;
+    }
+
     /// \brief If the BV is limited, return its bounds considering negation
     ///
     /// Do not invoke this method on unlimited BVs.
@@ -167,6 +175,9 @@ public:
       } else if (UpperBound == upperExtreme()) {
         return std::make_pair(CI::get(Int64, lowerExtreme(), isSigned()),
                               CI::get(Int64, LowerBound - 1, isSigned()));
+      } else if (Negated) {
+        return std::make_pair(CI::get(Int64, UpperBound + 1, isSigned()),
+                              CI::get(Int64, LowerBound - 1, isSigned()));
       }
 
       assert(false && "The BV is unlimited");
@@ -281,8 +292,8 @@ public:
     }
 
     static BoundedValue createLE(const llvm::Value *V,
-				 uint64_t Value,
-				 bool Sign) {
+                                 uint64_t Value,
+                                 bool Sign) {
       BoundedValue Result(V);
       Result.setSignedness(Sign);
       Result.Bounds = BoundsVector { { Result.lowerExtreme(), Value } };
@@ -313,6 +324,13 @@ public:
       return Result;
     }
 
+    static BoundedValue createNegatedConstant(const llvm::Value *V,
+                                              uint64_t Value) {
+      BoundedValue Result = createConstant(V, Value);
+      Result.flip();
+      return Result;
+    }
+
     static BoundedValue createBottom(const llvm::Value *V) {
       BoundedValue Result(V);
       Result.setBottom();
@@ -489,7 +507,7 @@ public:
       BV = NewBV;
     }
 
-    /// \brief Accessor method to BoundedValue associate to this OSR
+    /// \brief Accessor method to BoundedValue associated to this OSR
     const BoundedValue *boundedValue() const {
       assert(BV != nullptr);
       return BV;
@@ -606,6 +624,9 @@ public:
     /// \brief Return the size of the associated BoundedValue
     uint64_t size() const { return BV->size(); }
 
+    /// \brief Accessor to the factor value of this OSR (`b`)
+    uint64_t base() const { return Base; }
+
     /// \brief Accessor to the factor value of this OSR (`b`)
     uint64_t factor() const { return Factor; }
 
diff --git a/set.cpp b/set.cpp
index 42fc3d20f..62e3546e2 100644
--- a/set.cpp
+++ b/set.cpp
@@ -545,7 +545,7 @@ bool SET::handleInstructionWithOSRA(Instruction *Target, Value *V) {
     OS.explore(CI::get(Int64, O->constant()));
   } else {
     // Hard limit
-    if (O->size() >= 10000)
+    if (not O->boundedValue()->hasSignedness() or O->size() >= 10000)
       return false;
 
     // We have a limited range, let's use it all