diff --git a/.github/workflows/build.yaml b/.github/workflows/build.yaml
index be44b5b4bd..0f1ef0fb1b 100644
--- a/.github/workflows/build.yaml
+++ b/.github/workflows/build.yaml
@@ -2,9 +2,9 @@ name: CI
 
 on:
   pull_request:
-    branches: [main, utbot-main]
+    branches: [IndependentSolverReworkFinal, main, utbot-main]
   push:
-    branches: [main, utbot-main]
+    branches: [IndependentSolverReworkFinal, main, utbot-main]
 
 # Defaults for building KLEE
 env:
diff --git a/include/klee/ADT/DisjointSetUnion.h b/include/klee/ADT/DisjointSetUnion.h
new file mode 100644
index 0000000000..df56cc8702
--- /dev/null
+++ b/include/klee/ADT/DisjointSetUnion.h
@@ -0,0 +1,130 @@
+#ifndef KLEE_DISJOINEDSETUNION_H
+#define KLEE_DISJOINEDSETUNION_H
+#include "klee/ADT/Ref.h"
+
+#include <set>
+#include <unordered_map>
+#include <unordered_set>
+#include <vector>
+
+namespace klee {
+
+template <typename ValueType, typename SetType, typename HashType>
+class DisjointSetUnion {
+protected:
+  std::unordered_map<ValueType, ValueType, HashType> parent;
+  std::unordered_set<ValueType, HashType> roots;
+  std::unordered_map<ValueType, size_t, HashType> rank;
+
+  std::unordered_set<ValueType, HashType> internalStorage;
+  std::unordered_map<ValueType, ref<const SetType>, HashType> disjointSets;
+
+  ValueType find(const ValueType &v) { // findparent
+    assert(parent.find(v) != parent.end());
+    if (v == parent[v])
+      return v;
+    return parent[v] = find(parent[v]);
+  }
+
+  ValueType constFind(const ValueType &v) const {
+    assert(parent.find(v) != parent.end());
+    ValueType v1 = parent.find(v)->second;
+    if (v == v1)
+      return v;
+    return constFind(v1);
+  }
+
+  void merge(ValueType a, ValueType b) {
+    a = find(a);
+    b = find(b);
+    if (a == b) {
+      return;
+    }
+
+    if (rank[a] < rank[b]) {
+      std::swap(a, b);
+    }
+    parent[b] = a;
+    if (rank[a] == rank[b]) {
+      rank[a]++;
+    }
+
+    roots.erase(b);
+    disjointSets[a] = SetType::merge(disjointSets[a], disjointSets[b]);
+    disjointSets[b] = nullptr;
+  }
+
+  bool areJoined(const ValueType &i, const ValueType &j) const {
+    return constFind(i) == constFind(j);
+  }
+
+public:
+  using internalStorage_ty = std::unordered_set<ValueType, HashType>;
+  using disjointSets_ty =
+      std::unordered_map<ValueType, ref<const SetType>, HashType>;
+  using const_iterator = typename internalStorage_ty::const_iterator;
+
+  const_iterator begin() const { return internalStorage.begin(); }
+  const_iterator end() const { return internalStorage.end(); }
+
+  size_t numberOfValues() const noexcept { return internalStorage.size(); }
+
+  size_t numberOfGroups() const noexcept { return disjointSets.size(); }
+
+  bool empty() const noexcept { return numberOfValues() == 0; }
+
+  ref<const SetType> findGroup(const ValueType &i) const {
+    return disjointSets.find(constFind(i))->second;
+  }
+
+  ref<const SetType> findGroup(const_iterator it) const {
+    return disjointSets.find(constFind(*it))->second;
+  }
+
+  void addValue(const ValueType value) {
+    if (internalStorage.find(value) != internalStorage.end()) {
+      return;
+    }
+    parent[value] = value;
+    roots.insert(value);
+    rank[value] = 0;
+    disjointSets[value] = new SetType(value);
+
+    internalStorage.insert(value);
+    std::vector<ValueType> oldRoots(roots.begin(), roots.end());
+    for (ValueType v : oldRoots) {
+      if (!areJoined(v, value) &&
+          SetType::intersects(disjointSets[find(v)],
+                              disjointSets[find(value)])) {
+        merge(v, value);
+      }
+    }
+  }
+  void getAllIndependentSets(std::vector<ref<const SetType>> &result) const {
+    for (ValueType v : roots)
+      result.push_back(findGroup(v));
+  }
+
+  void add(const DisjointSetUnion &b) {
+    parent.insert(b.parent.begin(), b.parent.end());
+    roots.insert(b.roots.begin(), b.roots.end());
+    rank.insert(b.rank.begin(), b.rank.end());
+
+    internalStorage.insert(b.internalStorage.begin(), b.internalStorage.end());
+    disjointSets.insert(b.disjointSets.begin(), b.disjointSets.end());
+  }
+  DisjointSetUnion() {}
+
+  DisjointSetUnion(const internalStorage_ty &is) {
+    for (ValueType v : is) {
+      addValue(v);
+    }
+  }
+
+public:
+  internalStorage_ty is() const { return internalStorage; }
+
+  disjointSets_ty ds() const { return disjointSets; }
+};
+} // namespace klee
+#endif
\ No newline at end of file
diff --git a/include/klee/ADT/OrderMaintenanceTrie.h b/include/klee/ADT/OrderMaintenanceTrie.h
new file mode 100644
index 0000000000..a21cf08049
--- /dev/null
+++ b/include/klee/ADT/OrderMaintenanceTrie.h
@@ -0,0 +1,243 @@
+#ifndef KLEE_ORDERMAINTENANCETRIE_H
+#define KLEE_ORDERMAINTENANCETRIE_H
+#include <bitset>
+#include <cassert>
+#include <cmath>
+#include <cstddef>
+#include <iterator>
+#include <memory>
+#include <vector>
+
+#define ITEMSIZE 64 // depth of tree
+#define ALPHA 1.4   // balancing constant
+
+namespace klee {
+
+class OrderMaintenanaceTrie {
+private:
+  struct Node {
+
+    size_t height = 0;
+    size_t weight = 0;
+    size_t tag = 0;
+
+    Node *parent = nullptr;
+    Node *left = nullptr;
+    Node *right = nullptr;
+
+    Node(size_t h = 0, Node *p = nullptr) {
+      parent = p;
+      height = h;
+    }
+
+    bool isFull() {
+      return std::pow(0.5, ITEMSIZE - height) * weight >
+             std::pow(1.0 / ALPHA, height);
+    }
+    ~Node() {
+      if (left)
+        delete left;
+      if (right)
+        delete right;
+      if (parent) {
+        if (this == parent->left)
+          parent->left = nullptr;
+        if (this == parent->right)
+          parent->right = nullptr;
+      }
+      Node *current = parent;
+      while (current) {
+        current->weight -= weight;
+        current = current->parent;
+      }
+    }
+  };
+
+private:
+  Node *root;
+
+private:
+  Node *insert(size_t x) const {
+    std::bitset<ITEMSIZE> xbin(x);
+    Node *current = root;
+    for (int i = ITEMSIZE - 1; i > -1; i--) {
+      current->weight++;
+      if (!xbin[i]) {
+        if (!current->left)
+          current->left = new Node(current->height + 1, current);
+        current = current->left;
+      } else {
+        if (!current->right)
+          current->right = new Node(current->height + 1, current);
+        current = current->right;
+      }
+    }
+    current->tag = x;
+    return current;
+  }
+
+  Node *find(size_t x) const {
+    std::bitset<ITEMSIZE> xbin(x);
+    Node *current = root;
+    for (int i = ITEMSIZE - 1; i > -1; i--) {
+      if (!xbin[i]) {
+        if (!current->left)
+          return nullptr;
+        current = current->left;
+      } else {
+        if (!current->right)
+          return nullptr;
+        current = current->right;
+      }
+    }
+    return current;
+  }
+
+  Node *getNext(Node *x) const {
+    Node *current = x;
+    assert(current && "No such item in trie");
+    while (current->parent &&
+           (current == current->parent->right || !current->parent->left ||
+            !current->parent->right)) {
+      current = current->parent;
+    }
+    if (!current->parent)
+      return nullptr;
+
+    current = current->parent->right;
+    while (current->height != ITEMSIZE) {
+      if (current->left)
+        current = current->left;
+      else if (current->right)
+        current = current->right;
+      else
+        assert(false);
+    }
+    return current;
+  }
+
+  Node *getNext(size_t x) const {
+    Node *current = find(x);
+    return getNext(current);
+  }
+
+  bool getNextItem(size_t x, size_t &result) const {
+    if (!getNext(x))
+      return false;
+    Node *next = getNext(x);
+    result = next->tag;
+    return true;
+  }
+
+  void findAllLeafs(Node *item, std::vector<Node *> &result) {
+    if (item->height == ITEMSIZE)
+      result.push_back(item);
+    if (item->left) {
+      findAllLeafs(item->left, result);
+    }
+    if (item->right) {
+      findAllLeafs(item->right, result);
+    }
+  }
+
+  void rebalance(Node *item) {
+    while (item->parent && item->parent->isFull()) {
+      item = item->parent;
+    }
+    assert(item->parent && "Wrong choice of constants");
+    std::vector<Node *> leafs;
+    findAllLeafs(item, leafs);
+    assert(leafs.size() > 0);
+    size_t min;
+    min = leafs[0]->tag;
+    min = min >> (ITEMSIZE - item->height) << (ITEMSIZE - item->height);
+    size_t diff = ((1 << (ITEMSIZE - item->height)) - 1) / leafs.size();
+
+    for (Node *i : leafs) {
+      i->parent->left = nullptr;
+      i->parent->right = nullptr;
+    }
+    delete item;
+    for (Node *i : leafs) {
+      Node *newItem = insert(min);
+      *i = *(newItem);
+      Node *parent = newItem->parent;
+      if (newItem == parent->left) {
+        delete newItem;
+        parent->left = i;
+      } else {
+        delete newItem;
+        parent->right = i;
+      }
+      min += diff;
+    }
+  }
+
+public:
+  struct Iterator {
+    using iterator_category = std::input_iterator_tag;
+    using difference_type = std::ptrdiff_t;
+    using value_type = size_t;
+    using pointer = size_t *;
+    using reference = size_t &;
+
+  private:
+    OrderMaintenanaceTrie::Node *leaf;
+    const OrderMaintenanaceTrie *owner;
+
+  public:
+    Iterator(OrderMaintenanaceTrie::Node *leaf = nullptr,
+             const OrderMaintenanaceTrie *owner = nullptr)
+        : leaf(leaf), owner(owner) {}
+
+    Iterator &operator++() {
+      if (!owner->getNext(leaf)) {
+        leaf = nullptr;
+        owner = nullptr;
+        return *this;
+      }
+      leaf = owner->getNext(leaf);
+      return *this;
+    }
+
+    bool operator==(const Iterator &other) const { return leaf == other.leaf; }
+
+    bool operator!=(const Iterator &other) const { return !(*this == other); }
+
+    size_t operator*() const {
+      assert(leaf);
+      return leaf->tag;
+    }
+  };
+
+public:
+  Iterator begin() { return Iterator(find(0), this); }
+  Iterator end() { return Iterator(nullptr, nullptr); }
+
+  OrderMaintenanaceTrie() {
+    root = new Node();
+    insert(0);
+  }
+
+  ~OrderMaintenanaceTrie() {
+    std::vector<Node *> leafs;
+    findAllLeafs(root, leafs);
+    delete root;
+  }
+
+  Iterator insertAfter(Iterator it) {
+    size_t next = 0;
+    size_t p = *it;
+    if (!getNextItem(p, next) || next != p + 1) {
+      return Iterator(insert(p + 1), this);
+    }
+    Node *found = find(p);
+    rebalance(found);
+    return Iterator(insert(found->tag + 1), this);
+  }
+};
+} // namespace klee
+
+#undef ITEMSIZE
+#undef ALPHA
+#endif
\ No newline at end of file
diff --git a/include/klee/ADT/PersistentArray.h b/include/klee/ADT/PersistentArray.h
new file mode 100644
index 0000000000..61e1d36650
--- /dev/null
+++ b/include/klee/ADT/PersistentArray.h
@@ -0,0 +1,192 @@
+#ifndef KLEE_PERSISTENTARRAY_H
+#define KLEE_PERSISTENTARRAY_H
+
+#include <cassert>
+#include <cstddef>
+#include <iterator>
+#include <list>
+#include <memory>
+#include <set>
+#include <vector>
+
+#include "OrderMaintenanceTrie.h"
+
+namespace klee {
+
+template <typename ValueType> class PersistentArray {
+public:
+  struct Modification {
+    ValueType value;
+    OrderMaintenanaceTrie::Iterator listPosition;
+    Modification(ValueType v, OrderMaintenanaceTrie::Iterator lp =
+                                  OrderMaintenanaceTrie::Iterator())
+        : value(v), listPosition(lp) {}
+  };
+
+  typedef std::list<Modification> VersionList;
+
+  struct Sublist {
+    typename VersionList::const_iterator initialElement;
+    typename VersionList::const_iterator modifiedElement;
+    Sublist(typename VersionList::const_iterator iE,
+            typename VersionList::const_iterator mE) {
+      initialElement = iE;
+      modifiedElement = mE;
+    }
+  };
+
+  struct positionCmp {
+    bool operator()(const Sublist &a, const Sublist &b) const {
+      return *(a.initialElement->listPosition) <
+             *(b.initialElement->listPosition);
+    }
+  };
+  typedef std::set<Sublist, positionCmp> SublistSet;
+
+private:
+  std::shared_ptr<VersionList> versionList;
+  std::shared_ptr<OrderMaintenanaceTrie> versionListOrder;
+  std::shared_ptr<std::vector<SublistSet>> sublists;
+  typename VersionList::const_iterator version;
+
+  size_t capacity;
+
+public:
+  const typename VersionList::const_iterator getVersion() { return version; }
+  const std::shared_ptr<VersionList> getVersionList() { return versionList; }
+  const std::shared_ptr<std::vector<SublistSet>> getSublists() {
+    return sublists;
+  }
+  size_t size() const { return capacity; }
+
+  PersistentArray<ValueType>() {
+    versionList = std::shared_ptr<VersionList>(new VersionList);
+    versionListOrder =
+        std::shared_ptr<OrderMaintenanaceTrie>(new OrderMaintenanaceTrie);
+    sublists =
+        std::shared_ptr<std::vector<SublistSet>>(new std::vector<SublistSet>());
+    versionList->push_front(
+        Modification(ValueType(), versionListOrder->begin()));
+    version = versionList->begin();
+    capacity = 0;
+  }
+
+  PersistentArray(size_t n) {
+    versionList = new VersionList;
+    sublists = new std::vector<SublistSet>(n);
+    versionList->push_front(
+        Modification(ValueType(), versionListOrder->begin()));
+    version = versionList->begin();
+    for (auto &i : *sublists) {
+      i.insert(Sublist(version, version));
+    }
+    capacity = n;
+  }
+
+  static PersistentArray<ValueType>
+  storeInVersion(PersistentArray<ValueType> &array, const size_t &i,
+                 const ValueType &b) {
+    // insert modification to versionList
+    assert(i < array.size() && i >= 0);
+    PersistentArray<ValueType> newArray(array);
+    typename VersionList::const_iterator v = newArray.version;
+
+    Modification mod(b);
+    mod.listPosition =
+        newArray.versionListOrder->insertAfter(array.version->listPosition);
+    newArray.version = newArray.versionList->insert(++v, mod);
+
+    // insert sublists created with modification to sublists array
+
+    SublistSet &sI = (*newArray.sublists)[i];
+    Sublist SLE(newArray.version, newArray.version);
+    typename SublistSet::iterator lowerBound = sI.lower_bound(SLE);
+
+    typename VersionList::const_iterator nextElement = newArray.version;
+    nextElement++;
+
+    if (lowerBound != sI.begin() &&
+        nextElement != newArray.versionList->end()) {
+      Sublist prevSLE = *(--lowerBound);
+      sI.insert(Sublist(nextElement, prevSLE.modifiedElement));
+    }
+    sI.insert(SLE);
+    return newArray;
+  }
+
+  ValueType loadFromVersion(PersistentArray<ValueType> &array,
+                            const size_t &i) {
+    Sublist sample(array.version, array.version);
+    SublistSet &sI = (*array.sublists)[i];
+
+    typename SublistSet::iterator result = sI.upper_bound(sample);
+
+    if (result == sI.begin()) {
+      return ValueType();
+    }
+
+    return (--result)->modifiedElement->value;
+  }
+
+  PersistentArray<ValueType> store(const size_t &i, const ValueType &b) {
+    return storeInVersion(*this, i, b);
+  }
+
+  static PersistentArray<ValueType>
+  pushBackInVersion(PersistentArray<ValueType> &array, const ValueType &b) {
+    array.sublists->push_back(
+        {Sublist(array.versionList->begin(), array.versionList->begin())});
+    PersistentArray<ValueType> newArray(array);
+    newArray.capacity++;
+    newArray = newArray.store(newArray.capacity - 1, b);
+    return newArray;
+  }
+
+  PersistentArray<ValueType> push_back(const ValueType &b) {
+    return pushBackInVersion(*this, b);
+  }
+
+  ValueType load(const size_t &i) { return loadFromVersion(*this, i); }
+
+  ValueType operator[](const size_t &i) { return load(i); }
+
+  bool operator==(const PersistentArray<ValueType> &b) const {
+    if (this->size() != b.size())
+      return false;
+    for (int i = 0; i < this->size(); i++) {
+      if (this[i] != b[i])
+        return false;
+    }
+    return true;
+  }
+
+  bool operator!=(const PersistentArray<ValueType> &b) const {
+    return !(*this == b);
+  }
+
+  bool operator<(const PersistentArray<ValueType> &b) const {
+    std::vector<ValueType> aInternal;
+    std::vector<ValueType> bInternal;
+    for (int i = 0; i < this->size(); i++) {
+      aInternal.push_back(this[i]);
+    }
+    for (int i = 0; i < b.size(); i++) {
+      bInternal.push_back(b[i]);
+    }
+    return aInternal < bInternal;
+  }
+
+  bool operator>(const PersistentArray<ValueType> &b) const {
+    std::vector<ValueType> aInternal;
+    std::vector<ValueType> bInternal;
+    for (int i = 0; i < this->size(); i++) {
+      aInternal.push_back(this[i]);
+    }
+    for (int i = 0; i < b.size(); i++) {
+      bInternal.push_back(b[i]);
+    }
+    return aInternal > bInternal;
+  }
+};
+} // namespace klee
+#endif
diff --git a/include/klee/Expr/Assignment.h b/include/klee/Expr/Assignment.h
index a31ed3c22b..8116fbd839 100644
--- a/include/klee/Expr/Assignment.h
+++ b/include/klee/Expr/Assignment.h
@@ -53,9 +53,11 @@ class Assignment {
     }
   }
 
