diff --git a/doc/slides/cprover-overview-latex-beamer/cprover-overview-slides.tex b/doc/slides/cprover-overview-latex-beamer/cprover-overview-slides.tex
index dc111532b7..42799d60c3 100644
--- a/doc/slides/cprover-overview-latex-beamer/cprover-overview-slides.tex
+++ b/doc/slides/cprover-overview-latex-beamer/cprover-overview-slides.tex
@@ -105,8 +105,7 @@
   \node[rectangle,fill=tachameleon!25!white] (solvers) [right of=engine4,xshift=2cm,yshift=-0.5cm]
    {\begin{tikzpicture}[node distance=0.75cm]
     \node[rectangle,fill=tachameleon!50!white] (sat)                { SAT };
-    \node[rectangle,fill=tachameleon!50!white] (smt1) [below of=sat] { SMT1 };
-    \node[rectangle,fill=tachameleon!50!white] (smt2) [below of=smt1] { SMT2 };
+    \node[rectangle,fill=tachameleon!50!white] (smt2) [below of=sat] { SMT2 };
     \node (decproc) [below of=smt2] { \tiny decision procedure };
     \end{tikzpicture}};
 
diff --git a/scripts/vpath-setup.sh b/scripts/vpath-setup.sh
index 3f1cba8a94..f82ac4ece4 100755
--- a/scripts/vpath-setup.sh
+++ b/scripts/vpath-setup.sh
@@ -60,7 +60,7 @@ perl -p -i -e 's/^(irep_ids.cpp:)/#$1/' $DEST/src/util/Makefile
 # create sub-directories
 mkdir -p $DEST/src/ansi-c/library $DEST/src/ansi-c/literals
 mkdir -p $DEST/src/goto-instrument/{accelerate,wmm}
-mkdir -p $DEST/src/solvers/{flattening,floatbv,miniBDD,prop,qbf,refinement,sat,smt1,smt2}
+mkdir -p $DEST/src/solvers/{flattening,floatbv,miniBDD,prop,qbf,refinement,sat,smt2}
 
 # copy generated files for coverage reports
 for f in \
diff --git a/src/solvers/README.md b/src/solvers/README.md
index b70165d3d0..27a67e0c59 100644
--- a/src/solvers/README.md
+++ b/src/solvers/README.md
@@ -35,16 +35,8 @@ different decision procedures, roughly one per directory.
   post-processing function that adds extra constraints. This is not used
   by the SMT2 back-ends.
 
-* dplib/:   Provides the `dplib_dect` object which used the decision
-  procedure library from “Decision Procedures : An Algorithmic Point of
-  View”.
-
-* smt1/:   Provides the `smt1_dect` type which converts the formulae to
-  SMTLib version 1 and then invokes one of Boolector, CVC3, OpenSMT,
-  Yices, MathSAT or Z3. Again, note that this format is depreciated.
-
-* smt2/:   Provides the `smt2_dect` type which functions in a similar
-  way to `smt1_dect`, calling Boolector, CVC3, MathSAT, Yices or Z3.
+* smt2/:   Provides the `smt2_dect` type which converts the formulae to
+  SMTLib 2 and then invokes one of Boolector, CVC3, CVC4, MathSAT, Yices or Z3.
   Note that the interaction with the solver is batched and uses
   temporary files rather than using the interactive command supported by
   SMTLib 2. With the `–fpa` option, this output mode will not flatten