diff --git a/include/klee/Expr/AlphaBuilder.h b/include/klee/Expr/AlphaBuilder.h
new file mode 100644
index 0000000000..f00b324ae7
--- /dev/null
+++ b/include/klee/Expr/AlphaBuilder.h
@@ -0,0 +1,41 @@
+//===-- AlphaBuilder.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_BUILDER_H
+#define KLEE_ALPHA_BUILDER_H
+
+#include "klee/Expr/ArrayCache.h"
+#include "klee/Expr/ExprHashMap.h"
+#include "klee/Expr/ExprVisitor.h"
+
+namespace klee {
+
+class AlphaBuilder : 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:
+  AlphaBuilder(ArrayCache &_arrayCache);
+  constraints_ty visitConstraints(constraints_ty cs);
+  ref<Expr> visitExpr(ref<Expr> v);
+};
+
+} // namespace klee
+
+#endif /*KLEE_ALPHA_VERSION_BUILDER_H*/
diff --git a/include/klee/Expr/Parser/Parser.h b/include/klee/Expr/Parser/Parser.h
index 0f6ec291c0..5009125c85 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 1747fab458..6869ad0753 100644
--- a/include/klee/Expr/SourceBuilder.h
+++ b/include/klee/Expr/SourceBuilder.h
@@ -32,6 +32,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> alpha(int _index);
 };
 
 }; // namespace klee
diff --git a/include/klee/Expr/SymbolicSource.h b/include/klee/Expr/SymbolicSource.h
index ded381bb00..5829855543 100644
--- a/include/klee/Expr/SymbolicSource.h
+++ b/include/klee/Expr/SymbolicSource.h
@@ -45,7 +45,8 @@ class SymbolicSource {
     LazyInitializationSize,
     Instruction,
     Argument,
-    Irreproducible
+    Irreproducible,
+    Alpha
   };
 
 public:
@@ -349,6 +350,37 @@ class IrreproducibleSource : public SymbolicSource {
   }
 };
 
