diff --git a/docs/tree_incrementality.py b/docs/tree_incrementality.py
new file mode 100644
index 00000000000..c62e7b4a82e
--- /dev/null
+++ b/docs/tree_incrementality.py
@@ -0,0 +1,35 @@
+class TreeIncrementalSolver:
+  def __init__(self, Solver, max_solvers: int):
+    self.Solver = Solver
+    self.max_solvers = max_solvers
+    self.recently_used = Queue()
+    self.recycled_solvers = []
+
+  def reuseOrCreateZ3(self, query):
+    solver_from_scratch_cost = len(query)
+    min_cost, min_solver = solver_from_scratch_cost, None
+    for solver in self.recycled_solvers:
+      delta = distance(solver.query, query)
+      if delta < min_cost:
+        min_cost, min_solver = delta, solver
+    if min_solver is None:
+      return self.Solver()
+    return min_solver
+
+  def find_suitable_solver(self, query):
+    for solver in self.recently_used:
+      if solver.query is subsetOf(query):
+        self.recently_used.remove(solver)
+        return solver
+    if len(self.recently_used) < self.max_solvers:
+      return self.reuseOrCreateZ3(query)
+    return self.recently_used.pop_back()
+
+  def check_sat(self, query):
+    solver = self.find_suitable_solver(query)
+    push(solver, query)
+    self.recently_used.push_front(solver)
+    solver.check_sat()
+
+  def recycle_solver(self, id):
+    raise NotImplementedError()
diff --git a/include/klee/Solver/Solver.h b/include/klee/Solver/Solver.h
index 30b344efecb..c39d8a2ae39 100644
--- a/include/klee/Solver/Solver.h
+++ b/include/klee/Solver/Solver.h
@@ -191,6 +191,10 @@ class Solver {
 
   virtual char *getConstraintLog(const Query &query);
   virtual void setCoreSolverTimeout(time::Span timeout);
+
+  /// @brief Notify the solver that the state with specified id has been
+  /// terminated
+  void notifyStateTermination(std::uint32_t id);
 };
 
 /* *** */
@@ -264,6 +268,11 @@ std::unique_ptr<Solver> createCoreSolver(CoreSolverType cst);
 std::unique_ptr<Solver>
 createConcretizingSolver(std::unique_ptr<Solver> s,
                          AddressGenerator *addressGenerator);
+
+/// Return a list of all unique symbolic objects referenced by the
+/// given Query.
+void findSymbolicObjects(const Query &query,
+                         std::vector<const Array *> &results);
 } // namespace klee
 
 #endif /* KLEE_SOLVER_H */
diff --git a/include/klee/Solver/SolverCmdLine.h b/include/klee/Solver/SolverCmdLine.h
index 7fbfac03940..6bd0c285bbd 100644
--- a/include/klee/Solver/SolverCmdLine.h
+++ b/include/klee/Solver/SolverCmdLine.h
@@ -50,6 +50,8 @@ extern llvm::cl::opt<bool> CoreSolverOptimizeDivides;
 
 extern llvm::cl::opt<bool> UseAssignmentValidatingSolver;
 
+extern llvm::cl::opt<unsigned> MaxSolversApproxTreeInc;
+
 /// The different query logging solvers that can be switched on/off
 enum QueryLoggingSolverType {
   ALL_KQUERY,    ///< Log all queries in .kquery (KQuery) format
@@ -65,6 +67,7 @@ enum CoreSolverType {
   METASMT_SOLVER,
   DUMMY_SOLVER,
   Z3_SOLVER,
+  Z3_TREE_SOLVER,
   NO_SOLVER
 };
 
diff --git a/include/klee/Solver/SolverImpl.h b/include/klee/Solver/SolverImpl.h
index 3e24a16ed7f..c3d7ed40a2f 100644
--- a/include/klee/Solver/SolverImpl.h
+++ b/include/klee/Solver/SolverImpl.h
@@ -119,6 +119,8 @@ class SolverImpl {
   }
 
   virtual void setCoreSolverTimeout(time::Span timeout){};
+
+  virtual void notifyStateTermination(std::uint32_t id){};
 };
 
 } // namespace klee
