diff --git a/include/klee/Expr/AlphaVersionBuilder.h b/include/klee/Expr/AlphaVersionBuilder.h
new file mode 100644
index 00000000000..021c98af695
--- /dev/null
+++ b/include/klee/Expr/AlphaVersionBuilder.h
@@ -0,0 +1,41 @@
+//===-- AlphaVersionBuilder.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_ALPHA_EQUIVALENCY_BUILDER_H
+#define KLEE_ALPHA_EQUIVALENCY_BUILDER_H
+
+#include "klee/Expr/ArrayCache.h"
+#include "klee/Expr/ExprHashMap.h"
+#include "klee/Expr/ExprVisitor.h"
+
+namespace klee {
+
+class AlphaVersionBuilder : public ExprVisitor {
+public:
+  ExprHashMap<ref<Expr>> reverseExprMap;
+  ArrayCache::ArrayHashMap<const Array *> reverseAlphaArrayMap;
+  ArrayCache::ArrayHashMap<const Array *> alphaArrayMap;
+
+private:
+  ArrayCache &arrayCache;
+  unsigned index = 0;
+
+  const Array *visitArray(const Array *arr);
+  UpdateList visitUpdateList(UpdateList u);
+  Action visitRead(const ReadExpr &re);
+
+public:
+  AlphaVersionBuilder(ArrayCache &_arrayCache);
+  constraints_ty visitConstraints(constraints_ty cs);
+  ref<Expr> visitExpr(ref<Expr> v);
+};
+
+} // namespace klee
+
+#endif /*KLEE_ALPHA_EQUIVALENCY_BUILDER_H*/
diff --git a/include/klee/Expr/Parser/Parser.h b/include/klee/Expr/Parser/Parser.h
index 0f6ec291c08..5009125c858 100644
--- a/include/klee/Expr/Parser/Parser.h
+++ b/include/klee/Expr/Parser/Parser.h
@@ -220,6 +220,8 @@ class Parser {
   static Parser *Create(const std::string Name, const llvm::MemoryBuffer *MB,
                         ExprBuilder *Builder, ArrayCache *TheArrayCache,
                         KModule *km, bool ClearArrayAfterQuery);
+
+  virtual ArrayCache &getArrayCache() = 0;
 };
 } // namespace expr
 } // namespace klee
diff --git a/include/klee/Expr/SourceBuilder.h b/include/klee/Expr/SourceBuilder.h
index 7b57e2f8c9f..e3e236141f4 100644
--- a/include/klee/Expr/SourceBuilder.h
+++ b/include/klee/Expr/SourceBuilder.h
@@ -28,6 +28,7 @@ class SourceBuilder {
   static ref<SymbolicSource> value(const llvm::Value &_allocSite, int _index,
                                    KModule *km);
   static ref<SymbolicSource> irreproducible(const std::string &name);
+  static ref<SymbolicSource> alphaModulo(int _index);
 };
 
 }; // namespace klee
diff --git a/include/klee/Expr/SymbolicSource.h b/include/klee/Expr/SymbolicSource.h
index be65580f7bd..b49ee894a78 100644
--- a/include/klee/Expr/SymbolicSource.h
+++ b/include/klee/Expr/SymbolicSource.h
@@ -41,7 +41,8 @@ class SymbolicSource {
     LazyInitializationSize,
     Instruction,
     Argument,
-    Irreproducible
+    Irreproducible,
+    AlphaModulo
   };
 
 public:
@@ -361,6 +362,37 @@ class IrreproducibleSource : public SymbolicSource {
   }
 };
 
