[analyzer] Implemented SMT generic API

[mikhail.ramalho]

Summary

Created new SMT generic API.

Small changes to Z3ConstraintManager because of the new generic objects (SMTSort and SMTExpr) returned by SMTSolver.

[mikhail.ramalho]

Removed the changes to SMTConstraintManager for now.

[mikhail.ramalho]

Update API to handle shared pointer to SMTExprs/SMTSorts objects instead of the actual objects.

[george.karpenkov]

LGTM provided the semantics of the method in question is explained in comments here.

lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp

802

I'm quite confused about this method, is it only used in pure-z3-solving-mode?

[mikhail.ramalho]

Moved conversion methods to SMTSolver.

[mikhail.ramalho]

Create new method:

virtual SMTExprRef newExprRef(const SMTExpr &E) const = 0;

that creates and returns a shared pointer containing the SMTExpr object. It'll be useful in the future.

include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h

+//== SMTSolver.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 Solver API, which will be the base class
+//  for every SMT solver specific class.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSOLVER_H
+#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSOLVER_H
+
+#include "clang/StaticAnalyzer/Core/PathSensitive/SMTContext.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h"
+
+namespace clang {
+namespace ento {
+
+using SMTExprRef = std::shared_ptr<SMTExpr>;
+using SMTSortRef = std::shared_ptr<SMTSort>;
+
+class SMTSolver {
+public:
+  SMTSolver() = default;
+  virtual ~SMTSolver() = default;
+
+  LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
+
+  // Return a boolean sort.
+  virtual SMTSortRef getBoolSort() = 0;
+
+  // Return an appropriate bitvector sort for the given bitwidth.
+  virtual SMTSortRef getBitvectorSort(const unsigned BitWidth) = 0;
+
+  // Return a floating-point sort of width 16
+  virtual SMTSortRef getFloat16Sort() = 0;
+
+  // Return a floating-point sort of width 32
+  virtual SMTSortRef getFloat32Sort() = 0;
+
+  // Return a floating-point sort of width 64
+  virtual SMTSortRef getFloat64Sort() = 0;
+
+  // Return a floating-point sort of width 128
+  virtual SMTSortRef getFloat128Sort() = 0;
+
+  // Return an appropriate sort for the given AST.
+  virtual SMTSortRef getSort(const SMTExprRef &AST) = 0;
+
+  /// Given a constraint, add it to the solver
+  virtual void addConstraint(const SMTExprRef &Exp) = 0;
+
+  /// Create a bitvector addition operation
+  virtual SMTExprRef mkBVAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+  /// Create a bitvector subtraction operation
+  virtual SMTExprRef mkBVSub(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+  /// Create a bitvector multiplication operation
+  virtual SMTExprRef mkBVMul(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+  /// Create a bitvector signed modulus operation
+  virtual SMTExprRef mkBVSRem(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+  /// Create a bitvector unsigned modulus operation
+  virtual SMTExprRef mkBVURem(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+  /// Create a bitvector signed division operation
+  virtual SMTExprRef mkBVSDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+  /// Create a bitvector unsigned division operation
+  virtual SMTExprRef mkBVUDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+  /// Create a bitvector logical shift left operation
+  virtual SMTExprRef mkBVShl(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+  /// Create a bitvector arithmetic shift right operation
+  virtual SMTExprRef mkBVAshr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+  /// Create a bitvector logical shift right operation
+  virtual SMTExprRef mkBVLshr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+  /// Create a bitvector negation operation
+  virtual SMTExprRef mkBVNeg(const SMTExprRef &Exp) = 0;
+
+  /// Create a bitvector not operation
+  virtual SMTExprRef mkBVNot(const SMTExprRef &Exp) = 0;
+
+  /// Create a bitvector xor operation
+  virtual SMTExprRef mkBVXor(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+  /// Create a bitvector or operation
+  virtual SMTExprRef mkBVOr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+  /// Create a bitvector and operation
+  virtual SMTExprRef mkBVAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+  /// Create a bitvector unsigned less-than operation
+  virtual SMTExprRef mkBVUlt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+  /// Create a bitvector signed less-than operation
+  virtual SMTExprRef mkBVSlt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+  /// Create a bitvector unsigned greater-than operation
+  virtual SMTExprRef mkBVUgt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+  /// Create a bitvector signed greater-than operation
+  virtual SMTExprRef mkBVSgt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+  /// Create a bitvector unsigned less-equal-than operation
+  virtual SMTExprRef mkBVUle(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+  /// Create a bitvector signed less-equal-than operation
+  virtual SMTExprRef mkBVSle(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+  /// Create a bitvector unsigned greater-equal-than operation
+  virtual SMTExprRef mkBVUge(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+  /// Create a bitvector signed greater-equal-than operation
+  virtual SMTExprRef mkBVSge(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+  /// Create a boolean not operation
+  virtual SMTExprRef mkNot(const SMTExprRef &Exp) = 0;
+
+  /// Create a bitvector equality operation
+  virtual SMTExprRef mkEqual(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+  virtual SMTExprRef mkAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+  virtual SMTExprRef mkOr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+  virtual SMTExprRef mkIte(const SMTExprRef &Cond, const SMTExprRef &T,
+                           const SMTExprRef &F) = 0;
+
+  virtual SMTExprRef mkSignExt(unsigned i, const SMTExprRef &Exp) = 0;
+
+  virtual SMTExprRef mkZeroExt(unsigned i, const SMTExprRef &Exp) = 0;
+
+  virtual SMTExprRef mkExtract(unsigned High, unsigned Low,
+                               const SMTExprRef &Exp) = 0;
+
+  virtual SMTExprRef mkConcat(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+  virtual SMTExprRef mkFPNeg(const SMTExprRef &Exp) = 0;
+
+  virtual SMTExprRef mkFPIsInfinite(const SMTExprRef &Exp) = 0;
+
+  virtual SMTExprRef mkFPIsNaN(const SMTExprRef &Exp) = 0;
+
+  virtual SMTExprRef mkFPIsNormal(const SMTExprRef &Exp) = 0;
+
+  virtual SMTExprRef mkFPIsZero(const SMTExprRef &Exp) = 0;
+
+  virtual SMTExprRef mkFPMul(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+  virtual SMTExprRef mkFPDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+  virtual SMTExprRef mkFPRem(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+  virtual SMTExprRef mkFPAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+  virtual SMTExprRef mkFPSub(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+  virtual SMTExprRef mkFPLt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+  virtual SMTExprRef mkFPGt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+  virtual SMTExprRef mkFPLe(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+  virtual SMTExprRef mkFPGe(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+  virtual SMTExprRef mkFPEqual(const SMTExprRef &LHS,
+                               const SMTExprRef &RHS) = 0;
+
+  virtual SMTExprRef mkFPtoFP(const SMTExprRef &From, const SMTSortRef &To) = 0;
+
+  virtual SMTExprRef mkFPtoSBV(const SMTExprRef &From,
+                               const SMTSortRef &To) = 0;
+
+  virtual SMTExprRef mkFPtoUBV(const SMTExprRef &From,
+                               const SMTSortRef &To) = 0;
+
+  virtual SMTExprRef mkSBVtoFP(const SMTExprRef &From, unsigned ToWidth) = 0;
+
+  virtual SMTExprRef mkUBVtoFP(const SMTExprRef &From, unsigned ToWidth) = 0;
+
+  virtual SMTExprRef mkSymbol(const char *Name, SMTSortRef Sort) = 0;
+
+  // Return an appropriate floating-point rounding mode.
+  virtual SMTExprRef getFloatRoundingMode() = 0;
+
+  virtual const llvm::APSInt getBitvector(const SMTExprRef &Exp) = 0;
+
+  virtual bool getBoolean(const SMTExprRef &Exp) = 0;
+
+  /// Construct a const SMTExprRef &From a boolean.
+  virtual SMTExprRef mkBoolean(const bool b) = 0;
+
+  /// Construct a const SMTExprRef &From a finite APFloat.
+  virtual SMTExprRef mkFloat(const llvm::APFloat Float) = 0;
+
+  /// Construct a const SMTExprRef &From an APSInt.
+  virtual SMTExprRef mkBitvector(const llvm::APSInt Int, unsigned BitWidth) = 0;
+
+  SMTExprRef mkBitvector(const llvm::APSInt Int) {
+    return mkBitvector(Int, Int.getBitWidth());
+  }
+
+  /// Given an expression, extract the value of this operand in the model.
+  virtual bool getInterpretation(const SMTExprRef &Exp, llvm::APSInt &Int) = 0;
+
+  /// Given an expression extract the value of this operand in the model.
+  virtual bool getInterpretation(const SMTExprRef &Exp,
+                                 llvm::APFloat &Float) = 0;
+
+  /// Construct a const SMTExprRef &From a SymbolData, given a SMT_context.
+  virtual SMTExprRef fromData(const SymbolID ID, const QualType &Ty,
+                              uint64_t BitWidth) = 0;
+
+  /// Check if the constraints are satisfiable
+  virtual ConditionTruthVal check() const = 0;
+
+  /// Push the current solver state
+  virtual void push() = 0;
+
+  /// Pop the previous solver state
+  virtual void pop(unsigned NumStates = 1) = 0;
+
+  /// Reset the solver and remove all constraints.
+  virtual void reset() const = 0;
+
+  virtual void print(raw_ostream &OS) const = 0;
+};
+
+} // namespace ento
+} // namespace clang
+
+#endif

lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp

 //== Z3ConstraintManager.cpp --------------------------------*- C++ -*--==//
 //
 //                     The LLVM Compiler Infrastructure
 //
 // This file is distributed under the University of Illinois Open Source
 // License. See LICENSE.TXT for details.
 //
 //===----------------------------------------------------------------------===//
 
 #include "clang/Basic/TargetInfo.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
 #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/SMTExpr.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h"
 
 #include "clang/Config/config.h"
 
 using namespace clang;
 using namespace ento;
 
 #if CLANG_ANALYZER_WITH_Z3
struct ProgramStateTrait<ConstraintZ3>
   }
 };
 } // end namespace ento
 } // end namespace clang
 
 namespace {
 
 class Z3Expr;
+class Z3Sort;
 static const Z3Expr &toZ3Expr(const SMTExpr &E);
+static const Z3Sort &toZ3Sort(const SMTSort &S);
 
 class Z3Config {
   friend class Z3Context;
 
   Z3_config Config;
 
 public:
   Z3Config() : Config(Z3_mk_config()) {
static Z3Context &toZ3Context(SMTContext &C) {
   return static_cast<Z3Context &>(C);
 }
 
 class Z3Sort : public SMTSort {
   friend class Z3Solver;
 
   Z3_sort Sort;
 
+public:
   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) : SMTSort(Copy.Context), Sort(Copy.Sort) {
     Z3_inc_ref(toZ3Context(Context).Context, reinterpret_cast<Z3_ast>(Sort));
   }
 
   /// Provide move constructor
   Z3Sort(Z3Sort &&Move) : SMTSort(Move.Context), Sort(nullptr) {
     *this = std::move(Move);
Z3Sort &operator=(const Z3Sort &Move) {
     return *this;
   }
 
   void print(raw_ostream &OS) const override {
     OS << Z3_sort_to_string(toZ3Context(Context).Context, Sort);
   }
 }; // end class Z3Sort
 
+static const Z3Sort &toZ3Sort(const SMTSort &S) {
+  return static_cast<const Z3Sort &>(S);
+}
+
 class Z3Expr : public SMTExpr {
   friend class Z3Solver;
 
   Z3_ast AST;
 
+public:
   Z3Expr(SMTContext &C, Z3_ast ZA) : SMTExpr(C), AST(ZA) {
     Z3_inc_ref(toZ3Context(Context).Context, AST);
   }
 
-public:
   /// Override implicit copy constructor for correct reference counting.
   Z3Expr(const Z3Expr &Copy) : SMTExpr(Copy.Context), AST(Copy.AST) {
     Z3_inc_ref(toZ3Context(Context).Context, AST);
   }
 
   /// Provide move constructor
   Z3Expr(Z3Expr &&Move) : SMTExpr(Move.Context), AST(nullptr) {
     *this = std::move(Move);
return (llvm::APFloat::semanticsPrecision(LHS) ==
          (llvm::APFloat::semanticsMinExponent(LHS) ==
           llvm::APFloat::semanticsMinExponent(RHS)) &&
          (llvm::APFloat::semanticsMaxExponent(LHS) ==
           llvm::APFloat::semanticsMaxExponent(RHS)) &&
          (llvm::APFloat::semanticsSizeInBits(LHS) ==
           llvm::APFloat::semanticsSizeInBits(RHS));
 }
 
-class Z3Solver {
+class Z3Solver : public SMTSolver {
   friend class Z3ConstraintManager;
 
   Z3Context Context;
 
   Z3_solver Solver;
 
-  Z3Solver() : Solver(Z3_mk_simple_solver(Context.Context)) {
+  Z3Solver() : SMTSolver(), Solver(Z3_mk_simple_solver(Context.Context)) {
     Z3_solver_inc_ref(Context.Context, Solver);
   }
 
 public:
   /// Override implicit copy constructor for correct reference counting.
-  Z3Solver(const Z3Solver &Copy) : Context(Copy.Context), Solver(Copy.Solver) {
+  Z3Solver(const Z3Solver &Copy)
+      : SMTSolver(), Context(Copy.Context), Solver(Copy.Solver) {
     Z3_solver_inc_ref(Context.Context, Solver);
   }
 
   /// Provide move constructor
-  Z3Solver(Z3Solver &&Move) : Context(Move.Context), Solver(nullptr) {
+  Z3Solver(Z3Solver &&Move)
+      : SMTSolver(), Context(Move.Context), Solver(nullptr) {
     *this = std::move(Move);
   }
 
   /// Provide move assignment constructor
   Z3Solver &operator=(Z3Solver &&Move) {
     if (this != &Move) {
       if (Solver)
         Z3_solver_dec_ref(Context.Context, Solver);
       Solver = Move.Solver;
       Move.Solver = nullptr;
     }
     return *this;
   }
 
   ~Z3Solver() {
     if (Solver)
       Z3_solver_dec_ref(Context.Context, Solver);
   }
 
-  /// Given a constraint, add it to the solver
-  void addConstraint(const Z3Expr &Exp) {
-    Z3_solver_assert(Context.Context, Solver, Exp.AST);
+  void addConstraint(const SMTExprRef &Exp) override {
+    Z3_solver_assert(Context.Context, Solver, toZ3Expr(*Exp).AST);
   }
 
-  // Return a boolean sort.
-  Z3Sort getBoolSort() {
-    return Z3Sort(Context, Z3_mk_bool_sort(Context.Context));
+  SMTSortRef getBoolSort() override {
+    return std::make_shared<Z3Sort>(Context, Z3_mk_bool_sort(Context.Context));
   }
 
-  // Return an appropriate bitvector sort for the given bitwidth.
-  Z3Sort getBitvectorSort(unsigned BitWidth) {
-    return Z3Sort(Context, Z3_mk_bv_sort(Context.Context, BitWidth));
+  SMTSortRef getBitvectorSort(unsigned BitWidth) override {
+    return std::make_shared<Z3Sort>(Context,
+                                    Z3_mk_bv_sort(Context.Context, BitWidth));
   }
 
   // Return an appropriate floating-point sort for the given bitwidth.
-  Z3Sort getFloatSort(unsigned BitWidth) {
-    Z3_sort Sort;
-
+  SMTSortRef getFloatSort(unsigned BitWidth) {
     switch (BitWidth) {
-    default:
-      llvm_unreachable("Unsupported floating-point bitwidth!");
-      break;
     case 16:
-      Sort = Z3_mk_fpa_sort_16(Context.Context);
-      break;
+      return getFloat16Sort();
     case 32:
-      Sort = Z3_mk_fpa_sort_32(Context.Context);
-      break;
+      return getFloat32Sort();
     case 64:
-      Sort = Z3_mk_fpa_sort_64(Context.Context);
-      break;
+      return getFloat64Sort();
     case 128:
-      Sort = Z3_mk_fpa_sort_128(Context.Context);
-      break;
+      return getFloat128Sort();
+    default:;
     }
-    return Z3Sort(Context, Sort);
+    llvm_unreachable("Unsupported floating-point bitwidth!");
   }
 
   // Return an appropriate sort, given a QualType
-  Z3Sort MkSort(const QualType &Ty, unsigned BitWidth) {
+  SMTSortRef mkSort(const QualType &Ty, unsigned BitWidth) {
     if (Ty->isBooleanType())
       return getBoolSort();
 
     if (Ty->isRealFloatingType())
       return getFloatSort(BitWidth);
 
     return getBitvectorSort(BitWidth);
   }
 
-  // Return an appropriate sort for the given AST.
-  Z3Sort getSort(Z3_ast AST) {
-    return Z3Sort(Context, Z3_get_sort(Context.Context, AST));
+  SMTSortRef getSort(const SMTExprRef &Exp) override {
+    return std::make_shared<Z3Sort>(
+        Context, Z3_get_sort(Context.Context, toZ3Expr(*Exp).AST));
+  }
+
+  SMTSortRef getFloat16Sort() override {
+    return std::make_shared<Z3Sort>(Context,
+                                    Z3_mk_fpa_sort_16(Context.Context));
+  }
+
+  SMTSortRef getFloat32Sort() override {
+    return std::make_shared<Z3Sort>(Context,
+                                    Z3_mk_fpa_sort_32(Context.Context));
+  }
+
+  SMTSortRef getFloat64Sort() override {
+    return std::make_shared<Z3Sort>(Context,
+                                    Z3_mk_fpa_sort_64(Context.Context));
+  }
+
+  SMTSortRef getFloat128Sort() override {
+    return std::make_shared<Z3Sort>(Context,
+                                    Z3_mk_fpa_sort_128(Context.Context));
+  }
+
+  SMTExprRef mkBVNeg(const SMTExprRef &Exp) override {
+    return std::make_shared<Z3Expr>(
+        Context, Z3_mk_bvneg(Context.Context, toZ3Expr(*Exp).AST));
+  }
+
+  SMTExprRef mkBVNot(const SMTExprRef &Exp) override {
+    return std::make_shared<Z3Expr>(
+        Context, Z3_mk_bvnot(Context.Context, toZ3Expr(*Exp).AST));
+  }
+
+  SMTExprRef mkNot(const SMTExprRef &Exp) override {
+    return std::make_shared<Z3Expr>(
+        Context, Z3_mk_not(Context.Context, toZ3Expr(*Exp).AST));
+  }
+
+  SMTExprRef mkBVAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
+    return std::make_shared<Z3Expr>(
+        Context,
+        Z3_mk_bvadd(Context.Context, toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST));
+  }
+
+  SMTExprRef mkBVSub(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
+    return std::make_shared<Z3Expr>(
+        Context,
+        Z3_mk_bvsub(Context.Context, toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST));
+  }
+
+  SMTExprRef mkBVMul(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
+    return std::make_shared<Z3Expr>(
+        Context,
+        Z3_mk_bvmul(Context.Context, toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST));
+  }
+
+  SMTExprRef mkBVSRem(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
+    return std::make_shared<Z3Expr>(
+        Context,
+        Z3_mk_bvsrem(Context.Context, toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST));
+  }
+
+  SMTExprRef mkBVURem(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
+    return std::make_shared<Z3Expr>(
+        Context,
+        Z3_mk_bvurem(Context.Context, toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST));
+  }
+
+  SMTExprRef mkBVSDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
+    return std::make_shared<Z3Expr>(
+        Context,
+        Z3_mk_bvsdiv(Context.Context, toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST));
+  }
+
+  SMTExprRef mkBVUDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
+    return std::make_shared<Z3Expr>(
+        Context,
+        Z3_mk_bvudiv(Context.Context, toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST));
+  }
+
+  SMTExprRef mkBVShl(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
+    return std::make_shared<Z3Expr>(
+        Context,
+        Z3_mk_bvshl(Context.Context, toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST));
+  }
+
+  SMTExprRef mkBVAshr(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
+    return std::make_shared<Z3Expr>(
+        Context,
+        Z3_mk_bvashr(Context.Context, toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST));
+  }
+
+  SMTExprRef mkBVLshr(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
+    return std::make_shared<Z3Expr>(
+        Context,
+        Z3_mk_bvlshr(Context.Context, toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST));
+  }
+
+  SMTExprRef mkBVXor(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
+    return std::make_shared<Z3Expr>(
+        Context,
+        Z3_mk_bvxor(Context.Context, toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST));
+  }
+
+  SMTExprRef mkBVOr(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
+    return std::make_shared<Z3Expr>(
+        Context,
+        Z3_mk_bvor(Context.Context, toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST));
+  }
+
+  SMTExprRef mkBVAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
+    return std::make_shared<Z3Expr>(
+        Context,
+        Z3_mk_bvand(Context.Context, toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST));
+  }
+
+  SMTExprRef mkBVUlt(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
+    return std::make_shared<Z3Expr>(
+        Context,
+        Z3_mk_bvult(Context.Context, toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST));
+  }
+
+  SMTExprRef mkBVSlt(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
+    return std::make_shared<Z3Expr>(
+        Context,
+        Z3_mk_bvslt(Context.Context, toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST));
+  }
+
+  SMTExprRef mkBVUgt(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
+    return std::make_shared<Z3Expr>(
+        Context,
+        Z3_mk_bvugt(Context.Context, toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST));
+  }
+
+  SMTExprRef mkBVSgt(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
+    return std::make_shared<Z3Expr>(
+        Context,
+        Z3_mk_bvsgt(Context.Context, toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST));
+  }
+
+  SMTExprRef mkBVUle(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
+    return std::make_shared<Z3Expr>(
+        Context,
+        Z3_mk_bvule(Context.Context, toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST));
+  }
+
+  SMTExprRef mkBVSle(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
+    return std::make_shared<Z3Expr>(
+        Context,
+        Z3_mk_bvsle(Context.Context, toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST));
+  }
+
+  SMTExprRef mkBVUge(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
+    return std::make_shared<Z3Expr>(
+        Context,
+        Z3_mk_bvuge(Context.Context, toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST));
+  }
+
+  SMTExprRef mkBVSge(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
+    return std::make_shared<Z3Expr>(
+        Context,
+        Z3_mk_bvsge(Context.Context, toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST));
+  }
+
+  SMTExprRef mkAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
+    Z3_ast Args[2] = {toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST};
+    return std::make_shared<Z3Expr>(Context,
+                                    Z3_mk_and(Context.Context, 2, Args));
+  }
+
+  SMTExprRef mkOr(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
+    Z3_ast Args[2] = {toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST};
+    return std::make_shared<Z3Expr>(Context,
+                                    Z3_mk_or(Context.Context, 2, Args));
+  }
+
+  SMTExprRef mkEqual(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
+    return std::make_shared<Z3Expr>(
+        Context,
+        Z3_mk_eq(Context.Context, toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST));
+  }
+
+  SMTExprRef mkFPNeg(const SMTExprRef &Exp) override {
+    return std::make_shared<Z3Expr>(
+        Context, Z3_mk_fpa_neg(Context.Context, toZ3Expr(*Exp).AST));
+  }
+
+  SMTExprRef mkFPIsInfinite(const SMTExprRef &Exp) override {
+    return std::make_shared<Z3Expr>(
+        Context, Z3_mk_fpa_is_infinite(Context.Context, toZ3Expr(*Exp).AST));
+  }
+
+  SMTExprRef mkFPIsNaN(const SMTExprRef &Exp) override {
+    return std::make_shared<Z3Expr>(
+        Context, Z3_mk_fpa_is_nan(Context.Context, toZ3Expr(*Exp).AST));
+  }
+
+  SMTExprRef mkFPIsNormal(const SMTExprRef &Exp) override {
+    return std::make_shared<Z3Expr>(
+        Context, Z3_mk_fpa_is_normal(Context.Context, toZ3Expr(*Exp).AST));
+  }
+
+  SMTExprRef mkFPIsZero(const SMTExprRef &Exp) override {
+    return std::make_shared<Z3Expr>(
+        Context, Z3_mk_fpa_is_zero(Context.Context, toZ3Expr(*Exp).AST));
+  }
+
+  SMTExprRef mkFPMul(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
+    SMTExprRef RoundingMode = getFloatRoundingMode();
+    return std::make_shared<Z3Expr>(
+        Context,
+        Z3_mk_fpa_mul(Context.Context, toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST,
+                      toZ3Expr(*RoundingMode).AST));
+  }
+
+  SMTExprRef mkFPDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
+    SMTExprRef RoundingMode = getFloatRoundingMode();
+    return std::make_shared<Z3Expr>(
+        Context,
+        Z3_mk_fpa_div(Context.Context, toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST,
+                      toZ3Expr(*RoundingMode).AST));
+  }
+
+  SMTExprRef mkFPRem(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
+    return std::make_shared<Z3Expr>(
+        Context,
+        Z3_mk_fpa_rem(Context.Context, toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST));
+  }
+
+  SMTExprRef mkFPAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
+    SMTExprRef RoundingMode = getFloatRoundingMode();
+    return std::make_shared<Z3Expr>(
+        Context,
+        Z3_mk_fpa_add(Context.Context, toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST,
+                      toZ3Expr(*RoundingMode).AST));
+  }
+
+  SMTExprRef mkFPSub(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
+    SMTExprRef RoundingMode = getFloatRoundingMode();
+    return std::make_shared<Z3Expr>(
+        Context,
+        Z3_mk_fpa_sub(Context.Context, toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST,
+                      toZ3Expr(*RoundingMode).AST));
+  }
+
+  SMTExprRef mkFPLt(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
+    return std::make_shared<Z3Expr>(
+        Context,
+        Z3_mk_fpa_lt(Context.Context, toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST));
+  }
+
+  SMTExprRef mkFPGt(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
+    return std::make_shared<Z3Expr>(
+        Context,
+        Z3_mk_fpa_gt(Context.Context, toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST));
+  }
+
+  SMTExprRef mkFPLe(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
+    return std::make_shared<Z3Expr>(
+        Context,
+        Z3_mk_fpa_leq(Context.Context, toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST));
+  }
+
+  SMTExprRef mkFPGe(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
+    return std::make_shared<Z3Expr>(
+        Context,
+        Z3_mk_fpa_geq(Context.Context, toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST));
+  }
+
+  SMTExprRef mkFPEqual(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
+    return std::make_shared<Z3Expr>(
+        Context,
+        Z3_mk_fpa_eq(Context.Context, toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST));
+  }
+
+  SMTExprRef mkIte(const SMTExprRef &Cond, const SMTExprRef &T,
+                   const SMTExprRef &F) override {
+    return std::make_shared<Z3Expr>(
+        Context, Z3_mk_ite(Context.Context, toZ3Expr(*Cond).AST,
+                           toZ3Expr(*T).AST, toZ3Expr(*F).AST));
+  }
+
+  SMTExprRef mkSignExt(unsigned i, const SMTExprRef &Exp) override {
+    return std::make_shared<Z3Expr>(
+        Context, Z3_mk_sign_ext(Context.Context, i, toZ3Expr(*Exp).AST));
+  }
+
+  SMTExprRef mkZeroExt(unsigned i, const SMTExprRef &Exp) override {
+    return std::make_shared<Z3Expr>(
+        Context, Z3_mk_zero_ext(Context.Context, i, toZ3Expr(*Exp).AST));
+  }
+
+  SMTExprRef mkExtract(unsigned High, unsigned Low,
+                       const SMTExprRef &Exp) override {
+    return std::make_shared<Z3Expr>(
+        Context, Z3_mk_extract(Context.Context, High, Low, toZ3Expr(*Exp).AST));
+  }
+
+  SMTExprRef mkConcat(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
+    return std::make_shared<Z3Expr>(
+        Context,
+        Z3_mk_concat(Context.Context, toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST));
+  }
+
+  SMTExprRef mkFPtoFP(const SMTExprRef &From, const SMTSortRef &To) override {
+    SMTExprRef RoundingMode = getFloatRoundingMode();
+    return std::make_shared<Z3Expr>(
+        Context,
+        Z3_mk_fpa_to_fp_float(Context.Context, toZ3Expr(*RoundingMode).AST,
+                              toZ3Expr(*From).AST, toZ3Sort(*To).Sort));
+  }
+
+  SMTExprRef mkFPtoSBV(const SMTExprRef &From, const SMTSortRef &To) override {
+    SMTExprRef RoundingMode = getFloatRoundingMode();
+    return std::make_shared<Z3Expr>(
+        Context,
+        Z3_mk_fpa_to_fp_signed(Context.Context, toZ3Expr(*RoundingMode).AST,
+                               toZ3Expr(*From).AST, toZ3Sort(*To).Sort));
+  }
+
+  SMTExprRef mkFPtoUBV(const SMTExprRef &From, const SMTSortRef &To) override {
+    SMTExprRef RoundingMode = getFloatRoundingMode();
+    return std::make_shared<Z3Expr>(
+        Context,
+        Z3_mk_fpa_to_fp_unsigned(Context.Context, toZ3Expr(*RoundingMode).AST,
+                                 toZ3Expr(*From).AST, toZ3Sort(*To).Sort));
+  }
+
+  SMTExprRef mkSBVtoFP(const SMTExprRef &From, unsigned ToWidth) override {
+    SMTExprRef RoundingMode = getFloatRoundingMode();
+    return std::make_shared<Z3Expr>(
+        Context, Z3_mk_fpa_to_sbv(Context.Context, toZ3Expr(*RoundingMode).AST,
+                                  toZ3Expr(*From).AST, ToWidth));
+  }
+
+  SMTExprRef mkUBVtoFP(const SMTExprRef &From, unsigned ToWidth) override {
+    SMTExprRef RoundingMode = getFloatRoundingMode();
+    return std::make_shared<Z3Expr>(
+        Context, Z3_mk_fpa_to_ubv(Context.Context, toZ3Expr(*RoundingMode).AST,
+                                  toZ3Expr(*From).AST, ToWidth));
+  }
+
+  SMTExprRef mkBoolean(const bool b) override {
+    return std::make_shared<Z3Expr>(Context, b ? Z3_mk_true(Context.Context)
+                                               : Z3_mk_false(Context.Context));
+  }
+
+  SMTExprRef mkBitvector(const llvm::APSInt Int, unsigned BitWidth) override {
+    const SMTSortRef Sort = getBitvectorSort(BitWidth);
+    return std::make_shared<Z3Expr>(
+        Context, Z3_mk_numeral(Context.Context, Int.toString(10).c_str(),
+                               toZ3Sort(*Sort).Sort));
+  }
+
+  SMTExprRef mkFloat(const llvm::APFloat Float) override {
+    SMTSortRef Sort =
+        getFloatSort(llvm::APFloat::semanticsSizeInBits(Float.getSemantics()));
+
+    llvm::APSInt Int = llvm::APSInt(Float.bitcastToAPInt(), false);
+    SMTExprRef Z3Int = mkBitvector(Int, Int.getBitWidth());
+    return std::make_shared<Z3Expr>(
+        Context, Z3_mk_fpa_to_fp_bv(Context.Context, toZ3Expr(*Z3Int).AST,
+                                    toZ3Sort(*Sort).Sort));
+  }
+
+  SMTExprRef mkSymbol(const char *Name, SMTSortRef Sort) override {
+    return std::make_shared<Z3Expr>(
+        Context,
+        Z3_mk_const(Context.Context, Z3_mk_string_symbol(Context.Context, Name),
+                    toZ3Sort(*Sort).Sort));
+  }
+
+  const llvm::APSInt getBitvector(const SMTExprRef &Exp) override {
+    // FIXME: this returns a string and the bitWidth is overridden
+    return llvm::APSInt(
+        Z3_get_numeral_string(Context.Context, toZ3Expr(*Exp).AST));
+  }
+
+  bool getBoolean(const SMTExprRef &Exp) override {
+    return Z3_get_bool_value(Context.Context, toZ3Expr(*Exp).AST) == Z3_L_TRUE;
   }
 
   /// Given a program state, construct the logical conjunction and add it to
   /// the solver
   void addStateConstraints(ProgramStateRef State) {
     // TODO: Don't add all the constraints, only the relevant ones
     ConstraintZ3Ty CZ = State->get<ConstraintZ3>();
     ConstraintZ3Ty::iterator I = CZ.begin(), IE = CZ.end();
 
     // Construct the logical AND of all the constraints
     if (I != IE) {
-      std::vector<Z3_ast> ASTs;
+      std::vector<SMTExprRef> ASTs;
 
       while (I != IE)
-        ASTs.push_back(I++->second.AST);
+        ASTs.push_back(std::make_shared<Z3Expr>(I++->second));
 
-      Z3Expr Conj = fromNBinOp(BO_LAnd, ASTs);
-      addConstraint(Conj);
+      addConstraint(fromNBinOp(BO_LAnd, ASTs));
     }
   }
 
   // Return an appropriate floating-point rounding mode.
-  Z3Expr getFloatRoundingMode() {
+  SMTExprRef getFloatRoundingMode() override {
     // TODO: Don't assume nearest ties to even rounding mode
-    return Z3Expr(Context, Z3_mk_fpa_rne(Context.Context));
+    return std::make_shared<Z3Expr>(Context, Z3_mk_fpa_rne(Context.Context));
   }
 
   /// Construct a Z3Expr from a unary operator, given a Z3_context.
-  Z3Expr fromUnOp(const UnaryOperator::Opcode Op, const Z3Expr &Exp) {
-    Z3_ast AST;
-
+  SMTExprRef fromUnOp(const UnaryOperator::Opcode Op, const SMTExprRef &Exp) {
     switch (Op) {
-    default:
-      llvm_unreachable("Unimplemented opcode");
-      break;
-
     case UO_Minus:
-      AST = Z3_mk_bvneg(Context.Context, Exp.AST);
-      break;
+      return mkBVNeg(Exp);
 
     case UO_Not:
-      AST = Z3_mk_bvnot(Context.Context, Exp.AST);
-      break;
+      return mkBVNot(Exp);
 
     case UO_LNot:
-      AST = Z3_mk_not(Context.Context, Exp.AST);
-      break;
-    }
+      return mkNot(Exp);
 
-    return Z3Expr(Context, AST);
+    default:;
+    }
+    llvm_unreachable("Unimplemented opcode");
   }
 
   /// Construct a Z3Expr from a floating-point unary operator, given a
   /// Z3_context.
-  Z3Expr fromFloatUnOp(const UnaryOperator::Opcode Op, const Z3Expr &Exp) {
-    Z3_ast AST;
-
+  SMTExprRef fromFloatUnOp(const UnaryOperator::Opcode Op,
+                           const SMTExprRef &Exp) {
     switch (Op) {
-    default:
-      llvm_unreachable("Unimplemented opcode");
-      break;
-
     case UO_Minus:
-      AST = Z3_mk_fpa_neg(Context.Context, Exp.AST);
-      break;
+      return mkFPNeg(Exp);
 
     case UO_LNot:
       return fromUnOp(Op, Exp);
-    }
 
-    return Z3Expr(Context, AST);
+    default:;
+    }
+    llvm_unreachable("Unimplemented opcode");
   }
 
   /// Construct a Z3Expr from a n-ary binary operator.
-  Z3Expr fromNBinOp(const BinaryOperator::Opcode Op,
-                    const std::vector<Z3_ast> &ASTs) {
-    Z3_ast AST;
+  SMTExprRef fromNBinOp(const BinaryOperator::Opcode Op,
+                        const std::vector<SMTExprRef> &ASTs) {
+    assert(!ASTs.empty());
 
-    switch (Op) {
-    default:
+    if (Op != BO_LAnd && Op != BO_LOr)
       llvm_unreachable("Unimplemented opcode");
-      break;
-
-    case BO_LAnd:
-      AST = Z3_mk_and(Context.Context, ASTs.size(), ASTs.data());
-      break;
-
-    case BO_LOr:
-      AST = Z3_mk_or(Context.Context, ASTs.size(), ASTs.data());
-      break;
-    }
 
-    return Z3Expr(Context, AST);
+    SMTExprRef res = ASTs.front();
+    for (std::size_t i = 0; i < ASTs.size(); ++i)
+      res = (Op == BO_LAnd) ? mkAnd(res, ASTs[i]) : mkOr(res, ASTs[i]);
+    return res;
   }
 
   /// Construct a Z3Expr from a binary operator, given a Z3_context.
-  Z3Expr fromBinOp(const Z3Expr &LHS, const BinaryOperator::Opcode Op,
-                   const Z3Expr &RHS, bool isSigned) {
-    Z3_ast AST;
-
-    assert(getSort(LHS.AST) == getSort(RHS.AST) &&
-           "AST's must have the same sort!");
+  SMTExprRef fromBinOp(const SMTExprRef &LHS, const BinaryOperator::Opcode Op,
+                       const SMTExprRef &RHS, bool isSigned) {
+    assert(*getSort(LHS) == *getSort(RHS) && "AST's must have the same sort!");
 
     switch (Op) {
-    default:
-      llvm_unreachable("Unimplemented opcode");
-      break;
-
-      // Multiplicative operators
     case BO_Mul:
-      AST = Z3_mk_bvmul(Context.Context, LHS.AST, RHS.AST);
-      break;
+      return mkBVMul(LHS, RHS);
+
     case BO_Div:
-      AST = isSigned ? Z3_mk_bvsdiv(Context.Context, LHS.AST, RHS.AST)
-                     : Z3_mk_bvudiv(Context.Context, LHS.AST, RHS.AST);
-      break;
+      return isSigned ? mkBVSDiv(LHS, RHS) : mkBVUDiv(LHS, RHS);
+
     case BO_Rem:
-      AST = isSigned ? Z3_mk_bvsrem(Context.Context, LHS.AST, RHS.AST)
-                     : Z3_mk_bvurem(Context.Context, LHS.AST, RHS.AST);
-      break;
+      return isSigned ? mkBVSRem(LHS, RHS) : mkBVURem(LHS, RHS);
 
       // Additive operators
     case BO_Add:
-      AST = Z3_mk_bvadd(Context.Context, LHS.AST, RHS.AST);
-      break;
+      return mkBVAdd(LHS, RHS);
+
     case BO_Sub:
-      AST = Z3_mk_bvsub(Context.Context, LHS.AST, RHS.AST);
-      break;
+      return mkBVSub(LHS, RHS);
 
       // Bitwise shift operators
     case BO_Shl:
-      AST = Z3_mk_bvshl(Context.Context, LHS.AST, RHS.AST);
-      break;
+      return mkBVShl(LHS, RHS);
+
     case BO_Shr:
-      AST = isSigned ? Z3_mk_bvashr(Context.Context, LHS.AST, RHS.AST)
-                     : Z3_mk_bvlshr(Context.Context, LHS.AST, RHS.AST);
-      break;
+      return isSigned ? mkBVAshr(LHS, RHS) : mkBVLshr(LHS, RHS);
 
       // Relational operators
     case BO_LT:
-      AST = isSigned ? Z3_mk_bvslt(Context.Context, LHS.AST, RHS.AST)
-                     : Z3_mk_bvult(Context.Context, LHS.AST, RHS.AST);
-      break;
+      return isSigned ? mkBVSlt(LHS, RHS) : mkBVUlt(LHS, RHS);
+
     case BO_GT:
-      AST = isSigned ? Z3_mk_bvsgt(Context.Context, LHS.AST, RHS.AST)
-                     : Z3_mk_bvugt(Context.Context, LHS.AST, RHS.AST);
-      break;
+      return isSigned ? mkBVSgt(LHS, RHS) : mkBVUgt(LHS, RHS);
+
     case BO_LE:
-      AST = isSigned ? Z3_mk_bvsle(Context.Context, LHS.AST, RHS.AST)
-                     : Z3_mk_bvule(Context.Context, LHS.AST, RHS.AST);
-      break;
+      return isSigned ? mkBVSle(LHS, RHS) : mkBVUle(LHS, RHS);
+
     case BO_GE:
-      AST = isSigned ? Z3_mk_bvsge(Context.Context, LHS.AST, RHS.AST)
-                     : Z3_mk_bvuge(Context.Context, LHS.AST, RHS.AST);
-      break;
+      return isSigned ? mkBVSge(LHS, RHS) : mkBVUge(LHS, RHS);
 
       // Equality operators
     case BO_EQ:
-      AST = Z3_mk_eq(Context.Context, LHS.AST, RHS.AST);
-      break;
+      return mkEqual(LHS, RHS);
+
     case BO_NE:
       return fromUnOp(UO_LNot, fromBinOp(LHS, BO_EQ, RHS, isSigned));
-      break;
 
       // Bitwise operators
     case BO_And:
-      AST = Z3_mk_bvand(Context.Context, LHS.AST, RHS.AST);
-      break;
+      return mkBVAnd(LHS, RHS);
+
     case BO_Xor:
-      AST = Z3_mk_bvxor(Context.Context, LHS.AST, RHS.AST);
-      break;
+      return mkBVXor(LHS, RHS);
+
     case BO_Or:
-      AST = Z3_mk_bvor(Context.Context, LHS.AST, RHS.AST);
-      break;
+      return mkBVOr(LHS, RHS);
 
       // Logical operators
     case BO_LAnd:
-    case BO_LOr: {
-      std::vector<Z3_ast> Args = {LHS.AST, RHS.AST};
-      return fromNBinOp(Op, Args);
-    }
-    }
+      return mkAnd(LHS, RHS);
+
+    case BO_LOr:
+      return mkOr(LHS, RHS);
 
-    return Z3Expr(Context, AST);
+    default:;
+    }
+    llvm_unreachable("Unimplemented opcode");
   }
 
   /// Construct a Z3Expr from a special floating-point binary operator, given
   /// a Z3_context.
-  Z3Expr fromFloatSpecialBinOp(const Z3Expr &LHS,
+  SMTExprRef fromFloatSpecialBinOp(const SMTExprRef &LHS,
                                    const BinaryOperator::Opcode Op,
                                    const llvm::APFloat::fltCategory &RHS) {
-    Z3_ast AST;
-
     switch (Op) {
-    default:
-      llvm_unreachable("Unimplemented opcode");
-      break;
-
-      // Equality operators
     case BO_EQ:
       switch (RHS) {
       case llvm::APFloat::fcInfinity:
-        AST = Z3_mk_fpa_is_infinite(Context.Context, LHS.AST);
-        break;
+        return mkFPIsInfinite(LHS);
+
       case llvm::APFloat::fcNaN:
-        AST = Z3_mk_fpa_is_nan(Context.Context, LHS.AST);
-        break;
+        return mkFPIsNaN(LHS);
+
       case llvm::APFloat::fcNormal:
-        AST = Z3_mk_fpa_is_normal(Context.Context, LHS.AST);
-        break;
+        return mkFPIsNormal(LHS);
+
       case llvm::APFloat::fcZero:
-        AST = Z3_mk_fpa_is_zero(Context.Context, LHS.AST);
-        break;
+        return mkFPIsZero(LHS);
       }
       break;
+
     case BO_NE:
       return fromFloatUnOp(UO_LNot, fromFloatSpecialBinOp(LHS, BO_EQ, RHS));
-      break;
+
+    default:;
     }
 
-    return Z3Expr(Context, AST);
+    llvm_unreachable("Unimplemented opcode");
   }
 
   /// Construct a Z3Expr from a floating-point binary operator, given a
   /// Z3_context.
-  Z3Expr fromFloatBinOp(const Z3Expr &LHS, const BinaryOperator::Opcode Op,
-                        const Z3Expr &RHS) {
-    Z3_ast AST;
-
-    assert(getSort(LHS.AST) == getSort(RHS.AST) &&
-           "AST's must have the same sort!");
+  SMTExprRef fromFloatBinOp(const SMTExprRef &LHS,
+                            const BinaryOperator::Opcode Op,
+                            const SMTExprRef &RHS) {
+    assert(*getSort(LHS) == *getSort(RHS) && "AST's must have the same sort!");
 
     switch (Op) {
-    default:
-      llvm_unreachable("Unimplemented opcode");
-      break;
-
-      // Multiplicative operators
-    case BO_Mul: {
-      Z3Expr RoundingMode = getFloatRoundingMode();
-      AST = Z3_mk_fpa_mul(Context.Context, RoundingMode.AST, LHS.AST, RHS.AST);
-      break;
-    }
-    case BO_Div: {
-      Z3Expr RoundingMode = getFloatRoundingMode();
-      AST = Z3_mk_fpa_div(Context.Context, RoundingMode.AST, LHS.AST, RHS.AST);
-      break;
-    }
+    case BO_Mul:
+      return mkFPMul(LHS, RHS);
+
+    case BO_Div:
+      return mkFPDiv(LHS, RHS);
+
     case BO_Rem:
-      AST = Z3_mk_fpa_rem(Context.Context, LHS.AST, RHS.AST);
-      break;
+      return mkFPRem(LHS, RHS);
 
       // Additive operators
-    case BO_Add: {
-      Z3Expr RoundingMode = getFloatRoundingMode();
-      AST = Z3_mk_fpa_add(Context.Context, RoundingMode.AST, LHS.AST, RHS.AST);
-      break;
-    }
-    case BO_Sub: {
-      Z3Expr RoundingMode = getFloatRoundingMode();
-      AST = Z3_mk_fpa_sub(Context.Context, RoundingMode.AST, LHS.AST, RHS.AST);
-      break;
-    }
+    case BO_Add:
+      return mkFPAdd(LHS, RHS);
+
+    case BO_Sub:
+      return mkFPSub(LHS, RHS);
 
       // Relational operators
     case BO_LT:
-      AST = Z3_mk_fpa_lt(Context.Context, LHS.AST, RHS.AST);
-      break;
+      return mkFPLt(LHS, RHS);
+
     case BO_GT:
-      AST = Z3_mk_fpa_gt(Context.Context, LHS.AST, RHS.AST);
-      break;
+      return mkFPGt(LHS, RHS);
+
     case BO_LE:
-      AST = Z3_mk_fpa_leq(Context.Context, LHS.AST, RHS.AST);
-      break;
+      return mkFPLe(LHS, RHS);
+
     case BO_GE:
-      AST = Z3_mk_fpa_geq(Context.Context, LHS.AST, RHS.AST);
-      break;
+      return mkFPGe(LHS, RHS);
 
       // Equality operators
     case BO_EQ:
-      AST = Z3_mk_fpa_eq(Context.Context, LHS.AST, RHS.AST);
-      break;
+      return mkFPEqual(LHS, RHS);
+
     case BO_NE:
       return fromFloatUnOp(UO_LNot, fromFloatBinOp(LHS, BO_EQ, RHS));
-      break;
 
       // Logical operators
     case BO_LAnd:
     case BO_LOr:
       return fromBinOp(LHS, Op, RHS, false);
+
+    default:;
     }
 
-    return Z3Expr(Context, AST);
+    llvm_unreachable("Unimplemented opcode");
   }
 
   /// Construct a Z3Expr from a SymbolData, given a Z3_context.
-  Z3Expr fromData(const SymbolID ID, const QualType &Ty, uint64_t BitWidth) {
+  SMTExprRef fromData(const SymbolID ID, const QualType &Ty,
+                      uint64_t BitWidth) override {
     llvm::Twine Name = "$" + llvm::Twine(ID);
-
-    Z3Sort Sort = MkSort(Ty, BitWidth);
-
-    Z3_symbol Symbol = Z3_mk_string_symbol(Context.Context, Name.str().c_str());
-    Z3_ast AST = Z3_mk_const(Context.Context, Symbol, Sort.Sort);
-    return Z3Expr(Context, AST);
+    return mkSymbol(Name.str().c_str(), mkSort(Ty, BitWidth));
   }
 
   /// Construct a Z3Expr from a SymbolCast, given a Z3_context.
-  Z3Expr fromCast(const Z3Expr &Exp, QualType ToTy, uint64_t ToBitWidth,
+  SMTExprRef fromCast(const SMTExprRef &Exp, QualType ToTy, uint64_t ToBitWidth,
                       QualType FromTy, uint64_t FromBitWidth) {
-    Z3_ast AST;
-
     if ((FromTy->isIntegralOrEnumerationType() &&
          ToTy->isIntegralOrEnumerationType()) ||
         (FromTy->isAnyPointerType() ^ ToTy->isAnyPointerType()) ||
         (FromTy->isBlockPointerType() ^ ToTy->isBlockPointerType()) ||
         (FromTy->isReferenceType() ^ ToTy->isReferenceType())) {
-      // Special case: Z3 boolean type is distinct from bitvector type, so
-      // must use if-then-else expression instead of direct cast
+
       if (FromTy->isBooleanType()) {
         assert(ToBitWidth > 0 && "BitWidth must be positive!");
-        Z3Expr Zero = fromInt("0", ToBitWidth);
-        Z3Expr One = fromInt("1", ToBitWidth);
-        AST = Z3_mk_ite(Context.Context, Exp.AST, One.AST, Zero.AST);
-      } else if (ToBitWidth > FromBitWidth) {
-        AST = FromTy->isSignedIntegerOrEnumerationType()
-                  ? Z3_mk_sign_ext(Context.Context, ToBitWidth - FromBitWidth,
-                                   Exp.AST)
-                  : Z3_mk_zero_ext(Context.Context, ToBitWidth - FromBitWidth,
-                                   Exp.AST);
-      } else if (ToBitWidth < FromBitWidth) {
-        AST = Z3_mk_extract(Context.Context, ToBitWidth - 1, 0, Exp.AST);
-      } else {
-        // Both are bitvectors with the same width, ignore the type cast
-        return Exp;
-      }
-    } else if (FromTy->isRealFloatingType() && ToTy->isRealFloatingType()) {
-      if (ToBitWidth != FromBitWidth) {
-        Z3Expr RoundingMode = getFloatRoundingMode();
-        Z3Sort Sort = getFloatSort(ToBitWidth);
-        AST = Z3_mk_fpa_to_fp_float(Context.Context, RoundingMode.AST, Exp.AST,
-                                    Sort.Sort);
-      } else {
-        return Exp;
-      }
-    } else if (FromTy->isIntegralOrEnumerationType() &&
-               ToTy->isRealFloatingType()) {
-      Z3Expr RoundingMode = getFloatRoundingMode();
-      Z3Sort Sort = getFloatSort(ToBitWidth);
-      AST = FromTy->isSignedIntegerOrEnumerationType()
-                ? Z3_mk_fpa_to_fp_signed(Context.Context, RoundingMode.AST,
-                                         Exp.AST, Sort.Sort)
-                : Z3_mk_fpa_to_fp_unsigned(Context.Context, RoundingMode.AST,
-                                           Exp.AST, Sort.Sort);
-    } else if (FromTy->isRealFloatingType() &&
-               ToTy->isIntegralOrEnumerationType()) {
-      Z3Expr RoundingMode = getFloatRoundingMode();
-      AST = ToTy->isSignedIntegerOrEnumerationType()
-                ? Z3_mk_fpa_to_sbv(Context.Context, RoundingMode.AST, Exp.AST,
-                                   ToBitWidth)
-                : Z3_mk_fpa_to_ubv(Context.Context, RoundingMode.AST, Exp.AST,
-                                   ToBitWidth);
-    } else {
-      llvm_unreachable("Unsupported explicit type cast!");
+        return mkIte(Exp, mkBitvector(llvm::APSInt("1"), ToBitWidth),
+                     mkBitvector(llvm::APSInt("0"), ToBitWidth));
+      }
+
+      if (ToBitWidth > FromBitWidth)
+        return FromTy->isSignedIntegerOrEnumerationType()
+                   ? mkSignExt(ToBitWidth - FromBitWidth, Exp)
+                   : mkZeroExt(ToBitWidth - FromBitWidth, Exp);
+
+      if (ToBitWidth < FromBitWidth)
+        return mkExtract(ToBitWidth - 1, 0, Exp);
+
+
+    if (FromTy->isRealFloatingType() && ToTy->isRealFloatingType()) {
+      if (ToBitWidth != FromBitWidth)
+        return mkFPtoFP(Exp, getFloatSort(ToBitWidth));
+
+
+    if (FromTy->isIntegralOrEnumerationType() && ToTy->isRealFloatingType()) {
+      SMTSortRef Sort = getFloatSort(ToBitWidth);
+      return FromTy->isSignedIntegerOrEnumerationType() ? mkFPtoSBV(Exp, Sort)
+                                                        : mkFPtoUBV(Exp, Sort);
     }
 
-    return Z3Expr(Context, AST);
+    if (FromTy->isRealFloatingType() && ToTy->isIntegralOrEnumerationType())
+      return ToTy->isSignedIntegerOrEnumerationType()
+                 ? mkSBVtoFP(Exp, ToBitWidth)
+                 : mkUBVtoFP(Exp, ToBitWidth);
+
+    llvm_unreachable("Unsupported explicit type cast!");
   }
 
   /// Construct a Z3Expr from a boolean, given a Z3_context.
-  Z3Expr fromBoolean(const bool Bool) {
+  SMTExprRef fromBoolean(const bool Bool) {
     Z3_ast AST =
         Bool ? Z3_mk_true(Context.Context) : Z3_mk_false(Context.Context);
-    return Z3Expr(Context, AST);
+    return std::make_shared<Z3Expr>(Context, AST);
   }
 
   /// Construct a Z3Expr from a finite APFloat, given a Z3_context.
-  Z3Expr fromAPFloat(const llvm::APFloat &Float) {
-    Z3_ast AST;
-    Z3Sort Sort =
+  SMTExprRef fromAPFloat(const llvm::APFloat &Float) {
+    SMTSortRef Sort =
         getFloatSort(llvm::APFloat::semanticsSizeInBits(Float.getSemantics()));
 
     llvm::APSInt Int = llvm::APSInt(Float.bitcastToAPInt(), false);
-    Z3Expr Z3Int = fromAPSInt(Int);
-    AST = Z3_mk_fpa_to_fp_bv(Context.Context, Z3Int.AST, Sort.Sort);
-    return Z3Expr(Context, AST);
+    SMTExprRef Z3Int = fromAPSInt(Int);
+    return std::make_shared<Z3Expr>(
+        Context, Z3_mk_fpa_to_fp_bv(Context.Context, toZ3Expr(*Z3Int).AST,
+                                    toZ3Sort(*Sort).Sort));
   }
 
   /// Construct a Z3Expr from an APSInt, given a Z3_context.
-  Z3Expr fromAPSInt(const llvm::APSInt &Int) {
-    Z3Sort Sort = getBitvectorSort(Int.getBitWidth());
-    Z3_ast AST =
-        Z3_mk_numeral(Context.Context, Int.toString(10).c_str(), Sort.Sort);
-    return Z3Expr(Context, AST);
+  SMTExprRef fromAPSInt(const llvm::APSInt &Int) {
+    SMTSortRef Sort = getBitvectorSort(Int.getBitWidth());
+    Z3_ast AST = Z3_mk_numeral(Context.Context, Int.toString(10).c_str(),
+                               toZ3Sort(*Sort).Sort);
+    return std::make_shared<Z3Expr>(Context, AST);
   }
 
   /// Construct a Z3Expr from an integer, given a Z3_context.
-  Z3Expr fromInt(const char *Int, uint64_t BitWidth) {
-    Z3Sort Sort = getBitvectorSort(BitWidth);
-    Z3_ast AST = Z3_mk_numeral(Context.Context, Int, Sort.Sort);
-    return Z3Expr(Context, AST);
+  SMTExprRef fromInt(const char *Int, uint64_t BitWidth) {
+    SMTSortRef Sort = getBitvectorSort(BitWidth);
+    Z3_ast AST = Z3_mk_numeral(Context.Context, Int, toZ3Sort(*Sort).Sort);
+    return std::make_shared<Z3Expr>(Context, AST);
   }
 
-  /// 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.isFloatSort() && "Unsupported sort to floating-point!");
+  bool toAPFloat(const SMTSortRef &Sort, const SMTExprRef &AST,
+                 llvm::APFloat &Float, bool useSemantics) {
+    assert(Sort->isFloatSort() && "Unsupported sort to floating-point!");
 
-    llvm::APSInt Int(Sort.getFloatSortSize(), true);
+    llvm::APSInt Int(Sort->getFloatSortSize(), true);
     const llvm::fltSemantics &Semantics =
-        getFloatSemantics(Sort.getFloatSortSize());
-    Z3Sort BVSort = getBitvectorSort(Sort.getFloatSortSize());
+        getFloatSemantics(Sort->getFloatSortSize());
+    SMTSortRef BVSort = getBitvectorSort(Sort->getFloatSortSize());
     if (!toAPSInt(BVSort, AST, Int, true)) {
       return false;
     }
 
     if (useSemantics && !areEquivalent(Float.getSemantics(), Semantics)) {
       assert(false && "Floating-point types don't match!");
       return false;
     }
 
     Float = llvm::APFloat(Semantics, Int);
     return true;
   }
 
-  /// 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) {
-    if (Sort.isBitvectorSort()) {
-      if (useSemantics && Int.getBitWidth() != Sort.getBitvectorSortSize()) {
+  bool toAPSInt(const SMTSortRef &Sort, const SMTExprRef &AST,
+                llvm::APSInt &Int, bool useSemantics) {
+    if (Sort->isBitvectorSort()) {
+      if (useSemantics && Int.getBitWidth() != Sort->getBitvectorSortSize()) {
         assert(false && "Bitvector types don't match!");
         return false;
       }
 
       uint64_t Value[2];
       // Force cast because Z3 defines __uint64 to be a unsigned long long
       // type, which isn't compatible with a unsigned long type, even if they
       // are the same size.
-      Z3_get_numeral_uint64(Context.Context, AST,
+      Z3_get_numeral_uint64(Context.Context, toZ3Expr(*AST).AST,
                             reinterpret_cast<__uint64 *>(&Value[0]));
-      if (Sort.getBitvectorSortSize() <= 64) {
+      if (Sort->getBitvectorSortSize() <= 64) {
         Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), Value[0]),
                            Int.isUnsigned());
-      } else if (Sort.getBitvectorSortSize() == 128) {
-        Z3Expr ASTHigh =
-            Z3Expr(Context, Z3_mk_extract(Context.Context, 127, 64, AST));
-        Z3_get_numeral_uint64(Context.Context, AST,
+      } else if (Sort->getBitvectorSortSize() == 128) {
+        SMTExprRef ASTHigh = mkExtract(127, 64, AST);
+        Z3_get_numeral_uint64(Context.Context, toZ3Expr(*AST).AST,
                               reinterpret_cast<__uint64 *>(&Value[1]));
         Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), Value),
                            Int.isUnsigned());
       } else {
         assert(false && "Bitwidth not supported!");
         return false;
       }
       return true;
     }
 
-    if (Sort.isBooleanSort()) {
+    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
-                                                                           : 0),
+      Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), getBoolean(AST)),
                          Int.isUnsigned());
       return true;
     }
 
     llvm_unreachable("Unsupported sort to integer!");
   }
 
   /// Given an expression and a model, extract the value of this operand in
   /// the model.
-  bool getInterpretation(const Z3Model Model, const Z3Expr &Exp,
-                         llvm::APSInt &Int) {
-    Z3_func_decl Func =
-        Z3_get_app_decl(Context.Context, Z3_to_app(Context.Context, Exp.AST));
+  bool getInterpretation(const SMTExprRef &Exp, llvm::APSInt &Int) override {
+    Z3Model Model = getModel();
+    Z3_func_decl Func = Z3_get_app_decl(
+        Context.Context, Z3_to_app(Context.Context, toZ3Expr(*Exp).AST));
     if (Z3_model_has_interp(Context.Context, Model.Model, Func) != Z3_L_TRUE)
       return false;
 
-    Z3_ast Assign =
-        Z3_model_get_const_interp(Context.Context, Model.Model, Func);
-    Z3Sort Sort = getSort(Assign);
+    SMTExprRef Assign = std::make_shared<Z3Expr>(
+        Context, Z3_model_get_const_interp(Context.Context, Model.Model, Func));
+    SMTSortRef Sort = getSort(Assign);
     return toAPSInt(Sort, Assign, Int, true);
   }
 
   /// Given an expression and a model, extract the value of this operand in
   /// the model.
-  bool getInterpretation(const Z3Model Model, const Z3Expr &Exp,
-                         llvm::APFloat &Float) {
-    Z3_func_decl Func =
-        Z3_get_app_decl(Context.Context, Z3_to_app(Context.Context, Exp.AST));
+  bool getInterpretation(const SMTExprRef &Exp, llvm::APFloat &Float) override {
+    Z3Model Model = getModel();
+    Z3_func_decl Func = Z3_get_app_decl(
+        Context.Context, Z3_to_app(Context.Context, toZ3Expr(*Exp).AST));
     if (Z3_model_has_interp(Context.Context, Model.Model, Func) != Z3_L_TRUE)
       return false;
 
-    Z3_ast Assign =
-        Z3_model_get_const_interp(Context.Context, Model.Model, Func);
-    Z3Sort Sort = getSort(Assign);
+    SMTExprRef Assign = std::make_shared<Z3Expr>(
+        Context, Z3_model_get_const_interp(Context.Context, Model.Model, Func));
+    SMTSortRef Sort = getSort(Assign);
     return toAPFloat(Sort, Assign, Float, true);
   }
 
   // Callback function for doCast parameter on APSInt type.
   llvm::APSInt castAPSInt(const llvm::APSInt &V, QualType ToTy,
                           uint64_t ToWidth, QualType FromTy,
                           uint64_t FromWidth) {
     APSIntType TargetType(ToWidth, !ToTy->isSignedIntegerOrEnumerationType());
     return TargetType.convert(V);
   }
 
   /// Check if the constraints are satisfiable
-  Z3_lbool check() { return Z3_solver_check(Context.Context, Solver); }
+  ConditionTruthVal check() const override {
+    Z3_lbool res = Z3_solver_check(Context.Context, Solver);
+    if (res == Z3_L_TRUE)
+      return true;
+
+    if (res == Z3_L_FALSE)
+      return false;
+
+    return ConditionTruthVal();
+  }
 
   /// Push the current solver state
-  void push() { return Z3_solver_push(Context.Context, Solver); }
+  void push() override { return Z3_solver_push(Context.Context, Solver); }
 
   /// Pop the previous solver state
-  void pop(unsigned NumStates = 1) {
+  void pop(unsigned NumStates = 1) override {
     assert(Z3_solver_get_num_scopes(Context.Context, Solver) >= NumStates);
     return Z3_solver_pop(Context.Context, Solver, NumStates);
   }
 
   /// Get a model from the solver. Caller should check the model is
   /// satisfiable.
   Z3Model getModel() {
     return Z3Model(Context, Z3_solver_get_model(Context.Context, Solver));
   }
 
   /// Reset the solver and remove all constraints.
-  void reset() { Z3_solver_reset(Context.Context, Solver); }
+  void reset() const override { Z3_solver_reset(Context.Context, Solver); }
 
-  void print(raw_ostream &OS) const {
+  void print(raw_ostream &OS) const override {
     OS << Z3_solver_to_string(Context.Context, Solver);
   }
-
-  LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
 }; // end class Z3Solver
 
 class Z3ConstraintManager : public SMTConstraintManager {
   mutable Z3Solver Solver;
 
 public:
   Z3ConstraintManager(SubEngine *SE, SValBuilder &SB)
       : SMTConstraintManager(SE, SB) {}

 
 private:
   //===------------------------------------------------------------------===//
   // Internal implementation.
   //===------------------------------------------------------------------===//
 
   // Check whether a new model is satisfiable, and update the program state.
   ProgramStateRef assumeZ3Expr(ProgramStateRef State, SymbolRef Sym,
-                               const Z3Expr &Exp);
+                               const SMTExprRef &Exp);
 
   // Generate and check a Z3 model, using the given constraint.
-  Z3_lbool checkZ3Model(ProgramStateRef State, const Z3Expr &Exp) const;
+  ConditionTruthVal checkZ3Model(ProgramStateRef State,
+                                 const SMTExprRef &Exp) const;
 
   // Generate a Z3Expr that represents the given symbolic expression.
   // Sets the hasComparison parameter if the expression has a comparison
   // operator.
   // Sets the RetTy parameter to the final return type after promotions and
   // casts.
-  Z3Expr getZ3Expr(SymbolRef Sym, QualType *RetTy = nullptr,
+  SMTExprRef getZ3Expr(SymbolRef Sym, QualType *RetTy = nullptr,
                        bool *hasComparison = nullptr) const;
 
   // Generate a Z3Expr that takes the logical not of an expression.
-  Z3Expr getZ3NotExpr(const Z3Expr &Exp) const;
+  SMTExprRef getZ3NotExpr(const SMTExprRef &Exp) const;
 
   // Generate a Z3Expr that compares the expression to zero.
-  Z3Expr getZ3ZeroExpr(const Z3Expr &Exp, QualType RetTy,
+  SMTExprRef getZ3ZeroExpr(const SMTExprRef &Exp, QualType RetTy,
                            bool Assumption) const;
 
   // Recursive implementation to unpack and generate symbolic expression.
   // Sets the hasComparison and RetTy parameters. See getZ3Expr().
-  Z3Expr getZ3SymExpr(SymbolRef Sym, QualType *RetTy,
+  SMTExprRef getZ3SymExpr(SymbolRef Sym, QualType *RetTy,
                           bool *hasComparison) const;
 
   // Wrapper to generate Z3Expr from SymbolData.
-  Z3Expr getZ3DataExpr(const SymbolID ID, QualType Ty) const;
+  SMTExprRef getZ3DataExpr(const SymbolID ID, QualType Ty) const;
 
   // Wrapper to generate Z3Expr from SymbolCast.
-  Z3Expr getZ3CastExpr(const Z3Expr &Exp, QualType FromTy, QualType Ty) const;
+  SMTExprRef getZ3CastExpr(const SMTExprRef &Exp, QualType FromTy,
+                           QualType Ty) const;
 
   // Wrapper to generate Z3Expr from BinarySymExpr.
   // Sets the hasComparison and RetTy parameters. See getZ3Expr().
-  Z3Expr getZ3SymBinExpr(const BinarySymExpr *BSE, bool *hasComparison,
+  SMTExprRef getZ3SymBinExpr(const BinarySymExpr *BSE, bool *hasComparison,
                              QualType *RetTy) const;
 
   // Wrapper to generate Z3Expr from unpacked binary symbolic expression.
   // Sets the RetTy parameter. See getZ3Expr().
-  Z3Expr getZ3BinExpr(const Z3Expr &LHS, QualType LTy,
-                      BinaryOperator::Opcode Op, const Z3Expr &RHS,
+  SMTExprRef getZ3BinExpr(const SMTExprRef &LHS, QualType LTy,
+                          BinaryOperator::Opcode Op, const SMTExprRef &RHS,
                           QualType RTy, QualType *RetTy) const;
 
   // Wrapper to generate Z3Expr from a range. If From == To, an equality will
   // be created instead.
-  Z3Expr getZ3RangeExpr(SymbolRef Sym, const llvm::APSInt &From,
+  SMTExprRef getZ3RangeExpr(SymbolRef Sym, const llvm::APSInt &From,
                             const llvm::APSInt &To, bool InRange);
 
   //===------------------------------------------------------------------===//
   // Helper functions.
   //===------------------------------------------------------------------===//
 
   // Recover the QualType of an APSInt.
   // TODO: Refactor to put elsewhere
   QualType getAPSIntType(const llvm::APSInt &Int) const;
 
   // Get the QualTy for the input APSInt, and fix it if it has a bitwidth of 1.
   std::pair<llvm::APSInt, QualType> fixAPSInt(const llvm::APSInt &Int) const;
 
   // Perform implicit type conversion on binary symbolic expressions.
   // May modify all input parameters.
   // TODO: Refactor to use built-in conversion functions
-  void doTypeConversion(Z3Expr &LHS, Z3Expr &RHS, QualType &LTy,
+  void doTypeConversion(SMTExprRef &LHS, SMTExprRef &RHS, QualType &LTy,
                         QualType &RTy) const;
 
   // Perform implicit integer type conversion.
   // May modify all input parameters.
   // TODO: Refactor to use Sema::handleIntegerConversion()
   template <typename T, T (Z3Solver::*doCast)(const T &, QualType, uint64_t,
                                               QualType, uint64_t)>
   void doIntTypeConversion(T &LHS, QualType &LTy, T &RHS, QualType &RTy) const;

 
 } // end anonymous namespace
 
 ProgramStateRef Z3ConstraintManager::assumeSym(ProgramStateRef State,
                                                SymbolRef Sym, bool Assumption) {
   QualType RetTy;
   bool hasComparison;
 
-  Z3Expr Exp = getZ3Expr(Sym, &RetTy, &hasComparison);
+  SMTExprRef Exp = getZ3Expr(Sym, &RetTy, &hasComparison);
   // Create zero comparison for implicit boolean cast, with reversed assumption
   if (!hasComparison && !RetTy->isBooleanType())
     return assumeZ3Expr(State, Sym, getZ3ZeroExpr(Exp, RetTy, !Assumption));
 
   return assumeZ3Expr(State, Sym, Assumption ? Exp : getZ3NotExpr(Exp));
 }
 
 ProgramStateRef Z3ConstraintManager::assumeSymInclusiveRange(
bool Z3ConstraintManager::canReasonAbout(SVal X) const {
 
   llvm_unreachable("Unsupported expression to reason about!");
 }
 
 ConditionTruthVal Z3ConstraintManager::checkNull(ProgramStateRef State,
                                                  SymbolRef Sym) {
   QualType RetTy;
   // The expression may be casted, so we cannot call getZ3DataExpr() directly
-  Z3Expr VarExp = getZ3Expr(Sym, &RetTy);
-  Z3Expr Exp = getZ3ZeroExpr(VarExp, RetTy, true);
+  SMTExprRef VarExp = getZ3Expr(Sym, &RetTy);
+  SMTExprRef Exp = getZ3ZeroExpr(VarExp, RetTy, true);
+
   // Negate the constraint
-  Z3Expr NotExp = getZ3ZeroExpr(VarExp, RetTy, false);
+  SMTExprRef NotExp = getZ3ZeroExpr(VarExp, RetTy, false);
 
   Solver.reset();
   Solver.addStateConstraints(State);
 
   Solver.push();
   Solver.addConstraint(Exp);
-  Z3_lbool isSat = Solver.check();
+  ConditionTruthVal isSat = Solver.check();
 
   Solver.pop();
   Solver.addConstraint(NotExp);
-  Z3_lbool isNotSat = Solver.check();
+  ConditionTruthVal isNotSat = Solver.check();
 
   // Zero is the only possible solution
-  if (isSat == Z3_L_TRUE && isNotSat == Z3_L_FALSE)
+  if (isSat.isConstrainedTrue() && isNotSat.isConstrainedFalse())
     return true;
+
   // Zero is not a solution
-  else if (isSat == Z3_L_FALSE && isNotSat == Z3_L_TRUE)
+  if (isSat.isConstrainedFalse() && isNotSat.isConstrainedTrue())
     return false;
 
   // Zero may be a solution
   return ConditionTruthVal();
 }
 
 const llvm::APSInt *Z3ConstraintManager::getSymVal(ProgramStateRef State,
                                                    SymbolRef Sym) const {
   BasicValueFactory &BVF = getBasicVals();
   ASTContext &Ctx = BVF.getContext();
 
   if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
     QualType Ty = Sym->getType();
     assert(!Ty->isRealFloatingType());
     llvm::APSInt Value(Ctx.getTypeSize(Ty),
                        !Ty->isSignedIntegerOrEnumerationType());
 
-    Z3Expr Exp = getZ3DataExpr(SD->getSymbolID(), Ty);
+    SMTExprRef Exp = getZ3DataExpr(SD->getSymbolID(), Ty);
 
     Solver.reset();
     Solver.addStateConstraints(State);
 
     // Constraints are unsatisfiable
-    if (Solver.check() != Z3_L_TRUE)
+    ConditionTruthVal isSat = Solver.check();
+    if (!isSat.isConstrainedTrue())
       return nullptr;
 
-    Z3Model Model = Solver.getModel();
     // Model does not assign interpretation
-    if (!Solver.getInterpretation(Model, Exp, Value))
+    if (!Solver.getInterpretation(Exp, Value))
       return nullptr;
 
     // A value has been obtained, check if it is the only value
-    Z3Expr NotExp = Solver.fromBinOp(
+    SMTExprRef NotExp = Solver.fromBinOp(
         Exp, BO_NE,
         Ty->isBooleanType() ? Solver.fromBoolean(Value.getBoolValue())
                             : Solver.fromAPSInt(Value),
         false);
 
     Solver.addConstraint(NotExp);
-    if (Solver.check() == Z3_L_TRUE)
+
+    ConditionTruthVal isNotSat = Solver.check();
+    if (isNotSat.isConstrainedTrue())
       return nullptr;
 
     // This is the only solution, store it
     return &BVF.getValue(Value);
   } else if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
     SymbolRef CastSym = SC->getOperand();
     QualType CastTy = SC->getType();
     // Skip the void type

 }
 
 void Z3ConstraintManager::addRangeConstraints(ConstraintRangeTy CR) {
   Solver.reset();
 
   for (const auto &I : CR) {
     SymbolRef Sym = I.first;
 
-    Z3Expr Constraints = Solver.fromBoolean(false);
+    SMTExprRef Constraints = Solver.fromBoolean(false);
     for (const auto &Range : I.second) {
-      Z3Expr SymRange =
+      SMTExprRef SymRange =
           getZ3RangeExpr(Sym, Range.From(), Range.To(), /*InRange=*/true);
 
       // FIXME: the last argument (isSigned) is not used when generating the
       // or expression, as both arguments are booleans
       Constraints =
           Solver.fromBinOp(Constraints, BO_LOr, SymRange, /*IsSigned=*/true);
     }
     Solver.addConstraint(Constraints);
   }
 }
 
 clang::ento::ConditionTruthVal Z3ConstraintManager::isModelFeasible() {
-  if (Solver.check() == Z3_L_FALSE)
-    return false;
-
-  return ConditionTruthVal();
+  return Solver.check();
 }
 
 LLVM_DUMP_METHOD void Z3ConstraintManager::dump() const { Solver.dump(); }
 
 //===------------------------------------------------------------------===//
 // Internal implementation.
 //===------------------------------------------------------------------===//
 
 ProgramStateRef Z3ConstraintManager::assumeZ3Expr(ProgramStateRef State,
                                                   SymbolRef Sym,
-                                                  const Z3Expr &Exp) {
+                                                  const SMTExprRef &Exp) {
   // Check the model, avoid simplifying AST to save time
-  if (checkZ3Model(State, Exp) == Z3_L_TRUE)
-    return State->add<ConstraintZ3>(std::make_pair(Sym, Exp));
+  if (checkZ3Model(State, Exp).isConstrainedTrue())
+    return State->add<ConstraintZ3>(std::make_pair(Sym, toZ3Expr(*Exp)));
 
   return nullptr;
 }
 
-Z3_lbool Z3ConstraintManager::checkZ3Model(ProgramStateRef State,
-                                           const Z3Expr &Exp) const {
+ConditionTruthVal
+Z3ConstraintManager::checkZ3Model(ProgramStateRef State,
+                                  const SMTExprRef &Exp) const {
   Solver.reset();
   Solver.addConstraint(Exp);
   Solver.addStateConstraints(State);
   return Solver.check();
 }
 
-Z3Expr Z3ConstraintManager::getZ3Expr(SymbolRef Sym, QualType *RetTy,
+SMTExprRef Z3ConstraintManager::getZ3Expr(SymbolRef Sym, QualType *RetTy,
                                           bool *hasComparison) const {
   if (hasComparison) {
     *hasComparison = false;
   }
 
   return getZ3SymExpr(Sym, RetTy, hasComparison);
 }
 
-Z3Expr Z3ConstraintManager::getZ3NotExpr(const Z3Expr &Exp) const {
+SMTExprRef Z3ConstraintManager::getZ3NotExpr(const SMTExprRef &Exp) const {
   return Solver.fromUnOp(UO_LNot, Exp);
 }
 
-Z3Expr Z3ConstraintManager::getZ3ZeroExpr(const Z3Expr &Exp, QualType Ty,
+SMTExprRef Z3ConstraintManager::getZ3ZeroExpr(const SMTExprRef &Exp,
+                                              QualType Ty,
                                               bool Assumption) const {
   ASTContext &Ctx = getBasicVals().getContext();
   if (Ty->isRealFloatingType()) {
     llvm::APFloat Zero = llvm::APFloat::getZero(Ctx.getFloatTypeSemantics(Ty));
     return Solver.fromFloatBinOp(Exp, Assumption ? BO_EQ : BO_NE,
                                  Solver.fromAPFloat(Zero));
   } else if (Ty->isIntegralOrEnumerationType() || Ty->isAnyPointerType() ||
              Ty->isBlockPointerType() || Ty->isReferenceType()) {
     bool isSigned = Ty->isSignedIntegerOrEnumerationType();
     // Skip explicit comparison for boolean types
     if (Ty->isBooleanType())
       return Assumption ? getZ3NotExpr(Exp) : Exp;
     return Solver.fromBinOp(Exp, Assumption ? BO_EQ : BO_NE,
                             Solver.fromInt("0", Ctx.getTypeSize(Ty)), isSigned);
   }
 
   llvm_unreachable("Unsupported type for zero value!");
 }
 
-Z3Expr Z3ConstraintManager::getZ3SymExpr(SymbolRef Sym, QualType *RetTy,
+SMTExprRef Z3ConstraintManager::getZ3SymExpr(SymbolRef Sym, QualType *RetTy,
                                              bool *hasComparison) const {
   if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
     if (RetTy)
       *RetTy = Sym->getType();
 
     return getZ3DataExpr(SD->getSymbolID(), Sym->getType());
   } else if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
     if (RetTy)
       *RetTy = Sym->getType();
 
     QualType FromTy;
-    Z3Expr Exp = getZ3SymExpr(SC->getOperand(), &FromTy, hasComparison);
+    SMTExprRef Exp = getZ3SymExpr(SC->getOperand(), &FromTy, hasComparison);
     // Casting an expression with a comparison invalidates it. Note that this
     // must occur after the recursive call above.
     // e.g. (signed char) (x > 0)
     if (hasComparison)
       *hasComparison = false;
     return getZ3CastExpr(Exp, FromTy, Sym->getType());
   } else if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
-    Z3Expr Exp = getZ3SymBinExpr(BSE, hasComparison, RetTy);
+    SMTExprRef Exp = getZ3SymBinExpr(BSE, hasComparison, RetTy);
     // Set the hasComparison parameter, in post-order traversal order.
     if (hasComparison)
       *hasComparison = BinaryOperator::isComparisonOp(BSE->getOpcode());
     return Exp;
   }
 
   llvm_unreachable("Unsupported SymbolRef type!");
 }
 
-Z3Expr Z3ConstraintManager::getZ3DataExpr(const SymbolID ID,
+SMTExprRef Z3ConstraintManager::getZ3DataExpr(const SymbolID ID,
                                               QualType Ty) const {
   ASTContext &Ctx = getBasicVals().getContext();
   return Solver.fromData(ID, Ty, Ctx.getTypeSize(Ty));
 }
 
-Z3Expr Z3ConstraintManager::getZ3CastExpr(const Z3Expr &Exp, QualType FromTy,
+SMTExprRef Z3ConstraintManager::getZ3CastExpr(const SMTExprRef &Exp,
+                                              QualType FromTy,
                                               QualType ToTy) const {
   ASTContext &Ctx = getBasicVals().getContext();
   return Solver.fromCast(Exp, ToTy, Ctx.getTypeSize(ToTy), FromTy,
                          Ctx.getTypeSize(FromTy));
 }
 
-Z3Expr Z3ConstraintManager::getZ3SymBinExpr(const BinarySymExpr *BSE,
+SMTExprRef Z3ConstraintManager::getZ3SymBinExpr(const BinarySymExpr *BSE,
                                                 bool *hasComparison,
                                                 QualType *RetTy) const {
   QualType LTy, RTy;
   BinaryOperator::Opcode Op = BSE->getOpcode();
 
   if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
-    Z3Expr LHS = getZ3SymExpr(SIE->getLHS(), &LTy, hasComparison);
+    SMTExprRef LHS = getZ3SymExpr(SIE->getLHS(), &LTy, hasComparison);
     llvm::APSInt NewRInt;
     std::tie(NewRInt, RTy) = fixAPSInt(SIE->getRHS());
-    Z3Expr RHS = Solver.fromAPSInt(NewRInt);
+    SMTExprRef RHS = Solver.fromAPSInt(NewRInt);
     return getZ3BinExpr(LHS, LTy, Op, RHS, RTy, RetTy);
   } else if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
     llvm::APSInt NewLInt;
     std::tie(NewLInt, LTy) = fixAPSInt(ISE->getLHS());
-    Z3Expr LHS = Solver.fromAPSInt(NewLInt);
-    Z3Expr RHS = getZ3SymExpr(ISE->getRHS(), &RTy, hasComparison);
+    SMTExprRef LHS = Solver.fromAPSInt(NewLInt);
+    SMTExprRef RHS = getZ3SymExpr(ISE->getRHS(), &RTy, hasComparison);
     return getZ3BinExpr(LHS, LTy, Op, RHS, RTy, RetTy);
   } else if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
-    Z3Expr LHS = getZ3SymExpr(SSM->getLHS(), &LTy, hasComparison);
-    Z3Expr RHS = getZ3SymExpr(SSM->getRHS(), &RTy, hasComparison);
+    SMTExprRef LHS = getZ3SymExpr(SSM->getLHS(), &LTy, hasComparison);
+    SMTExprRef RHS = getZ3SymExpr(SSM->getRHS(), &RTy, hasComparison);
     return getZ3BinExpr(LHS, LTy, Op, RHS, RTy, RetTy);
   } else {
     llvm_unreachable("Unsupported BinarySymExpr type!");
   }
 }
 
-Z3Expr Z3ConstraintManager::getZ3BinExpr(const Z3Expr &LHS, QualType LTy,
-                                         BinaryOperator::Opcode Op,
-                                         const Z3Expr &RHS, QualType RTy,
-                                         QualType *RetTy) const {
-  Z3Expr NewLHS = LHS;
-  Z3Expr NewRHS = RHS;
+SMTExprRef Z3ConstraintManager::getZ3BinExpr(
+    const SMTExprRef &LHS, QualType LTy, BinaryOperator::Opcode Op,
+    const SMTExprRef &RHS, QualType RTy, QualType *RetTy) const {
+  SMTExprRef NewLHS = LHS;
+  SMTExprRef NewRHS = RHS;
   doTypeConversion(NewLHS, NewRHS, LTy, RTy);
   // Update the return type parameter if the output type has changed.
   if (RetTy) {
     // A boolean result can be represented as an integer type in C/C++, but at
     // this point we only care about the Z3 type. Set it as a boolean type to
     // avoid subsequent Z3 errors.
     if (BinaryOperator::isComparisonOp(Op) || BinaryOperator::isLogicalOp(Op)) {
       ASTContext &Ctx = getBasicVals().getContext();
SMTExprRef Z3ConstraintManager::getZ3BinExpr(
   }
 
   return LTy->isRealFloatingType()
              ? Solver.fromFloatBinOp(NewLHS, Op, NewRHS)
              : Solver.fromBinOp(NewLHS, Op, NewRHS,
                                 LTy->isSignedIntegerOrEnumerationType());
 }
 
-Z3Expr Z3ConstraintManager::getZ3RangeExpr(SymbolRef Sym,
+SMTExprRef Z3ConstraintManager::getZ3RangeExpr(SymbolRef Sym,
                                                const llvm::APSInt &From,
                                                const llvm::APSInt &To,
                                                bool InRange) {
   // Convert lower bound
   QualType FromTy;
   llvm::APSInt NewFromInt;
   std::tie(NewFromInt, FromTy) = fixAPSInt(From);
-  Z3Expr FromExp = Solver.fromAPSInt(NewFromInt);
+  SMTExprRef FromExp = Solver.fromAPSInt(NewFromInt);
 
   // Convert symbol
   QualType SymTy;
-  Z3Expr Exp = getZ3Expr(Sym, &SymTy);
+  SMTExprRef Exp = getZ3Expr(Sym, &SymTy);
 
   // Construct single (in)equality
   if (From == To)
     return getZ3BinExpr(Exp, SymTy, InRange ? BO_EQ : BO_NE, FromExp, FromTy,
                         /*RetTy=*/nullptr);
 
   QualType ToTy;
   llvm::APSInt NewToInt;
   std::tie(NewToInt, ToTy) = fixAPSInt(To);
-  Z3Expr ToExp = Solver.fromAPSInt(NewToInt);
+  SMTExprRef ToExp = Solver.fromAPSInt(NewToInt);
   assert(FromTy == ToTy && "Range values have different types!");
 
   // Construct two (in)equalities, and a logical and/or
-  Z3Expr LHS = getZ3BinExpr(Exp, SymTy, InRange ? BO_GE : BO_LT, FromExp,
+  SMTExprRef LHS = getZ3BinExpr(Exp, SymTy, InRange ? BO_GE : BO_LT, FromExp,
                                 FromTy, /*RetTy=*/nullptr);
-  Z3Expr RHS = getZ3BinExpr(Exp, SymTy, InRange ? BO_LE : BO_GT, ToExp, ToTy,
-                            /*RetTy=*/nullptr);
+  SMTExprRef RHS =
+      getZ3BinExpr(Exp, SymTy, InRange ? BO_LE : BO_GT, ToExp, ToTy,
 
   return Solver.fromBinOp(LHS, InRange ? BO_LAnd : BO_LOr, RHS,
                           SymTy->isSignedIntegerOrEnumerationType());
 }
 
 //===------------------------------------------------------------------===//
 // Helper functions.
 //===------------------------------------------------------------------===//
if (Int.getBitWidth() == 1 && getAPSIntType(Int).isNull()) {
     ASTContext &Ctx = getBasicVals().getContext();
     NewInt = Int.extend(Ctx.getTypeSize(Ctx.BoolTy));
   } else
     NewInt = Int;
 
   return std::make_pair(NewInt, getAPSIntType(NewInt));
 }
 
-void Z3ConstraintManager::doTypeConversion(Z3Expr &LHS, Z3Expr &RHS,
+void Z3ConstraintManager::doTypeConversion(SMTExprRef &LHS, SMTExprRef &RHS,
                                            QualType &LTy, QualType &RTy) const {
   ASTContext &Ctx = getBasicVals().getContext();
 
   assert(!LTy.isNull() && !RTy.isNull() && "Input type is null!");
   // Perform type conversion
   if (LTy->isIntegralOrEnumerationType() &&
       RTy->isIntegralOrEnumerationType()) {
     if (LTy->isArithmeticType() && RTy->isArithmeticType())
-      return doIntTypeConversion<Z3Expr, &Z3Solver::fromCast>(LHS, LTy, RHS,
+      return doIntTypeConversion<SMTExprRef, &Z3Solver::fromCast>(LHS, LTy, RHS,
                                                                   RTy);
   } else if (LTy->isRealFloatingType() || RTy->isRealFloatingType()) {
-    return doFloatTypeConversion<Z3Expr, &Z3Solver::fromCast>(LHS, LTy, RHS,
+    return doFloatTypeConversion<SMTExprRef, &Z3Solver::fromCast>(LHS, LTy, RHS,
                                                                   RTy);
   } else if ((LTy->isAnyPointerType() || RTy->isAnyPointerType()) ||
              (LTy->isBlockPointerType() || RTy->isBlockPointerType()) ||
              (LTy->isReferenceType() || RTy->isReferenceType())) {
     // TODO: Refactor to Sema::FindCompositePointerType(), and
     // Sema::CheckCompareOperands().
 
     uint64_t LBitWidth = Ctx.getTypeSize(LTy);
     uint64_t RBitWidth = Ctx.getTypeSize(RTy);