diff --git a/include/klee/Solver/SolverUtil.h b/include/klee/Solver/SolverUtil.h
index c1fdb2832c6..f05bd8d2646 100644
--- a/include/klee/Solver/SolverUtil.h
+++ b/include/klee/Solver/SolverUtil.h
@@ -41,6 +41,9 @@ enum class Validity { True = 1, False = -1, Unknown = 0 };
 struct SolverQueryMetaData {
   /// @brief Costs for all queries issued for this state
   time::Span queryCost;
+
+  /// @brief Caller state id
+  std::uint32_t id = 0;
 };
 
 struct Query {
diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp
index ddec6ec63b6..efa29ac3333 100644
--- a/lib/Core/ExecutionState.cpp
+++ b/lib/Core/ExecutionState.cpp
@@ -182,7 +182,9 @@ ExecutionState::ExecutionState(const ExecutionState &state)
       returnValue(state.returnValue), gepExprBases(state.gepExprBases),
       prevTargets_(state.prevTargets_), targets_(state.targets_),
       prevHistory_(state.prevHistory_), history_(state.history_),
-      isTargeted_(state.isTargeted_) {}
+      isTargeted_(state.isTargeted_) {
+  queryMetaData.id = state.id;
+}
 
 ExecutionState *ExecutionState::branch() {
   depth++;
diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h
index c0bfeb7301d..e2093c7c27e 100644
--- a/lib/Core/ExecutionState.h
+++ b/lib/Core/ExecutionState.h
@@ -441,7 +441,10 @@ class ExecutionState {
   bool visited(KBlock *block) const;
 
   std::uint32_t getID() const { return id; };
-  void setID() { id = nextID++; };
+  void setID() {
+    id = nextID++;
+    queryMetaData.id = id;
+  };
   llvm::BasicBlock *getInitPCBlock() const;
   llvm::BasicBlock *getPrevPCBlock() const;
   llvm::BasicBlock *getPCBlock() const;
diff --git a/lib/Core/TimingSolver.cpp b/lib/Core/TimingSolver.cpp
index edae9a3a5b9..f241b804796 100644
--- a/lib/Core/TimingSolver.cpp
+++ b/lib/Core/TimingSolver.cpp
@@ -351,3 +351,7 @@ TimingSolver::getRange(const ConstraintSet &constraints, ref<Expr> expr,
   metaData.queryCost += timer.delta();
   return result;
 }
+
+void TimingSolver::notifyStateTermination(std::uint32_t id) {
+  solver->notifyStateTermination(id);
+}
diff --git a/lib/Core/TimingSolver.h b/lib/Core/TimingSolver.h
index fbf65c4a56c..7692d503778 100644
--- a/lib/Core/TimingSolver.h
+++ b/lib/Core/TimingSolver.h
@@ -49,6 +49,10 @@ class TimingSolver {
     return solver->getConstraintLog(query);
   }
 
+  /// @brief Notify the solver that the state with specified id has been
+  /// terminated
+  void notifyStateTermination(std::uint32_t id);
+
   bool evaluate(const ConstraintSet &, ref<Expr>, PartialValidity &result,
                 SolverQueryMetaData &metaData,
                 bool produceValidityCore = false);
diff --git a/lib/Solver/AssignmentValidatingSolver.cpp b/lib/Solver/AssignmentValidatingSolver.cpp
index dde0f1a23d5..486a7f4a725 100644
--- a/lib/Solver/AssignmentValidatingSolver.cpp
+++ b/lib/Solver/AssignmentValidatingSolver.cpp
@@ -142,14 +142,8 @@ bool AssignmentValidatingSolver::check(const Query &query,
     return true;
   }
 
-  ExprHashSet expressions;
-  assert(!query.containsSymcretes());
-  expressions.insert(query.constraints.cs().begin(),
-                     query.constraints.cs().end());
-  expressions.insert(query.expr);
-
   std::vector<const Array *> objects;
-  findSymbolicObjects(expressions.begin(), expressions.end(), objects);
+  findSymbolicObjects(query, objects);
   std::vector<SparseStorage<unsigned char>> values;
 
   assert(isa<InvalidResponse>(result));
diff --git a/lib/Solver/CoreSolver.cpp b/lib/Solver/CoreSolver.cpp
index b6de1024b86..e44e8c37a1b 100644
--- a/lib/Solver/CoreSolver.cpp
+++ b/lib/Solver/CoreSolver.cpp
@@ -28,6 +28,7 @@ DISABLE_WARNING_POP
 namespace klee {
 
 std::unique_ptr<Solver> createCoreSolver(CoreSolverType cst) {
+  bool isTreeSolver = false;
   switch (cst) {
   case STP_SOLVER:
 #ifdef ENABLE_STP
@@ -54,16 +55,22 @@ std::unique_ptr<Solver> createCoreSolver(CoreSolverType cst) {
 #endif
   case DUMMY_SOLVER:
     return createDummySolver();
+  case Z3_TREE_SOLVER:
+    isTreeSolver = true;
   case Z3_SOLVER:
 #ifdef ENABLE_Z3
     klee_message("Using Z3 solver backend");
+    Z3BuilderType type;
 #ifdef ENABLE_FP
     klee_message("Using Z3 bitvector builder");
-    return std::make_unique<Z3Solver>(KLEE_BITVECTOR);
+    type = KLEE_BITVECTOR;
 #else
     klee_message("Using Z3 core builder");
-    return std::make_unique<Z3Solver>(KLEE_CORE);
+    type = KLEE_CORE;
 #endif
+    if (isTreeSolver)
+      return std::make_unique<Z3TreeSolver>(type, MaxSolversApproxTreeInc);
+    return std::make_unique<Z3Solver>(type);
 #else
     klee_message("Not compiled with Z3 support");
     return NULL;
diff --git a/lib/Solver/IncompleteSolver.cpp b/lib/Solver/IncompleteSolver.cpp
index 5fd7c74b3b2..2262423a561 100644
--- a/lib/Solver/IncompleteSolver.cpp
+++ b/lib/Solver/IncompleteSolver.cpp
@@ -119,13 +119,8 @@ bool StagedSolverImpl::computeInitialValues(
 }
 
 bool StagedSolverImpl::check(const Query &query, ref<SolverResponse> &result) {
-  ExprHashSet expressions;
-  expressions.insert(query.constraints.cs().begin(),
-                     query.constraints.cs().end());
-  expressions.insert(query.expr);
-
   std::vector<const Array *> objects;
-  findSymbolicObjects(expressions.begin(), expressions.end(), objects);
+  findSymbolicObjects(query, objects);
   std::vector<SparseStorage<unsigned char>> values;
 
   bool hasSolution;
diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp
index ec30aa9b19f..4aeff5adc8c 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -162,6 +162,10 @@ bool Solver::check(const Query &query, ref<SolverResponse> &queryResult) {
   return impl->check(query, queryResult);
 }
 
+void Solver::notifyStateTermination(std::uint32_t id) {
+  impl->notifyStateTermination(id);
+}
+
 static std::pair<ref<ConstantExpr>, ref<ConstantExpr>> getDefaultRange() {
   return std::make_pair(ConstantExpr::create(0, 64),
                         ConstantExpr::create(0, 64));
@@ -327,6 +331,15 @@ bool Query::containsSizeSymcretes() const {
   return false;
 }
 
+void klee::findSymbolicObjects(const Query &query,
+                               std::vector<const Array *> &results) {
+  ExprHashSet expressions;
+  expressions.insert(query.constraints.cs().begin(),
+                     query.constraints.cs().end());
+  expressions.insert(query.expr);
+  findSymbolicObjects(expressions.begin(), expressions.end(), results);
+}
+
 void Query::dump() const {
   constraints.dump();
   llvm::errs() << "Query [\n";
diff --git a/lib/Solver/SolverCmdLine.cpp b/lib/Solver/SolverCmdLine.cpp
index 0c96fb12634..0f51525d535 100644
--- a/lib/Solver/SolverCmdLine.cpp
+++ b/lib/Solver/SolverCmdLine.cpp
@@ -123,6 +123,13 @@ cl::opt<bool> UseAssignmentValidatingSolver(
     cl::desc("Debug the correctness of generated assignments (default=false)"),
     cl::cat(SolvingCat));
 
+cl::opt<unsigned>
+    MaxSolversApproxTreeInc("max-solvers-approx-tree-inc",
+                            cl::desc("Maximum size of the Z3 solver pool for "
+                                     "approximating tree incrementality."
+                                     " Set to 0 to disable (default=0)"),
+                            cl::init(0), cl::cat(SolvingCat));
+
 void KCommandLine::HideOptions(llvm::cl::OptionCategory &Category) {
   StringMap<cl::Option *> &map = cl::getRegisteredOptions();
 
@@ -196,11 +203,12 @@ cl::opt<klee::MetaSMTBackendType> MetaSMTBackend(
 
 cl::opt<CoreSolverType> CoreSolverToUse(
     "solver-backend", cl::desc("Specifiy the core solver backend to use"),
-    cl::values(clEnumValN(STP_SOLVER, "stp", "STP" STP_IS_DEFAULT_STR),
-               clEnumValN(METASMT_SOLVER, "metasmt",
-                          "metaSMT" METASMT_IS_DEFAULT_STR),
-               clEnumValN(DUMMY_SOLVER, "dummy", "Dummy solver"),
-               clEnumValN(Z3_SOLVER, "z3", "Z3" Z3_IS_DEFAULT_STR)),
+    cl::values(
+        clEnumValN(STP_SOLVER, "stp", "STP" STP_IS_DEFAULT_STR),
+        clEnumValN(METASMT_SOLVER, "metasmt", "metaSMT" METASMT_IS_DEFAULT_STR),
+        clEnumValN(DUMMY_SOLVER, "dummy", "Dummy solver"),
+        clEnumValN(Z3_SOLVER, "z3", "Z3" Z3_IS_DEFAULT_STR),
+        clEnumValN(Z3_TREE_SOLVER, "z3-tree", "Z3 tree-incremental solver")),
     cl::init(DEFAULT_CORE_SOLVER), cl::cat(SolvingCat));
 
 cl::opt<CoreSolverType> DebugCrossCheckCoreSolverWith(
diff --git a/lib/Solver/SolverImpl.cpp b/lib/Solver/SolverImpl.cpp
index 033f1d6d192..2768ce3ce9a 100644
--- a/lib/Solver/SolverImpl.cpp
+++ b/lib/Solver/SolverImpl.cpp
@@ -42,13 +42,8 @@ bool SolverImpl::computeValidity(const Query &query,
 }
 
 bool SolverImpl::check(const Query &query, ref<SolverResponse> &result) {
-  ExprHashSet expressions;
-  expressions.insert(query.constraints.cs().begin(),
-                     query.constraints.cs().end());
-  expressions.insert(query.expr);
-
   std::vector<const Array *> objects;
-  findSymbolicObjects(expressions.begin(), expressions.end(), objects);
+  findSymbolicObjects(query, objects);
   std::vector<SparseStorage<unsigned char>> values;
 
   bool hasSolution;
diff --git a/lib/Solver/Z3Solver.cpp b/lib/Solver/Z3Solver.cpp
index 3a92ae7fe1a..feef3911986 100644
--- a/lib/Solver/Z3Solver.cpp
+++ b/lib/Solver/Z3Solver.cpp
@@ -12,7 +12,12 @@
 #include "klee/Support/FileHandling.h"
 #include "klee/Support/OptionCategories.h"
 
+#include <cassert>
 #include <csignal>
+#include <deque>
+#include <memory>
+#include <numeric>
+#include <unordered_map>
 
 #ifdef ENABLE_Z3
 
@@ -30,9 +35,6 @@
 #include "llvm/Support/CommandLine.h"
 #include "llvm/Support/raw_ostream.h"
 
-#include <memory>
-#include <unordered_map>
-
 namespace {
 // NOTE: Very useful for debugging Z3 behaviour. These files can be given to
 // the z3 binary to replay all Z3 API calls using its `-log` option.
@@ -53,6 +55,12 @@ llvm::cl::opt<bool> Z3ValidateModels(
         "When generating Z3 models validate these against the query"),
     llvm::cl::cat(klee::SolvingCat));
 
+llvm::cl::opt<bool> Z3TreeUseGlobalMinDistanceSolver(
+    "use-global-min-distance-z3-solver", llvm::cl::init(false),
+    llvm::cl::desc("Use global min. distance algorithm instead of LRU for "
+                   "choosing solver from the pool"),
+    llvm::cl::cat(klee::SolvingCat));
+
 llvm::cl::opt<unsigned>
     Z3VerbosityLevel("debug-z3-verbosity", llvm::cl::init(0),
                      llvm::cl::desc("Z3 verbosity level (default=0)"),
@@ -67,20 +75,403 @@ DISABLE_WARNING_POP
 
 namespace klee {
 
-class Z3SolverImpl : public SolverImpl {
+typedef std::unordered_set<size_t> FrameIds;
+
+template <typename _Tp, typename _Alloc>
+void extend(std::vector<_Tp, _Alloc> &ths,
+            const std::vector<_Tp, _Alloc> &other) {
+  ths.reserve(ths.size() + other.size());
+  ths.insert(ths.end(), other.begin(), other.end());
+}
+
+template <typename _Tp, typename _Alloc = std::allocator<_Tp>> class inc_vector;
+typedef inc_vector<ref<Expr>> ConstraintFrames;
+
+template <typename _Tp, typename _Alloc> class inc_vector {
+  friend void dump(const ConstraintFrames &);
+
+public:
+  using vec = std::vector<_Tp, _Alloc>;
+  using frame_size_it = std::vector<size_t>::const_iterator;
+  using frame_it = typename vec::const_iterator;
+
+  /// It is public, so that all vector operations are supported
+  /// Everything pushed to v is pushed to the last frame
+  vec v;
+
+  std::vector<size_t> frame_sizes;
+
 private:
+  // v.size() == sum(frame_sizes) + size of the fresh frame
+
+  size_t freshFrameSize() const {
+    return v.size() -
+           std::accumulate(frame_sizes.begin(), frame_sizes.end(), 0);
+  }
+
+  void take(size_t n, size_t &frames_count, size_t &frame_index) const {
+    size_t i = 0;
+    size_t c = n;
+    for (; i < frame_sizes.size(); i++) {
+      if (frame_sizes[i] > c)
+        break;
+      c -= frame_sizes[i];
+    }
+    frames_count = c;
+    frame_index = i;
+  }
+
+public:
+  inc_vector() {}
+  inc_vector(const std::vector<_Tp> &constraints) : v(constraints) {}
+
+  frame_size_it begin() const { return frame_sizes.cbegin(); }
+  frame_size_it end() const { return frame_sizes.cend(); }
+  size_t framesSize() const { return frame_sizes.size() + 1; }
+
+  frame_it begin(int frame_index) const {
+    assert(-(long long)framesSize() <= (long long)frame_index &&
+           (long long)frame_index <= (long long)framesSize());
+    if (frame_index < 0)
+      frame_index += framesSize();
+    if ((long long)frame_index == (long long)framesSize())
+      return v.end();
+    auto fend = frame_sizes.begin() + frame_index;
+    auto shift = std::accumulate(frame_sizes.begin(), fend, 0);
+    return v.begin() + shift;
+  }
+  frame_it end(int frame_index) const { return begin(frame_index + 1); }
+  size_t size(size_t frame_index) const {
+    assert(frame_index < framesSize());
+    if (frame_index == framesSize() - 1) // last frame
+      return freshFrameSize();
+    return frame_sizes[frame_index];
+  }
+
+  void pop(size_t popFrames) {
+    assert(freshFrameSize() == 0);
+    if (popFrames == 0)
+      return;
+    size_t toPop =
+        std::accumulate(frame_sizes.end() - popFrames, frame_sizes.end(), 0);
+    v.resize(v.size() - toPop);
+    frame_sizes.resize(frame_sizes.size() - popFrames);
+  }
+
+  void push() {
+    auto freshSize = freshFrameSize();
+    frame_sizes.push_back(freshSize);
+    assert(freshFrameSize() == 0);
+  }
+
+  /// ensures that last frame is empty
+  void extend(const std::vector<_Tp, _Alloc> &other) {
+    assert(freshFrameSize() == 0);
+    // push();
+    klee::extend(v, other);
+    push();
+  }
+
+  /// ensures that last frame is empty
+  void extend(const inc_vector<_Tp, _Alloc> &other) {
+    assert(freshFrameSize() == 0);
+    for (size_t i = 0, e = other.framesSize(); i < e; i++) {
+      v.reserve(v.size() + other.size(i));
+      v.insert(v.end(), other.begin(i), other.end(i));
+      push();
+    }
+  }
+
+  void takeAfter(size_t n, inc_vector<_Tp, _Alloc> &result) const {
+    size_t frames_count, frame_index;
+    take(n, frames_count, frame_index);
+    result = *this;
+    std::vector<_Tp, _Alloc>(result.v.begin() + n, result.v.end())
+        .swap(result.v);
+    std::vector<size_t>(result.frame_sizes.begin() + frame_index,
+                        result.frame_sizes.end())
+        .swap(result.frame_sizes);
+    if (frames_count)
+      result.frame_sizes[0] -= frames_count;
+  }
+
+  void takeBefore(size_t n, size_t &toPop, size_t &takeFromOther) const {
+    take(n, takeFromOther, toPop);
+    toPop = frame_sizes.size() - toPop;
+  }
+};
+
+void dump(const ConstraintFrames &frames) {
+  llvm::errs() << "frame sizes:";
+  for (auto size : frames.frame_sizes) {
+    llvm::errs() << " " << size;
+  }
+  llvm::errs() << "\n";
+  llvm::errs() << "frames:\n";
+  for (auto &x : frames.v) {
+    llvm::errs() << x->toString() << "\n";
+  }
+}
+
+template <typename _Value, typename _Hash = std::hash<_Value>,
+          typename _Pred = std::equal_to<_Value>,
+          typename _Alloc = std::allocator<_Value>>
+class inc_uset {
+private:
+  using setT = std::unordered_set<_Value, _Hash, _Pred, _Alloc>;
+  using citerator = typename setT::const_iterator;
+  using idMap = std::unordered_map<_Value, FrameIds, _Hash, _Pred, _Alloc>;
+  setT set;
+  idMap ids;
+  size_t current_frame = 0;
+
+public:
+  citerator cbegin() const { return set.cbegin(); }
+  citerator cend() const { return set.cend(); }
+  size_t framesSize() const { return current_frame + 1; }
+
+  class frame_it
+      : public std::iterator<std::forward_iterator_tag, ref<Expr>, int> {
+    const setT &set;
+    const idMap &ids;
+    citerator set_it;
+    const size_t frame_index = 0;
+
+    void gotoNext() {
+      while (set_it != set.end() &&
+             ids.at(*set_it).find(frame_index) == ids.at(*set_it).end())
+        set_it++;
+    }
+
+  public:
+    using value_type = _Value;
+
+    explicit frame_it(const setT &set, const idMap &ids)
+        : set(set), ids(ids), set_it(set.end()) {}
+    explicit frame_it(const setT &set, const idMap &ids, size_t frame_index)
+        : set(set), ids(ids), set_it(set.begin()), frame_index(frame_index) {
+      gotoNext();
+    }
+
+    bool operator!=(const frame_it &other) const {
+      return set_it != other.set_it;
+    }
+
+    const _Value &operator*() const { return *set_it; }
+
+    frame_it &operator++() {
+      if (set_it != set.end()) {
+        set_it++;
+        gotoNext();
+      }
+      return *this;
+    }
+  };
+
+  frame_it begin(int frame_index) const {
+    assert(-(long long)framesSize() <= (long long)frame_index &&
+           (long long)frame_index <= (long long)framesSize());
+    if (frame_index < 0)
+      frame_index += framesSize();
+    return frame_it(set, ids, frame_index);
+  }
+  frame_it end(int frame_index) const { return frame_it(set, ids); }
+
+  void insert(const _Value &v) {
+    set.insert(v);
+    ids[v].insert(current_frame);
+  }
+
+  template <class _InputIterator>
+  void insert(_InputIterator __first, _InputIterator __last) {
+    set.insert(__first, __last);
+    for (; __first != __last; __first++)
+      ids[*__first].insert(current_frame);
+  }
+
+  void pop(size_t popFrames) {
+    current_frame -= popFrames;
+    idMap newIdMap;
+    for (auto &keyAndIds : ids) {
+      FrameIds newIds;
+      for (auto id : keyAndIds.second)
+        if (id <= current_frame)
+          newIds.insert(id);
+      if (newIds.empty())
+        set.erase(keyAndIds.first);
+      else
+        newIdMap.insert(std::make_pair(keyAndIds.first, newIds));
+    }
+    ids = newIdMap;
+  }
+
+  void push() { current_frame++; }
+};
+
+template <typename _Key, typename _Tp, typename _Hash = std::hash<_Key>,
+          typename _Pred = std::equal_to<_Key>,
+          typename _Alloc = std::allocator<std::pair<const _Key, _Tp>>>
+class inc_umap {
+private:
+  std::unordered_map<_Key, _Tp, _Hash, _Pred, _Alloc> map;
+  using idMap = std::unordered_map<_Key, FrameIds, _Hash, _Pred, _Alloc>;
+  idMap ids;
+  size_t current_frame = 0;
+
+public:
+  void insert(const std::pair<_Key, _Tp> &pair) {
+    map.insert(pair);
+    ids[pair.first].insert(current_frame);
+  }
+
+  _Tp &operator[](const _Key &key) {
+    ids[key].insert(current_frame);
+    return map[key];
+  }
+
+  size_t count(const _Key &key) const { return map.count(key); }
+
+  const _Tp &at(_Key &key) const { return map.at(key); }
+
+  void pop(size_t popFrames) {
+    current_frame -= popFrames;
+    idMap newIdMap;
+    for (auto &keyAndIds : ids) {
+      FrameIds newIds;
+      for (auto id : keyAndIds.second)
+        if (id <= current_frame)
+          newIds.insert(id);
+      if (newIds.empty())
+        map.erase(keyAndIds.first);
+      else
+        newIdMap.insert(std::make_pair(keyAndIds.first, newIds));
+    }
+    ids = newIdMap;
+  }
+
+  void push() { current_frame++; }
+};
+
+typedef inc_umap<Z3ASTHandle, ref<Expr>, Z3ASTHandleHash, Z3ASTHandleCmp>
+    ExprIncMap;
+typedef inc_umap<Z3ASTHandle, Z3ASTHandle, Z3ASTHandleHash, Z3ASTHandleCmp>
+    Z3ASTIncMap;
+typedef inc_uset<ref<Expr>, klee::util::ExprHash, klee::util::ExprCmp>
+    ExprIncSet;
+typedef inc_uset<Z3ASTHandle, Z3ASTHandleHash, Z3ASTHandleCmp> Z3ASTIncSet;
+
+class ConstraintQuery {
+private:
+  // this should be used when only query is needed, se comment below
+  ref<Expr> expr;
+
+public:
+  // KLEE Queries are validity queries i.e.
+  // ∀ X Constraints(X) → query(X)
+  // but Z3 works in terms of satisfiability so instead we ask the
+  // negation of the equivalent i.e.
+  // ∃ X Constraints(X) ∧ ¬ query(X)
+  // so this `constraints` field contains: Constraints(X) ∧ ¬ query(X)
+  ConstraintFrames constraints;
+
+  explicit ConstraintQuery() {}
+
+  ConstraintQuery(ConstraintFrames &frames) : constraints(frames) {
+    if (frames.v.size() == 0)
+      expr = Expr::createFalse();
+    else
+      expr = Expr::createIsZero(frames.v.back());
+  }
+
+  ConstraintQuery(const Query &q) : expr(q.expr) {
+    for (auto &constraint : q.constraints.cs()) {
+      constraints.v.push_back(constraint);
+      constraints.push();
+    }
+    if (!q.expr->isFalse())
+      constraints.v.push_back(Expr::createIsZero(q.expr));
+  }
+
+  size_t size() const { return constraints.v.size(); }
+
+  ref<Expr> getOriginalQueryExpr() const { return expr; }
+
+  std::vector<const Array *> gatherArrays() const;
+};
+
+std::vector<const Array *> ConstraintQuery::gatherArrays() const {
+  std::vector<const Array *> arrays;
+  findObjects(constraints.v.begin(), constraints.v.end(), arrays);
+  return arrays;
+}
+
+class Z3SolverEnv {
+public:
+  inc_vector<const Array *> objects;
+  inc_vector<Z3ASTHandle> z3_ast_expr_constraints;
+  ExprIncMap z3_ast_expr_to_klee_expr;
+  Z3ASTIncMap expr_to_track;
+  inc_umap<const Array *, ExprHashSet> usedArrayBytes;
+  ExprIncSet symbolicObjects;
+
+  explicit Z3SolverEnv(){};
+  explicit Z3SolverEnv(const std::vector<const Array *> &objects);
+
+  void pop(size_t popSize);
+  void push();
+};
+
+Z3SolverEnv::Z3SolverEnv(const std::vector<const Array *> &objects)
+    : objects(objects) {}
+
+void Z3SolverEnv::pop(size_t popSize) {
+  if (popSize == 0)
+    return;
+  objects.pop(popSize);
+  z3_ast_expr_constraints.pop(popSize);
+  z3_ast_expr_to_klee_expr.pop(popSize);
+  expr_to_track.pop(popSize);
+  usedArrayBytes.pop(popSize);
+  symbolicObjects.pop(popSize);
+}
+
+void Z3SolverEnv::push() {
+  objects.push();
+  z3_ast_expr_constraints.push();
+  z3_ast_expr_to_klee_expr.push();
+  expr_to_track.push();
+  usedArrayBytes.push();
+  symbolicObjects.push();
+}
+
+class Z3SolverImpl : public SolverImpl {
+protected:
   std::unique_ptr<Z3Builder> builder;
+  ::Z3_params solverParameters;
+
+private:
   Z3BuilderType builderType;
   time::Span timeout;
   SolverRunStatus runStatusCode;
   std::unique_ptr<llvm::raw_fd_ostream> dumpedQueriesFile;
-  ::Z3_params solverParameters;
   // Parameter symbols
   ::Z3_symbol timeoutParamStrSymbol;
   ::Z3_symbol unsatCoreParamStrSymbol;
 
-  bool internalRunSolver(const Query &,
-                         const std::vector<const Array *> *objects,
+  enum ObjectAssignment {
+    NotNeeded = 0,
+    NeededForObjectsFromEnv,
+    NeededForObjectsFromQuery
+  };
+
+public:
+  virtual Z3_solver initNativeZ3(const ConstraintQuery &query, Z3_probe probe,
+                                 Z3_goal goal) = 0;
+  virtual void deinitNativeZ3(Z3_solver theSolver) = 0;
+
+private:
+  bool internalRunSolver(const ConstraintQuery &query, Z3SolverEnv &env,
+                         ObjectAssignment needObjects,
                          std::vector<SparseStorage<unsigned char>> *values,
                          ValidityCore *validityCore, bool &hasSolution);
   bool validateZ3Model(::Z3_solver &theSolver, ::Z3_model &theModel);
@@ -115,18 +506,47 @@ class Z3SolverImpl : public SolverImpl {
                             const std::vector<const Array *> &objects,
                             std::vector<SparseStorage<unsigned char>> &values,
                             bool &hasSolution);
-  bool check(const Query &query, ref<SolverResponse> &result);
+  using SolverImpl::check;
+  bool check(const ConstraintQuery &query, Z3SolverEnv &env,
+             ref<SolverResponse> &result);
   bool computeValidityCore(const Query &query, ValidityCore &validityCore,
                            bool &isValid);
-  SolverRunStatus handleSolverResponse(
-      ::Z3_solver theSolver, ::Z3_lbool satisfiable,
-      const std::vector<const Array *> *objects,
-      std::vector<SparseStorage<unsigned char>> *values,
-      const std::unordered_map<const Array *, ExprHashSet> &usedArrayBytes,
-      bool &hasSolution);
+  SolverRunStatus
+  handleSolverResponse(::Z3_solver theSolver, ::Z3_lbool satisfiable,
+                       const Z3SolverEnv &env, ObjectAssignment needObjects,
+                       std::vector<SparseStorage<unsigned char>> *values,
+                       bool &hasSolution);
   SolverRunStatus getOperationStatusCode();
 };
 
+Z3_solver createNativeZ3(Z3_context ctx, Z3_params solverParameters,
+                         const ConstraintQuery &query, Z3_probe probe,
+                         Z3_goal goal) {
+  Z3_solver theSolver = nullptr;
+  std::vector<const Array *> arrays = query.gatherArrays();
+  bool forceTactic = true;
+  for (const Array *array : arrays) {
+    if (isa<SymbolicSizeConstantSource>(array->source)) {
+      forceTactic = false;
+      break;
+    }
+  }
+
+  if (forceTactic && Z3_probe_apply(ctx, probe, goal)) {
+    theSolver =
+        Z3_mk_solver_for_logic(ctx, Z3_mk_string_symbol(ctx, "QF_AUFBV"));
+  } else {
+    theSolver = Z3_mk_solver(ctx);
+  }
+  Z3_solver_inc_ref(ctx, theSolver);
+  Z3_solver_set_params(ctx, theSolver, solverParameters);
+  return theSolver;
+}
+
+void deleteNativeZ3(Z3_context ctx, Z3_solver theSolver) {
+  Z3_solver_dec_ref(ctx, theSolver);
+}
+
 Z3SolverImpl::Z3SolverImpl(Z3BuilderType type)
     : builderType(type), runStatusCode(SOLVER_RUN_STATUS_FAILURE) {
   switch (type) {
@@ -185,8 +605,52 @@ Z3SolverImpl::~Z3SolverImpl() {
   Z3_params_dec_ref(builder->ctx, solverParameters);
 }
 
+class Z3NonIncSolverImpl : public Z3SolverImpl {
+private:
+  using Z3SolverImpl::check;
+
+public:
+  Z3NonIncSolverImpl(Z3BuilderType type) : Z3SolverImpl(type) {}
+
+  /// implementation of Z3SolverImpl interface
+  Z3_solver initNativeZ3(const ConstraintQuery &query, Z3_probe probe,
+                         Z3_goal goal);
+  void deinitNativeZ3(Z3_solver theSolver);
+
+  /// implementation of the SolverImpl interface //TODO: return after
+  /// refactoring parent
+  // bool computeTruth(const Query &query, bool &isValid);
+  // bool computeValidity(const Query &query, Solver::Validity &result);
+  // bool computeValue(const Query &query, ref<Expr> &result);
+  // bool computeInitialValues(const Query &query,
+  //                           const std::vector<const Array *> &objects,
+  //                           std::vector<SparseStorage<unsigned char>>
+  //                           &values, bool &hasSolution);
+  bool check(const Query &query, ref<SolverResponse> &result);
+  // bool computeValidityCore(const Query &query, ValidityCore &validityCore,
+  //                          bool &isValid);
+  // SolverRunStatus getOperationStatusCode();
+  // void setCoreSolverTimeout(time::Span timeout);
+};
+
+Z3_solver Z3NonIncSolverImpl::initNativeZ3(const ConstraintQuery &query,
+                                           Z3_probe probe, Z3_goal goal) {
+  return createNativeZ3(builder->ctx, solverParameters, query, probe, goal);
+}
+
+void Z3NonIncSolverImpl::deinitNativeZ3(Z3_solver theSolver) {
+  deleteNativeZ3(builder->ctx, theSolver);
+}
+
+bool Z3NonIncSolverImpl::check(const Query &query,
+                               ref<SolverResponse> &result) {
+  Z3SolverEnv env;
+  bool solver_result = check(query, env, result);
+  return solver_result;
+}
+
 Z3Solver::Z3Solver(Z3BuilderType type)
-    : Solver(std::make_unique<Z3SolverImpl>(type)) {}
+    : Solver(std::make_unique<Z3NonIncSolverImpl>(type)) {}
 
 char *Z3Solver::getConstraintLog(const Query &query) {
   return impl->getConstraintLog(query);
@@ -274,8 +738,10 @@ char *Z3SolverImpl::getConstraintLog(const Query &query) {
 }
 
 bool Z3SolverImpl::computeTruth(const Query &query, bool &isValid) {
+  Z3SolverEnv env;
   bool hasSolution = false; // to remove compiler warning
-  bool status = internalRunSolver(query, /*objects=*/NULL, /*values=*/NULL,
+  bool status = internalRunSolver(query, /*env=*/env,
+                                  ObjectAssignment::NotNeeded, /*values=*/NULL,
                                   /*validityCore=*/NULL, hasSolution);
   isValid = !hasSolution;
   return status;
@@ -303,30 +769,25 @@ bool Z3SolverImpl::computeValue(const Query &query, ref<Expr> &result) {
 bool Z3SolverImpl::computeInitialValues(
     const Query &query, const std::vector<const Array *> &objects,
     std::vector<SparseStorage<unsigned char>> &values, bool &hasSolution) {
-  return internalRunSolver(query, &objects, &values, /*validityCore=*/NULL,
-                           hasSolution);
+  Z3SolverEnv env(objects);
+  return internalRunSolver(query, env,
+                           ObjectAssignment::NeededForObjectsFromEnv, &values,
+                           /*validityCore=*/NULL, hasSolution);
 }
 
-bool Z3SolverImpl::check(const Query &query, ref<SolverResponse> &result) {
-  ExprHashSet expressions;
-  assert(!query.containsSymcretes());
-  expressions.insert(query.constraints.cs().begin(),
-                     query.constraints.cs().end());
-  expressions.insert(query.expr);
-
-  std::vector<const Array *> objects;
-  findSymbolicObjects(expressions.begin(), expressions.end(), objects);
+bool Z3SolverImpl::check(const ConstraintQuery &query, Z3SolverEnv &env,
+                         ref<SolverResponse> &result) {
   std::vector<SparseStorage<unsigned char>> values;
 
   ValidityCore validityCore;
 
   bool hasSolution = false;
-
   bool status =
-      internalRunSolver(query, &objects, &values, &validityCore, hasSolution);
+      internalRunSolver(query, env, ObjectAssignment::NeededForObjectsFromQuery,
+                        &values, &validityCore, hasSolution);
   if (status) {
     result = hasSolution
-                 ? (SolverResponse *)new InvalidResponse(objects, values)
+                 ? (SolverResponse *)new InvalidResponse(env.objects.v, values)
                  : (SolverResponse *)new ValidResponse(validityCore);
   }
   return status;
@@ -335,20 +796,21 @@ bool Z3SolverImpl::check(const Query &query, ref<SolverResponse> &result) {
 bool Z3SolverImpl::computeValidityCore(const Query &query,
                                        ValidityCore &validityCore,
                                        bool &isValid) {
+  Z3SolverEnv env;
   bool hasSolution = false; // to remove compiler warning
-  bool status = internalRunSolver(query, /*objects=*/NULL, /*values=*/NULL,
-                                  &validityCore, hasSolution);
+  bool status =
+      internalRunSolver(query, /*env=*/env, ObjectAssignment::NotNeeded,
+                        /*values=*/NULL, &validityCore, hasSolution);
   isValid = !hasSolution;
   return status;
 }
 
 bool Z3SolverImpl::internalRunSolver(
-    const Query &query, const std::vector<const Array *> *objects,
+    const ConstraintQuery &query, Z3SolverEnv &env,
+    ObjectAssignment needObjects,
     std::vector<SparseStorage<unsigned char>> *values,
     ValidityCore *validityCore, bool &hasSolution) {
 
-  assert(!query.containsSymcretes());
-
   if (ProduceUnsatCore && validityCore) {
     enableUnsatCore();
   } else {
@@ -372,98 +834,98 @@ bool Z3SolverImpl::internalRunSolver(
 
   runStatusCode = SOLVER_RUN_STATUS_FAILURE;
 
-  ConstantArrayFinder constant_arrays_in_query;
-  std::vector<Z3ASTHandle> z3_ast_expr_constraints;
-  std::unordered_map<Z3ASTHandle, ref<Expr>, Z3ASTHandleHash, Z3ASTHandleCmp>
-      z3_ast_expr_to_klee_expr;
-
-  std::unordered_map<Z3ASTHandle, Z3ASTHandle, Z3ASTHandleHash, Z3ASTHandleCmp>
-      expr_to_track;
-  std::unordered_set<Z3ASTHandle, Z3ASTHandleHash, Z3ASTHandleCmp> exprs;
-
-  for (auto const &constraint : query.constraints.cs()) {
-    Z3ASTHandle z3Constraint = builder->construct(constraint);
-    if (ProduceUnsatCore && validityCore) {
-      Z3ASTHandle p = builder->buildFreshBoolConst();
-      z3_ast_expr_to_klee_expr.insert({p, constraint});
-      z3_ast_expr_constraints.push_back(p);
-      expr_to_track[z3Constraint] = p;
+  std::unordered_set<const Array *> all_constant_arrays_in_query;
+  Z3ASTIncSet exprs;
+
+  for (size_t i = 0; i < query.constraints.framesSize();
+       i++, env.push(), exprs.push()) {
+    ConstantArrayFinder constant_arrays_in_query;
+    if (needObjects == ObjectAssignment::NeededForObjectsFromQuery) {
+      env.symbolicObjects.insert(query.constraints.begin(i),
+                                 query.constraints.end(i));
+      // FIXME: findSymbolicObjects template does not support inc_uset::iterator
+      //  findSymbolicObjects(env.symbolicObjects.begin(-1),
+      //  env.symbolicObjects.end(-1), env.objects.v);
+      std::vector<ref<Expr>> tmp;
+      for (auto it = env.symbolicObjects.begin(-1),
+                ite = env.symbolicObjects.end(-1);
+           it != ite; ++it)
+        tmp.push_back(*it);
+      findSymbolicObjects(tmp.begin(), tmp.end(), env.objects.v);
     }
+    for (auto cs_it = query.constraints.begin(i),
+              cs_ite = query.constraints.end(i);
+         cs_it != cs_ite; cs_it++) {
+      const auto &constraint = *cs_it;
+      Z3ASTHandle z3Constraint = builder->construct(constraint);
+      if (ProduceUnsatCore && validityCore) {
+        Z3ASTHandle p = builder->buildFreshBoolConst();
+        env.z3_ast_expr_to_klee_expr.insert({p, constraint});
+        env.z3_ast_expr_constraints.v.push_back(p);
+        env.expr_to_track[z3Constraint] = p;
+      }
 
-    Z3_goal_assert(builder->ctx, goal, z3Constraint);
-    exprs.insert(z3Constraint);
-
-    constant_arrays_in_query.visit(constraint);
-  }
-  ++stats::solverQueries;
-  if (objects)
-    ++stats::queryCounterexamples;
+      Z3_goal_assert(builder->ctx, goal, z3Constraint);
+      exprs.insert(z3Constraint);
 
-  Z3ASTHandle z3QueryExpr =
-      Z3ASTHandle(builder->construct(query.expr), builder->ctx);
-  constant_arrays_in_query.visit(query.expr);
+      constant_arrays_in_query.visit(constraint);
 
-  for (auto const &constant_array : constant_arrays_in_query.results) {
-    assert(builder->constant_array_assertions.count(constant_array) == 1 &&
-           "Constant array found in query, but not handled by Z3Builder");
-    for (auto const &arrayIndexValueExpr :
-         builder->constant_array_assertions[constant_array]) {
-      Z3_goal_assert(builder->ctx, goal, arrayIndexValueExpr);
-      exprs.insert(arrayIndexValueExpr);
+      std::vector<ref<ReadExpr>> reads;
+      findReads(constraint, true, reads);
+      for (const auto &readExpr : reads) {
+        auto readFromArray = readExpr->updates.root;
+        assert(readFromArray);
+        env.usedArrayBytes[readFromArray].insert(readExpr->index);
+      }
     }
-  }
 
-  // KLEE Queries are validity queries i.e.
-  // ∀ X Constraints(X) → query(X)
-  // but Z3 works in terms of satisfiability so instead we ask the
-  // negation of the equivalent i.e.
-  // ∃ X Constraints(X) ∧ ¬ query(X)
-  Z3ASTHandle z3NotQueryExpr =
-      Z3ASTHandle(Z3_mk_not(builder->ctx, z3QueryExpr), builder->ctx);
-  Z3_goal_assert(builder->ctx, goal, z3NotQueryExpr);
-
-  // Assert an generated side constraints we have to this last so that all other
-  // constraints have been traversed so we have all the side constraints needed.
-  for (std::vector<Z3ASTHandle>::iterator it = builder->sideConstraints.begin(),
-                                          ie = builder->sideConstraints.end();
-       it != ie; ++it) {
-    Z3ASTHandle sideConstraint = *it;
-    Z3_goal_assert(builder->ctx, goal, sideConstraint);
-    exprs.insert(sideConstraint);
-  }
+    for (auto constant_array : constant_arrays_in_query.results) {
+      assert(builder->constant_array_assertions.count(constant_array) == 1 &&
+             "Constant array found in query, but not handled by Z3Builder");
+      if (all_constant_arrays_in_query.count(constant_array))
+        continue;
+      all_constant_arrays_in_query.insert(constant_array);
+      for (auto const &arrayIndexValueExpr :
+           builder->constant_array_assertions[constant_array]) {
+        Z3_goal_assert(builder->ctx, goal, arrayIndexValueExpr);
+        exprs.insert(arrayIndexValueExpr);
+      }
+    }
 
-  std::vector<const Array *> arrays = query.gatherArrays();
-  bool forceTactic = true;
-  for (const Array *array : arrays) {
-    if (isa<SymbolicSizeConstantSource>(array->source)) {
-      forceTactic = false;
-      break;
+    // Assert an generated side constraints we have to this last so that all
+    // other constraints have been traversed so we have all the side constraints
+    // needed.
+    for (auto it = builder->sideConstraints.begin(),
+              ie = builder->sideConstraints.end();
+         it != ie; ++it) {
+      Z3ASTHandle sideConstraint = *it;
+      Z3_goal_assert(builder->ctx, goal, sideConstraint);
+      exprs.insert(sideConstraint);
     }
   }
+  exprs.pop(1); // drop last empty frame
 
-  Z3_solver theSolver;
-  if (forceTactic && Z3_probe_apply(builder->ctx, probe, goal)) {
-    theSolver = Z3_mk_solver_for_logic(
-        builder->ctx, Z3_mk_string_symbol(builder->ctx, "QF_AUFBV"));
-  } else {
-    theSolver = Z3_mk_solver(builder->ctx);
-  }
-  Z3_solver_inc_ref(builder->ctx, theSolver);
-  Z3_solver_set_params(builder->ctx, theSolver, solverParameters);
-
-  for (std::unordered_set<Z3ASTHandle, Z3ASTHandleHash,
-                          Z3ASTHandleCmp>::iterator it = exprs.begin(),
-                                                    ie = exprs.end();
-       it != ie; ++it) {
-    Z3ASTHandle expr = *it;
-    if (expr_to_track.count(expr)) {
-      Z3_solver_assert_and_track(builder->ctx, theSolver, expr,
-                                 expr_to_track[expr]);
-    } else {
-      Z3_solver_assert(builder->ctx, theSolver, expr);
+  ++stats::solverQueries;
+  if (!env.objects.v.empty())
+    ++stats::queryCounterexamples;
+
+  Z3_solver theSolver = initNativeZ3(query, probe, goal);
+
+  for (size_t i = 0; i < exprs.framesSize(); i++) {
+    Z3_solver_push(builder->ctx, theSolver);
+    for (auto it = exprs.begin(i), ie = exprs.end(i); it != ie; ++it) {
+      Z3ASTHandle expr = *it;
+      if (env.expr_to_track.count(expr)) {
+        Z3_solver_assert_and_track(builder->ctx, theSolver, expr,
+                                   env.expr_to_track[expr]);
+      } else {
+        Z3_solver_assert(builder->ctx, theSolver, expr);
+      }
     }
   }
-  Z3_solver_assert(builder->ctx, theSolver, z3NotQueryExpr);
+  auto z3_scopes = Z3_solver_get_num_scopes(builder->ctx, theSolver);
+  auto our_scopes = env.objects.framesSize();
+  assert(z3_scopes + 1 == our_scopes);
 
   if (dumpedQueriesFile) {
     *dumpedQueriesFile << "; start Z3 query\n";
@@ -476,22 +938,9 @@ bool Z3SolverImpl::internalRunSolver(
     dumpedQueriesFile->flush();
   }
 
-  constraints_ty allConstraints = query.constraints.cs();
-  allConstraints.insert(query.expr);
-  std::unordered_map<const Array *, ExprHashSet> usedArrayBytes;
-  for (auto constraint : allConstraints) {
-    std::vector<ref<ReadExpr>> reads;
-    findReads(constraint, true, reads);
-    for (auto readExpr : reads) {
-      const Array *readFromArray = readExpr->updates.root;
-      assert(readFromArray);
-      usedArrayBytes[readFromArray].insert(readExpr->index);
-    }
-  }
-
   ::Z3_lbool satisfiable = Z3_solver_check(builder->ctx, theSolver);
-  runStatusCode = handleSolverResponse(theSolver, satisfiable, objects, values,
-                                       usedArrayBytes, hasSolution);
+  runStatusCode = handleSolverResponse(theSolver, satisfiable, env, needObjects,
+                                       values, hasSolution);
   if (ProduceUnsatCore && validityCore && satisfiable == Z3_L_FALSE) {
     constraints_ty unsatCore;
     Z3_ast_vector z3_unsat_core =
@@ -508,15 +957,15 @@ bool Z3SolverImpl::internalRunSolver(
       z3_ast_expr_unsat_core.insert(constraint);
     }
 
-    for (auto &z3_constraint : z3_ast_expr_constraints) {
+    for (const auto &z3_constraint : env.z3_ast_expr_constraints.v) {
       if (z3_ast_expr_unsat_core.find(z3_constraint) !=
           z3_ast_expr_unsat_core.end()) {
-        ref<Expr> constraint = z3_ast_expr_to_klee_expr[z3_constraint];
+        ref<Expr> constraint = env.z3_ast_expr_to_klee_expr[z3_constraint];
         unsatCore.insert(constraint);
       }
     }
     assert(validityCore && "validityCore cannot be nullptr");
-    *validityCore = ValidityCore(unsatCore, query.expr);
+    *validityCore = ValidityCore(unsatCore, query.getOriginalQueryExpr());
 
     Z3_ast_vector assertions =
         Z3_solver_get_assertions(builder->ctx, theSolver);
@@ -533,7 +982,7 @@ bool Z3SolverImpl::internalRunSolver(
 
   Z3_goal_dec_ref(builder->ctx, goal);
   Z3_probe_dec_ref(builder->ctx, probe);
-  Z3_solver_dec_ref(builder->ctx, theSolver);
+  deinitNativeZ3(theSolver);
 
   // Clear the builder's cache to prevent memory usage exploding.
   // By using ``autoClearConstructCache=false`` and clearning now
@@ -558,28 +1007,23 @@ bool Z3SolverImpl::internalRunSolver(
 }
 
 SolverImpl::SolverRunStatus Z3SolverImpl::handleSolverResponse(
-    ::Z3_solver theSolver, ::Z3_lbool satisfiable,
-    const std::vector<const Array *> *objects,
-    std::vector<SparseStorage<unsigned char>> *values,
-    const std::unordered_map<const Array *, ExprHashSet> &usedArrayBytes,
-    bool &hasSolution) {
+    ::Z3_solver theSolver, ::Z3_lbool satisfiable, const Z3SolverEnv &env,
+    ObjectAssignment needObjects,
+    std::vector<SparseStorage<unsigned char>> *values, bool &hasSolution) {
   switch (satisfiable) {
   case Z3_L_TRUE: {
     hasSolution = true;
-    if (!objects) {
+    if (needObjects == ObjectAssignment::NotNeeded) {
       // No assignment is needed
-      assert(values == NULL);
+      assert(!values);
       return SolverImpl::SOLVER_RUN_STATUS_SUCCESS_SOLVABLE;
     }
     assert(values && "values cannot be nullptr");
     ::Z3_model theModel = Z3_solver_get_model(builder->ctx, theSolver);
     assert(theModel && "Failed to retrieve model");
     Z3_model_inc_ref(builder->ctx, theModel);
-    values->reserve(objects->size());
-    for (std::vector<const Array *>::const_iterator it = objects->begin(),
-                                                    ie = objects->end();
-         it != ie; ++it) {
-      const Array *array = *it;
+    values->reserve(env.objects.v.size());
+    for (auto array : env.objects.v) {
       SparseStorage<unsigned char> data;
 
       ::Z3_ast arraySizeExpr;
@@ -596,9 +1040,9 @@ SolverImpl::SolverRunStatus Z3SolverImpl::handleSolverResponse(
       assert(success && "Failed to get size");
 
       data.resize(arraySize);
-      if (usedArrayBytes.count(array)) {
+      if (env.usedArrayBytes.count(array)) {
         std::unordered_set<uint64_t> offsetValues;
-        for (ref<Expr> offsetExpr : usedArrayBytes.at(array)) {
+        for (const ref<Expr> &offsetExpr : env.usedArrayBytes.at(array)) {
           ::Z3_ast arrayElementOffsetExpr;
           Z3_model_eval(builder->ctx, theModel, builder->construct(offsetExpr),
                         Z3_TRUE, &arrayElementOffsetExpr);
@@ -734,5 +1178,333 @@ bool Z3SolverImpl::validateZ3Model(::Z3_solver &theSolver,
 SolverImpl::SolverRunStatus Z3SolverImpl::getOperationStatusCode() {
   return runStatusCode;
 }
+
+struct ConstraintDistance {
+  size_t toPopSize = 0;
+  ConstraintQuery toPush;
+
+  explicit ConstraintDistance() {}
+  ConstraintDistance(const ConstraintQuery &q) : toPush(q) {}
+  explicit ConstraintDistance(size_t toPopSize, const ConstraintQuery &q)
+      : toPopSize(toPopSize), toPush(q) {}
+
+  size_t getDistance() const { return toPopSize + toPush.size(); }
+
+  bool isOnlyPush() const { return toPopSize == 0; }
+
+  void dump() const {
+    llvm::errs() << "ConstraintDistance: pop: " << toPopSize << "; push:\n";
+    klee::dump(toPush.constraints);
+  }
+};
+
+class Z3IncNativeSolver {
+private:
+  Z3_solver nativeSolver = nullptr;
+  Z3_context ctx;
+  Z3_params solverParameters;
+  /// underlying solver frames
+  /// saved only for calculating distances from next queries
+  ConstraintFrames frames;
+
+  void pop(size_t popSize);
+  void push();
+
+public:
+  Z3SolverEnv env;
+
+  Z3IncNativeSolver(Z3_context ctx, Z3_params solverParameters)
+      : ctx(ctx), solverParameters(solverParameters) {}
+  ~Z3IncNativeSolver();
+
+  void distance(const ConstraintQuery &query, ConstraintDistance &delta) const;
+
+  void popPush(ConstraintDistance &delta);
+
+  Z3_solver getOrInit(const ConstraintQuery &query, Z3_probe probe,
+                      Z3_goal goal);
+
+  bool isConsistent() const {
+    auto num_scopes =
+        nativeSolver ? Z3_solver_get_num_scopes(ctx, nativeSolver) : 0;
+    return num_scopes + 1 == frames.framesSize();
+  }
+
+  void dump() const { ::klee::dump(frames); }
+};
+
+void Z3IncNativeSolver::pop(size_t popSize) {
+  if (nativeSolver == nullptr)
+    return;
+  Z3_solver_pop(ctx, nativeSolver, popSize);
+}
+
+void Z3IncNativeSolver::popPush(ConstraintDistance &delta) {
+  env.pop(delta.toPopSize);
+  pop(delta.toPopSize);
+  frames.pop(delta.toPopSize);
+  frames.extend(delta.toPush.constraints);
+}
+
+Z3_solver Z3IncNativeSolver::getOrInit(const ConstraintQuery &query,
+                                       Z3_probe probe, Z3_goal goal) {
+  if (nativeSolver == nullptr) {
+    nativeSolver = createNativeZ3(ctx, solverParameters, query, probe, goal);
+  }
+  return nativeSolver;
+}
+
+Z3IncNativeSolver::~Z3IncNativeSolver() {
+  if (nativeSolver != nullptr)
+    deleteNativeZ3(ctx, nativeSolver);
+}
+
+void Z3IncNativeSolver::distance(const ConstraintQuery &query,
+                                 ConstraintDistance &delta) const {
+  auto sit = frames.v.begin();
+  auto site = frames.v.end();
+  auto qit = query.constraints.v.begin();
+  auto qite = query.constraints.v.end();
+  auto it = frames.begin();
+  auto ite = frames.end();
+  size_t intersect = 0;
+  for (; it != ite && sit != site && qit != qite && *sit == *qit; it++) {
+    size_t frame_size = *it;
+    for (size_t i = 0;
+         i < frame_size && sit != site && qit != qite && *sit == *qit;
+         i++, sit++, qit++, intersect++) {
+    }
+  }
+  for (; sit != site && qit != qite && *sit == *qit;
+       sit++, qit++, intersect++) {
+  }
+  size_t toPop, extraTakeFromOther;
+  ConstraintFrames d;
+  if (sit == site) { // solver frames ended
+    toPop = 0;
+    extraTakeFromOther = 0;
+  } else {
+    frames.takeBefore(intersect, toPop, extraTakeFromOther);
+  }
+  query.constraints.takeAfter(intersect - extraTakeFromOther, d);
+  delta = ConstraintDistance(toPop, d);
+}
+
+class Z3TreeSolverImpl : public Z3SolverImpl {
+private:
+  unsigned maxSolvers;
+  Z3IncNativeSolver *currentSolver = nullptr;
+
+  std::deque<Z3IncNativeSolver *> recentlyUsed;
+  std::vector<Z3IncNativeSolver *> recycledSolvers;
+
+  void reuseOrCreateZ3(const ConstraintQuery &query, ConstraintDistance &delta);
+  void findSuitableSolver(const ConstraintQuery &query,
+                          ConstraintDistance &delta);
+  void findSuitableSolverLRU(const ConstraintQuery &query,
+                             ConstraintDistance &delta);
+
+  using Z3SolverImpl::check;
+  bool check(ConstraintDistance &delta, ref<SolverResponse> &result);
+
+public:
+  Z3TreeSolverImpl(Z3BuilderType type, unsigned maxSolvers)
+      : Z3SolverImpl(type), maxSolvers(maxSolvers){};
+  ~Z3TreeSolverImpl();
+
+  /// implementation of Z3SolverImpl interface
+  Z3_solver initNativeZ3(const ConstraintQuery &query, Z3_probe probe,
+                         Z3_goal goal);
+  void deinitNativeZ3(Z3_solver theSolver);
+
+  void notifyStateTermination(std::uint32_t id);
+
+  /// implementation of the SolverImpl interface
+  bool computeTruth(const Query &query, bool &isValid);
+  bool computeValidity(const Query &query, PartialValidity &result);
+  bool computeInitialValues(const Query &query,
+                            const std::vector<const Array *> &objects,
+                            std::vector<SparseStorage<unsigned char>> &values,
+                            bool &hasSolution);
+  bool check(const Query &query, ref<SolverResponse> &result);
+  bool computeValidityCore(const Query &query, ValidityCore &validityCore,
+                           bool &isValid);
+  SolverRunStatus getOperationStatusCode();
+};
+
+Z3TreeSolverImpl::~Z3TreeSolverImpl() {
+  for (auto solver : recentlyUsed)
+    delete solver;
+  for (auto solver : recycledSolvers)
+    delete solver;
+}
+
+Z3_solver Z3TreeSolverImpl::initNativeZ3(const ConstraintQuery &query,
+                                         Z3_probe probe, Z3_goal goal) {
+  return currentSolver->getOrInit(query, probe, goal);
+}
+
+void Z3TreeSolverImpl::deinitNativeZ3(Z3_solver theSolver) {
+  assert(currentSolver->isConsistent());
+  recentlyUsed.push_front(currentSolver);
+  currentSolver = nullptr;
+}
+
+bool Z3TreeSolverImpl::check(ConstraintDistance &delta,
+                             ref<SolverResponse> &result) {
+  currentSolver->popPush(delta);
+  return check(delta.toPush, currentSolver->env, result);
+}
+
+void Z3TreeSolverImpl::reuseOrCreateZ3(const ConstraintQuery &query,
+                                       ConstraintDistance &delta) {
+  auto min_delta = ConstraintDistance(query);
+  auto min_distance = min_delta.getDistance();
+  Z3IncNativeSolver *min_solver = nullptr;
+  for (auto solver : recycledSolvers) {
+    ConstraintDistance d;
+    solver->distance(query, d);
+    auto distance = d.getDistance();
+    if (distance < min_distance) {
+      min_delta = d;
+      min_distance = distance;
+      min_solver = solver;
+    }
+  }
+  currentSolver = min_solver
+                      ? min_solver
+                      : new Z3IncNativeSolver(builder->ctx, solverParameters);
+  delta = min_delta;
+}
+
+void Z3TreeSolverImpl::findSuitableSolver(const ConstraintQuery &query,
+                                          ConstraintDistance &delta) {
+  ConstraintDistance min_delta;
+  auto min_distance = std::numeric_limits<size_t>::max();
+  Z3IncNativeSolver *min_solver = nullptr;
+  for (auto it = recentlyUsed.begin(), ite = recentlyUsed.end(); it != ite;
+       it++) {
+    currentSolver = *it;
+    currentSolver->distance(query, delta);
+    if (delta.isOnlyPush()) {
+      recentlyUsed.erase(it);
+      return;
+    }
+    auto distance = delta.getDistance();
+    if (distance < min_distance) {
+      min_delta = delta;
+      min_distance = distance;
+      min_solver = currentSolver;
+    }
+  }
+  auto query_delta = ConstraintDistance(query);
+  auto query_distance = query_delta.getDistance();
+  if (min_distance < query_distance) {
+    currentSolver = min_solver;
+    recentlyUsed.erase(
+        std::find(recentlyUsed.begin(), recentlyUsed.end(), min_solver));
+    delta = min_delta;
+    return;
+  }
+  auto min_distance2 = query_distance;
+  auto min_delta2 = query_delta;
+  Z3IncNativeSolver *min_solver2 = nullptr;
+  for (auto solver : recycledSolvers) {
+    solver->distance(query, delta);
+    auto distance = delta.getDistance();
+    if (distance < min_distance2) {
+      min_delta2 = delta;
+      min_distance2 = distance;
+      min_solver2 = solver;
+    }
+  }
+  if (!min_solver2 && recentlyUsed.size() >= maxSolvers) {
+    currentSolver = min_solver;
+    recentlyUsed.erase(
+        std::find(recentlyUsed.begin(), recentlyUsed.end(), min_solver));
+    delta = min_delta;
+    return;
+  }
+  if (min_solver2) {
+    currentSolver = min_solver2;
+    recycledSolvers.erase(
+        std::find(recycledSolvers.begin(), recycledSolvers.end(), min_solver2));
+  } else {
+    currentSolver = new Z3IncNativeSolver(builder->ctx, solverParameters);
+  }
+  delta = min_delta2;
+}
+
+void Z3TreeSolverImpl::findSuitableSolverLRU(const ConstraintQuery &query,
+                                             ConstraintDistance &delta) {
+  for (auto it = recentlyUsed.begin(), ite = recentlyUsed.end(); it != ite;
+       it++) {
+    currentSolver = *it;
+    ConstraintDistance d;
+    currentSolver->distance(query, d);
+    if (d.isOnlyPush()) {
+      recentlyUsed.erase(it);
+      delta = d;
+      return;
+    }
+  }
+  if (recentlyUsed.size() < maxSolvers) {
+    reuseOrCreateZ3(query, delta);
+    return;
+  }
+  currentSolver = recentlyUsed.back();
+  recentlyUsed.pop_back();
+  currentSolver->distance(query, delta);
+}
+
+bool Z3TreeSolverImpl::computeTruth(const Query &query, bool &isValid) {
+  assert(false);
+  return false; // TODO: not implemented
+}
+
+bool Z3TreeSolverImpl::computeValidity(const Query &query,
+                                       PartialValidity &result) {
+  assert(false);
+  return false; // TODO: not implemented
+}
+
+bool Z3TreeSolverImpl::computeInitialValues(
+    const Query &query, const std::vector<const Array *> &objects,
+    std::vector<SparseStorage<unsigned char>> &values, bool &hasSolution) {
+  assert(false);
+  return false; // TODO: not implemented
+}
+
+bool Z3TreeSolverImpl::check(const Query &q, ref<SolverResponse> &result) {
+  ConstraintDistance delta;
+  ConstraintQuery query(q);
+  if (Z3TreeUseGlobalMinDistanceSolver)
+    findSuitableSolver(query, delta);
+  else
+    findSuitableSolverLRU(query, delta);
+  auto ok = check(delta, result);
+  return ok;
+}
+
+bool Z3TreeSolverImpl::computeValidityCore(const Query &query,
+                                           ValidityCore &validityCore,
+                                           bool &isValid) {
+  assert(false);
+  return false; // TODO: not implemented
+}
+
+Z3TreeSolverImpl::SolverRunStatus Z3TreeSolverImpl::getOperationStatusCode() {
+  assert(false);
+  return SOLVER_RUN_STATUS_TIMEOUT; // TODO: not implemented
+}
+
+void Z3TreeSolverImpl::notifyStateTermination(std::uint32_t id) {
+  assert(false);
+  return; // TODO: not implemented
+}
+
+Z3TreeSolver::Z3TreeSolver(Z3BuilderType type, unsigned maxSolvers)
+    : Solver(std::make_unique<Z3TreeSolverImpl>(type, maxSolvers)) {}
+
 } // namespace klee
 #endif // ENABLE_Z3
diff --git a/lib/Solver/Z3Solver.h b/lib/Solver/Z3Solver.h
index 0189dec08f1..0e6649a6d10 100644
--- a/lib/Solver/Z3Solver.h
+++ b/lib/Solver/Z3Solver.h
@@ -33,6 +33,12 @@ class Z3Solver : public Solver {
   /// is off.
   virtual void setCoreSolverTimeout(time::Span timeout);
 };
+
+class Z3TreeSolver : public Solver {
+public:
+  Z3TreeSolver(Z3BuilderType type, unsigned maxSolvers);
+};
+
 } // namespace klee
 
 #endif /* KLEE_Z3SOLVER_H */