+class AlphaModuloSource : public SymbolicSource {
+public:
+  const unsigned index;
+
+  AlphaModuloSource(unsigned _index) : index(_index) {}
+  Kind getKind() const override { return Kind::AlphaModulo; }
+  virtual std::string getName() const override { return "AlphaModulo"; }
+
+  static bool classof(const SymbolicSource *S) {
+    return S->getKind() == Kind::AlphaModulo;
+  }
+  static bool classof(const AlphaModuloSource *) { return true; }
+
+  virtual unsigned computeHash() override {
+    unsigned res = getKind();
+    hashValue = res ^ (index * SymbolicSource::MAGIC_HASH_CONSTANT);
+    return hashValue;
+  }
+
+  virtual int internalCompare(const SymbolicSource &b) const override {
+    if (getKind() != b.getKind()) {
+      return getKind() < b.getKind() ? -1 : 1;
+    }
+    const AlphaModuloSource &amb = static_cast<const AlphaModuloSource &>(b);
+    if (index != amb.index) {
+      return index < amb.index ? -1 : 1;
+    }
+    return 0;
+  }
+};
+
 } // namespace klee
 
 #endif /* KLEE_SYMBOLICSOURCE_H */
diff --git a/include/klee/Solver/Common.h b/include/klee/Solver/Common.h
index 57ebad547d2..2a43b9eb672 100644
--- a/include/klee/Solver/Common.h
+++ b/include/klee/Solver/Common.h
@@ -29,7 +29,7 @@ std::unique_ptr<Solver> constructSolverChain(
     std::unique_ptr<Solver> coreSolver, std::string querySMT2LogPath,
     std::string baseSolverQuerySMT2LogPath, std::string queryKQueryLogPath,
     std::string baseSolverQueryKQueryLogPath,
-    AddressGenerator *addressGenerator);
+    AddressGenerator *addressGenerator, ArrayCache &arrayCache);
 } // namespace klee
 
 #endif /* KLEE_COMMON_H */
diff --git a/include/klee/Solver/Solver.h b/include/klee/Solver/Solver.h
index c39d8a2ae39..c7c1c223dd9 100644
--- a/include/klee/Solver/Solver.h
+++ b/include/klee/Solver/Solver.h
@@ -244,6 +244,14 @@ std::unique_ptr<Solver> createFastCexSolver(std::unique_ptr<Solver> s);
 /// \param s - The underlying solver to use.
 std::unique_ptr<Solver> createIndependentSolver(std::unique_ptr<Solver> s);
 
+/// createAlphaEquivalencySolver - Create a solver which will change
+/// independent queries to their alpha-equvalent version
+///
+/// \param s - The underlying solver to use.
+/// \param arrayCache - Class to create new arrays.
+std::unique_ptr<Solver> createAlphaEquivalencySolver(std::unique_ptr<Solver> s,
+                                                     ArrayCache &arrayCache);
+
 /// createKQueryLoggingSolver - Create a solver which will forward all queries
 /// after writing them to the given path in .kquery format.
 std::unique_ptr<Solver> createKQueryLoggingSolver(std::unique_ptr<Solver> s,
diff --git a/include/klee/Solver/SolverCmdLine.h b/include/klee/Solver/SolverCmdLine.h
index 6bd0c285bbd..692f7417343 100644
--- a/include/klee/Solver/SolverCmdLine.h
+++ b/include/klee/Solver/SolverCmdLine.h
@@ -32,6 +32,8 @@ extern llvm::cl::opt<bool> UseCexCache;
 
 extern llvm::cl::opt<bool> UseBranchCache;
 
+extern llvm::cl::opt<bool> UseAlphaEquivalence;
+
 extern llvm::cl::opt<bool> UseConcretizingSolver;
 
 extern llvm::cl::opt<bool> UseIndependentSolver;
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 63130c38d8c..83552c594a7 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -507,7 +507,7 @@ Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts,
       interpreterHandler->getOutputFilename(SOLVER_QUERIES_SMT2_FILE_NAME),
       interpreterHandler->getOutputFilename(ALL_QUERIES_KQUERY_FILE_NAME),
       interpreterHandler->getOutputFilename(SOLVER_QUERIES_KQUERY_FILE_NAME),
-      addressManager.get());
+      addressManager.get(), arrayCache);
 
   this->solver = std::make_unique<TimingSolver>(std::move(solver), optimizer,
                                                 EqualitySubstitution);
