Index: include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
===================================================================
--- include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
+++ include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
@@ -0,0 +1,43 @@
+//== SMTConstraintManager.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 API, which will be the base class for
+//  every SMT solver specific class.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONSTRAINTMANAGER_H
+#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONSTRAINTMANAGER_H
+
+#include "clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h"
+
+namespace clang {
+namespace ento {
+
+class SMTConstraintManager : public clang::ento::SimpleConstraintManager {
+
+public:
+  SMTConstraintManager(clang::ento::SubEngine *SE, clang::ento::SValBuilder &SB)
+      : SimpleConstraintManager(SE, SB) {}
+  virtual ~SMTConstraintManager() = default;
+
+  /// Converts the ranged constraints of a set of symbols to SMT
+  ///
+  /// \param CR The set of constraints.
+  virtual void addRangeConstraints(clang::ento::ConstraintRangeTy CR) = 0;
+
+  /// Checks if the added constraints are satisfiable
+  virtual clang::ento::ConditionTruthVal isModelFeasible() = 0;
+
+}; // end class SMTConstraintManager
+
+} // namespace ento
+} // namespace clang
+
+#endif
Index: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
===================================================================
--- lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
+++ lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
@@ -10,7 +10,7 @@
 #include "clang/Basic/TargetInfo.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h"
 
 #include "clang/Config/config.h"
 
@@ -880,6 +880,12 @@
 
   /// Reset the solver and remove all constraints.
   void reset() { Z3_solver_reset(Z3Context::ZC, Solver); }
+
+  void print(raw_ostream &OS) const {
+    OS << Z3_solver_to_string(Z3Context::ZC, Solver);
+  }
+
+  LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
 }; // end class Z3Solver
 
 void Z3ErrorHandler(Z3_context Context, Z3_error_code Error) {
@@ -887,16 +893,23 @@
                            llvm::Twine(Z3_get_error_msg_ex(Context, Error)));
 }
 
-class Z3ConstraintManager : public SimpleConstraintManager {
+class Z3ConstraintManager : public SMTConstraintManager {
   Z3Context Context;
   mutable Z3Solver Solver;
 
 public:
   Z3ConstraintManager(SubEngine *SE, SValBuilder &SB)
-      : SimpleConstraintManager(SE, SB),
+      : SMTConstraintManager(SE, SB),
         Solver(Z3_mk_simple_solver(Z3Context::ZC)) {
     Z3_set_error_handler(Z3Context::ZC, Z3ErrorHandler);
   }
+  //===------------------------------------------------------------------===//
+  // Implementation for Refutation.
+  //===------------------------------------------------------------------===//
+
+  void addRangeConstraints(clang::ento::ConstraintRangeTy CR) override;
+
+  ConditionTruthVal isModelFeasible() override;
 
   //===------------------------------------------------------------------===//
   // Implementation for interface from ConstraintManager.
@@ -1242,6 +1255,48 @@
   return State->set<ConstraintZ3>(CZ);
 }
 
+void Z3ConstraintManager::addRangeConstraints(ConstraintRangeTy CR) {
+  for (const auto &I : CR) {
+    SymbolRef Sym = I.first;
+
+    Z3Expr Constraints = Z3Expr::fromBoolean(false);
+
+    for (const auto &Range : I.second) {
+      const llvm::APSInt &From = Range.From();
+      const llvm::APSInt &To = Range.To();
+
+      QualType FromTy;
+      llvm::APSInt NewFromInt;
+      std::tie(NewFromInt, FromTy) = fixAPSInt(From);
+      Z3Expr FromExp = Z3Expr::fromAPSInt(NewFromInt);
+      QualType SymTy;
+      Z3Expr Exp = getZ3Expr(Sym, &SymTy);
+      bool IsSignedTy = SymTy->isSignedIntegerOrEnumerationType();
+      QualType ToTy;
+      llvm::APSInt NewToInt;
+      std::tie(NewToInt, ToTy) = fixAPSInt(To);
+      Z3Expr ToExp = Z3Expr::fromAPSInt(NewToInt);
+      assert(FromTy == ToTy && "Range values have different types!");
+
+      Z3Expr LHS =
+          getZ3BinExpr(Exp, SymTy, BO_GE, FromExp, FromTy, /*RetTy=*/nullptr);
+      Z3Expr RHS =
+          getZ3BinExpr(Exp, SymTy, BO_LE, ToExp, FromTy, /*RetTy=*/nullptr);
+      Z3Expr SymRange = Z3Expr::fromBinOp(LHS, BO_LAnd, RHS, IsSignedTy);
+      Constraints =
+          Z3Expr::fromBinOp(Constraints, BO_LOr, SymRange, IsSignedTy);
+    }
+    Solver.addConstraint(Constraints);
+  }
+}
+
+clang::ento::ConditionTruthVal Z3ConstraintManager::isModelFeasible() {
+  if (Solver.check() == Z3_L_FALSE)
+    return false;
+
+  return ConditionTruthVal();
+}
+
 //===------------------------------------------------------------------===//
 // Internal implementation.
 //===------------------------------------------------------------------===//