diff --git a/include/klee/Expr/Constraints.h b/include/klee/Expr/Constraints.h
index f4c0e22db8..3809238a1b 100644
--- a/include/klee/Expr/Constraints.h
+++ b/include/klee/Expr/Constraints.h
@@ -17,7 +17,6 @@
 #include "klee/Expr/Expr.h"
 #include "klee/Expr/ExprHashMap.h"
 #include "klee/Expr/ExprUtil.h"
-#include "klee/Expr/IndependentConstraintSetUnion.h"
 #include "klee/Expr/IndependentSet.h"
 #include "klee/Expr/Path.h"
 #include "klee/Expr/Symcrete.h"
diff --git a/include/klee/Expr/IndependentSet.h b/include/klee/Expr/IndependentSet.h
index cbcf9ec752..c2aeb7173f 100644
--- a/include/klee/Expr/IndependentSet.h
+++ b/include/klee/Expr/IndependentSet.h
@@ -23,6 +23,7 @@ DISABLE_WARNING_POP
 
 namespace klee {
 using ExprOrSymcrete = either<Expr, Symcrete>;
+class IndependentConstraintSetUnion;
 
 struct ExprOrSymcreteHash {
   unsigned operator()(const ref<ExprOrSymcrete> &e) const { return e->hash(); }
@@ -97,9 +98,7 @@ inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os,
 
 class IndependentConstraintSet {
 private:
-  using InnerSetUnion =
-      DisjointSetUnion<ref<ExprOrSymcrete>, IndependentConstraintSet,
-                       ExprOrSymcreteHash, ExprOrSymcreteCmp>;
+  using InnerSetUnion = IndependentConstraintSetUnion;
 
   void initIndependentConstraintSet(ref<Expr> e);
   void initIndependentConstraintSet(ref<Symcrete> s);
@@ -119,7 +118,7 @@ class IndependentConstraintSet {
 
   Assignment concretization;
 
-  InnerSetUnion concretizedSets;
+  std::shared_ptr<InnerSetUnion> concretizedSets;
 
   ref<const IndependentConstraintSet> addExpr(ref<Expr> e) const;
   ref<const IndependentConstraintSet>
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 575e8299cd..feb34f4470 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -48,6 +48,7 @@
 #include "klee/Expr/ExprPPrinter.h"
 #include "klee/Expr/ExprSMTLIBPrinter.h"
 #include "klee/Expr/ExprUtil.h"
+#include "klee/Expr/IndependentConstraintSetUnion.h"
 #include "klee/Expr/IndependentSet.h"
 #include "klee/Expr/Symcrete.h"
 #include "klee/Module/Cell.h"
@@ -1884,9 +1885,9 @@ void Executor::unwindToNextLandingpad(ExecutionState &state) {
   UnwindingInformation *ui = state.unwindingInformation.get();
   assert(ui && "unwinding without unwinding information");
 
-  std::size_t startIndex;
-  std::size_t lowestStackIndex;
-  bool popFrames;
+  std::size_t startIndex = 0;
+  std::size_t lowestStackIndex = 0;
+  bool popFrames = false;
 
   if (auto *sui = dyn_cast<SearchPhaseUnwindingInformation>(ui)) {
     startIndex = sui->unwindingProgress;
diff --git a/lib/Expr/Constraints.cpp b/lib/Expr/Constraints.cpp
index b88c204555..7669baad7d 100644
--- a/lib/Expr/Constraints.cpp
+++ b/lib/Expr/Constraints.cpp
@@ -15,6 +15,7 @@
 #include "klee/Expr/ExprHashMap.h"
 #include "klee/Expr/ExprUtil.h"
 #include "klee/Expr/ExprVisitor.h"
+#include "klee/Expr/IndependentConstraintSetUnion.h"
 #include "klee/Expr/IndependentSet.h"
 #include "klee/Expr/Path.h"
 #include "klee/Expr/Symcrete.h"
diff --git a/lib/Expr/IndependentConstraintSetUnion.cpp b/lib/Expr/IndependentConstraintSetUnion.cpp
index b2c67e5a14..ba0b57026c 100644
--- a/lib/Expr/IndependentConstraintSetUnion.cpp
+++ b/lib/Expr/IndependentConstraintSetUnion.cpp
@@ -1,5 +1,8 @@
 #include "klee/Expr/IndependentConstraintSetUnion.h"
 
+#include "klee/ADT/DisjointSetUnion.h"
+#include "klee/Expr/IndependentSet.h"
+
 namespace klee {
 
 IndependentConstraintSetUnion::IndependentConstraintSetUnion() {}
@@ -152,10 +155,11 @@ IndependentConstraintSetUnion::getConcretizedVersion() {
     ref<const IndependentConstraintSet> root = disjointSets.at(i);
     if (root->concretization.bindings.empty()) {
       for (ref<Expr> expr : root->exprs) {
-        icsu.addValue(new ExprOrSymcrete::left(expr));
+        icsu.addExpr(expr);
       }
     } else {
-      icsu.add(root->concretizedSets);
+      root->concretizedSets->calculateQueue();
+      icsu.add(*root->concretizedSets.get());
     }
     icsu.concretization.addIndependentAssignment(root->concretization);
   }
@@ -178,7 +182,15 @@ void IndependentConstraintSetUnion::calculateQueue() {
   calculateUpdateConcretizationQueue();
   calculateRemoveConcretizationQueue();
   while (!constraintQueue.empty()) {
-    addValue(constraintQueue[constraintQueue.size() - 1]);
+    auto constraint = constraintQueue[constraintQueue.size() - 1];
+    if (auto expr = dyn_cast<ExprOrSymcrete::left>(constraint)) {
+      if (auto ce = dyn_cast<ConstantExpr>(expr->value())) {
+        assert(ce->isTrue() && "Attempt to add invalid constraint");
+        constraintQueue.pop_back();
+        continue;
+      }
+    }
+    addValue(constraint);
     constraintQueue.pop_back();
   }
   calculateUpdateConcretizationQueue();
diff --git a/lib/Expr/IndependentSet.cpp b/lib/Expr/IndependentSet.cpp
index 888dc52fdd..79e3fad63e 100644
--- a/lib/Expr/IndependentSet.cpp
+++ b/lib/Expr/IndependentSet.cpp
@@ -5,6 +5,7 @@
 #include "klee/Expr/Constraints.h"
 #include "klee/Expr/ExprHashMap.h"
 #include "klee/Expr/ExprUtil.h"
+#include "klee/Expr/IndependentConstraintSetUnion.h"
 #include "klee/Expr/SymbolicSource.h"
 #include "klee/Expr/Symcrete.h"
 #include "klee/Solver/Solver.h"
@@ -29,32 +30,20 @@ IndependentConstraintSet::updateConcretization(
   InnerSetUnion DSU;
   for (ref<Expr> i : exprs) {
     ref<Expr> e = ics->concretization.evaluate(i);
-    if (auto ce = dyn_cast<ConstantExpr>(e)) {
-      assert(ce->isTrue() && "Attempt to add invalid constraint");
-      continue;
-    }
     concretizedExprs[i] = e;
-    DSU.addValue(new ExprOrSymcrete::left(e));
+    DSU.addExpr(e);
   }
   for (ref<Symcrete> s : symcretes) {
     ref<Expr> e = EqExpr::create(ics->concretization.evaluate(s->symcretized),
                                  s->symcretized);
-    if (auto ce = dyn_cast<ConstantExpr>(e)) {
-      assert(ce->isTrue() && "Attempt to add invalid constraint");
-      continue;
-    }
-    DSU.addValue(new ExprOrSymcrete::left(e));
+    DSU.addExpr(e);
   }
   auto concretizationConstraints =
       ics->concretization.createConstraintsFromAssignment();
   for (ref<Expr> e : concretizationConstraints) {
-    if (auto ce = dyn_cast<ConstantExpr>(e)) {
-      assert(ce->isTrue() && "Attempt to add invalid constraint");
-      continue;
-    }
-    DSU.addValue(new ExprOrSymcrete::left(e));
+    DSU.addExpr(e);
   }
-  ics->concretizedSets = DSU;
+  ics->concretizedSets.reset(new InnerSetUnion(DSU));
   return ics;
 }
 
@@ -71,33 +60,21 @@ IndependentConstraintSet::removeConcretization(
   InnerSetUnion DSU;
   for (ref<Expr> i : exprs) {
     ref<Expr> e = ics->concretization.evaluate(i);
-    if (auto ce = dyn_cast<ConstantExpr>(e)) {
-      assert(ce->isTrue() && "Attempt to add invalid constraint");
-      continue;
-    }
     concretizedExprs[i] = e;
-    DSU.addValue(new ExprOrSymcrete::left(e));
+    DSU.addExpr(e);
   }
   for (ref<Symcrete> s : symcretes) {
     ref<Expr> e = EqExpr::create(ics->concretization.evaluate(s->symcretized),
                                  s->symcretized);
-    if (auto ce = dyn_cast<ConstantExpr>(e)) {
-      assert(ce->isTrue() && "Attempt to add invalid constraint");
-      continue;
-    }
-    DSU.addValue(new ExprOrSymcrete::left(e));
+    DSU.addExpr(e);
   }
   auto concretizationConstraints =
       ics->concretization.createConstraintsFromAssignment();
   for (ref<Expr> e : concretizationConstraints) {
-    if (auto ce = dyn_cast<ConstantExpr>(e)) {
-      assert(ce->isTrue() && "Attempt to add invalid constraint");
-      continue;
-    }
-    DSU.addValue(new ExprOrSymcrete::left(e));
+    DSU.addExpr(e);
   }
 
-  ics->concretizedSets = DSU;
+  ics->concretizedSets.reset(new InnerSetUnion(DSU));
   return ics;
 }
 
@@ -346,32 +323,20 @@ IndependentConstraintSet::merge(ref<const IndependentConstraintSet> A,
     InnerSetUnion DSU;
     for (ref<Expr> i : a->exprs) {
       ref<Expr> e = a->concretization.evaluate(i);
-      if (auto ce = dyn_cast<ConstantExpr>(e)) {
-        assert(ce->isTrue() && "Attempt to add invalid constraint");
-        continue;
-      }
-      DSU.addValue(new ExprOrSymcrete::left(e));
+      DSU.addExpr(e);
     }
     for (ref<Symcrete> s : a->symcretes) {
       ref<Expr> e = EqExpr::create(a->concretization.evaluate(s->symcretized),
                                    s->symcretized);
-      if (auto ce = dyn_cast<ConstantExpr>(e)) {
-        assert(ce->isTrue() && "Attempt to add invalid constraint");
-        continue;
-      }
-      DSU.addValue(new ExprOrSymcrete::left(e));
+      DSU.addExpr(e);
     }
     auto concretizationConstraints =
         a->concretization.createConstraintsFromAssignment();
     for (ref<Expr> e : concretizationConstraints) {
-      if (auto ce = dyn_cast<ConstantExpr>(e)) {
-        assert(ce->isTrue() && "Attempt to add invalid constraint");
-        continue;
-      }
-      DSU.addValue(new ExprOrSymcrete::left(e));
+      DSU.addExpr(e);
     }
 
-    a->concretizedSets = DSU;
+    a->concretizedSets.reset(new InnerSetUnion(DSU));
   }
 
   return a;
diff --git a/lib/Solver/ConcretizingSolver.cpp b/lib/Solver/ConcretizingSolver.cpp
index 6f0327a226..645d1863f4 100644
--- a/lib/Solver/ConcretizingSolver.cpp
+++ b/lib/Solver/ConcretizingSolver.cpp
@@ -3,6 +3,7 @@
 #include "klee/Expr/Constraints.h"
 #include "klee/Expr/Expr.h"
 #include "klee/Expr/ExprUtil.h"
+#include "klee/Expr/IndependentConstraintSetUnion.h"
 #include "klee/Expr/IndependentSet.h"
 #include "klee/Expr/SymbolicSource.h"
 #include "klee/Expr/Symcrete.h"