diff --git a/lib/Expr/AlphaVersionBuilder.cpp b/lib/Expr/AlphaVersionBuilder.cpp
new file mode 100644
index 00000000000..9295074781f
--- /dev/null
+++ b/lib/Expr/AlphaVersionBuilder.cpp
@@ -0,0 +1,77 @@
+//===-- AlphaVersionBuilder.cpp ---------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#include "klee/Expr/AlphaVersionBuilder.h"
+#include "klee/Expr/ArrayCache.h"
+#include "klee/Expr/SourceBuilder.h"
+
+#include <vector>
+
+namespace klee {
+
+const Array *AlphaVersionBuilder::visitArray(const Array *arr) {
+  if (alphaArrayMap.find(arr) == alphaArrayMap.end()) {
+    ref<SymbolicSource> source = arr->source;
+    if (!arr->isConstantArray()) {
+      source = SourceBuilder::alphaModulo(index);
+    }
+    ref<Expr> size = visit(arr->getSize());
+    alphaArrayMap[arr] =
+        arrayCache.CreateArray(size, source, arr->getDomain(), arr->getRange());
+    reverseAlphaArrayMap[alphaArrayMap[arr]] = arr;
+    index++;
+  }
+  return alphaArrayMap[arr];
+}
+
+UpdateList AlphaVersionBuilder::visitUpdateList(UpdateList u) {
+  const Array *root = visitArray(u.root);
+  std::vector<ref<UpdateNode>> updates;
+
+  for (auto un = u.head; un; un = un->next) {
+    updates.push_back(un);
+  }
+
+  updates.push_back(nullptr);
+
+  for (int i = updates.size() - 2; i >= 0; i--) {
+    ref<Expr> index = visit(updates[i]->index);
+    ref<Expr> value = visit(updates[i]->value);
+    updates[i] = new UpdateNode(updates[i + 1], index, value);
+  }
+  return UpdateList(root, updates[0]);
+}
+
+ExprVisitor::Action AlphaVersionBuilder::visitRead(const ReadExpr &re) {
+  ref<Expr> v = visit(re.index);
+  UpdateList u = visitUpdateList(re.updates);
+  ref<Expr> e = ReadExpr::create(u, v);
+  return Action::changeTo(e);
+}
+
+AlphaVersionBuilder::AlphaVersionBuilder(ArrayCache &_arrayCache)
+    : arrayCache(_arrayCache) {}
+
+constraints_ty AlphaVersionBuilder::visitConstraints(constraints_ty cs) {
+  constraints_ty result;
+  for (auto arg : cs) {
+    ref<Expr> v = visit(arg);
+    reverseExprMap[v] = arg;
+    result.insert(v);
+  }
+  return result;
+}
+ref<Expr> AlphaVersionBuilder::visitExpr(ref<Expr> v) {
+  ref<Expr> e = visit(v);
+  reverseExprMap[e] = v;
+  reverseExprMap[Expr::createIsZero(e)] = Expr::createIsZero(v);
+  return e;
+}
+
+} // namespace klee
\ No newline at end of file
diff --git a/lib/Expr/CMakeLists.txt b/lib/Expr/CMakeLists.txt
index 758a4ca7433..d1838735a79 100644
--- a/lib/Expr/CMakeLists.txt
+++ b/lib/Expr/CMakeLists.txt
@@ -7,6 +7,7 @@
 #
 #===------------------------------------------------------------------------===#
 add_library(kleaverExpr
+  AlphaVersionBuilder.cpp
   APFloatEval.cpp
   ArrayCache.cpp
   ArrayExprOptimizer.cpp
diff --git a/lib/Expr/ExprPPrinter.cpp b/lib/Expr/ExprPPrinter.cpp
index bde8d30d6d1..08c253311df 100644
--- a/lib/Expr/ExprPPrinter.cpp
+++ b/lib/Expr/ExprPPrinter.cpp
@@ -413,6 +413,8 @@ class PPrinter : public ExprPPrinter {
          << " " << s->index;
     } else if (auto s = dyn_cast<IrreproducibleSource>(source)) {
       PC << s->name;
+    } else if (auto s = dyn_cast<AlphaModuloSource>(source)) {
+      PC << s->index;
     } else {
       assert(0 && "Not implemented");
     }
diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp
index b072cec8261..2d30a5ce778 100644
--- a/lib/Expr/Parser.cpp
+++ b/lib/Expr/Parser.cpp
@@ -280,6 +280,8 @@ class ParserImpl : public Parser {
     }
   }
 
