diff --git a/README.md b/README.md
index 2b0b3d1..f642a81 100644
--- a/README.md
+++ b/README.md
@@ -40,7 +40,6 @@ Manticore is officially supported on Linux and uses Python 2.7.
 
 - Python Dependencies: Run `pip install -r requirements.txt`
 - Z3 Theorem Prover: Download the latest release for your platform from https://github.com/Z3Prover/z3/releases/latest, and place the enclosed `z3` binary in your `$PATH`.
-  - Alternatively, CVC4 or Yices can be used.
 
 ### development dependencies
 
diff --git a/manticore/core/smtlib/solver.py b/manticore/core/smtlib/solver.py
index 1da0f60..d5dcea7 100644
--- a/manticore/core/smtlib/solver.py
+++ b/manticore/core/smtlib/solver.py
@@ -510,27 +510,4 @@ class Z3Solver(SMTSolver):
         except (IndexError, ValueError, TypeError):
             pass
 
-class Cvc4Solver(SMTSolver):
-    def __init__(self):
-        self.command = 'cvc4 --incremental --lang=smt2'
-        self.init = ['(set-logic QF_AUFBV)', '(set-option :produce-models true)']
-        self.get_value_fmt = (re.compile('\(\((?P<expr>(.*))\ \(_\ bv(?P<value>(\d*))\ \d*\)\)\)'), 10)
-        self.support_simplify =  False
-        self.support_reset = False
-        self.support_maximize = False
-        self.support_minimize = False
-        super(Cvc4Solver, self).__init__()
-
-class YicesSolver(SMTSolver):
-    def __init__(self):
-        self.command = 'yices-smt2 --incremental'
-        self.init = ['(set-logic QF_AUFBV)']
-        self.get_value_fmt = (re.compile('\(\((?P<expr>(.*))\ #b(?P<value>([0-1]*))\)\)'), 2)
-        self.support_simplify = False
-        self.support_reset = True
-        self.support_maximize = False
-        self.support_minimize = False
-        super(YicesSolver, self).__init__()
-
-
 solver = Z3Solver()