+  void add(const Assignment &b);
+
   ref<Expr> evaluate(const Array *mo, unsigned index) const;
   ref<Expr> evaluate(ref<Expr> e) const;
-  ConstraintSet createConstraintsFromAssignment() const;
+  constraints_ty createConstraintsFromAssignment() const;
 
   template <typename InputIterator>
   bool satisfies(InputIterator begin, InputIterator end);
diff --git a/include/klee/Expr/Constraints.h b/include/klee/Expr/Constraints.h
index a14b9e191e..ad06d415ea 100644
--- a/include/klee/Expr/Constraints.h
+++ b/include/klee/Expr/Constraints.h
@@ -12,10 +12,14 @@
 
 #include "klee/ADT/Ref.h"
 
+#include "klee/ADT/DisjointSetUnion.h"
+#include "klee/ADT/PersistentArray.h"
 #include "klee/Expr/Assignment.h"
 #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"
 
@@ -55,7 +59,8 @@ class ConstraintSet {
     return _constraints < b._constraints ||
            (_constraints == b._constraints && _symcretes < b._symcretes);
   }
-
+  ConstraintSet getConcretizedVersion() const;
+  ConstraintSet getConcretizedVersion(const Assignment &c) const;
   void dump() const;
   void print(llvm::raw_ostream &os) const;
 
