Index: include/clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h
===================================================================
--- /dev/null
+++ include/clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h
@@ -0,0 +1,70 @@
+//== SMTSort.h --------------------------------------------------*- C++ -*--==//
+//
+//                     The LLVM Compiler Infrastructure
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+//
+//  This file defines a SMT generic Sort API, which will be the base class
+//  for every SMT solver sort specific class.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSORT_H
+#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSORT_H
+
+#include "clang/StaticAnalyzer/Core/PathSensitive/SMTContext.h"
+
+namespace clang {
+namespace ento {
+
+class SMTSort {
+public:
+  SMTSort(SMTContext &C) : Context(C) {}
+  virtual ~SMTSort() = default;
+
+  virtual bool isBitvectorSort() const { return isBitvectorSortImpl(); }
+  virtual bool isFloatSort() const { return isFloatSortImpl(); }
+  virtual bool isBooleanSort() const { return isBooleanSortImpl(); }
+
+  virtual unsigned getBitvectorSortSize() const {
+    assert(isBitvectorSort() && "Not a bitvector sort!");
+    unsigned Size = getBitvectorSortSizeImpl();
+    assert(Size && "Size is zero!");
+    return Size;
+  };
+
+  virtual unsigned getFloatSortSize() const {
+    assert(isFloatSort() && "Not a floating-point sort!");
+    unsigned Size = getFloatSortSizeImpl();
+    assert(Size && "Size is zero!");
+    return Size;
+  };
+
+  friend bool operator==(SMTSort const &LHS, SMTSort const &RHS) {
+    return LHS.equal_to(RHS);
+  }
+
+  virtual void print(raw_ostream &OS) const {};
+
+  LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
+
+protected:
+  virtual bool equal_to(SMTSort const &other) const { return false; }
+
+  virtual bool isBitvectorSortImpl() const { return false; }
+  virtual bool isFloatSortImpl() const { return false; }
+  virtual bool isBooleanSortImpl() const { return false; }
+
+  virtual unsigned getBitvectorSortSizeImpl() const { return 0; }
+  virtual unsigned getFloatSortSizeImpl() const { return 0; }
+
+  SMTContext &Context;
+};
+
+} // namespace ento
+} // namespace clang
+
+#endif
Index: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
===================================================================
--- lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
+++ lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
@@ -12,6 +12,7 @@
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/SMTContext.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h"
 
 #include "clang/Config/config.h"
 
@@ -84,27 +85,27 @@
   }
 }; // end class Z3Context
 
-class Z3Sort {
-  friend class Z3Expr;
-  friend class Z3Solver;
+static Z3Context &toZ3Context(SMTContext &C) {
+  return static_cast<Z3Context &>(C);
+}
 
-  Z3Context &Context;
+class Z3Sort : public SMTSort {
+  friend class Z3Solver;
 
   Z3_sort Sort;
 
-  Z3Sort(Z3Context &C, Z3_sort ZS) : Context(C), Sort(ZS) {
-    assert(C.Context != nullptr);
-    Z3_inc_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort));
+  Z3Sort(SMTContext &C, Z3_sort ZS) : SMTSort(C), Sort(ZS) {
+    Z3_inc_ref(toZ3Context(Context).Context, reinterpret_cast<Z3_ast>(Sort));
   }
 
 public:
   /// Override implicit copy constructor for correct reference counting.
-  Z3Sort(const Z3Sort &Copy) : Context(Copy.Context), Sort(Copy.Sort) {
-    Z3_inc_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort));
+  Z3Sort(const Z3Sort &Copy) : SMTSort(Copy.Context), Sort(Copy.Sort) {
+    Z3_inc_ref(toZ3Context(Context).Context, reinterpret_cast<Z3_ast>(Sort));
   }
 
   /// Provide move constructor
-  Z3Sort(Z3Sort &&Move) : Context(Move.Context), Sort(nullptr) {
+  Z3Sort(Z3Sort &&Move) : SMTSort(Move.Context), Sort(nullptr) {
     *this = std::move(Move);
   }
 
@@ -112,7 +113,8 @@
   Z3Sort &operator=(Z3Sort &&Move) {
     if (this != &Move) {
       if (Sort)
-        Z3_dec_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort));
+        Z3_dec_ref(toZ3Context(Context).Context,
+                   reinterpret_cast<Z3_ast>(Sort));
       Sort = Move.Sort;
       Move.Sort = nullptr;
     }