+  ArrayCache &getArrayCache() { return *TheArrayCache; }
+
   /*** Grammar productions ****/
 
   /* Top level decls */
@@ -330,6 +332,7 @@ class ParserImpl : public Parser {
   SourceResult ParseLazyInitializationSizeSource();
   SourceResult ParseInstructionSource();
   SourceResult ParseArgumentSource();
+  SourceResult ParseAlphaModuloSource();
 
   /*** Diagnostics ***/
 
@@ -501,6 +504,9 @@ SourceResult ParserImpl::ParseSource() {
   } else if (type == "argument") {
     assert(km);
     source = ParseArgumentSource();
+  } else if (type == "alphaModulo") {
+    assert(km);
+    source = ParseAlphaModuloSource();
   } else {
     assert(0);
   }
@@ -599,6 +605,12 @@ SourceResult ParserImpl::ParseInstructionSource() {
   return SourceBuilder::instruction(*KI->inst, index, km);
 }
 
+SourceResult ParserImpl::ParseAlphaModuloSource() {
+  auto indexExpr = ParseNumber(64).get();
+  auto index = dyn_cast<ConstantExpr>(indexExpr)->getZExtValue();
+  return SourceBuilder::alphaModulo(index);
+}
+
 /// ParseCommandDecl - Parse a command declaration. The lexer should
 /// be positioned at the opening '('.
 ///
diff --git a/lib/Expr/SourceBuilder.cpp b/lib/Expr/SourceBuilder.cpp
index a667a19ba26..33fb9a61508 100644
--- a/lib/Expr/SourceBuilder.cpp
+++ b/lib/Expr/SourceBuilder.cpp
@@ -86,4 +86,10 @@ ref<SymbolicSource> SourceBuilder::irreproducible(const std::string &name) {
   ref<SymbolicSource> r(new IrreproducibleSource(name + llvm::utostr(++id)));
   r->computeHash();
   return r;
+}
+
+ref<SymbolicSource> SourceBuilder::alphaModulo(int _index) {
+  ref<SymbolicSource> r(new AlphaModuloSource(_index));
+  r->computeHash();
+  return r;
 }
\ No newline at end of file
diff --git a/lib/Solver/AlphaEquivalencySolver.cpp b/lib/Solver/AlphaEquivalencySolver.cpp
new file mode 100644
index 00000000000..d273036c145
--- /dev/null
+++ b/lib/Solver/AlphaEquivalencySolver.cpp
@@ -0,0 +1,229 @@
+//===-- AlphaEquivalencySolver.cpp-----------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#include "klee/Expr/SymbolicSource.h"
+#include "klee/Solver/SolverUtil.h"
+
+#include "klee/Solver/Solver.h"
+
+#include "klee/Expr/AlphaVersionBuilder.h"
+#include "klee/Expr/Assignment.h"
+#include "klee/Expr/Constraints.h"
+#include "klee/Expr/ExprHashMap.h"
+#include "klee/Solver/SolverImpl.h"
+#include "klee/Support/Debug.h"
+
+#include "klee/Support/CompilerWarning.h"
+DISABLE_WARNING_PUSH
+DISABLE_WARNING_DEPRECATED_DECLARATIONS
+#include "llvm/Support/Casting.h"
+#include "llvm/Support/raw_ostream.h"
+DISABLE_WARNING_POP
+
+using namespace klee;
+using namespace llvm;
+
+class AlphaEquivalencySolver : public SolverImpl {
+private:
+  std::unique_ptr<Solver> solver;
+  ArrayCache &arrayCache;
+
+public:
+  AlphaEquivalencySolver(std::unique_ptr<Solver> solver,
+                         ArrayCache &_arrayCache)
+      : solver(std::move(solver)), arrayCache(_arrayCache) {}
+
+  bool computeTruth(const Query &, bool &isValid);
+  bool computeValidity(const Query &, PartialValidity &result);
+  bool computeValue(const 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();
+  char *getConstraintLog(const Query &);
+  void setCoreSolverTimeout(time::Span timeout);
+  void notifyStateTermination(std::uint32_t id);
+  ValidityCore reverseAlphaVersion(const ValidityCore &validityCore,
+                                   const ExprHashMap<ref<Expr>> &reverse);
+  const std::vector<const Array *>
+  reverseAlphaVersion(const std::vector<const Array *> &objects,
+                      const ArrayCache::ArrayHashMap<const Array *> &reverse);
+  Assignment
+  reverseAlphaVersion(const Assignment &a,
+                      const ArrayCache::ArrayHashMap<const Array *> &reverse);
+  ref<SolverResponse> reverseAlphaVersion(ref<SolverResponse> res,
+                                          const AlphaVersionBuilder &builder);
+  ref<SolverResponse> createAlphaVersion(ref<SolverResponse> res,
+                                         const AlphaVersionBuilder &builder);
+};
+
+ValidityCore AlphaEquivalencySolver::reverseAlphaVersion(
+    const ValidityCore &validityCore, const ExprHashMap<ref<Expr>> &reverse) {
+  ValidityCore reverseValidityCore;
+  assert(reverse.find(validityCore.expr) != reverse.end());
+  reverseValidityCore.expr = reverse.at(validityCore.expr);
+  for (auto e : validityCore.constraints) {
+    assert(reverse.find(e) != reverse.end());
+    reverseValidityCore.constraints.insert(reverse.at(e));
+  }
+  return reverseValidityCore;
+}
+
+const std::vector<const Array *> AlphaEquivalencySolver::reverseAlphaVersion(
+    const std::vector<const Array *> &objects,
+    const ArrayCache::ArrayHashMap<const Array *> &reverse) {
+  std::vector<const Array *> reverseObjects;
+  for (auto it : objects) {
+    reverseObjects.push_back(reverse.at(it));
+  }
+  return reverseObjects;
+}
+
+Assignment AlphaEquivalencySolver::reverseAlphaVersion(
+    const Assignment &a,
+    const ArrayCache::ArrayHashMap<const Array *> &reverse) {
+  std::vector<const Array *> objects = a.keys();
+  std::vector<SparseStorage<unsigned char>> values = a.values();
+  objects = reverseAlphaVersion(objects, reverse);
+  return Assignment(objects, values);
+}
+
+ref<SolverResponse> AlphaEquivalencySolver::reverseAlphaVersion(
+    ref<SolverResponse> res, const AlphaVersionBuilder &builder) {
+  ref<SolverResponse> reverseRes;
+  if (!isa<InvalidResponse>(res) && !isa<ValidResponse>(res)) {
+    return res;
+  }
+
+  if (isa<InvalidResponse>(res)) {
+    Assignment a = cast<InvalidResponse>(res)->initialValues();
+    a = reverseAlphaVersion(a, builder.reverseAlphaArrayMap);
+    reverseRes = new InvalidResponse(a.bindings);
+  } else {
+    ValidityCore validityCore;
+    res->tryGetValidityCore(validityCore);
+    validityCore = reverseAlphaVersion(validityCore, builder.reverseExprMap);
+    reverseRes = new ValidResponse(validityCore);
+  }
+  return reverseRes;
+}
+
+ref<SolverResponse>
+AlphaEquivalencySolver::createAlphaVersion(ref<SolverResponse> res,
+                                           const AlphaVersionBuilder &builder) {
+  if (!res || !isa<InvalidResponse>(res)) {
+    return res;
+  }
+
+  Assignment a = cast<InvalidResponse>(res)->initialValues();
+  reverseAlphaVersion(a, builder.alphaArrayMap);
+  return new InvalidResponse(a.bindings);
+}
+
+bool AlphaEquivalencySolver::computeValidity(const Query &query,
+                                             PartialValidity &result) {
+  AlphaVersionBuilder builder(arrayCache);
+  constraints_ty factor = builder.visitConstraints(query.constraints.cs());
+  ref<Expr> factorExpr = builder.visitExpr(query.expr);
+  return solver->impl->computeValidity(
+      Query(ConstraintSet(factor, {}, {}), factorExpr, query.id), result);
+}
+
+bool AlphaEquivalencySolver::computeTruth(const Query &query, bool &isValid) {
+  AlphaVersionBuilder builder(arrayCache);
+  constraints_ty factor = builder.visitConstraints(query.constraints.cs());
+  ref<Expr> factorExpr = builder.visitExpr(query.expr);
+  return solver->impl->computeTruth(
+      Query(ConstraintSet(factor, {}, {}), factorExpr, query.id), isValid);
+}
+
+bool AlphaEquivalencySolver::computeValue(const Query &query,
+                                          ref<Expr> &result) {
+  AlphaVersionBuilder builder(arrayCache);
+  constraints_ty factor = builder.visitConstraints(query.constraints.cs());
+  ref<Expr> factorExpr = builder.visitExpr(query.expr);
+  return solver->impl->computeValue(
+      Query(ConstraintSet(factor, {}, {}), factorExpr, query.id), result);
+}
+
+bool AlphaEquivalencySolver::computeInitialValues(
+    const Query &query, const std::vector<const Array *> &objects,
+    std::vector<SparseStorage<unsigned char>> &values, bool &hasSolution) {
+  AlphaVersionBuilder builder(arrayCache);
+  constraints_ty factor = builder.visitConstraints(query.constraints.cs());
+  ref<Expr> factorExpr = builder.visitExpr(query.expr);
+  const std::vector<const Array *> newObjects =
+      reverseAlphaVersion(objects, builder.alphaArrayMap);
+
+  if (!solver->impl->computeInitialValues(
+          Query(ConstraintSet(factor, {}, {}), factorExpr, query.id),
+          newObjects, values, hasSolution)) {
+    return false;
+  }
+  return true;
+}
+
+bool AlphaEquivalencySolver::check(const Query &query,
+                                   ref<SolverResponse> &result) {
+  AlphaVersionBuilder builder(arrayCache);
+
+  constraints_ty factor = builder.visitConstraints(query.constraints.cs());
+  ref<Expr> factorExpr = builder.visitExpr(query.expr);
+  result = createAlphaVersion(result, builder);
+  if (!solver->impl->check(
+          Query(ConstraintSet(factor, {}, {}), factorExpr, query.id), result)) {
+    return false;
+  }
+
+  result = reverseAlphaVersion(result, builder);
+  return true;
+}
+
+bool AlphaEquivalencySolver::computeValidityCore(const Query &query,
+                                                 ValidityCore &validityCore,
+                                                 bool &isValid) {
+  AlphaVersionBuilder builder(arrayCache);
+
+  constraints_ty factor = builder.visitConstraints(query.constraints.cs());
+  ref<Expr> factorExpr = builder.visitExpr(query.expr);
+  if (!solver->impl->computeValidityCore(
+          Query(ConstraintSet(factor, {}, {}), factorExpr, query.id),
+          validityCore, isValid)) {
+    return false;
+  }
+  validityCore = reverseAlphaVersion(validityCore, builder.reverseExprMap);
+  return true;
+}
+
+SolverImpl::SolverRunStatus AlphaEquivalencySolver::getOperationStatusCode() {
+  return solver->impl->getOperationStatusCode();
+}
+
+char *AlphaEquivalencySolver::getConstraintLog(const Query &query) {
+  return solver->impl->getConstraintLog(query);
+}
+
+void AlphaEquivalencySolver::setCoreSolverTimeout(time::Span timeout) {
+  solver->impl->setCoreSolverTimeout(timeout);
+}
+
+void AlphaEquivalencySolver::notifyStateTermination(std::uint32_t id) {
+  solver->impl->notifyStateTermination(id);
+}
+
+std::unique_ptr<Solver>
+klee::createAlphaEquivalencySolver(std::unique_ptr<Solver> s,
+                                   ArrayCache &arrayCache) {
+  return std::make_unique<Solver>(
+      std::make_unique<AlphaEquivalencySolver>(std::move(s), arrayCache));
+}
diff --git a/lib/Solver/CMakeLists.txt b/lib/Solver/CMakeLists.txt
index a1b15052bc9..be6bf57de5d 100644
--- a/lib/Solver/CMakeLists.txt
+++ b/lib/Solver/CMakeLists.txt
@@ -7,6 +7,7 @@
 #
 #===------------------------------------------------------------------------===#
 add_library(kleaverSolver
+  AlphaEquivalencySolver.cpp
   AssignmentValidatingSolver.cpp
   CachingSolver.cpp
   CexCachingSolver.cpp
diff --git a/lib/Solver/ConstructSolverChain.cpp b/lib/Solver/ConstructSolverChain.cpp
index f8c9c8d5226..bfc847178f1 100644
--- a/lib/Solver/ConstructSolverChain.cpp
+++ b/lib/Solver/ConstructSolverChain.cpp
@@ -34,7 +34,7 @@ std::unique_ptr<Solver> constructSolverChain(
     std::unique_ptr<Solver> coreSolver, std::string querySMT2LogPath,
     std::string baseSolverQuerySMT2LogPath, std::string queryKQueryLogPath,
     std::string baseSolverQueryKQueryLogPath,
-    AddressGenerator *addressGenerator) {
+    AddressGenerator *addressGenerator, ArrayCache &arrayCache) {
   Solver *rawCoreSolver = coreSolver.get();
   std::unique_ptr<Solver> solver = std::move(coreSolver);
   const time::Span minQueryTimeToLog(MinQueryTimeToLog);
@@ -67,6 +67,9 @@ std::unique_ptr<Solver> constructSolverChain(
   if (UseBranchCache)
     solver = createCachingSolver(std::move(solver));
 
+  if (UseAlphaEquivalence)
+    solver = createAlphaEquivalencySolver(std::move(solver), arrayCache);
+
   if (UseIndependentSolver)
     solver = createIndependentSolver(std::move(solver));
 
diff --git a/lib/Solver/SolverCmdLine.cpp b/lib/Solver/SolverCmdLine.cpp
index 0f51525d535..4974abe1f82 100644
--- a/lib/Solver/SolverCmdLine.cpp
+++ b/lib/Solver/SolverCmdLine.cpp
@@ -56,6 +56,11 @@ cl::opt<bool> UseBranchCache("use-branch-cache", cl::init(true),
                              cl::desc("Use the branch cache (default=true)"),
                              cl::cat(SolvingCat));
 
+cl::opt<bool>
+    UseAlphaEquivalence("use-alpha-equivalence", cl::init(true),
+                        cl::desc("Use the alpha version builder(default=true)"),
+                        cl::cat(SolvingCat));
+
 cl::opt<bool>
     UseConcretizingSolver("use-concretizing-solver", cl::init(true),
                           cl::desc("Use concretization manager(default=true)"),
diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp
index 5488055bd26..2deedb3c0be 100644
--- a/tools/kleaver/main.cpp
+++ b/tools/kleaver/main.cpp
@@ -9,6 +9,7 @@
 
 #include "klee/ADT/SparseStorage.h"
 #include "klee/Config/Version.h"
+#include "klee/Expr/ArrayCache.h"
 #include "klee/Expr/Constraints.h"
 #include "klee/Expr/Expr.h"
 #include "klee/Expr/ExprBuilder.h"
@@ -212,7 +213,8 @@ static bool EvaluateInputAST(const char *Filename, const llvm::MemoryBuffer *MB,
       std::move(coreSolver), getQueryLogPath(ALL_QUERIES_SMT2_FILE_NAME),
       getQueryLogPath(SOLVER_QUERIES_SMT2_FILE_NAME),
       getQueryLogPath(ALL_QUERIES_KQUERY_FILE_NAME),
-      getQueryLogPath(SOLVER_QUERIES_KQUERY_FILE_NAME), nullptr);
+      getQueryLogPath(SOLVER_QUERIES_KQUERY_FILE_NAME), nullptr,
+      P->getArrayCache());
 
   unsigned Index = 0;
   for (std::vector<Decl *>::iterator it = Decls.begin(), ie = Decls.end();