@@ -64,11 +69,21 @@ class ConstraintSet {
   const constraints_ty &cs() const;
   const symcretes_ty &symcretes() const;
   const Assignment &concretization() const;
+  const IndependentConstraintSetUnion &independentElements() const;
+
+  void getAllIndependentConstraintsSets(
+      const ref<Expr> &queryExpr,
+      std::vector<ref<const IndependentConstraintSet>> &result) const;
+
+  ref<const IndependentConstraintSet>
+  getIndependentConstraints(const ref<Expr> &queryExpr,
+                            constraints_ty &result) const;
 
 private:
   constraints_ty _constraints;
   symcretes_ty _symcretes;
   Assignment _concretization;
+  IndependentConstraintSetUnion _independentElements;
 };
 
 class PathConstraints {
diff --git a/include/klee/Expr/IndependentConstraintSetUnion.h b/include/klee/Expr/IndependentConstraintSetUnion.h
new file mode 100644
index 0000000000..a2f16b0f94
--- /dev/null
+++ b/include/klee/Expr/IndependentConstraintSetUnion.h
@@ -0,0 +1,42 @@
+#ifndef KLEE_INDEPENDENTCONSTRAINTSETUNION_H
+#define KLEE_INDEPENDENTCONSTRAINTSETUNION_H
+
+#include "klee/Expr/Assignment.h"
+#include "klee/Expr/Expr.h"
+#include "klee/Expr/IndependentSet.h"
+
+namespace klee {
+class IndependentConstraintSetUnion
+    : public DisjointSetUnion<ref<Expr>, IndependentConstraintSet,
+                              util::ExprHash> {
+public:
+  Assignment concretization;
+
+public:
+  ExprHashMap<ref<Expr>> concretizedExprs;
+
+public:
+  void updateConcretization(const Assignment &c);
+  void removeConcretization(const Assignment &remove);
+  void reEvaluateConcretization(const Assignment &newConcretization);
+
+  IndependentConstraintSetUnion getConcretizedVersion() const;
+  IndependentConstraintSetUnion
+  getConcretizedVersion(const Assignment &c) const;
+
+  IndependentConstraintSetUnion();
+  IndependentConstraintSetUnion(const constraints_ty &is,
+                                const SymcreteOrderedSet &os,
+                                const Assignment &c);
+
+  ref<const IndependentConstraintSet>
+  getIndependentConstraints(const ref<Expr> &e, constraints_ty &result) const;
+  void getAllIndependentConstraintSets(
+      const ref<Expr> &e,
+      std::vector<ref<const IndependentConstraintSet>> &result) const;
+  void addExpr(const ref<Expr> e);
+  void addSymcrete(const ref<Symcrete> s);
+};
+} // namespace klee
+
+#endif
\ No newline at end of file
diff --git a/include/klee/Expr/IndependentSet.h b/include/klee/Expr/IndependentSet.h
index 581f42ac04..87e647b201 100644
--- a/include/klee/Expr/IndependentSet.h
+++ b/include/klee/Expr/IndependentSet.h
@@ -1,12 +1,18 @@
 #ifndef KLEE_INDEPENDENTSET_H
 #define KLEE_INDEPENDENTSET_H
 
+#include "klee/ADT/DisjointSetUnion.h"
+#include "klee/ADT/ImmutableMap.h"
+#include "klee/ADT/ImmutableSet.h"
+#include "klee/Expr/Assignment.h"
 #include "klee/Expr/Expr.h"
 #include "klee/Expr/ExprHashMap.h"
-#include "klee/Solver/Solver.h"
+#include "klee/Expr/Symcrete.h"
 #include "llvm/Support/raw_ostream.h"
-#include <list>
+#include <map>
 #include <set>
+#include <string>
+#include <vector>
 
 namespace klee {
 
@@ -36,7 +42,7 @@ template <class T> class DenseSet {
     return modified;
   }
 
-  bool intersects(const DenseSet &b) {
+  bool intersects(const DenseSet &b) const {
     for (typename set_ty::iterator it = s.begin(), ie = s.end(); it != ie; ++it)
       if (b.s.count(*it))
         return true;
@@ -70,54 +76,94 @@ inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os,
   return os;
 }
 
-class IndependentElementSet {
+class IndependentConstraintSet {
+private:
+  struct InnerSetUnion
+      : public DisjointSetUnion<ref<Expr>, IndependentConstraintSet,
+                                util::ExprHash> {
+    using DisjointSetUnion<ref<Expr>, IndependentConstraintSet,
+                           util::ExprHash>::DisjointSetUnion;
+    void addExpr(ref<Expr> e) {
+      if (internalStorage.find(e) != internalStorage.end()) {
+        return;
+      }
+      parent[e] = e;
+      roots.insert(e);
+      rank[e] = 0;
+      disjointSets[e] = new IndependentConstraintSet(e);
+
+      internalStorage.insert(e);
+      std::vector<ref<Expr>> oldRoots(roots.begin(), roots.end());
+      for (ref<Expr> v : oldRoots) {
+        if (!areJoined(v, e) &&
+            IndependentConstraintSet::intersects(disjointSets[find(v)],
+                                                 disjointSets[find(e)])) {
+          merge(v, e);
+        }
+      }
+    }
+  };
+
 public:
-  typedef std::map<const Array *, DenseSet<unsigned>> elements_ty;
+  // All containers need to become persistent to make fast copy and faster merge
+  // possible
+  // map from concretized to normal
+  typedef ImmutableMap<const Array *, DenseSet<unsigned>> elements_ty;
   elements_ty
       elements; // Represents individual elements of array accesses (arr[1])
-  std::set<const Array *>
+  ImmutableSet<const Array *>
       wholeObjects;     // Represents symbolically accessed arrays (arr[x])
   constraints_ty exprs; // All expressions (constraints) that are associated
                         // with this factor
   SymcreteOrderedSet symcretes; // All symcretes associated with this factor
 
-  IndependentElementSet();
-  IndependentElementSet(ref<Expr> e);
-  IndependentElementSet(ref<Symcrete> s);
-  IndependentElementSet(const IndependentElementSet &ies);
+  Assignment concretization;
+
+  InnerSetUnion concretizedSets;
+
+  ref<const IndependentConstraintSet> addExpr(ref<Expr> e) const;
+  ref<const IndependentConstraintSet>
+  updateConcretization(const Assignment &delta,
+                       ExprHashMap<ref<Expr>> &changedExprs) const;
+  ref<const IndependentConstraintSet>
+  removeConcretization(const Assignment &delta,
+                       ExprHashMap<ref<Expr>> &changedExprs) const;
 
-  IndependentElementSet &operator=(const IndependentElementSet &ies);
+  void
+  addValuesToAssignment(const std::vector<const Array *> &objects,
+                        const std::vector<SparseStorage<unsigned char>> &values,
+                        Assignment &assign) const;
+
+  IndependentConstraintSet();
+  IndependentConstraintSet(ref<Expr> e);
+  IndependentConstraintSet(ref<Symcrete> s);
+  IndependentConstraintSet(const ref<const IndependentConstraintSet> &ics);
+
+  IndependentConstraintSet &operator=(const IndependentConstraintSet &ies);
 
   void print(llvm::raw_ostream &os) const;
 
-  // more efficient when this is the smaller set
-  bool intersects(const IndependentElementSet &b);
+  static bool intersects(ref<const IndependentConstraintSet> a,
+                         ref<const IndependentConstraintSet> b);
 
-  // returns true iff set is changed by addition
-  bool add(const IndependentElementSet &b);
+  static ref<const IndependentConstraintSet>
+  merge(ref<const IndependentConstraintSet> a,
+        ref<const IndependentConstraintSet> b);
+
+  // Extracts which arrays are referenced from a particular independent set.
+  // Examines both the actual known array accesses arr[1] plus the undetermined
+  // accesses arr[x].Z
+  void calculateArrayReferences(std::vector<const Array *> &returnVector) const;
+
+  mutable class ReferenceCounter _refCount;
 };
 
 inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os,
-                                     const IndependentElementSet &ies) {
+                                     const IndependentConstraintSet &ies) {
   ies.print(os);
   return os;
 }
 
-// Breaks down a constraint into all of it's individual pieces, returning a
-// list of IndependentElementSets or the independent factors.
-//
-// Caller takes ownership of returned std::list.
-std::list<IndependentElementSet> *
-getAllIndependentConstraintsSets(const Query &query);
-
-IndependentElementSet getIndependentConstraints(const Query &query,
-                                                constraints_ty &result);
-
-// Extracts which arrays are referenced from a particular independent set.
-// Examines both the actual known array accesses arr[1] plus the undetermined
-// accesses arr[x].
-void calculateArrayReferences(const IndependentElementSet &ie,
-                              std::vector<const Array *> &returnVector);
 } // namespace klee
 
 #endif /* KLEE_INDEPENDENTSET_H */
diff --git a/include/klee/Module/TargetForest.h b/include/klee/Module/TargetForest.h
index 91cd347309..eac93e8ef4 100644
--- a/include/klee/Module/TargetForest.h
+++ b/include/klee/Module/TargetForest.h
@@ -298,6 +298,7 @@ class TargetForest {
   void add(ref<Target>);
   void remove(ref<Target>);
   void blockIn(ref<Target>, ref<Target>);
+  void block(const ref<Target> &);
   const ref<History> getHistory() { return history; };
   const ref<Layer> getTargets() { return forest; };
   void dump() const;
diff --git a/include/klee/Solver/SolverUtil.h b/include/klee/Solver/SolverUtil.h
index d61c188cc0..9833381f61 100644
--- a/include/klee/Solver/SolverUtil.h
+++ b/include/klee/Solver/SolverUtil.h
@@ -5,6 +5,7 @@
 #include "klee/Expr/Constraints.h"
 #include "klee/Expr/Expr.h"
 #include "klee/Expr/ExprHashMap.h"
+#include "klee/Expr/IndependentSet.h"
 #include "klee/System/Time.h"
 
 namespace klee {
@@ -80,6 +81,15 @@ struct Query {
            (lhs.constraints == rhs.constraints && lhs.expr < rhs.expr);
   }
 
+  void getAllIndependentConstraintsSets(
+      std::vector<ref<const IndependentConstraintSet>> &result) const {
+    constraints.getAllIndependentConstraintsSets(expr, result);
+  }
+
+  ref<const IndependentConstraintSet>
+  getIndependentConstraints(constraints_ty &result) const {
+    return constraints.getIndependentConstraints(expr, result);
+  }
   /// Dump query
   void dump() const;
 };
diff --git a/lib/Core/CMakeLists.txt b/lib/Core/CMakeLists.txt
index 202fa2fcec..b064c749f3 100644
--- a/lib/Core/CMakeLists.txt
+++ b/lib/Core/CMakeLists.txt
@@ -13,6 +13,7 @@ klee_add_component(kleeCore
   Context.cpp
   CoreStats.cpp
   CXXTypeSystem/CXXTypeManager.cpp
+  DistanceCalculator.cpp
   ExecutionState.cpp
   Executor.cpp
   ExecutorUtil.cpp
diff --git a/lib/Core/DistanceCalculator.cpp b/lib/Core/DistanceCalculator.cpp
new file mode 100644
index 0000000000..b87fbcf18a
--- /dev/null
+++ b/lib/Core/DistanceCalculator.cpp
@@ -0,0 +1,210 @@
+//===-- DistanceCalculator.cpp --------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#include "DistanceCalculator.h"
+#include "ExecutionState.h"
+#include "klee/Module/CodeGraphDistance.h"
+#include "klee/Module/KInstruction.h"
+#include "klee/Module/Target.h"
+
+using namespace llvm;
+using namespace klee;
+
+DistanceResult DistanceCalculator::getDistance(ExecutionState &es,
+                                               ref<Target> target) {
+  return getDistance(es.pc, es.prevPC, es.initPC, es.stack, es.error, target);
+}
+
+DistanceResult
+DistanceCalculator::getDistance(KInstruction *pc, KInstruction *prevPC,
+                                KInstruction *initPC,
+                                const ExecutionState::stack_ty &stack,
+                                ReachWithError error, ref<Target> target) {
+  weight_type weight = 0;
+
+  BasicBlock *pcBlock = pc->inst->getParent();
+  BasicBlock *prevPCBlock = prevPC->inst->getParent();
+
+  if (!target->shouldFailOnThisTarget() && target->atReturn()) {
+    if (prevPC->parent == target->getBlock() &&
+        prevPC == target->getBlock()->getLastInstruction()) {
+      return DistanceResult(Done);
+    } else if (pc->parent == target->getBlock()) {
+      return DistanceResult(Continue);
+    }
+  }
+
+  if (target->shouldFailOnThisTarget() && target->isTheSameAsIn(prevPC) &&
+      target->isThatError(error)) {
+    return DistanceResult(Done);
+  }
+
+  BasicBlock *bb = pcBlock;
+  KBlock *kb = pc->parent->parent->blockMap[bb];
+  const auto &distanceToTargetFunction =
+      codeGraphDistance.getBackwardDistance(target->getBlock()->parent);
+  unsigned int minCallWeight = UINT_MAX, minSfNum = UINT_MAX, sfNum = 0;
+  for (auto sfi = stack.rbegin(), sfe = stack.rend(); sfi != sfe; sfi++) {
+    unsigned callWeight;
+    if (distanceInCallGraph(sfi->kf, kb, callWeight, distanceToTargetFunction,
+                            target)) {
+      callWeight *= 2;
+      if (callWeight == 0 && target->shouldFailOnThisTarget()) {
+        return target->isTheSameAsIn(kb->getFirstInstruction()) &&
+                       target->isThatError(error)
+                   ? DistanceResult(Done)
+                   : DistanceResult(Continue);
+      } else {
+        callWeight += sfNum;
+      }
+
+      if (callWeight < minCallWeight) {
+        minCallWeight = callWeight;
+        minSfNum = sfNum;
+      }
+    }
+
+    if (sfi->caller) {
+      kb = sfi->caller->parent;
+      bb = kb->basicBlock;
+    }
+    sfNum++;
+
+    if (minCallWeight < sfNum)
+      break;
+  }
+
+  WeightResult res = Miss;
+  bool isInsideFunction = true;
+  if (minCallWeight == 0) {
+    res = tryGetTargetWeight(pc, initPC, pcBlock, prevPCBlock, weight, target);
+  } else if (minSfNum == 0) {
+    res = tryGetPreTargetWeight(pc, initPC, pcBlock, prevPCBlock, weight,
+                                distanceToTargetFunction, target);
+    isInsideFunction = false;
+  } else if (minSfNum != UINT_MAX) {
+    res = tryGetPostTargetWeight(pc, initPC, pcBlock, prevPCBlock, weight,
+                                 target);
+    isInsideFunction = false;
+  }
+  if (Done == res && target->shouldFailOnThisTarget()) {
+    if (!target->isThatError(error)) {
+      res = Continue;
+    }
+  }
+
+  return DistanceResult(res, weight, isInsideFunction);
+}
+
+bool DistanceCalculator::distanceInCallGraph(
+    KFunction *kf, KBlock *kb, unsigned int &distance,
+    const std::unordered_map<KFunction *, unsigned int>
+        &distanceToTargetFunction,
+    ref<Target> target) {
+  distance = UINT_MAX;
+  const std::unordered_map<KBlock *, unsigned> &dist =
+      codeGraphDistance.getDistance(kb);
+  KBlock *targetBB = target->getBlock();
+  KFunction *targetF = targetBB->parent;
+
+  if (kf == targetF && dist.count(targetBB) != 0) {
+    distance = 0;
+    return true;
+  }
+
+  for (auto &kCallBlock : kf->kCallBlocks) {
+    if (dist.count(kCallBlock) != 0) {
+      for (auto &calledFunction : kCallBlock->calledFunctions) {
+        KFunction *calledKFunction = kf->parent->functionMap[calledFunction];
+        if (distanceToTargetFunction.count(calledKFunction) != 0 &&
+            distance > distanceToTargetFunction.at(calledKFunction) + 1) {
+          distance = distanceToTargetFunction.at(calledKFunction) + 1;
+        }
+      }
+    }
+  }
+  return distance != UINT_MAX;
+}
+
+WeightResult DistanceCalculator::tryGetLocalWeight(
+    KInstruction *pc, KInstruction *initPC, BasicBlock *pcBlock,
+    BasicBlock *prevPCBlock, weight_type &weight,
+    const std::vector<KBlock *> &localTargets, ref<Target> target) {
+  KFunction *currentKF = pc->parent->parent;
+  KBlock *initKB = initPC->parent;
+  KBlock *currentKB = currentKF->blockMap[pcBlock];
+  KBlock *prevKB = currentKF->blockMap[prevPCBlock];
+  const std::unordered_map<KBlock *, unsigned> &dist =
+      codeGraphDistance.getDistance(currentKB);
+  weight = UINT_MAX;
+  for (auto &end : localTargets) {
+    if (dist.count(end) > 0) {
+      unsigned int w = dist.at(end);
+      weight = std::min(w, weight);
+    }
+  }
+
+  if (weight == UINT_MAX)
+    return Miss;
+  if (weight == 0 && (initKB == currentKB || prevKB != currentKB ||
+                      target->shouldFailOnThisTarget())) {
+    return Done;
+  }
+
+  return Continue;
+}
+
+WeightResult DistanceCalculator::tryGetPreTargetWeight(
+    KInstruction *pc, KInstruction *initPC, BasicBlock *pcBlock,
+    BasicBlock *prevPCBlock, weight_type &weight,
+    const std::unordered_map<KFunction *, unsigned int>
+        &distanceToTargetFunction,
+    ref<Target> target) {
+  KFunction *currentKF = pc->parent->parent;
+  std::vector<KBlock *> localTargets;
+  for (auto &kCallBlock : currentKF->kCallBlocks) {
+    for (auto &calledFunction : kCallBlock->calledFunctions) {
+      KFunction *calledKFunction =
+          currentKF->parent->functionMap[calledFunction];
+      if (distanceToTargetFunction.count(calledKFunction) > 0) {
+        localTargets.push_back(kCallBlock);
+      }
+    }
+  }
+
+  if (localTargets.empty())
+    return Miss;
+
+  WeightResult res = tryGetLocalWeight(pc, initPC, pcBlock, prevPCBlock, weight,
+                                       localTargets, target);
+  return res == Done ? Continue : res;
+}
+
+WeightResult DistanceCalculator::tryGetPostTargetWeight(
+    KInstruction *pc, KInstruction *initPC, BasicBlock *pcBlock,
+    BasicBlock *prevPCBlock, weight_type &weight, ref<Target> target) {
+  KFunction *currentKF = pc->parent->parent;
+  std::vector<KBlock *> &localTargets = currentKF->returnKBlocks;
+
+  if (localTargets.empty())
+    return Miss;
+
+  WeightResult res = tryGetLocalWeight(pc, initPC, pcBlock, prevPCBlock, weight,
+                                       localTargets, target);
+  return res == Done ? Continue : res;
+}
+
+WeightResult DistanceCalculator::tryGetTargetWeight(
+    KInstruction *pc, KInstruction *initPC, BasicBlock *pcBlock,
+    BasicBlock *prevPCBlock, weight_type &weight, ref<Target> target) {
+  std::vector<KBlock *> localTargets = {target->getBlock()};
+  WeightResult res = tryGetLocalWeight(pc, initPC, pcBlock, prevPCBlock, weight,
+                                       localTargets, target);
+  return res;
+}
diff --git a/lib/Core/DistanceCalculator.h b/lib/Core/DistanceCalculator.h
new file mode 100644
index 0000000000..45851a6d26
--- /dev/null
+++ b/lib/Core/DistanceCalculator.h
@@ -0,0 +1,83 @@
+//===-- DistanceCalculator.h ------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef KLEE_DISTANCE_CALCULATOR_H
+#define KLEE_DISTANCE_CALCULATOR_H
+
+#include "ExecutionState.h"
+
+namespace llvm {
+class BasicBlock;
+} // namespace llvm
+
+namespace klee {
+class CodeGraphDistance;
+struct Target;
+
+enum WeightResult : std::uint8_t {
+  Continue,
+  Done,
+  Miss,
+};
+
+using weight_type = unsigned;
+
+struct DistanceResult {
+  WeightResult result;
+  weight_type weight;
+  bool isInsideFunction;
+
+  explicit DistanceResult(WeightResult result_, weight_type weight_ = 0,
+                          bool isInsideFunction_ = true)
+      : result(result_), weight(weight_), isInsideFunction(isInsideFunction_) {}
+};
+
+class DistanceCalculator {
+public:
+  explicit DistanceCalculator(CodeGraphDistance &codeGraphDistance_)
+      : codeGraphDistance(codeGraphDistance_) {}
+
+  DistanceResult getDistance(ExecutionState &es, ref<Target> target);
+  DistanceResult getDistance(KInstruction *pc, KInstruction *prevPC,
+                             KInstruction *initPC,
+                             const ExecutionState::stack_ty &stack,
+                             ReachWithError error, ref<Target> target);
+
+private:
+  CodeGraphDistance &codeGraphDistance;
+
+  bool distanceInCallGraph(KFunction *kf, KBlock *kb, unsigned int &distance,
+                           const std::unordered_map<KFunction *, unsigned int>
+                               &distanceToTargetFunction,
+                           ref<Target> target);
+  WeightResult tryGetLocalWeight(KInstruction *pc, KInstruction *initPC,
+                                 llvm::BasicBlock *pcBlock,
+                                 llvm::BasicBlock *prevPCBlock,
+                                 weight_type &weight,
+                                 const std::vector<KBlock *> &localTargets,
+                                 ref<Target> target);
+  WeightResult
+  tryGetPreTargetWeight(KInstruction *pc, KInstruction *initPC,
+                        llvm::BasicBlock *pcBlock,
+                        llvm::BasicBlock *prevPCBlock, weight_type &weight,
+                        const std::unordered_map<KFunction *, unsigned int>
+                            &distanceToTargetFunction,
+                        ref<Target> target);
+  WeightResult tryGetTargetWeight(KInstruction *pc, KInstruction *initPC,
+                                  llvm::BasicBlock *pcBlock,
+                                  llvm::BasicBlock *prevPCBlock,
+                                  weight_type &weight, ref<Target> target);
+  WeightResult tryGetPostTargetWeight(KInstruction *pc, KInstruction *initPC,
+                                      llvm::BasicBlock *pcBlock,
+                                      llvm::BasicBlock *prevPCBlock,
+                                      weight_type &weight, ref<Target> target);
+};
+} // namespace klee
+
+#endif /* KLEE_DISTANCE_CALCULATOR_H */
\ No newline at end of file
diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h
index 8d9db68d2b..918db65bbb 100644
--- a/lib/Core/ExecutionState.h
+++ b/lib/Core/ExecutionState.h
@@ -203,6 +203,8 @@ class ExecutionState {
 
 public:
   using stack_ty = std::vector<StackFrame>;
+  using TargetHashSet =
+      std::unordered_set<ref<Target>, RefTargetHash, RefTargetCmp>;
 
   // Execution - Control Flow specific
 
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index e42a4a5bb8..b9ec9df856 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -13,6 +13,7 @@
 #include "CXXTypeSystem/CXXTypeManager.h"
 #include "Context.h"
 #include "CoreStats.h"
+#include "DistanceCalculator.h"
 #include "ExecutionState.h"
 #include "ExternalDispatcher.h"
 #include "GetElementPtrTypeIterator.h"
@@ -442,10 +443,11 @@ Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts,
                    InterpreterHandler *ih)
     : Interpreter(opts), interpreterHandler(ih), searcher(nullptr),
       externalDispatcher(new ExternalDispatcher(ctx)), statsTracker(0),
-      pathWriter(0), symPathWriter(0),
-      specialFunctionHandler(0), timers{time::Span(TimerInterval)},
+      pathWriter(0), symPathWriter(0), specialFunctionHandler(0),
+      timers{time::Span(TimerInterval)},
       concretizationManager(new ConcretizationManager(EqualitySubstitution)),
       codeGraphDistance(new CodeGraphDistance()),
+      distanceCalculator(new DistanceCalculator(*codeGraphDistance)),
       targetedExecutionManager(*codeGraphDistance), replayKTest(0),
       replayPath(0), usingSeeds(0), atMemoryLimit(false), inhibitForking(false),
       haltExecution(HaltExecution::NotHalt), ivcEnabled(false),
@@ -4182,7 +4184,7 @@ void Executor::targetedRun(ExecutionState &initialState, KBlock *target,
   states.insert(&initialState);
 
   TargetedSearcher *targetedSearcher =
-      new TargetedSearcher(Target::create(target), *codeGraphDistance);
+      new TargetedSearcher(Target::create(target), *distanceCalculator);
   searcher = targetedSearcher;
 
   std::vector<ExecutionState *> newStates(states.begin(), states.end());
@@ -4522,6 +4524,8 @@ void Executor::terminateStateOnExecError(ExecutionState &state,
 void Executor::terminateStateOnSolverError(ExecutionState &state,
                                            const llvm::Twine &message) {
   terminateStateOnError(state, message, StateTerminationType::Solver, "");
+  SetOfStates states = {&state};
+  decreaseConfidenceFromStoppedStates(states, HaltExecution::MaxSolverTime);
 }
 
 // XXX shoot me
@@ -5058,11 +5062,13 @@ MemoryObject *Executor::allocate(ExecutionState &state, ref<Expr> size,
       ZExtExpr::create(size, pointerWidthInBits)};
 
   constraints_ty required;
-  IndependentElementSet eltsClosure = getIndependentConstraints(
-      Query(state.constraints.cs(), ZExtExpr::create(size, pointerWidthInBits)),
-      required);
+  ref<const IndependentConstraintSet> eltsClosure =
+      Query(state.constraints.cs(), ZExtExpr::create(size, pointerWidthInBits))
+          .getIndependentConstraints(
+
+              required);
   /* Collect dependent size symcretes. */
-  for (ref<Symcrete> symcrete : eltsClosure.symcretes) {
+  for (ref<Symcrete> symcrete : eltsClosure->symcretes) {
     if (isa<SizeSymcrete>(symcrete)) {
       symbolicSizesTerms.push_back(
           ZExtExpr::create(symcrete->symcretized, pointerWidthInBits));
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index add4ff1b68..fb6744ff2f 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -70,6 +70,7 @@ class AddressManager;
 class Array;
 struct Cell;
 class CodeGraphDistance;
+class DistanceCalculator;
 class ExecutionState;
 class ExternalDispatcher;
 class Expr;
@@ -142,6 +143,7 @@ class Executor : public Interpreter {
   std::unique_ptr<ConcretizationManager> concretizationManager;
   std::unique_ptr<PForest> processForest;
   std::unique_ptr<CodeGraphDistance> codeGraphDistance;
+  std::unique_ptr<DistanceCalculator> distanceCalculator;
   std::unique_ptr<TargetCalculator> targetCalculator;
 
   /// Used to track states that have been added during the current
diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp
index ab6ef2e1a9..979d34b142 100644
--- a/lib/Core/Searcher.cpp
+++ b/lib/Core/Searcher.cpp
@@ -19,7 +19,6 @@
 #include "klee/ADT/DiscretePDF.h"
 #include "klee/ADT/RNG.h"
 #include "klee/ADT/WeightedQueue.h"
-#include "klee/Module/CodeGraphDistance.h"
 #include "klee/Module/InstructionInfoTable.h"
 #include "klee/Module/KInstruction.h"
 #include "klee/Module/KModule.h"
@@ -150,133 +149,15 @@ static unsigned int ulog2(unsigned int val) {
 ///
 
 TargetedSearcher::TargetedSearcher(ref<Target> target,
-                                   CodeGraphDistance &_distance)
+                                   DistanceCalculator &_distanceCalculator)
     : states(std::make_unique<
              WeightedQueue<ExecutionState *, ExecutionStateIDCompare>>()),
-      target(target), codeGraphDistance(_distance),
-      distanceToTargetFunction(
-          codeGraphDistance.getBackwardDistance(target->getBlock()->parent)) {}
+      target(target), distanceCalculator(_distanceCalculator) {}
 
 ExecutionState &TargetedSearcher::selectState() { return *states->choose(0); }
 
-bool TargetedSearcher::distanceInCallGraph(KFunction *kf, KBlock *kb,
-                                           unsigned int &distance) {
-  distance = UINT_MAX;
-  const std::unordered_map<KBlock *, unsigned> &dist =
-      codeGraphDistance.getDistance(kb);
-  KBlock *targetBB = target->getBlock();
-  KFunction *targetF = targetBB->parent;
-
-  if (kf == targetF && dist.count(targetBB) != 0) {
-    distance = 0;
-    return true;
-  }
-
-  for (auto &kCallBlock : kf->kCallBlocks) {
-    if (dist.count(kCallBlock) != 0) {
-      for (auto &calledFunction : kCallBlock->calledFunctions) {
-        KFunction *calledKFunction = kf->parent->functionMap[calledFunction];
-        if (distanceToTargetFunction.count(calledKFunction) != 0 &&
-            distance > distanceToTargetFunction.at(calledKFunction) + 1) {
-          distance = distanceToTargetFunction.at(calledKFunction) + 1;
-        }
-      }
-    }
-  }
-  return distance != UINT_MAX;
-}
-
-TargetedSearcher::WeightResult
-TargetedSearcher::tryGetLocalWeight(ExecutionState *es, weight_type &weight,
-                                    const std::vector<KBlock *> &localTargets) {
-  unsigned int intWeight = es->steppedMemoryInstructions;
-  KFunction *currentKF = es->pc->parent->parent;
-  KBlock *initKB = es->initPC->parent;
-  KBlock *currentKB = currentKF->blockMap[es->getPCBlock()];
-  KBlock *prevKB = currentKF->blockMap[es->getPrevPCBlock()];
-  const std::unordered_map<KBlock *, unsigned> &dist =
-      codeGraphDistance.getDistance(currentKB);
-  unsigned int localWeight = UINT_MAX;
-  for (auto &end : localTargets) {
-    if (dist.count(end) > 0) {
-      unsigned int w = dist.at(end);
-      localWeight = std::min(w, localWeight);
-    }
-  }
-
-  if (localWeight == UINT_MAX)
-    return Miss;
-  if (localWeight == 0 && (initKB == currentKB || prevKB != currentKB ||
-                           target->shouldFailOnThisTarget())) {
-    return Done;
-  }
-
-  intWeight += localWeight;
-  weight = ulog2(intWeight); // number on [0,32)-discrete-interval
-  return Continue;
-}
-
-TargetedSearcher::WeightResult
-TargetedSearcher::tryGetPreTargetWeight(ExecutionState *es,
-                                        weight_type &weight) {
-  KFunction *currentKF = es->pc->parent->parent;
-  std::vector<KBlock *> localTargets;
-  for (auto &kCallBlock : currentKF->kCallBlocks) {
-    for (auto &calledFunction : kCallBlock->calledFunctions) {
-      KFunction *calledKFunction =
-          currentKF->parent->functionMap[calledFunction];
-      if (distanceToTargetFunction.count(calledKFunction) > 0) {
-        localTargets.push_back(kCallBlock);
-      }
-    }
-  }
-
-  if (localTargets.empty())
-    return Miss;
-
-  WeightResult res = tryGetLocalWeight(es, weight, localTargets);
-  weight = weight + 32; // number on [32,64)-discrete-interval
-  return res == Done ? Continue : res;
-}
-
-TargetedSearcher::WeightResult
-TargetedSearcher::tryGetPostTargetWeight(ExecutionState *es,
-                                         weight_type &weight) {
-  KFunction *currentKF = es->pc->parent->parent;
-  std::vector<KBlock *> &localTargets = currentKF->returnKBlocks;
-
-  if (localTargets.empty())
-    return Miss;
-
-  WeightResult res = tryGetLocalWeight(es, weight, localTargets);
-  weight = weight + 32; // number on [32,64)-discrete-interval
-  return res == Done ? Continue : res;
-}
-
-TargetedSearcher::WeightResult
-TargetedSearcher::tryGetTargetWeight(ExecutionState *es, weight_type &weight) {
-  std::vector<KBlock *> localTargets = {target->getBlock()};
-  WeightResult res = tryGetLocalWeight(es, weight, localTargets);
-  return res;
-}
-
-TargetedSearcher::WeightResult
-TargetedSearcher::tryGetWeight(ExecutionState *es, weight_type &weight) {
-  if (target->atReturn() && !target->shouldFailOnThisTarget()) {
-    if (es->prevPC->parent == target->getBlock() &&
-        es->prevPC == target->getBlock()->getLastInstruction()) {
-      return Done;
-    } else if (es->pc->parent == target->getBlock()) {
-      weight = 0;
-      return Continue;
-    }
-  }
-
-  if (target->shouldFailOnThisTarget() && target->isTheSameAsIn(es->prevPC) &&
-      target->isThatError(es->error)) {
-    return Done;
-  }
-
+WeightResult TargetedSearcher::tryGetWeight(ExecutionState *es,
+                                            weight_type &weight) {
   BasicBlock *bb = es->getPCBlock();
   KBlock *kb = es->pc->parent->parent->blockMap[bb];
   KInstruction *ki = es->pc;
@@ -285,51 +166,14 @@ TargetedSearcher::tryGetWeight(ExecutionState *es, weight_type &weight) {
       states->tryGetWeight(es, weight)) {
     return Continue;
   }
-  unsigned int minCallWeight = UINT_MAX, minSfNum = UINT_MAX, sfNum = 0;
-  for (auto sfi = es->stack.rbegin(), sfe = es->stack.rend(); sfi != sfe;
-       sfi++) {
-    unsigned callWeight;
-    if (distanceInCallGraph(sfi->kf, kb, callWeight)) {
-      callWeight *= 2;
-      if (callWeight == 0 && target->shouldFailOnThisTarget()) {
-        weight = 0;
-        return target->isTheSameAsIn(kb->getFirstInstruction()) &&
-                       target->isThatError(es->error)
-                   ? Done
-                   : Continue;
-      } else {
-        callWeight += sfNum;
-      }
-
-      if (callWeight < minCallWeight) {
-        minCallWeight = callWeight;
-        minSfNum = sfNum;
-      }
-    }
 
-    if (sfi->caller) {
-      kb = sfi->caller->parent;
-      bb = kb->basicBlock;
-    }
-    sfNum++;
-
-    if (minCallWeight < sfNum)
-      break;
+  auto distRes = distanceCalculator.getDistance(*es, target);
+  weight = ulog2(distRes.weight + es->steppedMemoryInstructions); // [0, 32]
+  if (!distRes.isInsideFunction) {
+    weight += 32; // [32, 64]
   }
 
-  WeightResult res = Miss;
-  if (minCallWeight == 0)
-    res = tryGetTargetWeight(es, weight);
-  else if (minSfNum == 0)
-    res = tryGetPreTargetWeight(es, weight);
-  else if (minSfNum != UINT_MAX)
-    res = tryGetPostTargetWeight(es, weight);
-  if (Done == res && target->shouldFailOnThisTarget()) {
-    if (!target->isThatError(es->error)) {
-      res = Continue;
-    }
-  }
-  return res;
+  return distRes.result;
 }
 
 void TargetedSearcher::update(
@@ -436,10 +280,10 @@ void TargetedSearcher::removeReached() {
 ///
 
 GuidedSearcher::GuidedSearcher(
-    CodeGraphDistance &codeGraphDistance, TargetCalculator &stateHistory,
+    DistanceCalculator &distanceCalculator, TargetCalculator &stateHistory,
     std::set<ExecutionState *, ExecutionStateIDCompare> &pausedStates,
     std::size_t bound, RNG &rng, Searcher *baseSearcher)
-    : baseSearcher(baseSearcher), codeGraphDistance(codeGraphDistance),
+    : baseSearcher(baseSearcher), distanceCalculator(distanceCalculator),
       stateHistory(stateHistory), pausedStates(pausedStates), bound(bound),
       theRNG(rng) {
   guidance = baseSearcher ? CoverageGuidance : ErrorGuidance;
@@ -833,7 +677,7 @@ bool GuidedSearcher::tryAddTarget(ref<TargetForest::History> history,
   assert(targetedSearchers.count(history) == 0 ||
          targetedSearchers.at(history).count(target) == 0);
   targetedSearchers[history][target] =
-      std::make_unique<TargetedSearcher>(target, codeGraphDistance);
+      std::make_unique<TargetedSearcher>(target, distanceCalculator);
   auto it = std::find_if(
       historiesAndTargets.begin(), historiesAndTargets.end(),
       [&history, &target](
diff --git a/lib/Core/Searcher.h b/lib/Core/Searcher.h
index f307f46a77..c92e125c25 100644
--- a/lib/Core/Searcher.h
+++ b/lib/Core/Searcher.h
@@ -10,6 +10,7 @@
 #ifndef KLEE_SEARCHER_H
 #define KLEE_SEARCHER_H
 
+#include "DistanceCalculator.h"
 #include "ExecutionState.h"
 #include "PForest.h"
 #include "PTree.h"
@@ -34,13 +35,14 @@ class raw_ostream;
 } // namespace llvm
 
 namespace klee {
-class CodeGraphDistance;
+class DistanceCalculator;
 template <class T, class Comparator> class DiscretePDF;
 template <class T, class Comparator> class WeightedQueue;
 class ExecutionState;
 class Executor;
 class TargetCalculator;
 class TargetForest;
+class TargetReachability;
 
 /// A Searcher implements an exploration strategy for the Executor by selecting
 /// states for further exploration using different strategies or heuristics.
@@ -129,33 +131,17 @@ class RandomSearcher final : public Searcher {
 
 /// TargetedSearcher picks a state /*COMMENT*/.
 class TargetedSearcher final : public Searcher {
-public:
-  enum WeightResult : std::uint8_t {
-    Continue,
-    Done,
-    Miss,
-  };
-
 private:
-  typedef unsigned weight_type;
-
   std::unique_ptr<WeightedQueue<ExecutionState *, ExecutionStateIDCompare>>
       states;
   ref<Target> target;
-  CodeGraphDistance &codeGraphDistance;
-  const std::unordered_map<KFunction *, unsigned int> &distanceToTargetFunction;
+  DistanceCalculator &distanceCalculator;
   std::set<ExecutionState *> reachedOnLastUpdate;
 
-  bool distanceInCallGraph(KFunction *kf, KBlock *kb, unsigned int &distance);
-  WeightResult tryGetLocalWeight(ExecutionState *es, weight_type &weight,
-                                 const std::vector<KBlock *> &localTargets);
-  WeightResult tryGetPreTargetWeight(ExecutionState *es, weight_type &weight);
-  WeightResult tryGetTargetWeight(ExecutionState *es, weight_type &weight);
-  WeightResult tryGetPostTargetWeight(ExecutionState *es, weight_type &weight);
   WeightResult tryGetWeight(ExecutionState *es, weight_type &weight);
 
 public:
-  TargetedSearcher(ref<Target> target, CodeGraphDistance &distance);
+  TargetedSearcher(ref<Target> target, DistanceCalculator &distanceCalculator);
   ~TargetedSearcher() override;
 
   ExecutionState &selectState() override;
@@ -217,7 +203,7 @@ class GuidedSearcher final : public Searcher {
   Guidance guidance;
   std::unique_ptr<Searcher> baseSearcher;
   TargetForestHistoryToSearcherMap targetedSearchers;
-  CodeGraphDistance &codeGraphDistance;
+  DistanceCalculator &distanceCalculator;
   TargetCalculator &stateHistory;
   TargetHashSet reachedTargets;
   std::set<ExecutionState *, ExecutionStateIDCompare> &pausedStates;
@@ -255,7 +241,7 @@ class GuidedSearcher final : public Searcher {
 
 public:
   GuidedSearcher(
-      CodeGraphDistance &codeGraphDistance, TargetCalculator &stateHistory,
+      DistanceCalculator &distanceCalculator, TargetCalculator &stateHistory,
       std::set<ExecutionState *, ExecutionStateIDCompare> &pausedStates,
       std::size_t bound, RNG &rng, Searcher *baseSearcher = nullptr);
   ~GuidedSearcher() override = default;
diff --git a/lib/Core/UserSearcher.cpp b/lib/Core/UserSearcher.cpp
index c2e9f0bb63..72800087b9 100644
--- a/lib/Core/UserSearcher.cpp
+++ b/lib/Core/UserSearcher.cpp
@@ -183,7 +183,7 @@ Searcher *klee::constructUserSearcher(Executor &executor,
       searcher = nullptr;
     }
     searcher = new GuidedSearcher(
-        *executor.codeGraphDistance.get(), *executor.targetCalculator,
+        *executor.distanceCalculator, *executor.targetCalculator,
         executor.pausedStates, MaxCycles - 1, executor.theRNG, searcher);
   }
 
diff --git a/lib/Expr/Assignment.cpp b/lib/Expr/Assignment.cpp
index b176b8ed7b..798b774221 100644
--- a/lib/Expr/Assignment.cpp
+++ b/lib/Expr/Assignment.cpp
@@ -29,8 +29,24 @@ void Assignment::dump() const {
   }
 }
 
-ConstraintSet Assignment::createConstraintsFromAssignment() const {
-  ConstraintSet result;
+void Assignment::add(const Assignment &b) {
+  for (bindings_ty::const_iterator it = b.bindings.begin();
+       it != b.bindings.end(); it++) {
+    if (bindings.find(it->first) == bindings.end()) {
+      bindings[it->first] = {};
+    }
+    SparseStorage<unsigned char> &s = bindings[it->first];
+    size_t pos = s.size();
+    s.resize(s.size() + it->second.size());
+    for (unsigned char c : it->second) {
+      s.store(pos, c);
+      pos++;
+    }
+  }
+}
+
+constraints_ty Assignment::createConstraintsFromAssignment() const {
+  constraints_ty result;
   for (const auto &binding : bindings) {
     const auto &array = binding.first;
     const auto &values = binding.second;
@@ -40,17 +56,15 @@ ConstraintSet Assignment::createConstraintsFromAssignment() const {
     uint64_t arraySize = arrayConstantSize->getZExtValue();
     if (arraySize <= 8 && array->getRange() == Expr::Int8) {
       ref<Expr> e = Expr::createTempRead(array, arraySize * array->getRange());
-      result.addConstraint(EqExpr::create(e, evaluate(e)), {});
+      result.insert(EqExpr::create(e, evaluate(e)));
     } else {
       for (unsigned arrayIndex = 0; arrayIndex < arraySize; ++arrayIndex) {
         unsigned char value = values.load(arrayIndex);
-        result.addConstraint(
-            EqExpr::create(
-                ReadExpr::create(
-                    UpdateList(array, 0),
-                    ConstantExpr::alloc(arrayIndex, array->getDomain())),
-                ConstantExpr::alloc(value, array->getRange())),
-            {});
+        result.insert(EqExpr::create(
+            ReadExpr::create(
+                UpdateList(array, 0),
+                ConstantExpr::alloc(arrayIndex, array->getDomain())),
+            ConstantExpr::alloc(value, array->getRange())));
       }
     }
   }
@@ -89,7 +103,9 @@ Assignment Assignment::part(const SymcreteOrderedSet &symcretes) const {
   Assignment ret(allowFreeValues);
   for (auto symcrete : symcretes) {
     for (auto array : symcrete->dependentArrays()) {
-      ret.bindings.insert({array, bindings.at(array)});
+      if (bindings.find(array) != bindings.end()) {
+        ret.bindings.insert({array, bindings.at(array)});
+      }
     }
   }
   return ret;
diff --git a/lib/Expr/CMakeLists.txt b/lib/Expr/CMakeLists.txt
index 648abee448..d46995f482 100644
--- a/lib/Expr/CMakeLists.txt
+++ b/lib/Expr/CMakeLists.txt
@@ -22,6 +22,7 @@ klee_add_component(kleaverExpr
   ExprSMTLIBPrinter.cpp
   ExprUtil.cpp
   ExprVisitor.cpp
+  IndependentConstraintSetUnion.cpp
   IndependentSet.cpp
   Path.cpp
   SourceBuilder.cpp
diff --git a/lib/Expr/Constraints.cpp b/lib/Expr/Constraints.cpp
index 4ea34c677a..528ecb3ffc 100644
--- a/lib/Expr/Constraints.cpp
+++ b/lib/Expr/Constraints.cpp
@@ -246,18 +246,21 @@ class ExprReplaceVisitor3 : public ExprVisitor {
 
 ConstraintSet::ConstraintSet(constraints_ty cs, symcretes_ty symcretes,
                              Assignment concretization)
-    : _constraints(cs), _symcretes(symcretes), _concretization(concretization) {
-}
+    : _constraints(cs), _symcretes(symcretes), _concretization(concretization),
+      _independentElements(_constraints, _symcretes, _concretization) {}
 
-ConstraintSet::ConstraintSet() : _concretization(Assignment(true)) {}
+ConstraintSet::ConstraintSet()
+    : _concretization(Assignment(true)),
+      _independentElements({}, {}, _concretization) {}
 
 void ConstraintSet::addConstraint(ref<Expr> e, const Assignment &delta) {
   _constraints.insert(e);
-
+  _independentElements.addExpr(e);
   // Update bindings
   for (auto i : delta.bindings) {
     _concretization.bindings[i.first] = i.second;
   }
+  _independentElements.updateConcretization(delta);
 }
 
 IDType Symcrete::idCounter = 0;
@@ -265,9 +268,13 @@ IDType Symcrete::idCounter = 0;
 void ConstraintSet::addSymcrete(ref<Symcrete> s,
                                 const Assignment &concretization) {
   _symcretes.insert(s);
+  _independentElements.addSymcrete(s);
+  Assignment dependentConcretization(true);
   for (auto i : s->dependentArrays()) {
     _concretization.bindings[i] = concretization.bindings.at(i);
+    dependentConcretization.bindings[i] = concretization.bindings.at(i);
   }
+  _independentElements.updateConcretization(dependentConcretization);
 }
 
 bool ConstraintSet::isSymcretized(ref<Expr> expr) const {
@@ -285,6 +292,28 @@ void ConstraintSet::rewriteConcretization(const Assignment &a) {
       _concretization.bindings[i.first] = i.second;
     }
   }
+  _independentElements.updateConcretization(a);
+}
+
+ConstraintSet ConstraintSet::getConcretizedVersion() const {
+  ConstraintSet cs;
+  cs._independentElements = _independentElements.getConcretizedVersion();
+
+  for (ref<Expr> e : cs._independentElements.is()) {
+    cs._constraints.insert(e);
+  }
+  return cs;
+}
+
+ConstraintSet ConstraintSet::getConcretizedVersion(
+    const Assignment &newConcretization) const {
+  ConstraintSet cs;
+  cs._independentElements =
+      _independentElements.getConcretizedVersion(newConcretization);
+  for (ref<Expr> e : cs._independentElements.is()) {
+    cs._constraints.insert(e);
+  }
+  return cs;
 }
 
 void ConstraintSet::print(llvm::raw_ostream &os) const {
@@ -311,6 +340,11 @@ const constraints_ty &ConstraintSet::cs() const { return _constraints; }
 
 const symcretes_ty &ConstraintSet::symcretes() const { return _symcretes; }
 
+const IndependentConstraintSetUnion &
+ConstraintSet::independentElements() const {
+  return _independentElements;
+}
+
 const Path &PathConstraints::path() const { return _path; }
 
 const ExprHashMap<Path::PathIndex> &PathConstraints::indexes() const {
@@ -581,6 +615,18 @@ Simplificator::composeExprDependencies(const ExprHashMap<ExprHashSet> &upper,
   return result;
 }
 
+void ConstraintSet::getAllIndependentConstraintsSets(
+    const ref<Expr> &queryExpr,
+    std::vector<ref<const IndependentConstraintSet>> &result) const {
+  _independentElements.getAllIndependentConstraintSets(queryExpr, result);
+}
+
+ref<const IndependentConstraintSet>
+ConstraintSet::getIndependentConstraints(const ref<Expr> &queryExpr,
+                                         constraints_ty &result) const {
+  return _independentElements.getIndependentConstraints(queryExpr, result);
+}
+
 std::vector<const Array *> ConstraintSet::gatherArrays() const {
   std::vector<const Array *> arrays;
   findObjects(_constraints.begin(), _constraints.end(), arrays);
diff --git a/lib/Expr/IndependentConstraintSetUnion.cpp b/lib/Expr/IndependentConstraintSetUnion.cpp
new file mode 100644
index 0000000000..8bb8e0d6ea
--- /dev/null
+++ b/lib/Expr/IndependentConstraintSetUnion.cpp
@@ -0,0 +1,140 @@
+#include "klee/Expr/IndependentConstraintSetUnion.h"
+
+namespace klee {
+void IndependentConstraintSetUnion::updateConcretization(
+    const Assignment &delta) {
+  for (ref<Expr> e : roots) {
+    ref<const IndependentConstraintSet> &ics = disjointSets[e];
+    Assignment part = delta.part(ics->symcretes);
+    ics = ics->updateConcretization(part, concretizedExprs);
+  }
+  for (auto it : delta.bindings) {
+    concretization.bindings[it.first] = it.second;
+  }
+}
+
+void IndependentConstraintSetUnion::removeConcretization(
+    const Assignment &remove) {
+  for (ref<Expr> e : roots) {
+    ref<const IndependentConstraintSet> &ics = disjointSets[e];
+    Assignment part = remove.part(ics->symcretes);
+    ics = ics->removeConcretization(part, concretizedExprs);
+  }
+  for (auto it : remove.bindings) {
+    concretization.bindings.erase(it.first);
+  }
+}
+void IndependentConstraintSetUnion::reEvaluateConcretization(
+    const Assignment &newConcretization) {
+  Assignment delta(true);
+  Assignment removed(true);
+  for (const auto it : concretization) {
+    if (newConcretization.bindings.count(it.first) == 0) {
+      removed.bindings.insert(it);
+    } else if (newConcretization.bindings.at(it.first) != it.second) {
+      delta.bindings.insert(*(newConcretization.bindings.find(it.first)));
+    }
+  }
+  updateConcretization(delta);
+  removeConcretization(removed);
+}
+IndependentConstraintSetUnion::IndependentConstraintSetUnion()
+    : concretization(Assignment(true)) {}
+
+ref<const IndependentConstraintSet>
+IndependentConstraintSetUnion::getIndependentConstraints(
+    const ref<Expr> &e, constraints_ty &result) const {
+  ref<const IndependentConstraintSet> compare = new IndependentConstraintSet(e);
+
+  for (ref<Expr> i : internalStorage) {
+    ref<Expr> a = constFind(i);
+    ref<const IndependentConstraintSet> ics = disjointSets.find(a)->second;
+    if (IndependentConstraintSet::intersects(ics, compare)) {
+      for (ref<Expr> expr : ics->exprs) {
+        result.insert(expr);
+      }
+    }
+  }
+  return compare;
+}
+
+void IndependentConstraintSetUnion::getAllIndependentConstraintSets(
+    const ref<Expr> &e,
+    std::vector<ref<const IndependentConstraintSet>> &result) const {
+  IndependentConstraintSetUnion u = *this;
+  ConstantExpr *CE = dyn_cast<ConstantExpr>(e);
+  ref<Expr> neg;
+  if (CE) {
+    assert(CE && CE->isFalse() &&
+           "the expr should always be false and "
+           "therefore not included in factors");
+    u.getAllIndependentSets(result);
+  } else {
+    // factor that contains query expr should be checked first
+    neg = Expr::createIsZero(e);
+    u.addExpr(neg);
+    result.push_back(u.findGroup(neg));
+    for (ref<Expr> v : u.roots) {
+      if (!u.areJoined(v, neg)) {
+        result.push_back(u.findGroup(v));
+      }
+    }
+  }
+}
+void IndependentConstraintSetUnion::addExpr(const ref<Expr> e) {
+  addValue(e);
+  disjointSets[find(e)] = disjointSets[find(e)]->addExpr(e);
+}
+void IndependentConstraintSetUnion::addSymcrete(const ref<Symcrete> s) {
+  ref<Expr> value = s->symcretized;
+  if (internalStorage.find(value) != internalStorage.end()) {
+    return;
+  }
+  parent[value] = value;
+  roots.insert(value);
+  rank[value] = 0;
+  disjointSets[value] = new IndependentConstraintSet(s);
+
+  internalStorage.insert(value);
+  std::vector<ref<Expr>> oldRoots(roots.begin(), roots.end());
+  for (ref<Expr> v : oldRoots) {
+    if (!areJoined(v, value) &&
+        IndependentConstraintSet::intersects(disjointSets[find(v)],
+                                             disjointSets[find(value)])) {
+      merge(v, value);
+    }
+  }
+  disjointSets[find(value)] = disjointSets[find(value)]->addExpr(value);
+}
+
+IndependentConstraintSetUnion::IndependentConstraintSetUnion(
+    const constraints_ty &is, const SymcreteOrderedSet &os, const Assignment &c)
+    : concretization(Assignment(true)) {
+  for (ref<Expr> e : is) {
+    addValue(e);
+  }
+  for (ref<Symcrete> s : os) {
+    addSymcrete(s);
+  }
+  updateConcretization(c);
+}
+
+IndependentConstraintSetUnion
+IndependentConstraintSetUnion::getConcretizedVersion() const {
+  IndependentConstraintSetUnion icsu;
+  for (ref<Expr> i : roots) {
+    ref<const IndependentConstraintSet> root = disjointSets.at(i);
+    icsu.add(root->concretizedSets);
+  }
+  icsu.concretizedExprs = concretizedExprs;
+  return icsu;
+}
+
+IndependentConstraintSetUnion
+IndependentConstraintSetUnion::getConcretizedVersion(
+    const Assignment &newConcretization) const {
+  IndependentConstraintSetUnion icsu = *this;
+  icsu.reEvaluateConcretization(newConcretization);
+  return icsu.getConcretizedVersion();
+}
+} // namespace klee
\ No newline at end of file
diff --git a/lib/Expr/IndependentSet.cpp b/lib/Expr/IndependentSet.cpp
index d4fade9ef1..2dd50cb196 100644
--- a/lib/Expr/IndependentSet.cpp
+++ b/lib/Expr/IndependentSet.cpp
@@ -1,6 +1,7 @@
 #include "klee/Expr/IndependentSet.h"
 
 #include "klee/ADT/Ref.h"
+#include "klee/Expr/Assignment.h"
 #include "klee/Expr/Constraints.h"
 #include "klee/Expr/ExprHashMap.h"
 #include "klee/Expr/ExprUtil.h"
@@ -16,9 +17,88 @@
 
 namespace klee {
 
-IndependentElementSet::IndependentElementSet() {}
+ref<const IndependentConstraintSet>
+IndependentConstraintSet::addExpr(ref<Expr> e) const {
+  ref<IndependentConstraintSet> ics = new IndependentConstraintSet(this);
+  ics->concretizedSets.addValue(concretization.evaluate(e));
+  return ics;
+}
+
+ref<const IndependentConstraintSet>
+IndependentConstraintSet::updateConcretization(
+    const Assignment &delta, ExprHashMap<ref<Expr>> &concretizedExprs) const {
+  ref<IndependentConstraintSet> ics = new IndependentConstraintSet(this);
+  if (delta.bindings.size() == 0) {
+    return ics;
+  }
+  for (auto i : delta.bindings) {
+    ics->concretization.bindings[i.first] = i.second;
+  }
+  InnerSetUnion DSU;
+  for (ref<Expr> i : exprs) {
+    ref<Expr> e = ics->concretization.evaluate(i);
+    concretizedExprs[i] = e;
+    DSU.addValue(e);
+  }
+  for (ref<Symcrete> s : symcretes) {
+    DSU.addValue(EqExpr::create(ics->concretization.evaluate(s->symcretized),
+                                s->symcretized));
+  }
+  ics->concretizedSets = DSU;
+  return ics;
+}
+
+ref<const IndependentConstraintSet>
+IndependentConstraintSet::removeConcretization(
+    const Assignment &delta, ExprHashMap<ref<Expr>> &concretizedExprs) const {
+  ref<IndependentConstraintSet> ics = new IndependentConstraintSet(this);
+  if (delta.bindings.size() == 0) {
+    return ics;
+  }
+  for (auto i : delta.bindings) {
+    ics->concretization.bindings.erase(i.first);
+  }
+  InnerSetUnion DSU;
+  for (ref<Expr> i : exprs) {
+    ref<Expr> e = ics->concretization.evaluate(i);
+    concretizedExprs[i] = e;
+    DSU.addValue(e);
+  }
+  for (ref<Symcrete> s : symcretes) {
+    DSU.addValue(EqExpr::create(ics->concretization.evaluate(s->symcretized),
+                                s->symcretized));
+  }
+
+  ics->concretizedSets = DSU;
+  return ics;
+}
 
-IndependentElementSet::IndependentElementSet(ref<Expr> e) {
+void IndependentConstraintSet::addValuesToAssignment(
+    const std::vector<const Array *> &objects,
+    const std::vector<SparseStorage<unsigned char>> &values,
+    Assignment &assign) const {
+  for (unsigned i = 0; i < values.size(); i++) {
+    if (assign.bindings.count(objects[i])) {
+      SparseStorage<unsigned char> &value = assign.bindings[objects[i]];
+      assert(value.size() == values[i].size() &&
+             "we're talking about the same array here");
+      DenseSet<unsigned> ds = (elements.find(objects[i]))->second;
+      for (std::set<unsigned>::iterator it2 = ds.begin(); it2 != ds.end();
+           it2++) {
+        unsigned index = *it2;
+        value.store(index, values[i].load(index));
+      }
+    } else {
+      assign.bindings[objects[i]] = values[i];
+    }
+  }
+}
+
+IndependentConstraintSet::IndependentConstraintSet()
+    : concretization(Assignment(true)) {}
+
+IndependentConstraintSet::IndependentConstraintSet(ref<Expr> e)
+    : concretization(Assignment(true)) {
   exprs.insert(e);
   // Track all reads in the program.  Determines whether reads are
   // concrete or symbolic.  If they are symbolic, "collapses" array
@@ -39,19 +119,24 @@ IndependentElementSet::IndependentElementSet(ref<Expr> e) {
       if (ConstantExpr *CE = dyn_cast<ConstantExpr>(re->index)) {
         // if index constant, then add to set of constraints operating
         // on that array (actually, don't add constraint, just set index)
-        DenseSet<unsigned> &dis = elements[array];
+        DenseSet<unsigned> dis;
+        if (elements.find(array) != elements.end()) {
+          dis = (elements.find(array))->second;
+        }
         dis.add((unsigned)CE->getZExtValue(32));
+        elements = elements.replace({array, dis});
       } else {
         elements_ty::iterator it2 = elements.find(array);
         if (it2 != elements.end())
-          elements.erase(it2);
-        wholeObjects.insert(array);
+          elements = elements.remove(it2->first);
+        wholeObjects = wholeObjects.insert(array);
       }
     }
   }
 }
 
-IndependentElementSet::IndependentElementSet(ref<Symcrete> s) {
+IndependentConstraintSet::IndependentConstraintSet(ref<Symcrete> s)
+    : concretization(Assignment(true)) {
   symcretes.insert(s);
 
   for (Symcrete &dependentSymcrete : s->dependentSymcretes()) {
@@ -93,35 +178,45 @@ IndependentElementSet::IndependentElementSet(ref<Symcrete> s) {
       if (ConstantExpr *CE = dyn_cast<ConstantExpr>(re->index)) {
         // if index constant, then add to set of constraints operating
         // on that array (actually, don't add constraint, just set index)
-        DenseSet<unsigned> &dis = elements[array];
+        DenseSet<unsigned> dis;
+        if (elements.find(array) != elements.end()) {
+          dis = (elements.find(array))->second;
+        }
         dis.add((unsigned)CE->getZExtValue(32));
+        elements = elements.replace({array, dis});
       } else {
         elements_ty::iterator it2 = elements.find(array);
         if (it2 != elements.end())
-          elements.erase(it2);
-        wholeObjects.insert(array);
+          elements = elements.remove(it2->first);
+        wholeObjects = wholeObjects.insert(array);
       }
     }
   }
 }
 
-IndependentElementSet::IndependentElementSet(const IndependentElementSet &ies)
-    : elements(ies.elements), wholeObjects(ies.wholeObjects), exprs(ies.exprs) {
-}
-
-IndependentElementSet &
-IndependentElementSet::operator=(const IndependentElementSet &ies) {
-  elements = ies.elements;
-  wholeObjects = ies.wholeObjects;
-  exprs = ies.exprs;
+IndependentConstraintSet::IndependentConstraintSet(
+    const ref<const IndependentConstraintSet> &ics)
+    : elements(ics->elements), wholeObjects(ics->wholeObjects),
+      exprs(ics->exprs), symcretes(ics->symcretes),
+      concretization(ics->concretization),
+      concretizedSets(ics->concretizedSets) {}
+
+IndependentConstraintSet &
+IndependentConstraintSet::operator=(const IndependentConstraintSet &ics) {
+  elements = ics.elements;
+  wholeObjects = ics.wholeObjects;
+  exprs = ics.exprs;
+  symcretes = ics.symcretes;
+  concretization = ics.concretization;
+  concretizedSets = ics.concretizedSets;
   return *this;
 }
 
-void IndependentElementSet::print(llvm::raw_ostream &os) const {
+void IndependentConstraintSet::print(llvm::raw_ostream &os) const {
   os << "{";
   bool first = true;
-  for (std::set<const Array *>::iterator it = wholeObjects.begin(),
-                                         ie = wholeObjects.end();
+  for (ImmutableSet<const Array *>::iterator it = wholeObjects.begin(),
+                                             ie = wholeObjects.end();
        it != ie; ++it) {
     const Array *array = *it;
 
@@ -133,7 +228,7 @@ void IndependentElementSet::print(llvm::raw_ostream &os) const {
 
     os << "MO" << array->getIdentifier();
   }
-  for (elements_ty::const_iterator it = elements.begin(), ie = elements.end();
+  for (elements_ty::iterator it = elements.begin(), ie = elements.end();
        it != ie; ++it) {
     const Array *array = it->first;
     const DenseSet<unsigned> &dis = it->second;
@@ -149,216 +244,104 @@ void IndependentElementSet::print(llvm::raw_ostream &os) const {
   os << "}";
 }
 
-// more efficient when this is the smaller set
-bool IndependentElementSet::intersects(const IndependentElementSet &b) {
+bool IndependentConstraintSet::intersects(
+    ref<const IndependentConstraintSet> a,
+    ref<const IndependentConstraintSet> b) {
+  if (a->exprs.size() + a->symcretes.size() >
+      b->exprs.size() + b->symcretes.size()) {
+    std::swap(a, b);
+  }
   // If there are any symbolic arrays in our query that b accesses
-  for (std::set<const Array *>::iterator it = wholeObjects.begin(),
-                                         ie = wholeObjects.end();
+  for (ImmutableSet<const Array *>::iterator it = a->wholeObjects.begin(),
+                                             ie = a->wholeObjects.end();
        it != ie; ++it) {
     const Array *array = *it;
-    if (b.wholeObjects.count(array) ||
-        b.elements.find(array) != b.elements.end())
+    if (b->wholeObjects.count(array) ||
+        b->elements.find(array) != b->elements.end())
       return true;
   }
-  for (elements_ty::iterator it = elements.begin(), ie = elements.end();
+  for (elements_ty::iterator it = a->elements.begin(), ie = a->elements.end();
        it != ie; ++it) {
     const Array *array = it->first;
     // if the array we access is symbolic in b
-    if (b.wholeObjects.count(array))
+    if (b->wholeObjects.count(array))
       return true;
-    elements_ty::const_iterator it2 = b.elements.find(array);
+    elements_ty::iterator it2 = b->elements.find(array);
     // if any of the elements we access are also accessed by b
-    if (it2 != b.elements.end()) {
-      if (it->second.intersects(it2->second))
+    if (it2 != b->elements.end()) {
+      if (it->second.intersects(it2->second)) {
         return true;
+      }
     }
   }
   // No need to check symcretes here, arrays must be sufficient.
   return false;
 }
 
-// returns true iff set is changed by addition
-bool IndependentElementSet::add(const IndependentElementSet &b) {
-  for (auto expr : b.exprs) {
-    exprs.insert(expr);
-  }
+ref<const IndependentConstraintSet>
+IndependentConstraintSet::merge(ref<const IndependentConstraintSet> A,
+                                ref<const IndependentConstraintSet> B) {
+  ref<IndependentConstraintSet> a = new IndependentConstraintSet(A);
+  ref<IndependentConstraintSet> b = new IndependentConstraintSet(B);
 
-  for (const ref<Symcrete> &symcrete : b.symcretes) {
-    symcretes.insert(symcrete);
+  if (a->exprs.size() + a->symcretes.size() <
+      b->exprs.size() + b->symcretes.size()) {
+    std::swap(a, b);
+  }
+  for (ref<Expr> expr : b->exprs) {
+    a->exprs.insert(expr);
+  }
+  for (const ref<Symcrete> &symcrete : b->symcretes) {
+    a->symcretes.insert(symcrete);
   }
 
-  bool modified = false;
-  for (std::set<const Array *>::const_iterator it = b.wholeObjects.begin(),
-                                               ie = b.wholeObjects.end();
+  for (ImmutableSet<const Array *>::iterator it = b->wholeObjects.begin(),
+                                             ie = b->wholeObjects.end();
        it != ie; ++it) {
     const Array *array = *it;
-    elements_ty::iterator it2 = elements.find(array);
-    if (it2 != elements.end()) {
-      modified = true;
-      elements.erase(it2);
-      wholeObjects.insert(array);
+    elements_ty::iterator it2 = a->elements.find(array);
+    if (it2 != a->elements.end()) {
+      a->elements = a->elements.remove(it2->first);
+      a->wholeObjects = a->wholeObjects.insert(array);
     } else {
-      if (!wholeObjects.count(array)) {
-        modified = true;
-        wholeObjects.insert(array);
+      if (!a->wholeObjects.count(array)) {
+        a->wholeObjects = a->wholeObjects.insert(array);
       }
     }
   }
-  for (elements_ty::const_iterator it = b.elements.begin(),
-                                   ie = b.elements.end();
+  for (elements_ty::iterator it = b->elements.begin(), ie = b->elements.end();
        it != ie; ++it) {
     const Array *array = it->first;
-    if (!wholeObjects.count(array)) {
-      elements_ty::iterator it2 = elements.find(array);
-      if (it2 == elements.end()) {
-        modified = true;
-        elements.insert(*it);
+    if (!a->wholeObjects.count(array)) {
+      elements_ty::iterator it2 = a->elements.find(array);
+      if (it2 == a->elements.end()) {
+        a->elements = a->elements.insert(*it);
       } else {
-        // Now need to see if there are any (z=?)'s
-        if (it2->second.add(it->second))
-          modified = true;
+        DenseSet<unsigned> dis = it2->second;
+        dis.add(it->second);
+        a->elements = a->elements.replace({array, dis});
       }
     }
   }
-  return modified;
-}
-
-// Breaks down a constraint into all of it's individual pieces, returning a
-// list of IndependentElementSets or the independent factors.
-//
-// Caller takes ownership of returned std::list.
-std::list<IndependentElementSet> *
-getAllIndependentConstraintsSets(const Query &query) {
-  std::list<IndependentElementSet> *factors =
-      new std::list<IndependentElementSet>();
-  ConstantExpr *CE = dyn_cast<ConstantExpr>(query.expr);
-  if (CE) {
-    assert(CE && CE->isFalse() &&
-           "the expr should always be false and "
-           "therefore not included in factors");
-  } else {
-    ref<Expr> neg = Expr::createIsZero(query.expr);
-    factors->push_back(IndependentElementSet(neg));
-  }
-
-  for (const auto &constraint : query.constraints.cs()) {
-    // iterate through all the previously separated constraints.  Until we
-    // actually return, factors is treated as a queue of expressions to be
-    // evaluated.  If the queue property isn't maintained, then the exprs
-    // could be returned in an order different from how they came it, negatively
-    // affecting later stages.
-    factors->push_back(IndependentElementSet(constraint));
-  }
-
-  for (const auto &symcrete : query.constraints.symcretes()) {
-    factors->push_back(IndependentElementSet(symcrete));
-  }
-
-  bool doneLoop = false;
-  do {
-    doneLoop = true;
-    std::list<IndependentElementSet> *done =
-        new std::list<IndependentElementSet>;
-    while (factors->size() > 0) {
-      IndependentElementSet current = factors->front();
-      factors->pop_front();
-      // This list represents the set of factors that are separate from current.
-      // Those that are not inserted into this list (queue) intersect with
-      // current.
-      std::list<IndependentElementSet> *keep =
-          new std::list<IndependentElementSet>;
-      while (factors->size() > 0) {
-        IndependentElementSet compare = factors->front();
-        factors->pop_front();
-        if (current.intersects(compare)) {
-          if (current.add(compare)) {
-            // Means that we have added (z=y)added to (x=y)
-            // Now need to see if there are any (z=?)'s
-            doneLoop = false;
-          }
-        } else {
-          keep->push_back(compare);
-        }
-      }
-      done->push_back(current);
-      delete factors;
-      factors = keep;
-    }
-    delete factors;
-    factors = done;
-  } while (!doneLoop);
-
-  return factors;
-}
-
-IndependentElementSet getIndependentConstraints(const Query &query,
-                                                constraints_ty &result) {
-  IndependentElementSet eltsClosure(query.expr);
-  std::vector<std::pair<ref<Expr>, IndependentElementSet>> worklist;
-
-  for (const auto &constraint : query.constraints.cs())
-    worklist.push_back(
-        std::make_pair(constraint, IndependentElementSet(constraint)));
-
-  for (const ref<Symcrete> &symcrete : query.constraints.symcretes()) {
-    worklist.push_back(
-        std::make_pair(symcrete->symcretized, IndependentElementSet(symcrete)));
-  }
-
-  // XXX This should be more efficient (in terms of low level copy stuff).
-  bool done = false;
-  do {
-    done = true;
-    std::vector<std::pair<ref<Expr>, IndependentElementSet>> newWorklist;
-    for (std::vector<std::pair<ref<Expr>, IndependentElementSet>>::iterator
-             it = worklist.begin(),
-             ie = worklist.end();
-         it != ie; ++it) {
-      if (it->second.intersects(eltsClosure)) {
-        if (eltsClosure.add(it->second))
-          done = false;
-        result.insert(it->first);
-        // Means that we have added (z=y)added to (x=y)
-        // Now need to see if there are any (z=?)'s
-      } else {
-        newWorklist.push_back(*it);
-      }
-    }
-    worklist.swap(newWorklist);
-  } while (!done);
-
-  // KLEE_DEBUG(
-  //     std::set<ref<Expr>> reqset(result.begin(), result.end());
-  //     errs() << "--\n"; errs() << "Q: " << query.expr << "\n";
-  //     errs() << "\telts: " << IndependentElementSet(query.expr) << "\n";
-  //     int i = 0; for (const auto &constraint
-  //                     : query.constraints) {
-  //       errs() << "C" << i++ << ": " << constraint;
-  //       errs() << " "
-  //              << (reqset.count(constraint) ? "(required)" : "(independent)")
-  //              << "\n";
-  //       errs() << "\telts: " << IndependentElementSet(constraint) << "\n";
-  //     } errs() << "elts closure: "
-  //              << eltsClosure << "\n";);
-
-  return eltsClosure;
+  b->addValuesToAssignment(b->concretization.keys(), b->concretization.values(),
+                           a->concretization);
+  a->concretizedSets.add(b->concretizedSets);
+  return a;
 }
 
-void calculateArrayReferences(const IndependentElementSet &ie,
-                              std::vector<const Array *> &returnVector) {
+void IndependentConstraintSet::calculateArrayReferences(
+    std::vector<const Array *> &returnVector) const {
   std::set<const Array *> thisSeen;
-  for (std::map<const Array *, DenseSet<unsigned>>::const_iterator it =
-           ie.elements.begin();
-       it != ie.elements.end(); it++) {
+  for (IndependentConstraintSet::elements_ty::iterator it = elements.begin();
+       it != elements.end(); ++it) {
     thisSeen.insert(it->first);
   }
-  for (std::set<const Array *>::iterator it = ie.wholeObjects.begin();
-       it != ie.wholeObjects.end(); it++) {
-    assert(*it);
+  for (ImmutableSet<const Array *>::iterator it = wholeObjects.begin();
+       it != wholeObjects.end(); ++it) {
     thisSeen.insert(*it);
   }
   for (std::set<const Array *>::iterator it = thisSeen.begin();
-       it != thisSeen.end(); it++) {
+       it != thisSeen.end(); ++it) {
     returnVector.push_back(*it);
   }
 }
diff --git a/lib/Module/TargetForest.cpp b/lib/Module/TargetForest.cpp
index d3c80efd30..bc54d1949e 100644
--- a/lib/Module/TargetForest.cpp
+++ b/lib/Module/TargetForest.cpp
@@ -15,6 +15,8 @@
 #include "klee/Module/KModule.h"
 #include "klee/Module/TargetHash.h"
 
+#include "klee/Support/ErrorHandling.h"
+
 using namespace klee;
 using namespace llvm;
 
@@ -510,6 +512,14 @@ void TargetForest::blockIn(ref<Target> subtarget, ref<Target> target) {
   forest = forest->blockLeafInChild(subtarget, target);
 }
 
+void TargetForest::block(const ref<Target> &target) {
+  if (!forest->deepFind(target)) {
+    return;
+  }
+
+  forest = forest->blockLeaf(target);
+}
+
 void TargetForest::dump() const {
   llvm::errs() << "History:\n";
   history->dump();
diff --git a/lib/Solver/AssignmentValidatingSolver.cpp b/lib/Solver/AssignmentValidatingSolver.cpp
index 993af59043..3bdab35df2 100644
--- a/lib/Solver/AssignmentValidatingSolver.cpp
+++ b/lib/Solver/AssignmentValidatingSolver.cpp
@@ -168,7 +168,8 @@ void AssignmentValidatingSolver::dumpAssignmentQuery(
     const Query &query, const Assignment &assignment) {
   // Create a Query that is augmented with constraints that
   // enforce the given assignment.
-  auto constraints = assignment.createConstraintsFromAssignment();
+  auto constraints =
+      ConstraintSet(assignment.createConstraintsFromAssignment(), {}, {});
 
   // Add Constraints from `query`
   assert(!query.containsSymcretes());
diff --git a/lib/Solver/ConcretizingSolver.cpp b/lib/Solver/ConcretizingSolver.cpp
index 8d1886ae57..f4058d2b2b 100644
--- a/lib/Solver/ConcretizingSolver.cpp
+++ b/lib/Solver/ConcretizingSolver.cpp
@@ -54,18 +54,59 @@ class ConcretizingSolver : public SolverImpl {
 
 private:
   bool assertConcretization(const Query &query, const Assignment &assign) const;
+  bool getBrokenArrays(const Query &query, const Assignment &diff,
+                       ref<SolverResponse> &result,
+                       std::vector<const Array *> &brokenArrays);
   bool relaxSymcreteConstraints(const Query &query,
                                 ref<SolverResponse> &result);
   Query constructConcretizedQuery(const Query &, const Assignment &);
+  Query getConcretizedVersion(const Query &);
+
+private:
+  void reverseConcretization(ValidityCore &validityCore,
+                             const ExprHashMap<ref<Expr>> &reverse,
+                             ref<Expr> reverseExpr);
+  void reverseConcretization(ref<SolverResponse> &res,
+                             const ExprHashMap<ref<Expr>> &reverse,
+                             ref<Expr> reverseExpr);
 };
 
 Query ConcretizingSolver::constructConcretizedQuery(const Query &query,
                                                     const Assignment &assign) {
-  ConstraintSet constraints = assign.createConstraintsFromAssignment();
-  for (auto e : query.constraints.cs()) {
-    constraints.addConstraint(e, {});
+  ConstraintSet cs = query.constraints;
+  ref<Expr> concretizedExpr = assign.evaluate(query.expr);
+  return Query(cs.getConcretizedVersion(assign), concretizedExpr);
+}
+
+Query ConcretizingSolver::getConcretizedVersion(const Query &query) {
+  ConstraintSet cs = query.constraints;
+  ref<Expr> concretizedExpr = cs.concretization().evaluate(query.expr);
+  return Query(cs.getConcretizedVersion(), concretizedExpr);
+}
+
+void ConcretizingSolver::reverseConcretization(
+    ValidityCore &validityCore, const ExprHashMap<ref<Expr>> &reverse,
+    ref<Expr> reverseExpr) {
+  validityCore.expr = reverseExpr;
+  for (auto e : reverse) {
+    if (validityCore.constraints.find(e.second) !=
+        validityCore.constraints.end()) {
+      validityCore.constraints.erase(e.second);
+      validityCore.constraints.insert(e.first);
+    }
   }
-  return Query(constraints, query.expr);
+}
+
+void ConcretizingSolver::reverseConcretization(
+    ref<SolverResponse> &res, const ExprHashMap<ref<Expr>> &reverse,
+    ref<Expr> reverseExpr) {
+  if (!isa<ValidResponse>(res)) {
+    return;
+  }
+  ValidityCore validityCore;
+  res->tryGetValidityCore(validityCore);
+  reverseConcretization(validityCore, reverse, reverseExpr);
+  res = new ValidResponse(validityCore);
 }
 
 bool ConcretizingSolver::assertConcretization(const Query &query,
@@ -79,6 +120,41 @@ bool ConcretizingSolver::assertConcretization(const Query &query,
   return true;
 }
 
+bool ConcretizingSolver::getBrokenArrays(
+    const Query &query, const Assignment &assign, ref<SolverResponse> &result,
+    std::vector<const Array *> &brokenArrays) {
+  Query concretizedQuery = constructConcretizedQuery(query, assign);
+  ref<ConstantExpr> CE = dyn_cast<ConstantExpr>(concretizedQuery.expr);
+  if (CE && CE->isTrue()) {
+    findObjects(query.expr, brokenArrays);
+    result = new UnknownResponse();
+    return true;
+  }
+  const ExprHashMap<ref<Expr>> &reverse =
+      concretizedQuery.constraints.independentElements().concretizedExprs;
+  ref<Expr> reverseExpr = query.expr;
+  if (!solver->impl->check(concretizedQuery, result)) {
+    return false;
+  }
+  reverseConcretization(result, reverse, reverseExpr);
+
+  /* No unsat cores were found for the query, so we can try to find new
+   * solution. */
+  if (isa<InvalidResponse>(result)) {
+    return true;
+  }
+
+  ValidityCore validityCore;
+  bool success = result->tryGetValidityCore(validityCore);
+  assert(success);
+
+  constraints_ty allValidityCoreConstraints = validityCore.constraints;
+  allValidityCoreConstraints.insert(validityCore.expr);
+  findObjects(allValidityCoreConstraints.begin(),
+              allValidityCoreConstraints.end(), brokenArrays);
+  return true;
+}
+
 bool ConcretizingSolver::relaxSymcreteConstraints(const Query &query,
                                                   ref<SolverResponse> &result) {
   if (!query.containsSizeSymcretes()) {
@@ -110,28 +186,17 @@ bool ConcretizingSolver::relaxSymcreteConstraints(const Query &query,
   bool wereConcretizationsRemoved = true;
   while (wereConcretizationsRemoved) {
     wereConcretizationsRemoved = false;
-    if (!solver->impl->check(constructConcretizedQuery(query, assignment),
-                             result)) {
+
+    std::vector<const Array *> currentlyBrokenSymcretizedArrays;
+    if (!getBrokenArrays(query, assignment, result,
+                         currentlyBrokenSymcretizedArrays)) {
       return false;
     }
 
-    /* No unsat cores were found for the query, so we can try to find new
-     * solution. */
     if (isa<InvalidResponse>(result)) {
       break;
     }
 
-    ValidityCore validityCore;
-    bool success = result->tryGetValidityCore(validityCore);
-    assert(success);
-
-    constraints_ty allValidityCoreConstraints = validityCore.constraints;
-    allValidityCoreConstraints.insert(validityCore.expr);
-    std::vector<const Array *> currentlyBrokenSymcretizedArrays;
-    findObjects(allValidityCoreConstraints.begin(),
-                allValidityCoreConstraints.end(),
-                currentlyBrokenSymcretizedArrays);
-
     std::queue<const Array *> arrayQueue;
     std::queue<const Array *> addressQueue;
 
@@ -161,6 +226,7 @@ bool ConcretizingSolver::relaxSymcreteConstraints(const Query &query,
         assignment.bindings.erase(addressQueue.front());
         addressQueue.pop();
       }
+
       if (!solver->impl->check(constructConcretizedQuery(query, assignment),
                                result)) {
         return false;
@@ -299,8 +365,14 @@ bool ConcretizingSolver::relaxSymcreteConstraints(const Query &query,
     assignment.bindings[addressArray] = storage;
   }
 
-  if (!solver->impl->check(constructConcretizedQuery(query, assignment),
-                           result)) {
+  Query concretizedQuery = constructConcretizedQuery(query, assignment);
+  ref<ConstantExpr> CE = dyn_cast<ConstantExpr>(concretizedQuery.expr);
+  if (CE && CE->isTrue()) {
+    result = new UnknownResponse();
+    return true;
+  }
+
+  if (!solver->impl->check(concretizedQuery, result)) {
     return false;
   }
 
@@ -352,59 +424,21 @@ bool ConcretizingSolver::computeValidity(
   assert(assertConcretization(query, assign) &&
          "Assignment does not contain concretization for all symcrete arrays!");
 
-  auto concretizedQuery = constructConcretizedQuery(query, assign);
-  if (!solver->impl->computeValidity(concretizedQuery, queryResult,
-                                     negatedQueryResult)) {
+  if (!check(query, queryResult) ||
+      !check(query.negateExpr(), negatedQueryResult)) {
     return false;
   }
-
-  std::vector<SparseStorage<unsigned char>> queryResultValues,
-      negatedQueryResultValues;
-
-  std::vector<const Array *> objects = assign.keys();
-
-  assert(isa<InvalidResponse>(queryResult) ||
-         isa<InvalidResponse>(negatedQueryResult));
-
-  // *No more than one* of queryResult and negatedQueryResult is possible,
-  // i.e. `mustBeTrue` with values from `assign`.
-  // Take one which is `mustBeTrue` with symcretes from `assign`
-  // and try to relax them to `mayBeFalse`. This solution should be
-  // appropriate for the remain branch.
-
-  if (isa<ValidResponse>(queryResult)) {
-    concretizationManager->add(
-        query,
-        cast<InvalidResponse>(negatedQueryResult)->initialValuesFor(objects));
-    if (!relaxSymcreteConstraints(query, queryResult)) {
-      return false;
-    }
-    if (ref<InvalidResponse> queryInvalidResponse =
-            dyn_cast<InvalidResponse>(queryResult)) {
-      concretizationManager->add(
-          query.negateExpr(), queryInvalidResponse->initialValuesFor(objects));
-    }
-  } else if (isa<ValidResponse>(negatedQueryResult)) {
-    concretizationManager->add(
-        query.negateExpr(),
-        cast<InvalidResponse>(queryResult)->initialValuesFor(objects));
-    if (!relaxSymcreteConstraints(query.negateExpr(), negatedQueryResult)) {
-      return false;
-    }
-    if (ref<InvalidResponse> negatedQueryInvalidResponse =
-            dyn_cast<InvalidResponse>(negatedQueryResult)) {
-      concretizationManager->add(
-          query, negatedQueryInvalidResponse->initialValuesFor(objects));
-    }
-  } else {
+  if (!isa<InvalidResponse>(queryResult) &&
+      isa<InvalidResponse>(negatedQueryResult)) {
+    concretizationManager->add(query, cast<InvalidResponse>(negatedQueryResult)
+                                          ->initialValuesFor(assign.keys()));
+  }
+  if (isa<InvalidResponse>(queryResult) &&
+      !isa<InvalidResponse>(negatedQueryResult)) {
     concretizationManager->add(
         query.negateExpr(),
-        cast<InvalidResponse>(queryResult)->initialValuesFor(objects));
-    concretizationManager->add(
-        query,
-        cast<InvalidResponse>(negatedQueryResult)->initialValuesFor(objects));
+        cast<InvalidResponse>(queryResult)->initialValuesFor(assign.keys()));
   }
-
   return true;
 }
 
@@ -417,12 +451,15 @@ bool ConcretizingSolver::check(const Query &query,
   assert(assertConcretization(query, assign) &&
          "Assignment does not contain concretization for all symcrete arrays!");
 
-  auto concretizedQuery = constructConcretizedQuery(query, assign);
-  if (!solver->impl->check(concretizedQuery, result)) {
-    return false;
-  }
+  auto concretizedQuery = getConcretizedVersion(query);
 
-  if (isa<ValidResponse>(result)) {
+  ref<ConstantExpr> CE = dyn_cast<ConstantExpr>(concretizedQuery.expr);
+  if (!CE || !CE->isTrue()) {
+    if (!solver->impl->check(concretizedQuery, result)) {
+      return false;
+    }
+  }
+  if ((CE && CE->isTrue()) || isa<ValidResponse>(result)) {
     if (!relaxSymcreteConstraints(query, result)) {
       return false;
     }
@@ -462,8 +499,7 @@ bool ConcretizingSolver::computeTruth(const Query &query, bool &isValid) {
           query.constraints.concretization().evaluate(query.expr))) {
     isValid = CE->isTrue();
   } else {
-    auto concretizedQuery = constructConcretizedQuery(query, assign);
-
+    auto concretizedQuery = getConcretizedVersion(query);
     if (!solver->impl->computeTruth(concretizedQuery, isValid)) {
       return false;
     }
@@ -502,7 +538,7 @@ bool ConcretizingSolver::computeValidityCore(const Query &query,
   assert(assertConcretization(query, assign) &&
          "Assignment does not contain concretization for all symcrete arrays!");
 
-  Query concretizedQuery = constructConcretizedQuery(query, assign);
+  Query concretizedQuery = getConcretizedVersion(query);
 
   if (ref<ConstantExpr> CE = dyn_cast<ConstantExpr>(
           query.constraints.concretization().evaluate(query.expr))) {
@@ -556,7 +592,7 @@ bool ConcretizingSolver::computeValue(const Query &query, ref<Expr> &result) {
     result = expr;
     return true;
   }
-  auto concretizedQuery = constructConcretizedQuery(query, assign);
+  auto concretizedQuery = getConcretizedVersion(query);
   return solver->impl->computeValue(concretizedQuery, result);
 }
 
@@ -572,7 +608,7 @@ bool ConcretizingSolver::computeInitialValues(
   assert(assertConcretization(query, assign) &&
          "Assignment does not contain concretization for all symcrete arrays!");
 
-  auto concretizedQuery = constructConcretizedQuery(query, assign);
+  auto concretizedQuery = getConcretizedVersion(query);
   if (!solver->impl->computeInitialValues(concretizedQuery, objects, values,
                                           hasSolution)) {
     return false;
@@ -591,9 +627,10 @@ bool ConcretizingSolver::computeInitialValues(
       assign = resultInvalidResponse->initialValuesFor(assign.keys());
       concretizationManager->add(query.negateExpr(), assign);
       values = std::vector<SparseStorage<unsigned char>>();
-      return solver->impl->computeInitialValues(
-          constructConcretizedQuery(query, assign), objects, values,
-          hasSolution);
+      return solver->impl
+          ->computeInitialValues( // initialvaluesfor objects and values
+              constructConcretizedQuery(query, assign), objects, values,
+              hasSolution);
     }
   } else {
     concretizationManager->add(query.negateExpr(), assign);
diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp
index 1c0a5c9cb5..8d12b7023d 100644
--- a/lib/Solver/IndependentSolver.cpp
+++ b/lib/Solver/IndependentSolver.cpp
@@ -58,31 +58,31 @@ class IndependentSolver : public SolverImpl {
 bool IndependentSolver::computeValidity(const Query &query,
                                         PartialValidity &result) {
   constraints_ty required;
-  IndependentElementSet eltsClosure =
-      getIndependentConstraints(query, required);
+  ref<const IndependentConstraintSet> eltsClosure =
+      query.getIndependentConstraints(required);
   ConstraintSet tmp(
-      required, eltsClosure.symcretes,
-      query.constraints.concretization().part(eltsClosure.symcretes));
+      required, eltsClosure->symcretes,
+      query.constraints.concretization().part(eltsClosure->symcretes));
   return solver->impl->computeValidity(query.withConstraints(tmp), result);
 }
 
 bool IndependentSolver::computeTruth(const Query &query, bool &isValid) {
   constraints_ty required;
-  IndependentElementSet eltsClosure =
-      getIndependentConstraints(query, required);
+  ref<const IndependentConstraintSet> eltsClosure =
+      query.getIndependentConstraints(required);
   ConstraintSet tmp(
-      required, eltsClosure.symcretes,
-      query.constraints.concretization().part(eltsClosure.symcretes));
+      required, eltsClosure->symcretes,
+      query.constraints.concretization().part(eltsClosure->symcretes));
   return solver->impl->computeTruth(query.withConstraints(tmp), isValid);
 }
 
 bool IndependentSolver::computeValue(const Query &query, ref<Expr> &result) {
   constraints_ty required;
-  IndependentElementSet eltsClosure =
-      getIndependentConstraints(query, required);
+  ref<const IndependentConstraintSet> eltsClosure =
+      query.getIndependentConstraints(required);
   ConstraintSet tmp(
-      required, eltsClosure.symcretes,
-      query.constraints.concretization().part(eltsClosure.symcretes));
+      required, eltsClosure->symcretes,
+      query.constraints.concretization().part(eltsClosure->symcretes));
   return solver->impl->computeValue(query.withConstraints(tmp), result);
 }
 
@@ -144,17 +144,14 @@ bool IndependentSolver::computeInitialValues(
   // This is important in case we don't have any constraints but
   // we need initial values for requested array objects.
   hasSolution = true;
-  // FIXME: When we switch to C++11 this should be a std::unique_ptr so we don't
-  // need to remember to manually call delete
-  std::list<IndependentElementSet> *factors =
-      getAllIndependentConstraintsSets(query);
+  std::vector<ref<const IndependentConstraintSet>> factors;
+  query.getAllIndependentConstraintsSets(factors);
 
   // Used to rearrange all of the answers into the correct order
-  std::map<const Array *, SparseStorage<unsigned char>> retMap;
-  for (std::list<IndependentElementSet>::iterator it = factors->begin();
-       it != factors->end(); ++it) {
+  Assignment retMap(true);
+  for (ref<const IndependentConstraintSet> it : factors) {
     std::vector<const Array *> arraysInFactor;
-    calculateArrayReferences(*it, arraysInFactor);
+    it->calculateArrayReferences(arraysInFactor);
     // Going to use this as the "fresh" expression for the Query() invocation
     // below
     assert(it->exprs.size() >= 1 && "No null/empty factors");
@@ -168,58 +165,44 @@ bool IndependentSolver::computeInitialValues(
             Query(tmp, ConstantExpr::alloc(0, Expr::Bool)), arraysInFactor,
             tempValues, hasSolution)) {
       values.clear();
-      delete factors;
+
       return false;
     } else if (!hasSolution) {
       values.clear();
-      delete factors;
+
       return true;
     } else {
       assert(tempValues.size() == arraysInFactor.size() &&
              "Should be equal number arrays and answers");
-      for (unsigned i = 0; i < tempValues.size(); i++) {
-        if (retMap.count(arraysInFactor[i])) {
-          // We already have an array with some partially correct answers,
-          // so we need to place the answers to the new query into the right
-          // spot while avoiding the undetermined values also in the array
-          SparseStorage<unsigned char> *tempPtr = &retMap[arraysInFactor[i]];
-          assert(tempPtr->size() == tempValues[i].size() &&
-                 "we're talking about the same array here");
-          klee::DenseSet<unsigned> *ds = &(it->elements[arraysInFactor[i]]);
-          for (std::set<unsigned>::iterator it2 = ds->begin(); it2 != ds->end();
-               it2++) {
-            unsigned index = *it2;
-            tempPtr->store(index, tempValues[i].load(index));
-          }
-        } else {
-          // Dump all the new values into the array
-          retMap[arraysInFactor[i]] = tempValues[i];
-        }
-      }
+      // We already have an array with some partially correct answers,
+      // so we need to place the answers to the new query into the right
+      // spot while avoiding the undetermined values also in the array
+      it->addValuesToAssignment(arraysInFactor, tempValues, retMap);
     }
   }
 
-  Assignment solutionAssignment(retMap, true);
   for (std::vector<const Array *>::const_iterator it = objects.begin();
        it != objects.end(); it++) {
     const Array *arr = *it;
-    if (!retMap.count(arr)) {
+    if (!retMap.bindings.count(arr)) {
       // this means we have an array that is somehow related to the
       // constraint, but whose values aren't actually required to
       // satisfy the query.
       ref<ConstantExpr> arrayConstantSize =
-          dyn_cast<ConstantExpr>(solutionAssignment.evaluate(arr->size));
+          dyn_cast<ConstantExpr>(retMap.evaluate(arr->size));
       assert(arrayConstantSize &&
              "Array of symbolic size had not receive value for size!");
       SparseStorage<unsigned char> ret(arrayConstantSize->getZExtValue());
       values.push_back(ret);
     } else {
-      values.push_back(retMap[arr]);
+      values.push_back(retMap.bindings[arr]);
     }
   }
-  assert(assertCreatedPointEvaluatesToTrue(query, objects, values, retMap) &&
+
+  assert(assertCreatedPointEvaluatesToTrue(query, objects, values,
+                                           retMap.bindings) &&
          "should satisfy the equation");
-  delete factors;
+
   return true;
 }
 
@@ -228,17 +211,14 @@ bool IndependentSolver::check(const Query &query, ref<SolverResponse> &result) {
   // This is important in case we don't have any constraints but
   // we need initial values for requested array objects.
 
-  // FIXME: When we switch to C++11 this should be a std::unique_ptr so we don't
-  // need to remember to manually call delete
-  std::list<IndependentElementSet> *factors =
-      getAllIndependentConstraintsSets(query);
+  std::vector<ref<const IndependentConstraintSet>> factors;
+  query.getAllIndependentConstraintsSets(factors);
 
   // Used to rearrange all of the answers into the correct order
-  std::map<const Array *, SparseStorage<unsigned char>> retMap;
-  for (std::list<IndependentElementSet>::iterator it = factors->begin();
-       it != factors->end(); ++it) {
+  Assignment retMap;
+  for (ref<const IndependentConstraintSet> it : factors) {
     std::vector<const Array *> arraysInFactor;
-    calculateArrayReferences(*it, arraysInFactor);
+    it->calculateArrayReferences(arraysInFactor);
     // Going to use this as the "fresh" expression for the Query() invocation
     // below
     assert(it->exprs.size() >= 1 && "No null/empty factors");
@@ -264,10 +244,8 @@ bool IndependentSolver::check(const Query &query, ref<SolverResponse> &result) {
                       query.constraints.concretization().part(it->symcretes)),
                   factorExpr),
             tempResult)) {
-      delete factors;
       return false;
     } else if (isa<ValidResponse>(tempResult)) {
-      delete factors;
       result = tempResult;
       return true;
     } else {
@@ -276,34 +254,20 @@ bool IndependentSolver::check(const Query &query, ref<SolverResponse> &result) {
       assert(success && "Can not get initial values (Independent solver)!");
       assert(tempValues.size() == arraysInFactor.size() &&
              "Should be equal number arrays and answers");
-      for (unsigned i = 0; i < tempValues.size(); i++) {
-        if (retMap.count(arraysInFactor[i])) {
-          // We already have an array with some partially correct answers,
-          // so we need to place the answers to the new query into the right
-          // spot while avoiding the undetermined values also in the array
-          SparseStorage<unsigned char> *tempPtr = &retMap[arraysInFactor[i]];
-          assert(tempPtr->size() == tempValues[i].size() &&
-                 "we're talking about the same array here");
-          klee::DenseSet<unsigned> *ds = &(it->elements[arraysInFactor[i]]);
-          for (std::set<unsigned>::iterator it2 = ds->begin(); it2 != ds->end();
-               it2++) {
-            unsigned index = *it2;
-            tempPtr->store(index, tempValues[i].load(index));
-          }
-        } else {
-          // Dump all the new values into the array
-          retMap[arraysInFactor[i]] = tempValues[i];
-        }
-      }
+      // We already have an array with some partially correct answers,
+      // so we need to place the answers to the new query into the right
+      // spot while avoiding the undetermined values also in the array
+      it->addValuesToAssignment(arraysInFactor, tempValues, retMap);
     }
   }
-  result = new InvalidResponse(retMap);
+  result = new InvalidResponse(retMap.bindings);
   std::map<const Array *, SparseStorage<unsigned char>> bindings;
   bool success = result->tryGetInitialValues(bindings);
   assert(success);
-  assert(assertCreatedPointEvaluatesToTrue(query, bindings, retMap) &&
+
+  assert(assertCreatedPointEvaluatesToTrue(query, bindings, retMap.bindings) &&
          "should satisfy the equation");
-  delete factors;
+
   return true;
 }
 
@@ -311,11 +275,11 @@ bool IndependentSolver::computeValidityCore(const Query &query,
                                             ValidityCore &validityCore,
                                             bool &isValid) {
   constraints_ty required;
-  IndependentElementSet eltsClosure =
-      getIndependentConstraints(query, required);
+  ref<const IndependentConstraintSet> eltsClosure =
+      query.getIndependentConstraints(required);
   ConstraintSet tmp(
-      required, eltsClosure.symcretes,
-      query.constraints.concretization().part(eltsClosure.symcretes));
+      required, eltsClosure->symcretes,
+      query.constraints.concretization().part(eltsClosure->symcretes));
   return solver->impl->computeValidityCore(query.withConstraints(tmp),
                                            validityCore, isValid);
 }
diff --git a/lib/Solver/QueryLoggingSolver.cpp b/lib/Solver/QueryLoggingSolver.cpp
index 32f1d7d996..ce53f40a7e 100644
--- a/lib/Solver/QueryLoggingSolver.cpp
+++ b/lib/Solver/QueryLoggingSolver.cpp
@@ -10,6 +10,7 @@
 
 #include "klee/Config/config.h"
 #include "klee/Expr/Constraints.h"
+#include "klee/Expr/ExprUtil.h"
 #include "klee/Statistics/Statistics.h"
 #include "klee/Support/ErrorHandling.h"
 #include "klee/Support/FileHandling.h"
@@ -169,8 +170,17 @@ bool QueryLoggingSolver::computeInitialValues(
     std::vector<SparseStorage<unsigned char>> &values, bool &hasSolution) {
   startQuery(query, "InitialValues", 0, &objects);
 
-  bool success =
-      solver->impl->computeInitialValues(query, objects, values, hasSolution);
+  ExprHashSet expressions;
+  expressions.insert(query.constraints.cs().begin(),
+                     query.constraints.cs().end());
+  expressions.insert(query.expr);
+
+  std::vector<const Array *> allObjects;
+  findSymbolicObjects(expressions.begin(), expressions.end(), allObjects);
+  std::vector<SparseStorage<unsigned char>> allValues;
+
+  bool success = solver->impl->computeInitialValues(query, allObjects,
+                                                    allValues, hasSolution);
 
   finishQuery(success);
 
@@ -178,6 +188,11 @@ bool QueryLoggingSolver::computeInitialValues(
     logBuffer << queryCommentSign
               << "   Solvable: " << (hasSolution ? "true" : "false") << "\n";
     if (hasSolution) {
+      ref<InvalidResponse> invalidResponse =
+          new InvalidResponse(allObjects, allValues);
+      success = invalidResponse->tryGetInitialValuesFor(objects, values);
+      assert(success);
+      Assignment allSolutionAssignment(allObjects, allValues, true);
       std::vector<SparseStorage<unsigned char>>::iterator values_it =
           values.begin();
 
@@ -190,7 +205,7 @@ bool QueryLoggingSolver::computeInitialValues(
         logBuffer << queryCommentSign << "     " << array->getIdentifier()
                   << " = [";
         ref<ConstantExpr> arrayConstantSize =
-            dyn_cast<ConstantExpr>(solutionAssignment.evaluate(array->size));
+            dyn_cast<ConstantExpr>(allSolutionAssignment.evaluate(array->size));
         assert(arrayConstantSize &&
                "Array of symbolic size had not receive value for size!");
 
diff --git a/test/Feature/SymbolicSizes/ImplicitArrayExtension.c b/test/Feature/SymbolicSizes/ImplicitArrayExtension.c
index 389a1adcab..2f97c3aa17 100644
--- a/test/Feature/SymbolicSizes/ImplicitArrayExtension.c
+++ b/test/Feature/SymbolicSizes/ImplicitArrayExtension.c
@@ -1,6 +1,8 @@
 // REQUIRES: z3
 // RUN: %clang %s -g -emit-llvm %O0opt -c -o %t1.bc
 // RUN: rm -rf %t.klee-out
+// RUN: rm -rf %t.klee-outfailnew
+// RUN: %klee --output-dir=%t.klee-outfailnew --out-of-mem-allocs=true --solver-backend=z3 --use-query-log=all:kquery,solver:kquery --write-kqueries %t1.bc 2> %t2.log
 // RUN: %klee --output-dir=%t.klee-out --out-of-mem-allocs=true --solver-backend=z3 %t1.bc 2>&1 | FileCheck %s
 
 #include "klee/klee.h"