Index: include/clang/StaticAnalyzer/Core/Analyses.def
===================================================================
--- include/clang/StaticAnalyzer/Core/Analyses.def
+++ include/clang/StaticAnalyzer/Core/Analyses.def
@@ -22,6 +22,7 @@
 #endif
 
 ANALYSIS_CONSTRAINTS(RangeConstraints, "range", "Use constraint tracking of concrete value ranges", CreateRangeConstraintManager)
+ANALYSIS_CONSTRAINTS(SMTConstraints, "smt", "Use an SMT solver for constraint tracking", StubCreateSMTConstraintManager)
 
 #ifndef ANALYSIS_DIAGNOSTICS
 #define ANALYSIS_DIAGNOSTICS(NAME, CMDFLAG, DESC, CREATEFN)
Index: include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
===================================================================
--- include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
+++ include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
@@ -152,6 +152,10 @@
 CreateRangeConstraintManager(ProgramStateManager &statemgr,
                              SubEngine *subengine);
 
+std::unique_ptr<ConstraintManager>
+StubCreateSMTConstraintManager(ProgramStateManager& statemgr,
+                               SubEngine *subengine);
+
 } // end GR namespace
 
 } // end clang namespace
Index: lib/StaticAnalyzer/Core/CMakeLists.txt
===================================================================
--- lib/StaticAnalyzer/Core/CMakeLists.txt
+++ lib/StaticAnalyzer/Core/CMakeLists.txt
@@ -37,6 +37,7 @@
   SimpleConstraintManager.cpp
   SimpleSValBuilder.cpp
   Store.cpp
+  StubSMTConstraintManager.cpp
   SubEngine.cpp
   SymbolManager.cpp
 