+class AlphaSource : public SymbolicSource {
+public:
+  const unsigned index;
+
+  AlphaSource(unsigned _index) : index(_index) {}
+  Kind getKind() const override { return Kind::Alpha; }
+  virtual std::string getName() const override { return "alpha"; }
+
+  static bool classof(const SymbolicSource *S) {
+    return S->getKind() == Kind::Alpha;
+  }
+  static bool classof(const AlphaSource *) { 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 AlphaSource &amb = static_cast<const AlphaSource &>(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 57ebad547d..2a43b9eb67 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 c39d8a2ae3..93fad34f54 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);
 
+/// createAlphaEquivalenceSolver - 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> createAlphaEquivalenceSolver(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 6bd0c285bb..692f741734 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/include/klee/Solver/SolverUtil.h b/include/klee/Solver/SolverUtil.h
index d68d3ea77e..ffd3849c62 100644
--- a/include/klee/Solver/SolverUtil.h
+++ b/include/klee/Solver/SolverUtil.h
@@ -299,7 +299,21 @@ class InvalidResponse : public SolverResponse {
   }
 
   bool satisfies(const std::set<ref<Expr>> &key, bool allowFreeValues = true) {
-    return result.satisfies(key.begin(), key.end(), allowFreeValues);
+    std::set<ref<Expr>> booleanKey;
+    std::set<ref<Expr>> nonBooleanKey;
+
+    for (auto i : key) {
+      if (i->getWidth() == Expr::Bool) {
+        booleanKey.insert(i);
+      } else {
+        nonBooleanKey.insert(i);
+      }
+    }
+
+    return result.satisfies(booleanKey.begin(), booleanKey.end(),
+                            allowFreeValues) &&
+           result.satisfiesNonBoolean(nonBooleanKey.begin(),
+                                      nonBooleanKey.end(), allowFreeValues);
   }
 
   bool satisfiesNonBoolean(const std::set<ref<Expr>> &key,
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index dd34b18d5d..3217f33f92 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -515,7 +515,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/AlphaBuilder.cpp b/lib/Expr/AlphaBuilder.cpp
new file mode 100644
index 0000000000..fa52783660
--- /dev/null
+++ b/lib/Expr/AlphaBuilder.cpp
@@ -0,0 +1,85 @@
+//===-- AlphaBuilder.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/AlphaBuilder.h"
+#include "klee/Expr/ArrayCache.h"
+#include "klee/Expr/SourceBuilder.h"
+
+#include <vector>
+
+namespace klee {
+
+const Array *AlphaBuilder::visitArray(const Array *arr) {
+  if (alphaArrayMap.find(arr) == alphaArrayMap.end()) {
+    ref<SymbolicSource> source = arr->source;
+    ref<Expr> size = visit(arr->getSize());
+
+    if (!arr->isConstantArray()) {
+      source = SourceBuilder::alpha(index);
+      index++;
+      alphaArrayMap[arr] = arrayCache.CreateArray(
+          size, source, arr->getDomain(), arr->getRange());
+      reverseAlphaArrayMap[alphaArrayMap[arr]] = arr;
+    } else if (size != arr->getSize()) {
+      alphaArrayMap[arr] = arrayCache.CreateArray(
+          size, source, arr->getDomain(), arr->getRange());
+      reverseAlphaArrayMap[alphaArrayMap[arr]] = arr;
+    } else {
+      alphaArrayMap[arr] = arr;
+      reverseAlphaArrayMap[arr] = arr;
+    }
+  }
+  return alphaArrayMap[arr];
+}
+
+UpdateList AlphaBuilder::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 AlphaBuilder::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);
+}
+
+AlphaBuilder::AlphaBuilder(ArrayCache &_arrayCache) : arrayCache(_arrayCache) {}
+
+constraints_ty AlphaBuilder::visitConstraints(constraints_ty cs) {
+  constraints_ty result;
+  for (auto arg : cs) {
+    ref<Expr> v = visit(arg);
+    reverseExprMap[v] = arg;
+    reverseExprMap[Expr::createIsZero(v)] = Expr::createIsZero(arg);
+    result.insert(v);
+  }
+  return result;
+}
+ref<Expr> AlphaBuilder::visitExpr(ref<Expr> v) {
+  ref<Expr> e = visit(v);
+  reverseExprMap[e] = v;
+  reverseExprMap[Expr::createIsZero(e)] = Expr::createIsZero(v);
+  return e;
+}
+
+} // namespace klee
diff --git a/lib/Expr/CMakeLists.txt b/lib/Expr/CMakeLists.txt
index 03137ef820..6167bbf721 100644
--- a/lib/Expr/CMakeLists.txt
+++ b/lib/Expr/CMakeLists.txt
@@ -7,6 +7,7 @@
 #
 #===------------------------------------------------------------------------===#
 add_library(kleaverExpr
+  AlphaBuilder.cpp
   APFloatEval.cpp
   ArrayCache.cpp
   ArrayExprOptimizer.cpp
diff --git a/lib/Expr/ExprPPrinter.cpp b/lib/Expr/ExprPPrinter.cpp
index 46d4a1072b..5ffba87725 100644
--- a/lib/Expr/ExprPPrinter.cpp
+++ b/lib/Expr/ExprPPrinter.cpp
@@ -410,6 +410,8 @@ class PPrinter : public ExprPPrinter {
          << kf->getName().str() << " " << s->index;
     } else if (auto s = dyn_cast<IrreproducibleSource>(source)) {
       PC << s->name;
+    } else if (auto s = dyn_cast<AlphaSource>(source)) {
+      PC << s->index;
     } else {
       assert(0 && "Not implemented");
     }
diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp
index 19b72f7321..a144437fd8 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 */
@@ -329,6 +331,7 @@ class ParserImpl : public Parser {
   SourceResult ParseLazyInitializationSizeSource();
   SourceResult ParseInstructionSource();
   SourceResult ParseArgumentSource();
+  SourceResult ParseAlphaSource();
 
   /*** Diagnostics ***/
 
@@ -498,6 +501,8 @@ SourceResult ParserImpl::ParseSource() {
   } else if (type == "argument") {
     assert(km);
     source = ParseArgumentSource();
+  } else if (type == "alpha") {
+    source = ParseAlphaSource();
   } else {
     assert(0);
   }
@@ -626,6 +631,12 @@ SourceResult ParserImpl::ParseInstructionSource() {
   return SourceBuilder::instruction(*KI->inst, index, km);
 }
 
+SourceResult ParserImpl::ParseAlphaSource() {
+  auto indexExpr = ParseNumber(64).get();
+  auto index = dyn_cast<ConstantExpr>(indexExpr)->getZExtValue();
+  return SourceBuilder::alpha(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 2a3a09908d..866f89da6d 100644
--- a/lib/Expr/SourceBuilder.cpp
+++ b/lib/Expr/SourceBuilder.cpp
@@ -88,3 +88,9 @@ ref<SymbolicSource> SourceBuilder::irreproducible(const std::string &name) {
   r->computeHash();
   return r;
 }
+
+ref<SymbolicSource> SourceBuilder::alpha(int _index) {
+  ref<SymbolicSource> r(new AlphaSource(_index));
+  r->computeHash();
+  return r;
+}
diff --git a/lib/Solver/AlphaEquivalenceSolver.cpp b/lib/Solver/AlphaEquivalenceSolver.cpp
new file mode 100644
index 0000000000..4f29759cc3
--- /dev/null
+++ b/lib/Solver/AlphaEquivalenceSolver.cpp
@@ -0,0 +1,235 @@
+//===-- AlphaEquivalenceSolver.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/AlphaBuilder.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 AlphaEquivalenceSolver : public SolverImpl {
+private:
+  std::unique_ptr<Solver> solver;
+  ArrayCache &arrayCache;
+
+public:
+  AlphaEquivalenceSolver(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 changeVersion(const ValidityCore &validityCore,
+                             const ExprHashMap<ref<Expr>> &reverse);
+  const std::vector<const Array *>
+  changeVersion(const std::vector<const Array *> &objects,
+                const ArrayCache::ArrayHashMap<const Array *> &reverse);
+  Assignment
+  changeVersion(const Assignment &a,
+                const ArrayCache::ArrayHashMap<const Array *> &reverse);
+  ref<SolverResponse> changeVersion(ref<SolverResponse> res,
+                                    const AlphaBuilder &builder);
+  ref<SolverResponse> createAlphaVersion(ref<SolverResponse> res,
+                                         const AlphaBuilder &builder);
+};
+
+ValidityCore
+AlphaEquivalenceSolver::changeVersion(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 *> AlphaEquivalenceSolver::changeVersion(
+    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 AlphaEquivalenceSolver::changeVersion(
+    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 = changeVersion(objects, reverse);
+  return Assignment(objects, values);
+}
+
+ref<SolverResponse>
+AlphaEquivalenceSolver::changeVersion(ref<SolverResponse> res,
+                                      const AlphaBuilder &builder) {
+  ref<SolverResponse> reverseRes;
+  if (!isa<InvalidResponse>(res) && !isa<ValidResponse>(res)) {
+    return res;
+  }
+
+  if (isa<InvalidResponse>(res)) {
+    Assignment a = cast<InvalidResponse>(res)->initialValues();
+    a = changeVersion(a, builder.reverseAlphaArrayMap);
+    reverseRes = new InvalidResponse(a.bindings);
+  } else {
+    ValidityCore validityCore;
+    res->tryGetValidityCore(validityCore);
+    validityCore = changeVersion(validityCore, builder.reverseExprMap);
+    reverseRes = new ValidResponse(validityCore);
+  }
+  return reverseRes;
+}
+
+ref<SolverResponse>
+AlphaEquivalenceSolver::createAlphaVersion(ref<SolverResponse> res,
+                                           const AlphaBuilder &builder) {
+  if (!res || !isa<InvalidResponse>(res)) {
+    return res;
+  }
+
+  Assignment a = cast<InvalidResponse>(res)->initialValues();
+  changeVersion(a, builder.alphaArrayMap);
+  return new InvalidResponse(a.bindings);
+}
+
+bool AlphaEquivalenceSolver::computeValidity(const Query &query,
+                                             PartialValidity &result) {
+  AlphaBuilder builder(arrayCache);
+  constraints_ty alphaQuery = builder.visitConstraints(query.constraints.cs());
+  ref<Expr> alphaQueryExpr = builder.visitExpr(query.expr);
+  return solver->impl->computeValidity(
+      Query(ConstraintSet(alphaQuery, {}, {}), alphaQueryExpr, query.id),
+      result);
+}
+
+bool AlphaEquivalenceSolver::computeTruth(const Query &query, bool &isValid) {
+  AlphaBuilder builder(arrayCache);
+  constraints_ty alphaQuery = builder.visitConstraints(query.constraints.cs());
+  ref<Expr> alphaQueryExpr = builder.visitExpr(query.expr);
+  return solver->impl->computeTruth(
+      Query(ConstraintSet(alphaQuery, {}, {}), alphaQueryExpr, query.id),
+      isValid);
+}
+
+bool AlphaEquivalenceSolver::computeValue(const Query &query,
+                                          ref<Expr> &result) {
+  AlphaBuilder builder(arrayCache);
+  constraints_ty alphaQuery = builder.visitConstraints(query.constraints.cs());
+  ref<Expr> alphaQueryExpr = builder.visitExpr(query.expr);
+  return solver->impl->computeValue(
+      Query(ConstraintSet(alphaQuery, {}, {}), alphaQueryExpr, query.id),
+      result);
+}
+
+bool AlphaEquivalenceSolver::computeInitialValues(
+    const Query &query, const std::vector<const Array *> &objects,
+    std::vector<SparseStorage<unsigned char>> &values, bool &hasSolution) {
+  AlphaBuilder builder(arrayCache);
+  constraints_ty alphaQuery = builder.visitConstraints(query.constraints.cs());
+  ref<Expr> alphaQueryExpr = builder.visitExpr(query.expr);
+  const std::vector<const Array *> newObjects =
+      changeVersion(objects, builder.alphaArrayMap);
+
+  if (!solver->impl->computeInitialValues(
+          Query(ConstraintSet(alphaQuery, {}, {}), alphaQueryExpr, query.id),
+          newObjects, values, hasSolution)) {
+    return false;
+  }
+  return true;
+}
+
+bool AlphaEquivalenceSolver::check(const Query &query,
+                                   ref<SolverResponse> &result) {
+  AlphaBuilder builder(arrayCache);
+
+  constraints_ty alphaQuery = builder.visitConstraints(query.constraints.cs());
+  ref<Expr> alphaQueryExpr = builder.visitExpr(query.expr);
+  result = createAlphaVersion(result, builder);
+  if (!solver->impl->check(
+          Query(ConstraintSet(alphaQuery, {}, {}), alphaQueryExpr, query.id),
+          result)) {
+    return false;
+  }
+
+  result = changeVersion(result, builder);
+  return true;
+}
+
+bool AlphaEquivalenceSolver::computeValidityCore(const Query &query,
+                                                 ValidityCore &validityCore,
+                                                 bool &isValid) {
+  AlphaBuilder builder(arrayCache);
+
+  constraints_ty alphaQuery = builder.visitConstraints(query.constraints.cs());
+  ref<Expr> alphaQueryExpr = builder.visitExpr(query.expr);
+  if (!solver->impl->computeValidityCore(
+          Query(ConstraintSet(alphaQuery, {}, {}), alphaQueryExpr, query.id),
+          validityCore, isValid)) {
+    return false;
+  }
+  validityCore = changeVersion(validityCore, builder.reverseExprMap);
+  return true;
+}
+
+SolverImpl::SolverRunStatus AlphaEquivalenceSolver::getOperationStatusCode() {
+  return solver->impl->getOperationStatusCode();
+}
+
+char *AlphaEquivalenceSolver::getConstraintLog(const Query &query) {
+  return solver->impl->getConstraintLog(query);
+}
+
+void AlphaEquivalenceSolver::setCoreSolverTimeout(time::Span timeout) {
+  solver->impl->setCoreSolverTimeout(timeout);
+}
+
+void AlphaEquivalenceSolver::notifyStateTermination(std::uint32_t id) {
+  solver->impl->notifyStateTermination(id);
+}
+
+std::unique_ptr<Solver>
+klee::createAlphaEquivalenceSolver(std::unique_ptr<Solver> s,
+                                   ArrayCache &arrayCache) {
+  return std::make_unique<Solver>(
+      std::make_unique<AlphaEquivalenceSolver>(std::move(s), arrayCache));
+}
diff --git a/lib/Solver/CMakeLists.txt b/lib/Solver/CMakeLists.txt
index a1b15052bc..9ee7805b64 100644
--- a/lib/Solver/CMakeLists.txt
+++ b/lib/Solver/CMakeLists.txt
@@ -7,6 +7,7 @@
 #
 #===------------------------------------------------------------------------===#
 add_library(kleaverSolver
+  AlphaEquivalenceSolver.cpp
   AssignmentValidatingSolver.cpp
   CachingSolver.cpp
   CexCachingSolver.cpp
diff --git a/lib/Solver/CachingSolver.cpp b/lib/Solver/CachingSolver.cpp
index 75dbe1dfec..f01d760d32 100644
--- a/lib/Solver/CachingSolver.cpp
+++ b/lib/Solver/CachingSolver.cpp
@@ -36,12 +36,12 @@ class CachingSolver : public SolverImpl {
 
   struct CacheEntry {
     CacheEntry(const ConstraintSet &c, ref<Expr> q)
-        : constraints(c), query(q) {}
+        : constraints(c.cs()), query(q) {}
 
     CacheEntry(const CacheEntry &ce)
         : constraints(ce.constraints), query(ce.query) {}
 
-    ConstraintSet constraints;
+    constraints_ty constraints;
     ref<Expr> query;
 
     bool operator==(const CacheEntry &b) const {
@@ -53,7 +53,7 @@ class CachingSolver : public SolverImpl {
     unsigned operator()(const CacheEntry &ce) const {
       unsigned result = ce.query->hash();
 
-      for (auto const &constraint : ce.constraints.cs()) {
+      for (auto const &constraint : ce.constraints) {
         result ^= constraint->hash();
       }
 
diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp
index 20d35f8bd6..ddb5861c88 100644
--- a/lib/Solver/CexCachingSolver.cpp
+++ b/lib/Solver/CexCachingSolver.cpp
@@ -128,23 +128,12 @@ struct isInvalidResponse {
 };
 
 struct isValidOrSatisfyingResponse {
-  KeyType booleanKey;
-  KeyType nonBooleanKey;
-  isValidOrSatisfyingResponse(KeyType &_key) {
-    for (auto i : _key) {
-      if (i->getWidth() == Expr::Bool) {
-        booleanKey.insert(i);
-      } else {
-        nonBooleanKey.insert(i);
-      }
-    }
-  }
+  KeyType key;
+  isValidOrSatisfyingResponse(KeyType &_key) : key(_key) {}
 
   bool operator()(ref<SolverResponse> a) const {
-    return isa<ValidResponse>(a) ||
-           (isa<InvalidResponse>(a) &&
-            cast<InvalidResponse>(a)->satisfies(booleanKey) &&
-            cast<InvalidResponse>(a)->satisfiesNonBoolean(nonBooleanKey));
+    return isa<ValidResponse>(a) || (isa<InvalidResponse>(a) &&
+                                     cast<InvalidResponse>(a)->satisfies(key));
   }
 };
 
diff --git a/lib/Solver/ConstructSolverChain.cpp b/lib/Solver/ConstructSolverChain.cpp
index f8c9c8d522..c734db9c64 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 = createAlphaEquivalenceSolver(std::move(solver), arrayCache);
+
   if (UseIndependentSolver)
     solver = createIndependentSolver(std::move(solver));
 
diff --git a/lib/Solver/SolverCmdLine.cpp b/lib/Solver/SolverCmdLine.cpp
index 0f51525d53..4974abe1f8 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/test/Feature/ExprLogging.c b/test/Feature/ExprLogging.c
index 8109647a57..ca8d7a7913 100644
--- a/test/Feature/ExprLogging.c
+++ b/test/Feature/ExprLogging.c
@@ -1,7 +1,7 @@
 // RUN: %clang %s -emit-llvm -g %O0opt -c -o %t1.bc
 // We disable the cex-cache to eliminate nondeterminism across different solvers, in particular when counting the number of queries in the last two commands
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --use-cex-cache=false --use-query-log=all:kquery,all:smt2,solver:kquery,solver:smt2 --write-kqueries --write-cvcs --write-smt2s %t1.bc 2> %t2.log
+// RUN: %klee --output-dir=%t.klee-out --use-cex-cache=false --use-alpha-equivalence=false --use-query-log=all:kquery,all:smt2,solver:kquery,solver:smt2 --write-kqueries --write-cvcs --write-smt2s %t1.bc 2> %t2.log
 // RUN: %kleaver -print-ast %t.klee-out/all-queries.kquery > %t3.log
 // RUN: %kleaver -print-ast %t3.log > %t4.log
 // RUN: diff %t3.log %t4.log
diff --git a/test/Solver/AlphaEquivalenceCheck.c b/test/Solver/AlphaEquivalenceCheck.c
new file mode 100644
index 0000000000..160fdee515
--- /dev/null
+++ b/test/Solver/AlphaEquivalenceCheck.c
@@ -0,0 +1,19 @@
+// RUN: %clang %s -emit-llvm -g %O0opt -c -o %t1.bc
+// RUN: rm -rf %t1.klee-out
+// RUN: %klee --output-dir=%t1.klee-out --use-alpha-equivalence=false --use-cex-cache=true --use-query-log=solver:kquery,solver:smt2 --write-kqueries --write-cvcs --write-smt2s %t1.bc 2> %t2.log
+// RUN: rm -rf %t2.klee-out
+// RUN: %klee --output-dir=%t2.klee-out --use-alpha-equivalence=true --use-cex-cache=true --use-query-log=solver:kquery,solver:smt2 --write-kqueries --write-cvcs --write-smt2s %t1.bc 2> %t2.log
+// RUN: grep "^; Query" %t1.klee-out/solver-queries.smt2 | wc -l | grep -q 2
+// RUN: grep "^; Query" %t2.klee-out/solver-queries.smt2 | wc -l | grep -q 1
+
+#include "klee/klee.h"
+
+int main(int argc, char **argv) {
+  int a, b, c, d;
+  klee_make_symbolic(&a, sizeof(a), "a");
+  klee_make_symbolic(&b, sizeof(b), "b");
+  klee_make_symbolic(&c, sizeof(c), "c");
+  klee_make_symbolic(&d, sizeof(d), "d");
+  klee_assume(a + b == 0);
+  klee_assume(c + d == 0);
+}
diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp
index 5488055bd2..2deedb3c0b 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();