@@ -121,41 +123,48 @@
 
   ~Z3Sort() {
     if (Sort)
-      Z3_dec_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort));
+      Z3_dec_ref(toZ3Context(Context).Context, reinterpret_cast<Z3_ast>(Sort));
+  }
+
+  bool isBitvectorSortImpl() const override {
+    return (Z3_get_sort_kind(toZ3Context(Context).Context, Sort) == Z3_BV_SORT);
+  }
+
+  bool isFloatSortImpl() const override {
+    return (Z3_get_sort_kind(toZ3Context(Context).Context, Sort) ==
+            Z3_FLOATING_POINT_SORT);
   }
 
-  Z3_sort_kind getSortKind() const {
-    return Z3_get_sort_kind(Context.Context, Sort);
+  bool isBooleanSortImpl() const override {
+    return (Z3_get_sort_kind(toZ3Context(Context).Context, Sort) ==
+            Z3_BOOL_SORT);
   }
 
-  unsigned getBitvectorSortSize() const {
-    assert(getSortKind() == Z3_BV_SORT && "Not a bitvector sort!");
-    return Z3_get_bv_sort_size(Context.Context, Sort);
+  unsigned getBitvectorSortSizeImpl() const override {
+    return Z3_get_bv_sort_size(toZ3Context(Context).Context, Sort);
   }
 
-  unsigned getFloatSortSize() const {
-    assert(getSortKind() == Z3_FLOATING_POINT_SORT &&
-           "Not a floating-point sort!");
-    return Z3_fpa_get_ebits(Context.Context, Sort) +
-           Z3_fpa_get_sbits(Context.Context, Sort);
+  unsigned getFloatSortSizeImpl() const override {
+    return Z3_fpa_get_ebits(toZ3Context(Context).Context, Sort) +
+           Z3_fpa_get_sbits(toZ3Context(Context).Context, Sort);
   }
 
-  bool operator==(const Z3Sort &Other) const {
-    return Z3_is_eq_sort(Context.Context, Sort, Other.Sort);
+  bool equal_to(SMTSort const &Other) const override {
+    return Z3_is_eq_sort(toZ3Context(Context).Context, Sort,
+                         static_cast<const Z3Sort *>(&Other)->Sort);
   }
 
   Z3Sort &operator=(const Z3Sort &Move) {
-    Z3_inc_ref(Context.Context, reinterpret_cast<Z3_ast>(Move.Sort));
-    Z3_dec_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort));
+    Z3_inc_ref(toZ3Context(Context).Context,
+               reinterpret_cast<Z3_ast>(Move.Sort));
+    Z3_dec_ref(toZ3Context(Context).Context, reinterpret_cast<Z3_ast>(Sort));
     Sort = Move.Sort;
     return *this;
   }
 
-  void print(raw_ostream &OS) const {
-    OS << Z3_sort_to_string(Context.Context, Sort);
+  void print(raw_ostream &OS) const override {
+    OS << Z3_sort_to_string(toZ3Context(Context).Context, Sort);
   }
-
-  LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
 }; // end class Z3Sort
 
 class Z3Expr {
@@ -804,8 +813,7 @@
   /// Construct an APFloat from a Z3Expr, given the AST representation
   bool toAPFloat(const Z3Sort &Sort, const Z3_ast &AST, llvm::APFloat &Float,
                  bool useSemantics = true) {
-    assert(Sort.getSortKind() == Z3_FLOATING_POINT_SORT &&
-           "Unsupported sort to floating-point!");
+    assert(Sort.isFloatSort() && "Unsupported sort to floating-point!");
 
     llvm::APSInt Int(Sort.getFloatSortSize(), true);
     const llvm::fltSemantics &Semantics =
@@ -828,10 +836,7 @@
   /// Construct an APSInt from a Z3Expr, given the AST representation
   bool toAPSInt(const Z3Sort &Sort, const Z3_ast &AST, llvm::APSInt &Int,
                 bool useSemantics = true) {
-    switch (Sort.getSortKind()) {
-    default:
-      llvm_unreachable("Unsupported sort to integer!");
-    case Z3_BV_SORT: {
+    if (Sort.isBitvectorSort()) {
       if (useSemantics && Int.getBitWidth() != Sort.getBitvectorSortSize()) {
         assert(false && "Bitvector types don't match!");
         return false;
@@ -859,11 +864,13 @@
       }
       return true;
     }
-    case Z3_BOOL_SORT:
+
+    if (Sort.isBooleanSort()) {
       if (useSemantics && Int.getBitWidth() < 1) {
         assert(false && "Boolean type doesn't match!");
         return false;
       }
+
       Int = llvm::APSInt(
           llvm::APInt(Int.getBitWidth(),
                       Z3_get_bool_value(Context.Context, AST) == Z3_L_TRUE ? 1
@@ -871,6 +878,8 @@
           Int.isUnsigned());
       return true;
     }
+
+    llvm_unreachable("Unsupported sort to integer!");
   }
 
   /// Given an expression and a model, extract the value of this operand in