Index: lib/StaticAnalyzer/Core/SValBuilder.cpp
===================================================================
--- lib/StaticAnalyzer/Core/SValBuilder.cpp
+++ lib/StaticAnalyzer/Core/SValBuilder.cpp
@@ -305,8 +305,9 @@
                                    BinaryOperator::Opcode Op,
                                    NonLoc LHS, NonLoc RHS,
                                    QualType ResultTy) {
-  if (!State->isTainted(RHS) && !State->isTainted(LHS))
-    return UnknownVal();
+  // TODO: Ask the ConstraintManager if it can handle this SymExpr
+  //if (!State->isTainted(RHS) && !State->isTainted(LHS))
+  //  return UnknownVal();
     
   const SymExpr *symLHS = LHS.getAsSymExpr();
   const SymExpr *symRHS = RHS.getAsSymExpr();
Index: lib/StaticAnalyzer/Core/StubSMTConstraintManager.cpp
===================================================================
--- /dev/null
+++ lib/StaticAnalyzer/Core/StubSMTConstraintManager.cpp
@@ -0,0 +1,50 @@
+//== StubSMTConstraintManager.cpp -------------------------------*- 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 implements a stub for CreateSMTConstraintManager() that
+//  simply errors if it is invoked without the plug-in enabled.
+//
+//===----------------------------------------------------------------------===//
+
+#include "clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
+
+#include "llvm/Support/DynamicLibrary.h"
+#include "llvm/Support/ErrorHandling.h"
+
+
+using llvm::sys::DynamicLibrary;
+
+
+namespace clang {
+
+namespace ento {
+
+std::unique_ptr<ConstraintManager>
+StubCreateSMTConstraintManager(ProgramStateManager &StMgr, SubEngine *Eng) {
+  static ConstraintManagerCreator CMCreator = NULL;
+  
+  // Attempt to look up the real CreateSMTConstraintManager implementation;
+  // cache the result for the future. 
+  if (!CMCreator) {
+    CMCreator = (ConstraintManagerCreator)(intptr_t)
+      DynamicLibrary::SearchForAddressOfSymbol("CreateSMTConstraintManager");
+  }
+  
+  if (CMCreator)
+    return CMCreator(StMgr, Eng);
+  
+  llvm::report_fatal_error("The SMT constraint manager plug-in is not loaded.");
+  return NULL;
+}
+
+} // end of namespace ento
+
+} // end of namespace clang
Index: tools/CMakeLists.txt
===================================================================
--- tools/CMakeLists.txt
+++ tools/CMakeLists.txt
@@ -15,6 +15,7 @@
 if(CLANG_ENABLE_STATIC_ANALYZER)
   add_subdirectory(clang-check)
 endif()
+add_subdirectory(smt-constraint-manager)
 
 # We support checking out the clang-tools-extra repository into the 'extra'
 # subdirectory. It contains tools developed as part of the Clang/LLVM project
Index: tools/Makefile
===================================================================
--- tools/Makefile
+++ tools/Makefile
@@ -32,4 +32,9 @@
   OPTIONAL_PARALLEL_DIRS :=
 endif
 
+# Build the SMT constraint manager plug-in if STPPREFIX is set.
+ifdef STPPREFIX
+	DIRS += smt-constraint-manager
+endif
+
 include $(CLANG_LEVEL)/Makefile
Index: tools/smt-constraint-manager/CMakeLists.txt
===================================================================
--- /dev/null
+++ tools/smt-constraint-manager/CMakeLists.txt
@@ -0,0 +1,28 @@
+set(MODULE TRUE)
+
+set( LLVM_LINK_COMPONENTS support mc)
+
+add_library(SMTConstraintManagerPlugin SHARED
+ SMTConstraintManager.cpp)
+
+# add_dependencies(SMTConstraintManagerPlugin
+#   ClangAttrClasses
+#   ClangAttrList
+#   ClangCommentNodes
+#   ClangDeclNodes
+#   ClangDiagnosticCommon
+#   ClangStmtNodes
+#   )
+
+target_link_libraries(SMTConstraintManagerPlugin
+  clangStaticAnalyzerCore
+  )
+
+set_target_properties(SMTConstraintManagerPlugin
+  PROPERTIES
+  LINKER_LANGUAGE CXX
+  PREFIX "")
+
+set (CMAKE_CXX_FLAGS "-std=c++11 -fPIC -pedantic -fno-common -Wcast-qual -fno-strict-aliasing -Wno-long-long -Wall -Wno-unused-parameter -Wwrite-strings -fno-rtti")
+
+set (CMAKE_SHARED_LINKER_FLAGS "-L/usr/local/lib -lstp")
Index: tools/smt-constraint-manager/Makefile
===================================================================
--- /dev/null
+++ tools/smt-constraint-manager/Makefile
@@ -0,0 +1,23 @@
+##===- examples/smt-constraint-manager/Makefile ------------*- Makefile -*-===##
+# 
+#                     The LLVM Compiler Infrastructure
+#
+# This file is distributed under the University of Illinois Open Source
+# License. See LICENSE.TXT for details.
+# 
+##===----------------------------------------------------------------------===##
+
+CLANG_LEVEL := ../..
+LIBRARYNAME = SMTConstraintManagerPlugin
+
+LINK_LIBS_IN_SHARED = 0
+LOADABLE_MODULE = 1
+
+include $(CLANG_LEVEL)/Makefile
+
+ifeq ($(OS),Darwin)
+  LDFLAGS=-Wl,-undefined,dynamic_lookup
+endif
+
+CXXFLAGS+=-I$(STPPREFIX)/include
+LDFLAGS+=-L$(STPPREFIX)/lib -lstp
Index: tools/smt-constraint-manager/README
===================================================================
--- /dev/null
+++ tools/smt-constraint-manager/README
@@ -0,0 +1,51 @@
+This plug-in implements a constraint manager for the Clang Static Analyzer
+backed by the STP constraint solver:
+
+https://sites.google.com/site/stpfastprover/STP-Fast-Prover
+
+
+## Building
+
+Please build and install STP first.
+
+To build this plug-in, pass the path to the STP installation prefix to make(1):
+
+    make ... STPPREFIX=/usr/local
+
+Please note that CMake is not supported at this time.
+
+
+## Usage
+
+Use the plug-in like so (TODO: easier invocation):
+
+   clang -Xclang -load -Xclang path/to/SMTConstraintManagerPlugin.dylib \
+         -Xanalyzer -analyzer-constraints=smt \
+         --analyze ...
+
+
+## Future
+
+This is an incomplete list.
+
+### Changes to Clang
+
+- Refactor the ConstraintManager base class to eliminate
+    VerySimpleConstraintManager
+- Remove StubSMTConstraintManager with plugin support for constraint managers
+- Make SymIntExpr, IntSymExpr, SymSymExpr subclasses of a BinarySymExpr class,
+    to simplify a number of redundancies
+- Implement a UnarySymExpr for bitwise not (~) and unary minus (-) 
+- Generate implicit SymbolCasts
+
+### Changes to SMTConstraintManager
+
+- Abstract away STP to allow other SMT solvers
+- Verify the memory management of STPExprs
+- Avoid constructing a SymExpr in VerySimpleConstraintManager::assumeSymExpr();
+    it's nice, but the temporary SymExpr is never disposed of
+- Reconsider use of container types; replace with LLVM's efficient containers
+    where possible
+- Improve readability with typedefs for complex types
+- Replace ProgramStateTrait code with REGISTER_TRAIT_WITH_PROGRAMSTATE macro
+- Stop using 'Axiom' and 'Constraint' interchangeably
\ No newline at end of file