Index: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
===================================================================
--- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
+++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
@@ -218,6 +218,52 @@
     OS << nl;
   }
 
+  bool canReasonAbout(SVal X) const override {
+    const TargetInfo &TI = getBasicVals().getContext().getTargetInfo();
+
+    Optional<nonloc::SymbolVal> SymVal = X.getAs<nonloc::SymbolVal>();
+    if (!SymVal)
+      return true;
+
+    const SymExpr *Sym = SymVal->getSymbol();
+    QualType Ty = Sym->getType();
+
+    // Complex types are not modeled
+    if (Ty->isComplexType() || Ty->isComplexIntegerType())
+      return false;
+
+    // Non-IEEE 754 floating-point types are not modeled
+    if ((Ty->isSpecificBuiltinType(BuiltinType::LongDouble) &&
+         (&TI.getLongDoubleFormat() == &llvm::APFloat::x87DoubleExtended() ||
+          &TI.getLongDoubleFormat() == &llvm::APFloat::PPCDoubleDouble())))
+      return false;
+
+    if (Ty->isRealFloatingType())
+      return Solver->isFPSupported();
+
+    if (isa<SymbolData>(Sym))
+      return true;
+
+    SValBuilder &SVB = getSValBuilder();
+
+    if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym))
+      return canReasonAbout(SVB.makeSymbolVal(SC->getOperand()));
+
+    if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
+      if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE))
+        return canReasonAbout(SVB.makeSymbolVal(SIE->getLHS()));
+
+      if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE))
+        return canReasonAbout(SVB.makeSymbolVal(ISE->getRHS()));
+
+      if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(BSE))
+        return canReasonAbout(SVB.makeSymbolVal(SSE->getLHS())) &&
+               canReasonAbout(SVB.makeSymbolVal(SSE->getRHS()));
+    }
+
+    llvm_unreachable("Unsupported expression to reason about!");
+  }
+
   /// Dumps SMT formula
   LLVM_DUMP_METHOD void dump() const { Solver->dump(); }
 
Index: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h
===================================================================
--- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h
+++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h
@@ -285,6 +285,9 @@
   /// Reset the solver and remove all constraints.
   virtual void reset() = 0;
 
+  /// Checks if the solver supports floating-points.
+  virtual bool isFPSupported() = 0;
+
   virtual void print(raw_ostream &OS) const = 0;
 };
 
Index: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
===================================================================
--- cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
+++ cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
@@ -860,6 +860,8 @@
     return Z3Model(Context, Z3_solver_get_model(Context.Context, Solver));
   }
 
+  bool isFPSupported() override { return true; }
+
   /// Reset the solver and remove all constraints.
   void reset() override { Z3_solver_reset(Context.Context, Solver); }
 
@@ -874,49 +876,6 @@
 public:
   Z3ConstraintManager(SubEngine *SE, SValBuilder &SB)
       : SMTConstraintManager(SE, SB, Solver) {}
-
-  bool canReasonAbout(SVal X) const override {
-    const TargetInfo &TI = getBasicVals().getContext().getTargetInfo();
-
-    Optional<nonloc::SymbolVal> SymVal = X.getAs<nonloc::SymbolVal>();
-    if (!SymVal)
-      return true;
-
-    const SymExpr *Sym = SymVal->getSymbol();
-    QualType Ty = Sym->getType();
-
-    // Complex types are not modeled
-    if (Ty->isComplexType() || Ty->isComplexIntegerType())
-      return false;
-
-    // Non-IEEE 754 floating-point types are not modeled
-    if ((Ty->isSpecificBuiltinType(BuiltinType::LongDouble) &&
-         (&TI.getLongDoubleFormat() == &llvm::APFloat::x87DoubleExtended() ||
-          &TI.getLongDoubleFormat() == &llvm::APFloat::PPCDoubleDouble())))
-      return false;
-
-    if (isa<SymbolData>(Sym))
-      return true;
-
-    SValBuilder &SVB = getSValBuilder();
-
-    if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym))
-      return canReasonAbout(SVB.makeSymbolVal(SC->getOperand()));
-
-    if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
-      if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE))
-        return canReasonAbout(SVB.makeSymbolVal(SIE->getLHS()));
-
-      if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE))
-        return canReasonAbout(SVB.makeSymbolVal(ISE->getRHS()));
-
-      if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(BSE))
-        return canReasonAbout(SVB.makeSymbolVal(SSE->getLHS())) &&
-               canReasonAbout(SVB.makeSymbolVal(SSE->getRHS()));
-    }
-
-    llvm_unreachable("Unsupported expression to reason about!");
-  }
 }; // end class Z3ConstraintManager
 
 } // end anonymous namespace