Repository: pysmt/pysmt
Pull request #365 (2016-10-13 16:21:59)

Exceptions common ancestor
Added a base class ```PysmtException``` to all the exeption used within pysmt. Also the default exceptions such as ```ValueError``` have been sub-classed to derive from the common ancestor.


Patch:
diff --git a/pysmt/cmd/install.py b/pysmt/cmd/install.py
index c51f485..81cec54 100755
--- a/pysmt/cmd/install.py
+++ b/pysmt/cmd/install.py
@@ -25,6 +25,7 @@ from pysmt.cmd.installers import CVC4Installer, YicesInstaller, BtorInstaller
 from pysmt.cmd.installers import CuddInstaller
 
 from pysmt.environment import get_env
+from pysmt.exceptions import PysmtException
 from pysmt import git_version
 
 # Build a list of installers, one for each solver
@@ -72,7 +73,7 @@ def check_installed(required_solvers, install_dir, bindings_dir, mirror_link):
     pypath_solvers = get_env().factory.all_solvers()
     for solver in required_solvers:
         if solver not in pypath_solvers:
-            raise Exception("Was expecting to find %s installed" % solver)
+            raise PysmtException("Was expecting to find %s installed" % solver)
 
     #
     # Output information
diff --git a/pysmt/configuration.py b/pysmt/configuration.py
index b017c8f..7c8afa4 100644
--- a/pysmt/configuration.py
+++ b/pysmt/configuration.py
@@ -43,6 +43,7 @@ import six.moves.configparser as cp
 from warnings import warn
 
 from pysmt.logics import get_logic_by_name
+from pysmt.exceptions import PysmtIOError
 
 def configure_environment(config_filename, environment):
     """
@@ -52,7 +53,7 @@ def configure_environment(config_filename, environment):
     factory = environment.factory
 
     if not os.path.exists(config_filename):
-        raise IOError("File '%s' does not exists." % config_filename)
+        raise PysmtIOError("File '%s' does not exists." % config_filename)
 
     # We do not use variable inside the config file
     config = cp.RawConfigParser()
diff --git a/pysmt/constants.py b/pysmt/constants.py
index ee3ef5c..099bdb4 100644
--- a/pysmt/constants.py
+++ b/pysmt/constants.py
@@ -16,6 +16,7 @@
 
 import os
 from six import PY2
+from pysmt.exceptions import PysmtImportError
 # The environment variable can be used to force the configuration
 # of the Fraction class.
 #
@@ -38,7 +39,7 @@ try:
     HAS_GMPY = True
 except ImportError as ex:
     if ENV_USE_GMPY is True:
-        raise ex
+        raise PysmtImportError(str(ex))
 
 if ENV_USE_GMPY is False:
     # Explicitely disable GMPY
diff --git a/pysmt/exceptions.py b/pysmt/exceptions.py
index 0acc84f..75494d4 100644
--- a/pysmt/exceptions.py
+++ b/pysmt/exceptions.py
@@ -19,69 +19,74 @@
 
 import pysmt.operators as op
 
-class UnknownSmtLibCommandError(Exception):
+
+class PysmtException(Exception):
+    """Base class for all custom exceptions of pySMT"""
+    pass
+
+class UnknownSmtLibCommandError(PysmtException):
     """Raised when the parser finds an unknown command."""
     pass
 
-class SolverReturnedUnknownResultError(Exception):
+class SolverReturnedUnknownResultError(PysmtException):
     """This exception is raised if a solver returns 'unknown' as a result"""
     pass
 
-class UnknownSolverAnswerError(Exception):
+class UnknownSolverAnswerError(PysmtException):
     """Raised when the a solver returns an invalid response."""
     pass
 
-class NoSolverAvailableError(Exception):
+class NoSolverAvailableError(PysmtException):
     """No solver is available for the selected Logic."""
     pass
 
-class NonLinearError(Exception):
+class NonLinearError(PysmtException):
     """The provided expression is not linear."""
     pass
 
-class UndefinedLogicError(Exception):
+class UndefinedLogicError(PysmtException):
     """This exception is raised if an undefined Logic is attempted to be used."""
     pass
 
-class InternalSolverError(Exception):
+class InternalSolverError(PysmtException):
     """Generic exception to capture errors provided by a solver."""
     pass
 
-class NoLogicAvailableError(Exception):
+class NoLogicAvailableError(PysmtException):
     """Generic exception to capture errors caused by missing support for logics."""
     pass
 
-class SolverRedefinitionError(Exception):
+class SolverRedefinitionError(PysmtException):
     """Exception representing errors caused by multiple defintion of solvers
        having the same name."""
     pass
 
-class SolverNotConfiguredForUnsatCoresError(Exception):
+class SolverNotConfiguredForUnsatCoresError(PysmtException):
     """
     Exception raised if a solver not configured for generating unsat
     cores is required to produce a core.
     """
     pass
 
-class SolverStatusError(Exception):
+class SolverStatusError(PysmtException):
     """
     Exception raised if a method requiring a specific solver status is
     incorrectly called in the wrong status.
     """
     pass
 
-class ConvertExpressionError(Exception):
+class ConvertExpressionError(PysmtException):
     """Exception raised if the converter cannot convert an expression."""
 
     def __init__(self, message=None, expression=None):
-        Exception.__init__(self)
+        PysmtException.__init__(self)
         self.message = message
         self.expression=expression
 
     def __str__(self):
         return self.message
 
-class UnsupportedOperatorError(Exception):
+class UnsupportedOperatorError(PysmtException):
     """The expression contains an operator that is not supported.
 
     The argument node_type contains the unsupported operator id.
@@ -90,7 +95,7 @@ class UnsupportedOperatorError(Exception):
     def __init__(self, message=None, node_type=None, expression=None):
         if message is None:
             message = "Unsupported operator '%s' (node_type: %d)" % (op.op_to_str(node_type), node_type)
-        Exception.__init__(self)
+        PysmtException.__init__(self)
         self.message = message
         self.expression = expression
         self.node_type = node_type
@@ -99,17 +104,37 @@ class UnsupportedOperatorError(Exception):
         return self.message
 
 
-class SolverAPINotFound(Exception):
+class SolverAPINotFound(PysmtException):
     """The Python API of the selected solver cannot be found."""
     pass
 
 
-class UndefinedSymbolError(Exception):
+class UndefinedSymbolError(PysmtException):
     """The given Symbol is not in the FormulaManager."""
 
     def __init__(self, name):
-        Exception.__init__(self)
+        PysmtException.__init__(self)
         self.name = name
 
     def __str__(self):
         return "'%s' is not defined!" % self.name
+
+class PysmtModeError(PysmtException):
+    """The current mode is not supported for this operation"""
+    pass
+
+
+class PysmtImportError(PysmtException, ImportError):
+    pass
+
+class PysmtValueError(PysmtException, ValueError):
+    pass
+
+class PysmtTypeError(PysmtException, TypeError):
+    pass
+
+class PysmtSyntaxError(PysmtException, SyntaxError):
+    pass
+
+class PysmtIOError(PysmtException, IOError):
+    pass
diff --git a/pysmt/fnode.py b/pysmt/fnode.py
index 0228cfe..c77b9d4 100644
--- a/pysmt/fnode.py
+++ b/pysmt/fnode.py
@@ -47,6 +47,7 @@ from pysmt.decorators import deprecated
 from pysmt.utils import twos_complement
 from pysmt.constants import (Fraction, is_python_integer,
                              is_python_rational, is_python_boolean)
+from pysmt.exceptions import PysmtValueError, PysmtModeError
 
 
 FNodeContent = collections.namedtuple("FNodeContent",
@@ -145,8 +146,8 @@ class FNode(object):
                     if not c.is_constant():
                         return False
                 if _type is not None or value is not None:
-                    raise ValueError("constant type and value checking is " \
-                                     "not available for array values")
+                    raise PysmtValueError("constant type and value checking " \
+                                          "is not available for array values")
                 return True
             return False
         if _type is not None:
@@ -657,7 +658,7 @@ class FNode(object):
                 right = mgr.Real(right)
             return function(self, right)
         else:
-            raise Exception("Cannot use infix notation")
+            raise PysmtModeError("Cannot use infix notation")
 
     def Implies(self, right):
         return self._apply_infix(right, _mgr().Implies)
@@ -673,9 +674,9 @@ class FNode(object):
             if isinstance(then_, FNode) and isinstance(else_, FNode):
                 return _mgr().Ite(self, then_, else_)
             else:
-                raise Exception("Cannot infix ITE with implicit argument types.")
+                raise PysmtModeError("Cannot infix ITE with implicit argument types.")
         else:
-            raise Exception("Cannot use infix notation")
+            raise PysmtModeError("Cannot use infix notation")
 
     def And(self, right):
         return self._apply_infix(right, _mgr().And)
@@ -807,14 +808,14 @@ class FNode(object):
 
     def __invert__(self):
         if not _env().enable_infix_notation:
-            raise Exception("Cannot use infix notation")
+            raise PysmtModeError("Cannot use infix notation")
         if _is_bv(self):
             return _mgr().BVNot(self)
         return _mgr().Not(self)
 
     def __getitem__(self, idx):
         if not _env().enable_infix_notation:
-            raise Exception("Cannot use infix notation")
+            raise PysmtModeError("Cannot use infix notation")
         if isinstance(idx, slice):
             end = idx.stop
             start = idx.start
diff --git a/pysmt/formula.py b/pysmt/formula.py
index 518df39..42851d4 100644
--- a/pysmt/formula.py
+++ b/pysmt/formula.py
@@ -35,7 +35,7 @@ import pysmt.typing as types
 import pysmt.operators as op
 
 from pysmt.fnode import FNode, FNodeContent
-from pysmt.exceptions import UndefinedSymbolError
+from pysmt.exceptions import UndefinedSymbolError, PysmtValueError,PysmtTypeError
 from pysmt.walkers.identitydag import IdentityDagWalker
 from pysmt.constants import Fraction
 from pysmt.constants import (is_pysmt_fraction, is_python_rational,
@@ -89,7 +89,7 @@ class FormulaManager(object):
 
     def _create_symbol(self, name, typename=types.BOOL):
         if len(name) == 0:
-            raise ValueError("Empty string is not a valid name")
+            raise PysmtValueError("Empty string is not a valid name")
         n = self.create_node(node_type=op.SYMBOL,
                              args=tuple(),
                              payload=(name, typename))
@@ -121,9 +121,9 @@ class FormulaManager(object):
         if s is None:
             return self._create_symbol(name, typename)
         if not s.symbol_type() == typename:
-            raise TypeError("Trying to redefine symbol '%s' with a new type. "
-                            "Previous type was '%s' new type is '%s'" %
-                            (name, s.symbol_type(), typename))
+            raise PysmtTypeError("Trying to redefine symbol '%s' with a new type"
+                                 ". Previous type was '%s' new type is '%s'" %
+                                 (name, s.symbol_type(), typename))
         return s
 
     # Node definitions start here
@@ -223,7 +223,7 @@ class FormulaManager(object):
         """
         tuple_args = self._polymorph_args_to_tuple(args)
         if len(tuple_args) == 0:
-            raise TypeError("Cannot create a Times without arguments.")
+            raise PysmtTypeError("Cannot create a Times without arguments.")
 
         if len(tuple_args) == 1:
             return tuple_args[0]
@@ -237,7 +237,7 @@ class FormulaManager(object):
         The exponent must be a constant.
         """
         if not exponent.is_constant():
-            raise ValueError("The exponent of POW must be a constant.", exponent)
+            raise PysmtValueError("The exponent of POW must be a constant.", exponent)
 
         if base.is_constant():
             val = base.constant_value() ** exponent.constant_value()
@@ -331,8 +331,8 @@ class FormulaManager(object):
         elif is_python_rational(value):
             val = pysmt_fraction_from_rational(value)
         else:
-            raise TypeError("Invalid type in constant. The type was:" + \
-                            str(type(value)))
+            raise PysmtTypeError("Invalid type in constant. The type was:" + \
+                                 str(type(value)))
 
         n = self.create_node(node_type=op.REAL_CONSTANT,
                              args=tuple(),
@@ -350,8 +350,8 @@ class FormulaManager(object):
         elif is_python_integer(value):
             val = pysmt_integer_from_integer(value)
         else:
-            raise TypeError("Invalid type in constant. The type was:" + \
-                            str(type(value)))
+            raise PysmtTypeError("Invalid type in constant. The type was:" + \
+                                 str(type(value)))
         n = self.create_node(node_type=op.INT_CONSTANT,
                              args=tuple(),
                              payload=val)
@@ -368,7 +368,7 @@ class FormulaManager(object):
 
     def Bool(self, value):
         if type(value) != bool:
-            raise TypeError("Expecting bool, got %s" % type(value))
+            raise PysmtTypeError("Expecting bool, got %s" % type(value))
 
         if value:
             return self.true_formula
@@ -426,7 +426,7 @@ class FormulaManager(object):
         """
         tuple_args = self._polymorph_args_to_tuple(args)
         if len(tuple_args) == 0:
-            raise TypeError("Cannot create a Plus without arguments.")
+            raise PysmtTypeError("Cannot create a Plus without arguments.")
 
         if len(tuple_args) == 1:
             return tuple_args[0]
@@ -446,7 +446,8 @@ class FormulaManager(object):
             return self.create_node(node_type=op.TOREAL,
                                     args=(formula,))
         else:
-            raise TypeError("Argument is of type %s, but INT was expected!\n" % t)
+            raise PysmtTypeError("Argument is of type %s, but INT was "
+                                 "expected!\n" % t)
 
     def AtMostOne(self, *args):
         """ At most one of the bool expressions can be true at anytime.
@@ -551,30 +552,32 @@ class FormulaManager(object):
                 str_width = len(value)
                 value = int(value, 2)
             else:
-                raise ValueError("Expecting binary value as string, got %s" \
-                                 " instead." % value)
+                raise PysmtValueError("Expecting binary value as string, got " \
+                                      "%s instead." % value)
 
             if width is not None and width != str_width:
-                raise ValueError("Specified width does not match string width" \
-                                 " (%d != %d)" % (width, str_width))
+                raise PysmtValueError("Specified width does not match string " \
+                                      "width (%d != %d)" % (width, str_width))
             width = str_width
 
         if width is None:
-            raise ValueError("Need to specify a width for the constant")
+            raise PysmtValueError("Need to specify a width for the constant")
 
         if is_python_integer(value):
             if value < 0:
-                raise ValueError("Cannot specify a negative value: %d" % value)
+                raise PysmtValueError("Cannot specify a negative value: %d" \
+                                      % value)
             if value >= 2**width:
-                raise ValueError("Cannot express %d in %d bits" % (value, width))
+                raise PysmtValueError("Cannot express %d in %d bits" \
+                                      % (value, width))
 
             return self.create_node(node_type=op.BV_CONSTANT,
                                     args=tuple(),
                                     payload=(value, width))
 
         else:
-            raise TypeError("Invalid type in constant. The type was:" + \
-                            str(type(value)))
+            raise PysmtTypeError("Invalid type in constant. The type was:" + \
+                                 str(type(value)))
 
     def SBV(self, value, width=None):
         """Returns a constant of type BitVector interpreting the sign.
@@ -585,16 +588,18 @@ class FormulaManager(object):
         """
         if is_python_integer(value):
             if width is None:
-                raise ValueError("Need to specify a width for the constant")
+                raise PysmtValueError("Need to specify a width for the constant")
 
             min_val = -(2**(width-1))
             max_val = (2**(width-1)) - 1
             if value < min_val:
-                raise ValueError("Cannot represent a value (%d) lower than %d" \
-                                 " in %d bits" % (value, min_val, width))
+                raise PysmtValueError("Cannot represent a value (%d) lower " \
+                                      "than %d in %d bits" % (value, min_val,
+                                                              width))
             if value > max_val:
-                raise ValueError("Cannot represent a value (%d) greater than " \
-                                 "%d in %d bits" % (value, max_val, width))
+                raise PysmtValueError("Cannot represent a value (%d) greater " \
+                                      "than %d in %d bits" % (value, max_val,
+                                                              width))
 
             if value >= 0:
                 return self.BV(value, width)
@@ -731,7 +736,8 @@ class FormulaManager(object):
     def BVRol(self, formula, steps):
         """Returns the LEFT rotation of the BV by the number of steps."""
         if not is_python_integer(steps):
-            raise TypeError("BVRol: 'steps' should be an integer. Got %s" % steps)
+            raise PysmtTypeError("BVRol: 'steps' should be an integer. Got %s" \
+                                 % steps)
         return self.create_node(node_type=op.BV_ROL,
                                 args=(formula,),
                                 payload=(formula.bv_width(), steps))
@@ -739,7 +745,8 @@ class FormulaManager(object):
     def BVRor(self, formula, steps):
         """Returns the RIGHT rotation of the BV by the number of steps."""
         if not is_python_integer(steps):
-            raise TypeError("BVRor: 'steps' should be an integer. Got %s" % steps)
+            raise PysmtTypeError("BVRor: 'steps' should be an integer. Got %s" \
+                                 % steps)
         return self.create_node(node_type=op.BV_ROR,
                                 args=(formula,),
                                 payload=(formula.bv_width(), steps))
@@ -750,7 +757,8 @@ class FormulaManager(object):
         New bits are set to zero.
         """
         if not is_python_integer(increase):
-            raise TypeError("BVZext: 'increase' should be an integer. Got %s" % increase)
+            raise PysmtTypeError("BVZext: 'increase' should be an integer. "
+                                 "Got %s" % increase)
         return self.create_node(node_type=op.BV_ZEXT,
                                 args=(formula,),
                                 payload=(formula.bv_width()+increase,
@@ -762,7 +770,8 @@ class FormulaManager(object):
         New bits are set according to the most-significant-bit.
         """
         if not is_python_integer(increase):
-            raise TypeError("BVSext: 'increase' should be an integer. Got %s" % increase)
+            raise PysmtTypeError("BVSext: 'increase' should be an integer. "
+                                 "Got %s" % increase)
         return self.create_node(node_type=op.BV_SEXT,
                                 args=(formula,),
                                 payload=(formula.bv_width()+increase,
@@ -896,13 +905,14 @@ class FormulaManager(object):
            default and the array is initialized correspondingly.
         """
         if not isinstance(idx_type, types.PySMTType):
-            raise TypeError("idx_type is not a valid type: '%s'" % idx_type)
+            raise PysmtTypeError("idx_type is not a valid type: '%s'" % idx_type)
 
         args = [default]
         if assigned_values:
             for k in sorted(assigned_values, key=id):
                 if not k.is_constant():
-                    raise ValueError("Array initialization indexes must be constants")
+                    raise PysmtValueError("Array initialization indexes must "
+                                          "be constants")
                 # It is useless to represent assignments equal to the default
                 if assigned_values[k] != default:
                     args.append(k)
diff --git a/pysmt/parsing.py b/pysmt/parsing.py
index b0f13d2..84c438a 100644
--- a/pysmt/parsing.py
+++ b/pysmt/parsing.py
@@ -20,6 +20,7 @@ from collections import namedtuple
 
 import pysmt.typing as types
 from pysmt.environment import get_env
+from pysmt.exceptions import PysmtSyntaxError, UndefinedSymbolError
 from pysmt.constants import Fraction
 
 
@@ -59,7 +60,7 @@ class Lexer(object):
         self.scanner = re.compile("|".join(rule.regex for rule in self.rules),
                                   re.DOTALL | re.VERBOSE)
     def lexing_error(self, read):
-        raise SyntaxError("Unexpected input: %s" % read)
+        raise PysmtSyntaxError("Unexpected input: %s" % read)
 
     def tokenize(self, data):
         """The token generator for the given string"""
@@ -88,10 +89,10 @@ class GrammarSymbol(object):
         self.payload = payload
 
     def nud(self, parser):
-        raise SyntaxError("Syntax error at token '%s'." % parser.token)
+        raise PysmtSyntaxError("Syntax error at token '%s'." % parser.token)
 
     def led(self, parser, left):
-        raise SyntaxError("Syntax error at token '%s' (Read: '%s')." % \
+        raise PysmtSyntaxError("Syntax error at token '%s' (Read: '%s')." % \
                           (parser.token, left))
 
 #
@@ -254,7 +255,7 @@ class HRLexer(Lexer):
             if b.is_constant():
                 return op(a, b.constant_value())
             else:
-                raise SyntaxError("Constant expected, got '%s'" % b)
+                raise PysmtSyntaxError("Constant expected, got '%s'" % b)
         return _res
 
 # EOC HRLexer
@@ -320,7 +321,7 @@ class Identifier(GrammarSymbol):
         GrammarSymbol.__init__(self)
         self.value = env.formula_manager.get_symbol(name)
         if self.value is None:
-            raise ValueError("Undefined symbol: '%s'" % name)
+            raise UndefinedSymbolError(name)
 
     def nud(self, parser):
         return self.value
@@ -411,7 +412,7 @@ class OpenBrak(GrammarSymbol):
             parser.expect(CloseBrak, "]")
             return parser.mgr.Store(op, e1, e2)
         else:
-            raise SyntaxError("Unexpected token:" + str(parser.token))
+            raise PysmtSyntaxError("Unexpected token:" + str(parser.token))
 
 
 class Quantifier(GrammarSymbol):
@@ -479,8 +480,8 @@ class PrattParser(object):
         result = self.expression()
         try:
             bd = next(self.tokenizer)
-            raise SyntaxError("Bogus data after expression: '%s' (Partial: %s)" \
-                              % (bd, result))
+            raise PysmtSyntaxError("Bogus data after expression: '%s' "
+                                   "(Partial: %s)" % (bd, result))
         except StopIteration:
             return result
 
@@ -495,7 +496,7 @@ class PrattParser(object):
         ParserError
         """
         if type(self.token) != token_class:
-            raise SyntaxError("Expected '%s'" % token_repr)
+            raise PysmtSyntaxError("Expected '%s'" % token_repr)
         self.advance()
 
 # EOC PrattParser
diff --git a/pysmt/simplifier.py b/pysmt/simplifier.py
index 2aa2834..513ca4a 100644
--- a/pysmt/simplifier.py
+++ b/pysmt/simplifier.py
@@ -21,6 +21,7 @@ import pysmt.walkers
 import pysmt.operators as op
 import pysmt.typing as types
 from pysmt.utils import set_bit
+from pysmt.exceptions import PysmtValueError
 
 
 class Simplifier(pysmt.walkers.DagWalker):
@@ -722,7 +723,8 @@ class BddSimplifier(Simplifier):
         possible_solvers = [sname for sname in self.env.factory.all_solvers()\
                             if sname!="bdd"]
         if len(possible_solvers) == 0:
-            raise ValueError("To validate at least another solver must be available!")
+            raise PysmtValueError("To validate at least another solver must "
+                                  "be available!")
         self._validation_sname = possible_solvers[0]
         self._validate_simplifications = value
 
diff --git a/pysmt/smtlib/parser.py b/pysmt/smtlib/parser.py
index 774f577..e5a909f 100644
--- a/pysmt/smtlib/parser.py
+++ b/pysmt/smtlib/parser.py
@@ -26,7 +26,7 @@ import pysmt.smtlib.commands as smtcmd
 from pysmt.environment import get_env
 from pysmt.typing import BOOL, REAL, INT, FunctionType, BVType, ArrayType
 from pysmt.logics import get_logic_by_name, UndefinedLogicError
-from pysmt.exceptions import UnknownSmtLibCommandError
+from pysmt.exceptions import UnknownSmtLibCommandError, PysmtSyntaxError
 from pysmt.smtlib.script import SmtLibCommand, SmtLibScript
 from pysmt.smtlib.annotations import Annotations
 from pysmt.utils import interactive_char_iterator
@@ -172,12 +172,13 @@ def tokenizer(handle, interactive=False):
                             c = next(reader)
                             if c != "|" and c != "\\":
                                 # Only \| and \\ are supported escapings
-                                raise SyntaxError("Unknown escaping in " \
-                                                  "quoted symbol: '\\%s'" % c)
+                                raise PysmtSyntaxError("Unknown escaping in " \
+                                                       "quoted symbol: "
+                                                       "'\\%s'" % c)
                         s.append(c)
                         c = next(reader)
                     if not c:
-                        raise SyntaxError("Expected '|'")
+                        raise PysmtSyntaxError("Expected '|'")
                     yield "".join(s)
                     c = next(reader)
 
@@ -197,7 +198,7 @@ def tokenizer(handle, interactive=False):
                             s.append(c)
                             c = next(reader)
                     if not c:
-                        raise SyntaxError("Expected '|'")
+                        raise PysmtSyntaxError("Expected '|'")
                     yield '"%s"' % ("".join(s)) # string literals maintain their quoting
 
                 else:
@@ -373,7 +374,7 @@ class SmtLibParser(object):
         #pylint: disable=unused-argument
         const = self.parse_atom(tokens, "expression")
         if const != "const":
-            raise SyntaxError("expected 'const' in expression after 'as'")
+            raise PysmtSyntaxError("expected 'const' in expression after 'as'")
         tyname = self.parse_type(tokens, "expression")
         ty = self._get_basic_type(tyname)
 
@@ -399,7 +400,8 @@ class SmtLibParser(object):
                 start = int(sstart)
                 end = int(send)
             except ValueError:
-                raise SyntaxError("Expected number in '_ extract' expression")
+                raise PysmtSyntaxError("Expected number in '_ extract' "
+                                       "expression")
             fun = lambda x : mgr.BVExtract(x, start, end)
 
         elif op == "zero_extend":
@@ -407,7 +409,8 @@ class SmtLibParser(object):
             try:
                 width = int(swidth)
             except ValueError:
-                raise SyntaxError("Expected number in '_ zero_extend' expression")
+                raise PysmtSyntaxError("Expected number in '_ zero_extend' "
+                                       "expression")
             fun = lambda x: mgr.BVZExt(x, width)
 
         elif op == "repeat":
@@ -415,7 +418,8 @@ class SmtLibParser(object):
             try:
                 count = int(scount)
             except ValueError:
-                raise SyntaxError("Expected number in '_ repeat' expression")
+                raise PysmtSyntaxError("Expected number in '_ repeat' "
+                                       "expression")
             fun = lambda x: mgr.BVRepeat(x, count)
 
         elif op == "rotate_left":
@@ -423,7 +427,8 @@ class SmtLibParser(object):
             try:
                 step = int(sstep)
             except ValueError:
-                raise SyntaxError("Expected number in '_ rotate_left' expression")
+                raise PysmtSyntaxError("Expected number in '_ rotate_left' "
+                                       "expression")
             fun = lambda x: mgr.BVRol(x, step)
 
         elif op == "rotate_right":
@@ -431,7 +436,8 @@ class SmtLibParser(object):
             try:
                 step = int(sstep)
             except ValueError:
-                raise SyntaxError("Expected number in '_ rotate_left' expression")
+                raise PysmtSyntaxError("Expected number in '_ rotate_left' "
+                                       "expression")
             fun = lambda x: mgr.BVRor(x, step)
 
         elif op == "sign_extend":
@@ -439,7 +445,8 @@ class SmtLibParser(object):
             try:
                 width = int(swidth)
             except ValueError:
-                raise SyntaxError("Expected number in '(_ sign_extend) expression'")
+                raise PysmtSyntaxError("Expected number in '(_ sign_extend) "
+                                       "expression'")
             fun = lambda x: mgr.BVSExt(x, width)
 
         elif op.startswith("bv"):
@@ -447,11 +454,12 @@ class SmtLibParser(object):
                 v = int(op[2:])
                 width = int(self.parse_atom(tokens, "expression"))
             except ValueError:
-                raise SyntaxError("Expected number in '_ bv' expression: '%s'" % op)
+                raise PysmtSyntaxError("Expected number in '_ bv' expression: "
+                                       "'%s'" % op)
             fun = mgr.BV(v, width)
 
         else:
-            raise SyntaxError("Unexpected '_' expression '%s'" % op)
+            raise PysmtSyntaxError("Unexpected '_' expression '%s'" % op)
 
         # Consume the closed parenthesis of the (_ ...) term and add the
         # resulting function to the correct level in the stack
@@ -531,7 +539,8 @@ class SmtLibParser(object):
                     value = int("0" + token[1:], 2)
                 else:
                     if token[1] != "x":
-                        raise SyntaxError("Invalid bit-vector constant '%s'" % token)
+                        raise PysmtSyntaxError("Invalid bit-vector constant "
+                                               "'%s'" % token)
                     width = (len(token) - 2) * 16
                     value = int("0" + token[1:], 16)
                 res = mgr.BV(value, width)
@@ -584,13 +593,15 @@ class SmtLibParser(object):
             if i+1 < len(attrs) and str(attrs[i+1])[0] != ":" :
                 key, value = str(attrs[i]), str(attrs[i+1])
                 if key[0] != ":":
-                    raise SyntaxError("Annotations keys should start with colon")
+                    raise PysmtSyntaxError("Annotations keys should start "
+                                           "with colon")
                 self.cache.annotations.add(pyterm, key[1:], value)
                 i += 2
             else:
                 key = str(attrs[i])
                 if key[0] != ":":
-                    raise SyntaxError("Annotations keys should start with colon")
+                    raise PysmtSyntaxError("Annotations keys should start "
+                                           "with colon")
                 self.cache.annotations.add(pyterm, key[1:])
                 i += 1
 
@@ -607,7 +618,7 @@ class SmtLibParser(object):
         self.consume_opening(tokens, "expression")
         while current != ")":
             if current != "(":
-                raise SyntaxError("Expected '(' in let binding")
+                raise PysmtSyntaxError("Expected '(' in let binding")
             vname = self.parse_atom(tokens, "expression")
             expr = self.get_expression(tokens)
             newvals[vname] = expr
@@ -636,7 +647,7 @@ class SmtLibParser(object):
         self.consume_opening(tokens, "expression")
         while current != ")":
             if current != "(":
-                raise SyntaxError("Expected '(' in let binding")
+                raise PysmtSyntaxError("Expected '(' in let binding")
             vname = self.parse_atom(tokens, "expression")
             typename = self.parse_type(tokens, "expression")
 
@@ -690,7 +701,7 @@ class SmtLibParser(object):
                     lst = stack.pop()
                     fun = lst.pop(0)
                 except IndexError:
-                    raise SyntaxError("Unexpected ')'")
+                    raise PysmtSyntaxError("Unexpected ')'")
 
                 try:
                     res = fun(*lst)
@@ -714,7 +725,8 @@ class SmtLibParser(object):
 
     def get_script(self, script):
         """
-        Takes a file object and returns a SmtLibScript object representing the file
+        Takes a file object and returns a SmtLibScript object representing
+        the file
         """
         self._reset() # prepare the parser
         res = SmtLibScript()
@@ -753,10 +765,12 @@ class SmtLibParser(object):
         for _ in xrange(min_size):
             current = next(tokens)
             if current == ")":
-                raise SyntaxError("Expected at least %d arguments in %s command." %\
+                raise PysmtSyntaxError("Expected at least %d arguments in "
+                                       "%s command." %\
                                   (min_size, command))
             if current == "(":
-                raise SyntaxError("Unexpected token '(' in %s command." % command)
+                raise PysmtSyntaxError("Unexpected token '(' in %s "
+                                       "command." % command)
             res.append(current)
 
         for _ in xrange(min_size, max_size + 1):
@@ -764,10 +778,12 @@ class SmtLibParser(object):
             if current == ")":
                 return res
             if current == "(":
-                raise SyntaxError("Unexpected token '(' in %s command." % command)
+                raise PysmtSyntaxError("Unexpected token '(' in %s "
+                                       "command." % command)
             res.append(current)
-        raise SyntaxError("Unexpected token '%s' in %s command. Expected at " \
-                          "most %d arguments." % (current, command, max_size))
+        raise PysmtSyntaxError("Unexpected token '%s' in %s command. Expected " \
+                               "at most %d arguments." % (current, command,
+                                                          max_size))
 
 
     def parse_type(self, tokens, command, additional_token=None):
@@ -786,11 +802,11 @@ class SmtLibParser(object):
                 return ("Array", idxtype, elemtype)
 
             if op != "_":
-                raise SyntaxError("Unexpected token '%s' in %s command." % \
+                raise PysmtSyntaxError("Unexpected token '%s' in %s command." % \
                                   (op, command))
             ts = next(tokens)
             if ts != "BitVec":
-                raise SyntaxError("Unexpected token '%s' in %s command." % \
+                raise PysmtSyntaxError("Unexpected token '%s' in %s command." % \
                                   (ts, command))
 
             size = 0
@@ -798,14 +814,14 @@ class SmtLibParser(object):
             try:
                 size = int(dim)
             except ValueError:
-                raise SyntaxError("Unexpected token '%s' in %s command." % \
+                raise PysmtSyntaxError("Unexpected token '%s' in %s command." % \
                                   (dim, command))
 
             self.consume_closing(tokens, command)
             return "BV%d" % size
 
         elif var == ")":
-            raise SyntaxError("Unexpected token '%s' in %s command." % \
+            raise PysmtSyntaxError("Unexpected token '%s' in %s command." % \
                               (var, command))
         return var
 
@@ -814,7 +830,7 @@ class SmtLibParser(object):
         """Parses a single name from the tokens"""
         var = next(tokens)
         if var == "(" or var == ")":
-            raise SyntaxError("Unexpected token '%s' in %s command." % \
+            raise PysmtSyntaxError("Unexpected token '%s' in %s command." % \
                               (var, command))
         return var
 
@@ -849,21 +865,21 @@ class SmtLibParser(object):
             try:
                 current = self.get_expression(tokens)
                 res.append(current)
-            except SyntaxError:
+            except PysmtSyntaxError:
                 return res
 
     def consume_opening(self, tokens, command):
         """ Consumes a single '(' """
         p = next(tokens)
         if p != "(":
-            raise SyntaxError("Unexpected token '%s' in %s command. " \
+            raise PysmtSyntaxError("Unexpected token '%s' in %s command. " \
                               "Expected '('" % (p, command))
 
     def consume_closing(self, tokens, command):
         """ Consumes a single ')' """
         p = next(tokens)
         if p != ")":
-            raise SyntaxError("Unexpected token '%s' in %s command. " \
+            raise PysmtSyntaxError("Unexpected token '%s' in %s command. " \
                               "Expected ')'" % (p, command))
 
     def _function_call_helper(self, v, *args):
@@ -883,7 +899,7 @@ class SmtLibParser(object):
         current = next(tokens)
         while current != ")":
             if current != "(":
-                raise SyntaxError("'(' expected")
+                raise PysmtSyntaxError("'(' expected")
             vname = self.get_expression(tokens)
             expr = self.get_expression(tokens)
             self.consume_closing(tokens, current)
@@ -1123,8 +1139,10 @@ class SmtLibZ3Parser(SmtLibParser):
 
         # Z3 prints Pow as "^"
         self.interpreted["^"] = self.interpreted["pow"]
-        self.interpreted["ext_rotate_left"] = self._operator_adapter(self._ext_rotate_left)
-        self.interpreted["ext_rotate_right"] = self._operator_adapter(self._ext_rotate_right)
+        self.interpreted["ext_rotate_left"] = \
+                                self._operator_adapter(self._ext_rotate_left)
+        self.interpreted["ext_rotate_right"] =\
+                                self._operator_adapter(self._ext_rotate_right)
 
     def _ext_rotate_left(self, x, y):
         return self.env.formula_manager.BVRol(x, y.simplify().constant_value())
diff --git a/pysmt/smtlib/script.py b/pysmt/smtlib/script.py
index 14807e2..3073f73 100644
--- a/pysmt/smtlib/script.py
+++ b/pysmt/smtlib/script.py
@@ -23,7 +23,7 @@ from six.moves import xrange
 
 import pysmt.smtlib.commands as smtcmd
 from pysmt.exceptions import (UnknownSmtLibCommandError, NoLogicAvailableError,
-                              UndefinedLogicError)
+                              UndefinedLogicError, PysmtValueError)
 from pysmt.smtlib.printers import SmtPrinter, SmtDagPrinter, quote
 from pysmt.oracles import get_logic
 from pysmt.logics import get_closer_smtlib_logic, Logic, SMTLIB2_LOGICS
@@ -170,8 +170,9 @@ class SmtLibScript(object):
     def get_strict_formula(self, mgr=None):
         if self.contains_command(smtcmd.PUSH) or \
            self.contains_command(smtcmd.POP):
-            raise Exception("Was not expecting push-pop commands")
-        assert self.count_command_occurrences(smtcmd.CHECK_SAT) == 1
+            raise PysmtValueError("Was not expecting push-pop commands")
+        if self.count_command_occurrences(smtcmd.CHECK_SAT) != 1:
+            raise PysmtValueError("Was expecting exactly one check-sat command")
         _And = mgr.And if mgr else get_env().formula_manager.And
 
         assertions = [cmd.args[0]
diff --git a/pysmt/smtlib/solver.py b/pysmt/smtlib/solver.py
index 177511c..3738537 100644
--- a/pysmt/smtlib/solver.py
+++ b/pysmt/smtlib/solver.py
@@ -24,7 +24,7 @@ from pysmt.smtlib.parser import SmtLibParser
 from pysmt.smtlib.script import SmtLibCommand
 from pysmt.solvers.solver import Solver, SolverOptions
 from pysmt.exceptions import (SolverReturnedUnknownResultError,
-                              UnknownSolverAnswerError)
+                              UnknownSolverAnswerError, PysmtValueError)
 
 
 class SmtLibOptions(SolverOptions):
@@ -36,7 +36,7 @@ class SmtLibOptions(SolverOptions):
     def __init__(self, **base_options):
         SolverOptions.__init__(self, **base_options)
         if self.unsat_cores_mode is not None:
-            raise ValueError("'unsat_cores_mode' option not supported.")
+            raise PysmtValueError("'unsat_cores_mode' option not supported.")
         self.debug_interaction = False
 
         if 'debug_interaction' in self.solver_options:
@@ -58,7 +58,7 @@ class SmtLibOptions(SolverOptions):
 
         for k,v in self.solver_options.items():
             if k in (':print-success', 'diagnostic-output-channel'):
-                raise ValueError("Cannot override %s." % k)
+                raise PysmtValueError("Cannot override %s." % k)
             solver.set_option(k, str(v))
 
 # EOC SmtLibOptions
diff --git a/pysmt/solvers/bdd.py b/pysmt/solvers/bdd.py
index 31a3eb1..184ef19 100644
--- a/pysmt/solvers/bdd.py
+++ b/pysmt/solvers/bdd.py
@@ -30,7 +30,8 @@ from pysmt.solvers.solver import Solver, Converter, SolverOptions
 from pysmt.solvers.eager import EagerModel
 from pysmt.walkers import DagWalker
 from pysmt.decorators import clear_pending_pop, catch_conversion_error
-from pysmt.exceptions import ConvertExpressionError
+from pysmt.exceptions import (ConvertExpressionError, PysmtValueError,
+                              PysmtTypeError)
 from pysmt.oracles import get_logic
 from pysmt.solvers.qelim import QuantifierEliminator
 
@@ -79,9 +80,9 @@ class BddOptions(SolverOptions):
         SolverOptions.__init__(self, **base_options)
 
         if self.random_seed is not None:
-            raise ValueError("'random_seed' option not supported.")
+            raise PysmtValueError("'random_seed' option not supported.")
         if self.unsat_cores_mode is not None:
-            raise ValueError("'unsat_cores_mode' option not supported.")
+            raise PysmtValueError("'unsat_cores_mode' option not supported.")
 
         for k,v in self.solver_options.items():
             if k == "static_ordering":
@@ -91,18 +92,18 @@ class BddOptions(SolverOptions):
                     except:
                         valid = False
                     if not valid:
-                        raise ValueError("The BDD static ordering must be a " \
-                                         "list of Boolean variables")
+                        raise PysmtValueError("The BDD static ordering must be" \
+                                              " a list of Boolean variables")
             elif k == "dynamic_reordering":
                 if v not in (True, False):
-                    raise ValueError("Invalid value %s for '%s'" % \
-                                     (str(k),str(v)))
+                    raise PysmtValueError("Invalid value %s for '%s'" % \
+                                          (str(k),str(v)))
             elif k == "reordering_algorithm":
                 if v not in BddOptions.CUDD_ALL_REORDERING_ALGORITHMS:
-                    raise ValueError("Invalid value %s for '%s'" % \
-                                     (str(k),str(v)))
+                    raise PysmtValueError("Invalid value %s for '%s'" % \
+                                          (str(k),str(v)))
             else:
-                raise ValueError("Unrecognized option '%s'." % k)
+                raise PysmtValueError("Unrecognized option '%s'." % k)
             # Store option
             setattr(self, k, v)
 
@@ -119,7 +120,8 @@ class BddOptions(SolverOptions):
 
         # Consistency check
         if not self.dynamic_reordering and self.reordering_algorithm is not None:
-            raise ValueError("reordering_algorithm requires dynamic_reordering.")
+            raise PysmtValueError("reordering_algorithm requires "
+                                  "dynamic_reordering.")
 
     def __call__(self, solver):
         # Impose initial ordering
@@ -285,7 +287,9 @@ class BddConverter(Converter, DagWalker):
         return cube
 
     def declare_variable(self, var):
-        if not var.is_symbol(type_=types.BOOL): raise TypeError
+        if not var.is_symbol(type_=types.BOOL):
+            raise PysmtTypeError("Trying to declare as a variable something "
+                                 "that is not a symbol: %s" % var)
         if var not in self.var2node:
             node = self.ddmanager.NewVar()
             self.idx2var[node.NodeReadIndex()] = var
diff --git a/pysmt/solvers/btor.py b/pysmt/solvers/btor.py
index d454dfc..2973547 100644
--- a/pysmt/solvers/btor.py
+++ b/pysmt/solvers/btor.py
@@ -31,7 +31,7 @@ from pysmt.solvers.smtlib import SmtLibBasicSolver, SmtLibIgnoreMixin
 from pysmt.solvers.eager import EagerModel
 from pysmt.walkers import DagWalker
 from pysmt.exceptions import (SolverReturnedUnknownResultError,
-                              ConvertExpressionError)
+                              ConvertExpressionError, PysmtValueError)
 from pysmt.decorators import clear_pending_pop, catch_conversion_error
 from pysmt.logics import QF_BV, QF_UFBV, QF_ABV, QF_AUFBV, QF_AX
 
@@ -40,7 +40,7 @@ class BoolectorOptions(SolverOptions):
     def __init__(self, **base_options):
         SolverOptions.__init__(self, **base_options)
         if self.random_seed is not None:
-            raise ValueError("BTOR Does not support Random Seed setting.")
+            raise PysmtValueError("BTOR Does not support Random Seed setting.")
 
         # Disabling Incremental usage is not allowed.
         # This needs to be set to 1
@@ -51,9 +51,11 @@ class BoolectorOptions(SolverOptions):
         try:
             btor.Set_opt(name, value)
         except TypeError:
-            raise ValueError("Error setting the option '%s=%s'" % (name,value))
+            raise PysmtValueError("Error setting the option '%s=%s'" \
+                                  % (name,value))
         except boolector.BoolectorException:
-            raise ValueError("Error setting the option '%s=%s'" % (name,value))
+            raise PysmtValueError("Error setting the option '%s=%s'" \
+                                  % (name,value))
 
     def __call__(self, solver):
         if self.generate_models:
diff --git a/pysmt/solvers/cvc4.py b/pysmt/solvers/cvc4.py
index 3ab13bf..ee32390 100644
--- a/pysmt/solvers/cvc4.py
+++ b/pysmt/solvers/cvc4.py
@@ -30,7 +30,8 @@ from pysmt.logics import PYSMT_LOGICS, ARRAYS_CONST_LOGICS
 from pysmt.solvers.solver import Solver, Converter, SolverOptions
 from pysmt.exceptions import (SolverReturnedUnknownResultError,
                               InternalSolverError,
-                              NonLinearError)
+                              NonLinearError, PysmtValueError,
+                              PysmtTypeError)
 from pysmt.walkers import DagWalker
 from pysmt.solvers.smtlib import SmtLibBasicSolver, SmtLibIgnoreMixin
 from pysmt.solvers.eager import EagerModel
@@ -45,14 +46,14 @@ class CVC4Options(SolverOptions):
         # TODO: CVC4 Supports UnsatCore extraction
         # but we did not wrapped it yet. (See #349)
         if self.unsat_cores_mode is not None:
-            raise ValueError("'unsat_cores_mode' option not supported.")
+            raise PysmtValueError("'unsat_cores_mode' option not supported.")
 
     @staticmethod
     def _set_option(cvc4, name, value):
         try:
             cvc4.setOption(name, CVC4.SExpr(value))
         except:
-            raise ValueError("Error setting the option '%s=%s'" % (name,value))
+            raise PysmtValueError("Error setting the option '%s=%s'" % (name,value))
 
     def __call__(self, solver):
         self._set_option(solver.cvc4,
@@ -198,7 +199,8 @@ class CVC4Converter(Converter, DagWalker):
 
     def declare_variable(self, var):
         if not var.is_symbol():
-            raise TypeError
+            raise PysmtTypeError("Trying to declare as a variable something "
+                                 "that is not a symbol: %s" % var)
         if var.symbol_name() not in self.declared_vars:
             cvc4_type = self._type_to_cvc4(var.symbol_type())
             decl = self.mkVar(var.symbol_name(), cvc4_type)
@@ -228,10 +230,10 @@ class CVC4Converter(Converter, DagWalker):
                 res = self.mgr.Array(array_type.index_type,
                                      base_value)
             else:
-                raise TypeError("Unsupported constant type:",
-                                expr.getType().toString())
+                raise PysmtTypeError("Unsupported constant type:",
+                                     expr.getType().toString())
         else:
-            raise TypeError("Unsupported expression:", expr.toString())
+            raise PysmtTypeError("Unsupported expression:", expr.toString())
 
         return res
 
diff --git a/pysmt/solvers/eager.py b/pysmt/solvers/eager.py
index df4d0a8..89b767b 100644
--- a/pysmt/solvers/eager.py
+++ b/pysmt/solvers/eager.py
@@ -17,6 +17,7 @@
 #
 from pysmt.solvers.solver import Model
 from pysmt.environment import get_env
+from pysmt.exceptions import PysmtTypeError
 
 
 class EagerModel(Model):
@@ -47,7 +48,7 @@ class EagerModel(Model):
 
         res = r.simplify()
         if not res.is_constant():
-            raise TypeError("Was expecting a constant but got %s" % res)
+            raise PysmtTypeError("Was expecting a constant but got %s" % res)
         return res
 
 
@@ -58,7 +59,7 @@ class EagerModel(Model):
 
         for s in undefined_symbols:
             if not s.is_symbol():
-                raise TypeError("Was expecting a symbol but got %s" %s)
+                raise PysmtTypeError("Was expecting a symbol but got %s" %s)
 
             if s.symbol_type().is_bool_type():
                 value = mgr.Bool(False)
@@ -69,8 +70,8 @@ class EagerModel(Model):
             elif s.symbol_type().is_bv_type():
                 value = mgr.BVZero(s.bv_width())
             else:
-                raise TypeError("Unhandled type for %s: %s" %
-                                (s, s.symbol_type()))
+                raise PysmtTypeError("Unhandled type for %s: %s" %
+                                     (s, s.symbol_type()))
 
             self.completed_assignment[s] = value
 
diff --git a/pysmt/solvers/msat.py b/pysmt/solvers/msat.py
index 93ddd6e..641fd5c 100644
--- a/pysmt/solvers/msat.py
+++ b/pysmt/solvers/msat.py
@@ -39,7 +39,7 @@ from pysmt.exceptions import (SolverReturnedUnknownResultError,
                               SolverNotConfiguredForUnsatCoresError,
                               SolverStatusError,
                               InternalSolverError,
-                              NonLinearError)
+                              NonLinearError, PysmtValueError, PysmtTypeError)
 from pysmt.decorators import clear_pending_pop, catch_conversion_error
 from pysmt.solvers.qelim import QuantifierEliminator
 from pysmt.solvers.interpolation import Interpolator
@@ -144,7 +144,7 @@ class MathSATOptions(SolverOptions):
         """Sets the given option. Might raise a ValueError."""
         check = mathsat.msat_set_option(msat_config, name, value)
         if check != 0:
-            raise ValueError("Error setting the option '%s=%s'" % (name,value))
+            raise PysmtValueError("Error setting the option '%s=%s'" % (name,value))
 
     def __call__(self, solver):
         if self.generate_models:
@@ -546,8 +546,8 @@ class MSatConverter(Converter, DagWalker):
             return types.FunctionType(pyty, [self.env.stc.get_type(args[0])])
 
         else:
-            raise TypeError("Unsupported expression:",
-                            mathsat.msat_term_repr(term))
+            raise PysmtTypeError("Unsupported expression:",
+                                 mathsat.msat_term_repr(term))
         return res
 
     def _back_single_term(self, term, mgr, args):
@@ -780,8 +780,8 @@ class MSatConverter(Converter, DagWalker):
             res = mgr.Array(pyty.index_type, args[0])
 
         else:
-            raise TypeError("Unsupported expression:",
-                            mathsat.msat_term_repr(term))
+            raise PysmtTypeError("Unsupported expression:",
+                                 mathsat.msat_term_repr(term))
         return res
 
     def get_symbol_from_declaration(self, decl):
@@ -1126,7 +1126,9 @@ class MSatConverter(Converter, DagWalker):
 
 
     def declare_variable(self, var):
-        if not var.is_symbol(): raise TypeError(var)
+        if not var.is_symbol():
+            raise PysmtTypeError("Trying to declare as a variable something "
+                                 "that is not a symbol: %s" % var)
         if var.symbol_name() not in self.symbol_to_decl:
             tp = self._type_to_msat(var.symbol_type())
             decl = mathsat.msat_declare_function(self.msat_env(),
@@ -1152,7 +1154,7 @@ if hasattr(mathsat, "MSAT_EXIST_ELIM_ALLSMT_FM"):
             lw: Loos-Weisspfenning
             """
             if algorithm not in ['fm', 'lw']:
-                raise ValueError("Algorithm can be either 'fm' or 'lw'")
+                raise PysmtValueError("Algorithm can be either 'fm' or 'lw'")
             QuantifierEliminator.__init__(self)
             IdentityDagWalker.__init__(self, env=environment)
             self.msat_config = mathsat.msat_create_default_config("QF_LRA")
@@ -1251,7 +1253,7 @@ class MSatInterpolator(Interpolator):
             self._check_logic(formulas)
 
             if len(formulas) < 2:
-                raise Exception("interpolation needs at least 2 formulae")
+                raise PysmtValueError("interpolation needs at least 2 formulae")
 
             cfg = mathsat.msat_create_config()
             mathsat.msat_set_option(cfg, "interpolation", "true")
@@ -1270,8 +1272,8 @@ class MSatInterpolator(Interpolator):
 
             res = mathsat.msat_solve(env)
             if res == mathsat.MSAT_UNKNOWN:
-                raise Exception("error in mathsat interpolation: %s" %
-                                mathsat.msat_last_error_message(env))
+                raise InternalSolverError("Error in mathsat interpolation: %s" %
+                                          mathsat.msat_last_error_message(env))
 
             if res == mathsat.MSAT_SAT:
                 return None
diff --git a/pysmt/solvers/pico.py b/pysmt/solvers/pico.py
index b09e78c..824dbd5 100644
--- a/pysmt/solvers/pico.py
+++ b/pysmt/solvers/pico.py
@@ -31,7 +31,7 @@ from pysmt.solvers.solver import Solver, SolverOptions
 from pysmt.solvers.eager import EagerModel
 from pysmt.rewritings import CNFizer
 from pysmt.decorators import clear_pending_pop, catch_conversion_error
-from pysmt.exceptions import ConvertExpressionError
+from pysmt.exceptions import ConvertExpressionError, PysmtValueError
 from pysmt.constants import is_python_integer
 
 
@@ -71,7 +71,7 @@ class PicosatOptions(SolverOptions):
     def __init__(self, **base_options):
         SolverOptions.__init__(self, **base_options)
         if self.unsat_cores_mode is not None:
-            raise ValueError("'unsat_cores_mode' option not supported.")
+            raise PysmtValueError("'unsat_cores_mode' option not supported.")
 
         # Set Defaults
         self.preprocessing = True
@@ -86,28 +86,28 @@ class PicosatOptions(SolverOptions):
         for k,v in self.solver_options.items():
             if k == "enable_trace_generation":
                 if v not in (True, False):
-                    raise ValueError("Invalid value for %s: %s" % \
+                    raise PysmtValueError("Invalid value for %s: %s" % \
                                      (str(k),str(v)))
             elif k == "output":
                 if v is not None and not hasattr(v, "fileno"):
-                    raise ValueError("Invalid value for %s: %s" % \
+                    raise PysmtValueError("Invalid value for %s: %s" % \
                                      (str(k),str(v)))
 
             elif k == "global_default_phase":
                 if v is not None and v not in PicosatOptions.ALL_GLOBAL_DEFAULT_PHASE:
-                    raise ValueError("Invalid value for %s: %s" % \
+                    raise PysmtValueError("Invalid value for %s: %s" % \
                                      (str(k),str(v)))
             elif k == "preprocessing":
                 if v not in (True, False):
-                    raise ValueError("Invalid value for %s: %s" % \
+                    raise PysmtValueError("Invalid value for %s: %s" % \
                                      (str(k),str(v)))
             elif k == "verbosity":
                 if not is_python_integer(v):
-                    raise ValueError("Invalid value for %s: %s" % \
+                    raise PysmtValueError("Invalid value for %s: %s" % \
                                      (str(k),str(v)))
             elif k == "propagation_limit":
                 if not is_python_integer(v):
-                    raise ValueError("Invalid value for %s: %s" % \
+                    raise PysmtValueError("Invalid value for %s: %s" % \
                                      (str(k),str(v)))
             elif k in ("more_important_lit", "less_important_lit"):
                 if v is not None:
@@ -116,10 +116,11 @@ class PicosatOptions(SolverOptions):
                     except:
                         valid = False
                     if not valid:
-                        raise ValueError("'more_important_lit' and 'less_important_lit' require a "
-                                         "list of Boolean variables")
+                        raise PysmtValueError("'more_important_lit' and "
+                                              "'less_important_lit' require a "
+                                              "list of Boolean variables")
             else:
-                raise ValueError("Unrecognized option '%s'." % k)
+                raise PysmtValueError("Unrecognized option '%s'." % k)
             # Store option
             setattr(self, k, v)
 
@@ -161,7 +162,8 @@ class PicosatOptions(SolverOptions):
 
         if self.enable_trace_generation:
             rv = picosat.picosat_enable_trace_generation(pico)
-            if rv == 0: raise ValueError("Picosat: Cannot enable Trace Generation")
+            if rv == 0: raise PysmtValueError("Picosat: Cannot enable Trace"
+                                              " Generation")
 
         if self.verbosity > 0:
             picosat.picosat_set_verbosity(pico, self.verbosity)
diff --git a/pysmt/solvers/solver.py b/pysmt/solvers/solver.py
index 306bd72..62f86de 100644
--- a/pysmt/solvers/solver.py
+++ b/pysmt/solvers/solver.py
@@ -18,9 +18,8 @@
 import abc
 
 from pysmt.typing import BOOL
-from pysmt.exceptions import (SolverReturnedUnknownResultError,
-                              SolverStatusError)
-from pysmt.decorators import deprecated
+from pysmt.exceptions import (SolverReturnedUnknownResultError, PysmtValueError,
+                              PysmtTypeError, SolverStatusError)
 from six.moves import xrange
 
 
@@ -50,31 +49,31 @@ class SolverOptions(object):
                  solver_options=None):
 
         if generate_models not in (True, False):
-            raise ValueError("Invalid value %s for 'generate_models'" \
-                             % generate_models)
+            raise PysmtValueError("Invalid value %s for 'generate_models'" \
+                                  % generate_models)
         self.generate_models = generate_models
 
         if incremental not in (True, False):
-            raise ValueError("Invalid value %s for 'incremental'" \
-                             % incremental)
+            raise PysmtValueError("Invalid value %s for 'incremental'" \
+                                  % incremental)
         self.incremental = incremental
 
         if unsat_cores_mode not in (None, "named", "all"):
-            raise ValueError("Invalid value %s for 'unsat_cores_mode'" \
-                             % unsat_cores_mode)
+            raise PysmtValueError("Invalid value %s for 'unsat_cores_mode'" \
+                                  % unsat_cores_mode)
         self.unsat_cores_mode = unsat_cores_mode
 
         if random_seed is not None and type(random_seed) != int:
-            raise ValueError("Invalid value %s for 'random_seed'" \
-                             % random_seed)
+            raise PysmtValueError("Invalid value %s for 'random_seed'" \
+                                  % random_seed)
         self.random_seed = random_seed
 
         if solver_options is not None:
             try:
                 solver_options = dict(solver_options)
             except:
-                raise ValueError("Invalid value %s for 'solver_options'" \
-                                 % solver_options)
+                raise PysmtValueError("Invalid value %s for 'solver_options'" \
+                                      % solver_options)
         else:
             solver_options = dict()
         self.solver_options = solver_options
@@ -98,7 +97,7 @@ class Solver(object):
 
     def __init__(self, environment, logic, **options):
         if logic is None:
-            raise ValueError("Cannot provide 'None' as logic")
+            raise PysmtValueError("Cannot provide 'None' as logic")
 
         self.environment = environment
         self.pending_pop = False
@@ -326,7 +325,7 @@ class Solver(object):
         Raises TypeError.
         """
         if item.is_symbol() and item.symbol_type().is_function_type():
-            raise TypeError("Cannot call get_value() on a FunctionType")
+            raise PysmtTypeError("Cannot call get_value() on a FunctionType")
 
     def _assert_is_boolean(self, formula):
         """Enforces that argument 'formula' is of type Boolean.
@@ -334,7 +333,7 @@ class Solver(object):
         Raises TypeError.
         """
         if formula.get_type() != BOOL:
-            raise TypeError("Argument must be boolean.")
+            raise PysmtTypeError("Argument must be boolean.")
 
 
 class IncrementalTrackingSolver(Solver):
diff --git a/pysmt/solvers/yices.py b/pysmt/solvers/yices.py
index e54483c..8b64676 100644
--- a/pysmt/solvers/yices.py
+++ b/pysmt/solvers/yices.py
@@ -34,7 +34,8 @@ from pysmt.solvers.smtlib import SmtLibBasicSolver, SmtLibIgnoreMixin
 
 from pysmt.walkers import DagWalker
 from pysmt.exceptions import SolverReturnedUnknownResultError
-from pysmt.exceptions import InternalSolverError, NonLinearError
+from pysmt.exceptions import (InternalSolverError, NonLinearError,
+                              PysmtValueError, PysmtTypeError)
 from pysmt.decorators import clear_pending_pop, catch_conversion_error
 from pysmt.constants import Fraction, is_pysmt_integer
 
@@ -75,7 +76,7 @@ class YicesOptions(SolverOptions):
         # TODO: Yices Supports UnsatCore extraction
         # but we did not wrapped it yet.
         if self.unsat_cores_mode is not None:
-            raise ValueError("'unsat_cores_mode' option not supported.")
+            raise PysmtValueError("'unsat_cores_mode' option not supported.")
 
     @staticmethod
     def _set_option(cfg, name, value):
@@ -86,7 +87,8 @@ class YicesOptions(SolverOptions):
             # provided to the parameter is invalid.
             err = yicespy.yices_error_code()
             if err == yicespy.CTX_INVALID_PARAMETER_VALUE:
-                raise ValueError("Error setting the option '%s=%s'" % (name,value))
+                raise PysmtValueError("Error setting the option "
+                                      "'%s=%s'" % (name,value))
 
     def __call__(self, solver):
         if self.generate_models:
@@ -120,7 +122,7 @@ class YicesOptions(SolverOptions):
         for k,v in self.solver_options.items():
             rv = yicespy.yices_set_param(params, k, v)
             if rv != 0:
-                raise ValueError("Error setting the option '%s=%s'" % (k,v))
+                raise PysmtValueError("Error setting the option '%s=%s'" % (k,v))
         solver.yices_params = params
 
 # EOC YicesOptions
@@ -620,7 +622,9 @@ class YicesConverter(Converter, DagWalker):
             raise NotImplementedError(tp)
 
     def declare_variable(self, var):
-        if not var.is_symbol(): raise TypeError
+        if not var.is_symbol():
+            raise PysmtTypeError("Trying to declare as a variable something "
+                                 "that is not a symbol: %s" % var)
         if var.symbol_name() not in self.symbol_to_decl:
             tp = self._type_to_yices(var.symbol_type())
             decl = yicespy.yices_new_uninterpreted_term(tp)
diff --git a/pysmt/solvers/z3.py b/pysmt/solvers/z3.py
index d787013..3b8b364 100644
--- a/pysmt/solvers/z3.py
+++ b/pysmt/solvers/z3.py
@@ -42,7 +42,7 @@ from pysmt.exceptions import (SolverReturnedUnknownResultError,
                               SolverNotConfiguredForUnsatCoresError,
                               SolverStatusError,
                               ConvertExpressionError,
-                              UndefinedSymbolError)
+                              UndefinedSymbolError, PysmtValueError)
 from pysmt.decorators import clear_pending_pop, catch_conversion_error
 from pysmt.logics import LRA, LIA, QF_UFLIA, QF_UFLRA, PYSMT_LOGICS
 from pysmt.oracles import get_logic
@@ -113,7 +113,8 @@ class Z3Options(SolverOptions):
         try:
             z3solver.set(name, value)
         except z3.Z3Exception:
-            raise ValueError("Error setting the option '%s=%s'" % (name, value))
+            raise PysmtValueError("Error setting the option '%s=%s'" \
+                                  % (name, value))
 
     def __call__(self, solver):
         self._set_option(solver.z3, 'model', self.generate_models)
@@ -122,11 +123,11 @@ class Z3Options(SolverOptions):
             self._set_option(solver.z3, 'unsat_core', True)
         if self.random_seed is not None:
             self._set_option(solver.z3, 'random_seed', self.random_seed)
-        for k,v in self.solver_options:
+        for k,v in self.solver_options.items():
             try:
                 self._set_option(solver.z3, str(k), v)
             except z3.Z3Exception:
-                raise ValueError("Error setting the option '%s=%s'" % (k,v))
+                raise PysmtValueError("Error setting the option '%s=%s'" % (k,v))
 
 # EOC Z3Options
 
diff --git a/pysmt/substituter.py b/pysmt/substituter.py
index 81077f3..ef2a2ba 100644
--- a/pysmt/substituter.py
+++ b/pysmt/substituter.py
@@ -21,6 +21,7 @@ from six import iteritems
 
 import pysmt.walkers
 import pysmt.operators as op
+from pysmt.exceptions import PysmtTypeError
 
 
 class Substituter(pysmt.walkers.DagWalker):
@@ -104,25 +105,25 @@ class Substituter(pysmt.walkers.DagWalker):
 
         # Check that formula is a term
         if not formula.is_term():
-            raise TypeError("substitute() can only be used on terms.")
+            raise PysmtTypeError("substitute() can only be used on terms.")
 
         for (i, k) in enumerate(subs):
             v = subs[k]
             # Check that substitutions are terms
             if not k.is_term():
-                raise TypeError(
+                raise PysmtTypeError(
                     "Only terms should be provided as substitutions." +
                     " Non-term '%s' found." % k)
             if not v.is_term():
-                raise TypeError(
+                raise PysmtTypeError(
                     "Only terms should be provided as substitutions." +
                     " Non-term '%s' found." % v)
             # Check that substitutions belong to the current formula manager
             if k not in self.manager:
-                raise TypeError(
+                raise PysmtTypeError(
                     "Key %d does not belong to the Formula Manager." % i)
             if v not in self.manager:
-                raise TypeError(
+                raise PysmtTypeError(
                     "Value %d does not belong to the Formula Manager." % i)
 
         self.orig_subs = subs
diff --git a/pysmt/type_checker.py b/pysmt/type_checker.py
index 76b8b65..6c3863d 100644
--- a/pysmt/type_checker.py
+++ b/pysmt/type_checker.py
@@ -25,7 +25,7 @@ reasoning about the type of formulae.
 import pysmt.walkers as walkers
 import pysmt.operators as op
 from pysmt.typing import BOOL, REAL, INT, BVType, ArrayType
-
+from pysmt.exceptions import PysmtTypeError
 
 class SimpleTypeChecker(walkers.DagWalker):
 
@@ -68,7 +68,8 @@ class SimpleTypeChecker(walkers.DagWalker):
         """ Returns the pysmt.types type of the formula """
         res = self.walk(formula)
         if not self.be_nice and res is None:
-            raise TypeError("The formula '%s' is not well-formed" % str(formula))
+            raise PysmtTypeError("The formula '%s' is not well-formed" \
+                                 % str(formula))
         return res
 
     def walk_type_to_type(self, formula, args, type_in, type_out):
@@ -286,7 +287,8 @@ def assert_no_boolean_in_args(args):
     """ Enforces that the elements in args are not of BOOL type."""
     for arg in args:
         if (arg.get_type() == BOOL):
-            raise TypeError("Boolean Expressions are not allowed in arguments")
+            raise PysmtTypeError("Boolean Expressions are not allowed "
+                                 "in arguments")
 
 
 def assert_boolean_args(args):
@@ -294,7 +296,7 @@ def assert_boolean_args(args):
     for arg in args:
         t = arg.get_type()
         if (t != BOOL):
-            raise TypeError("%s is not allowed in arguments" % t)
+            raise PysmtTypeError("%s is not allowed in arguments" % t)
 
 
 def assert_same_type_args(args):
@@ -303,7 +305,7 @@ def assert_same_type_args(args):
     for arg in args[1:]:
         t = arg.get_type()
         if (t != ref_t):
-            raise TypeError("Arguments should be of the same type!\n" +
+            raise PysmtTypeError("Arguments should be of the same type!\n" +
                              str([str((a, a.get_type())) for a in args]))
 
 
@@ -312,6 +314,6 @@ def assert_args_type_in(args, allowed_types):
     for arg in args:
         t = arg.get_type()
         if (t not in allowed_types):
-            raise TypeError(
+            raise PysmtTypeError(
                 "Argument is of type %s, but one of %s was expected!\n" %
                 (t, str(allowed_types)))
diff --git a/pysmt/walkers/dag.py b/pysmt/walkers/dag.py
index 48adf6b..9d5f391 100644
--- a/pysmt/walkers/dag.py
+++ b/pysmt/walkers/dag.py
@@ -71,13 +71,8 @@ class DagWalker(Walker):
             except KeyError:
                 f = self.walk_error
 
-            try:
-                args = [self.memoization[self._get_key(s, **kwargs)] \
-                        for s in self._get_children(formula)]
-            except KeyError as ex:
-                # This should never happen in nominal execution.
-                # We catch the exception to simplify debugging
-                raise KeyError(ex.message, formula, self._get_key(s, **kwargs))
+            args = [self.memoization[self._get_key(s, **kwargs)] \
+                    for s in self._get_children(formula)]
             self.memoization[key] = f(formula, args=args, **kwargs)
         else:
             pass


Test patch:
diff --git a/pysmt/test/smtlib/test_parser_extensibility.py b/pysmt/test/smtlib/test_parser_extensibility.py
index 064b70b..1fe152e 100644
--- a/pysmt/test/smtlib/test_parser_extensibility.py
+++ b/pysmt/test/smtlib/test_parser_extensibility.py
@@ -20,7 +20,7 @@ from six.moves import cStringIO
 
 from pysmt.test import TestCase, main
 from pysmt.smtlib.parser import SmtLibParser
-from pysmt.exceptions import UnknownSmtLibCommandError
+from pysmt.exceptions import UnknownSmtLibCommandError, PysmtValueError
 
 TS = collections.namedtuple('TS', ['init', 'trans'])
 TSFormula = collections.namedtuple('TSFormula', ['formula', "is_init"])
@@ -57,7 +57,7 @@ class TSSmtLibParser(SmtLibParser):
             ty = symbol.symbol_type()
             return self.env.formula_manager.Symbol("next_" + name, ty)
         else:
-            raise ValueError("'next' operator can be applied only to symbols")
+            raise PysmtValueError("'next' operator can be applied only to symbols")
 
     def get_ts(self, script):
         init = self.env.formula_manager.TRUE()
diff --git a/pysmt/test/smtlib/test_parser_type_error.py b/pysmt/test/smtlib/test_parser_type_error.py
index 6d8af52..f2f9b3e 100644
--- a/pysmt/test/smtlib/test_parser_type_error.py
+++ b/pysmt/test/smtlib/test_parser_type_error.py
@@ -19,6 +19,7 @@ import os
 
 from pysmt.test import TestCase, main
 from pysmt.smtlib.parser import SmtLibParser
+from pysmt.exceptions import PysmtTypeError
 
 class TestTypeError(TestCase):
 
@@ -26,7 +27,7 @@ class TestTypeError(TestCase):
         d = os.path.dirname(os.path.realpath(__file__))
         smtfile = d + "/small_set/negative/wrong1.smt2.bz2"
         parser = SmtLibParser()
-        with self.assertRaises(TypeError):
+        with self.assertRaises(PysmtTypeError):
             parser.get_script_fname(smtfile)
 
 
diff --git a/pysmt/test/smtlib/test_smtlibscript.py b/pysmt/test/smtlib/test_smtlibscript.py
index 3bbd5ad..556445c 100644
--- a/pysmt/test/smtlib/test_smtlibscript.py
+++ b/pysmt/test/smtlib/test_smtlibscript.py
@@ -26,7 +26,7 @@ from pysmt.smtlib.script import smtlibscript_from_formula, evaluate_command
 from pysmt.smtlib.parser import get_formula_strict, get_formula, SmtLibParser
 from pysmt.solvers.smtlib import SmtLibIgnoreMixin
 from pysmt.logics import QF_UFLIRA
-from pysmt.exceptions import UndefinedLogicError
+from pysmt.exceptions import UndefinedLogicError, PysmtValueError
 
 
 
@@ -118,7 +118,7 @@ class TestSmtLibScript(TestCase):
         self.assertEqual(f, target_two)
 
         stream_in = cStringIO(smtlib_double)
-        with self.assertRaises(AssertionError):
+        with self.assertRaises(PysmtValueError):
             f = get_formula_strict(stream_in)
 
 
diff --git a/pysmt/test/test_array.py b/pysmt/test/test_array.py
index 81fe0e0..0c0ce37 100644
--- a/pysmt/test/test_array.py
+++ b/pysmt/test/test_array.py
@@ -23,7 +23,7 @@ from pysmt.typing import ARRAY_INT_INT, ArrayType, INT, REAL, BV8
 from pysmt.shortcuts import (Solver,
                              Symbol, Not, Equals, Int, BV, Real, FreshSymbol,
                              Select, Store, Array)
-from pysmt.exceptions import ConvertExpressionError
+from pysmt.exceptions import ConvertExpressionError, PysmtTypeError, PysmtValueError
 
 
 class TestArray(TestCase):
@@ -84,7 +84,7 @@ class TestArray(TestCase):
                                       FreshSymbol(ArrayType(BV8, BV8))))
 
     def test_complex_types(self):
-        with self.assertRaises(TypeError):
+        with self.assertRaises(PysmtTypeError):
             # Not(Store(Array<Real,BV8>(8d_0), 1.0, 8d_5) =
             #     Store(Array<Int,BV8>(8d_0), 1, 8d_5))
             Not(Equals(Store(Array(REAL, BV(0, 8)), Real(1), BV(5, 8)),
@@ -92,7 +92,7 @@ class TestArray(TestCase):
 
         nested_a = Symbol("a_arb_aii", ArrayType(ArrayType(REAL, BV8),
                                                  ARRAY_INT_INT))
-        with self.assertRaises(TypeError):
+        with self.assertRaises(PysmtTypeError):
         # This is wrong, because the first elemnt of Array must be a Type
             Equals(nested_a, Array(Array(REAL, BV(0,8)),
                                    Array(INT, Int(7))))
@@ -131,10 +131,10 @@ class TestArray(TestCase):
         self.assertFalse(ax2.is_constant())
         self.assertTrue(ax3.is_constant())
 
-        with self.assertRaises(ValueError):
+        with self.assertRaises(PysmtValueError):
             self.assertTrue(ax3.is_constant(_type=REAL))
 
-        with self.assertRaises(ValueError):
+        with self.assertRaises(PysmtValueError):
             self.assertTrue(ax3.is_constant(value=Real(2)))
 
 
diff --git a/pysmt/test/test_bdd.py b/pysmt/test/test_bdd.py
index 33c0389..f1dbcd1 100644
--- a/pysmt/test/test_bdd.py
+++ b/pysmt/test/test_bdd.py
@@ -20,6 +20,7 @@ from pysmt.shortcuts import get_env, qelim, Or
 from pysmt.test import TestCase, skipIfSolverNotAvailable, main
 from pysmt.test.examples import get_example_formulae
 from pysmt.logics import BOOL
+from pysmt.exceptions import PysmtValueError
 
 class TestBdd(TestCase):
 
@@ -154,7 +155,7 @@ class TestBdd(TestCase):
 
     @skipIfSolverNotAvailable("bdd")
     def test_invalid_ordering(self):
-        with self.assertRaises(ValueError):
+        with self.assertRaises(PysmtValueError):
             Solver(name="bdd", logic=BOOL,
                    solver_options={'static_ordering':
                                    [And(self.x, self.y), self.y]})
diff --git a/pysmt/test/test_bv.py b/pysmt/test/test_bv.py
index 434ea4b..75da07f 100644
--- a/pysmt/test/test_bv.py
+++ b/pysmt/test/test_bv.py
@@ -20,7 +20,7 @@ from pysmt.shortcuts import Symbol, And, Symbol, Equals, TRUE
 from pysmt.shortcuts import is_sat, is_valid, get_model, is_unsat
 from pysmt.typing import BVType, BV32, BV128
 from pysmt.logics import QF_BV
-
+from pysmt.exceptions import PysmtValueError, PysmtTypeError
 
 class TestBV(TestCase):
 
@@ -48,10 +48,10 @@ class TestBV(TestCase):
         self.assertFalse(BV32 == BV128)
         self.assertTrue(BV32 == BV32)
 
-        with self.assertRaises(ValueError):
+        with self.assertRaises(PysmtValueError):
             # Negative numbers are not supported
             BV(-1, 10)
-        with self.assertRaises(ValueError):
+        with self.assertRaises(PysmtValueError):
             # Number should fit in the width
             BV(10, 2)
 
@@ -95,7 +95,7 @@ class TestBV(TestCase):
         self.assertTrue(is_sat(f3, logic=QF_BV), f3)
         self.assertTrue(is_valid(f4, logic=QF_BV), f4)
 
-        with self.assertRaises(TypeError):
+        with self.assertRaises(PysmtTypeError):
             mgr.BVAnd(b128, zero)
 
         f = mgr.BVAnd(b32, zero)
@@ -211,9 +211,9 @@ class TestBV(TestCase):
         mgr.SBV(1, 2)
 
         # Overflow and Underflow
-        with self.assertRaises(ValueError):
+        with self.assertRaises(PysmtValueError):
             mgr.SBV(2, 2)
-        with self.assertRaises(ValueError):
+        with self.assertRaises(PysmtValueError):
             mgr.SBV(-3, 2)
 
         # These should work without exceptions
@@ -222,10 +222,10 @@ class TestBV(TestCase):
         mgr.BV(2, 2)
         mgr.BV(3, 2)
         # Overflow
-        with self.assertRaises(ValueError):
+        with self.assertRaises(PysmtValueError):
             mgr.BV(4, 2)
         # No negative number allowed
-        with self.assertRaises(ValueError):
+        with self.assertRaises(PysmtValueError):
             mgr.BV(-1, 2)
 
         # SBV should behave as BV for positive numbers
diff --git a/pysmt/test/test_configuration.py b/pysmt/test/test_configuration.py
index 3d05bb7..77ad8a1 100644
--- a/pysmt/test/test_configuration.py
+++ b/pysmt/test/test_configuration.py
@@ -23,6 +23,7 @@ from pysmt.shortcuts import get_env
 from pysmt.configuration import (configure_environment,
                                  write_environment_configuration)
 from pysmt.environment import Environment
+from pysmt.exceptions import PysmtIOError
 
 from pysmt.test import TestCase, main
 BASE_DIR = os.path.dirname(os.path.abspath(__file__))
@@ -99,7 +100,7 @@ class TestConfiguration(TestCase):
         self.assertTrue("z3-smt" in new_env.factory.all_solvers())
 
     def test_nonexistent_conf(self):
-        with self.assertRaises(IOError):
+        with self.assertRaises(PysmtIOError):
             read_configuration("/tmp/nonexistent")
 
     def test_bad_conf(self):
diff --git a/pysmt/test/test_eager_model.py b/pysmt/test/test_eager_model.py
index f8d193e..91138b1 100644
--- a/pysmt/test/test_eager_model.py
+++ b/pysmt/test/test_eager_model.py
@@ -22,6 +22,7 @@ from pysmt.shortcuts import And, Or, FALSE, TRUE, FreshSymbol, Solver
 from pysmt.solvers.eager import EagerModel
 from pysmt.typing import REAL, INT
 from pysmt.test import skipIfSolverNotAvailable
+from pysmt.exceptions import PysmtTypeError
 
 
 class TestEagerModel(TestCase):
@@ -54,12 +55,12 @@ class TestEagerModel(TestCase):
         d = {x:TRUE()}
 
         model = EagerModel(assignment=d)
-        with self.assertRaises(TypeError):
+        with self.assertRaises(PysmtTypeError):
             model.get_value(And(x,y), model_completion=False)
 
         d2 = {x:TRUE(), y:x}
         model = EagerModel(assignment=d2)
-        with self.assertRaises(TypeError):
+        with self.assertRaises(PysmtTypeError):
             model.get_value(And(x,y))
 
     def test_complete_model(self):
@@ -77,11 +78,11 @@ class TestEagerModel(TestCase):
         self.assertTrue(model.get_value(r).is_constant(REAL))
 
         self.assertEqual(model.get_value(x, model_completion=False), TRUE())
-        with self.assertRaises(TypeError):
+        with self.assertRaises(PysmtTypeError):
             model.get_value(And(x,y), model_completion=False)
-        with self.assertRaises(TypeError):
+        with self.assertRaises(PysmtTypeError):
             model.get_value(p, model_completion=False)
-        with self.assertRaises(TypeError):
+        with self.assertRaises(PysmtTypeError):
             model.get_value(r, model_completion=False)
 
 
diff --git a/pysmt/test/test_formula.py b/pysmt/test/test_formula.py
index be9f5a1..a3f0413 100644
--- a/pysmt/test/test_formula.py
+++ b/pysmt/test/test_formula.py
@@ -26,7 +26,8 @@ from pysmt.shortcuts import get_env
 from pysmt.environment import Environment
 from pysmt.test import TestCase, skipIfNoSolverForLogic, main
 from pysmt.logics import QF_BOOL
-from pysmt.exceptions import NonLinearError, UndefinedSymbolError
+from pysmt.exceptions import (UndefinedSymbolError, PysmtTypeError,
+                              PysmtModeError, PysmtValueError)
 from pysmt.formula import FormulaManager
 from pysmt.constants import Fraction, Integer
 
@@ -78,7 +79,7 @@ class TestFormulaManager(TestCase):
         self.assertIsNotNone(a, "Symbol was not created")
         a2 = self.mgr.get_or_create_symbol("a", REAL)
         self.assertEqual(a, a2, "Symbol was not memoized")
-        with self.assertRaises(TypeError):
+        with self.assertRaises(PysmtTypeError):
             self.mgr.get_or_create_symbol("a", BOOL)
 
     def test_symbol(self):
@@ -212,13 +213,13 @@ class TestFormulaManager(TestCase):
         self.assertTrue(n.is_bool_op())
 
     def test_ge_node_type(self):
-        with self.assertRaises(TypeError):
+        with self.assertRaises(PysmtTypeError):
             self.mgr.GE(self.x, self.r)
 
-        with self.assertRaises(TypeError):
+        with self.assertRaises(PysmtTypeError):
             self.mgr.GE(self.r, self.x)
 
-        with self.assertRaises(TypeError):
+        with self.assertRaises(PysmtTypeError):
             self.mgr.GE(self.p, self.r)
 
     def test_ge_node(self):
@@ -268,7 +269,7 @@ class TestFormulaManager(TestCase):
         self.assertEqual(n.get_free_variables(), set([self.p, self.q]))
         self.assertTrue(n.is_theory_op())
 
-        with self.assertRaises(TypeError):
+        with self.assertRaises(PysmtTypeError):
             n = self.mgr.Minus(self.r, self.q)
 
     def test_times_node(self):
@@ -335,17 +336,17 @@ class TestFormulaManager(TestCase):
         self.assertEqual(n.get_free_variables(), set([self.p, self.q]))
         self.assertTrue(n.is_theory_relation())
 
-        with self.assertRaises(TypeError):
+        with self.assertRaises(PysmtTypeError):
             n = self.mgr.Equals(self.p, self.r)
 
     def test_gt_node_type(self):
-        with self.assertRaises(TypeError):
+        with self.assertRaises(PysmtTypeError):
             self.mgr.GT(self.x, self.r)
 
-        with self.assertRaises(TypeError):
+        with self.assertRaises(PysmtTypeError):
             self.mgr.GT(self.r, self.x)
 
-        with self.assertRaises(TypeError):
+        with self.assertRaises(PysmtTypeError):
             self.mgr.GT(self.r, self.p)
 
     def test_gt_node(self):
@@ -370,10 +371,10 @@ class TestFormulaManager(TestCase):
         self.assertTrue(n.is_theory_relation())
 
     def test_le_node_type(self):
-        with self.assertRaises(TypeError):
+        with self.assertRaises(PysmtTypeError):
             self.mgr.LE(self.x, self.r)
 
-        with self.assertRaises(TypeError):
+        with self.assertRaises(PysmtTypeError):
             self.mgr.LE(self.r, self.x)
 
     def test_le_node(self):
@@ -398,10 +399,10 @@ class TestFormulaManager(TestCase):
         self.assertTrue(n.is_theory_relation())
 
     def test_lt_node_type(self):
-        with self.assertRaises(TypeError):
+        with self.assertRaises(PysmtTypeError):
             self.mgr.LT(self.x, self.r)
 
-        with self.assertRaises(TypeError):
+        with self.assertRaises(PysmtTypeError):
             self.mgr.LT(self.r, self.x)
 
     def test_lt_node(self):
@@ -443,7 +444,7 @@ class TestFormulaManager(TestCase):
         self.assertTrue(n.is_ite())
         self.assertEqual(n.get_free_variables(), set([self.x, self.p, self.q]))
 
-        with self.assertRaises(TypeError):
+        with self.assertRaises(PysmtTypeError):
             self.mgr.Ite(self.x, self.p, self.r)
 
     def test_function(self):
@@ -487,7 +488,7 @@ class TestFormulaManager(TestCase):
         nd = self.mgr.Real(Fraction(100,1))
         self.assertNotEqual(nd, n1)
 
-        with self.assertRaises(TypeError):
+        with self.assertRaises(PysmtTypeError):
             self.mgr.Real(True)
 
         nd = self.mgr.Int(10)
@@ -522,17 +523,17 @@ class TestFormulaManager(TestCase):
         self.assertTrue(n.is_constant())
         self.assertTrue(n.is_bool_constant())
 
-        with self.assertRaises(TypeError):
+        with self.assertRaises(PysmtTypeError):
             self.mgr.Bool(42)
 
     def test_plus_node(self):
-        with self.assertRaises(TypeError):
+        with self.assertRaises(PysmtTypeError):
             self.mgr.Plus([self.x, self.r])
 
-        with self.assertRaises(TypeError):
+        with self.assertRaises(PysmtTypeError):
             self.mgr.Plus([self.p, self.r])
 
-        with self.assertRaises(TypeError):
+        with self.assertRaises(PysmtTypeError):
             self.mgr.Plus()
 
         n1 = self.mgr.Plus([self.r, self.s])
@@ -593,7 +594,7 @@ class TestFormulaManager(TestCase):
         xor1 = self.mgr.Xor(self.x, self.y)
         self.assertIsNotNone(xor1)
 
-        with self.assertRaises(TypeError):
+        with self.assertRaises(PysmtTypeError):
             self.mgr.Xor(self.p, self.q)
 
         xor_false = self.mgr.Xor(self.mgr.TRUE(), self.mgr.TRUE()).simplify()
@@ -629,7 +630,7 @@ class TestFormulaManager(TestCase):
         min1 = self.mgr.Min(self.p, Plus(self.q, self.mgr.Int(1)))
         self.assertIsNotNone(min1)
 
-        with self.assertRaises(TypeError):
+        with self.assertRaises(PysmtTypeError):
             self.mgr.Min(self.p, self.r)
 
         min_int = self.mgr.Min(self.mgr.Int(1), self.mgr.Int(2), self.mgr.Int(3))
@@ -644,7 +645,7 @@ class TestFormulaManager(TestCase):
         max1 = self.mgr.Max(self.p, Plus(self.q, self.mgr.Int(1)))
         self.assertIsNotNone(max1)
 
-        with self.assertRaises(TypeError):
+        with self.assertRaises(PysmtTypeError):
             self.mgr.Max(self.p, self.r)
 
         max_int = self.mgr.Max(self.mgr.Int(1), self.mgr.Int(2), self.mgr.Int(3))
@@ -700,13 +701,13 @@ class TestFormulaManager(TestCase):
     def test_infix(self):
         x, y, p = self.x, self.y, self.p
 
-        with self.assertRaises(Exception):
+        with self.assertRaises(PysmtModeError):
             x.Implies(y)
-        with self.assertRaises(Exception):
+        with self.assertRaises(PysmtModeError):
             ~x
-        with self.assertRaises(Exception):
+        with self.assertRaises(PysmtModeError):
             x[1]
-        with self.assertRaises(Exception):
+        with self.assertRaises(PysmtModeError):
             x.Ite(x,y)
 
         get_env().enable_infix_notation = True
@@ -737,7 +738,7 @@ class TestFormulaManager(TestCase):
         self.assertEqual(Plus(r, Real(1.5)), 1.5 + r)
         self.assertEqual(Times(r, Real(1.5)), 1.5 * r)
 
-        with self.assertRaises(TypeError):
+        with self.assertRaises(PysmtTypeError):
             foo = p + 1.5
 
         self.assertEqual(Not(x), ~x)
@@ -845,7 +846,7 @@ class TestFormulaManager(TestCase):
         # BV_NOT:
         # !!!WARNING!!! Cannot be applied to python constants!!
         # This results in a negative number
-        with self.assertRaises(ValueError):
+        with self.assertRaises(PysmtValueError):
             _8bv(~const1)
 
         # For symbols and expressions this works as expected
@@ -965,7 +966,7 @@ class TestFormulaManager(TestCase):
         f = self.mgr.Equals(self.rconst, self.mgr.ToReal(self.p))
         self.assertIsNotNone(f)
 
-        with self.assertRaises(TypeError):
+        with self.assertRaises(PysmtTypeError):
             self.mgr.ToReal(self.x)
 
         f1 = self.mgr.ToReal(self.p)
@@ -976,7 +977,7 @@ class TestFormulaManager(TestCase):
         self.assertEqual(set([self.p]), f1.get_free_variables())
 
         f3 = self.mgr.Equals(self.iconst, self.p)
-        with self.assertRaises(TypeError):
+        with self.assertRaises(PysmtTypeError):
             self.mgr.ToReal(f3)
 
         f4 = self.mgr.Plus(self.rconst, self.r)
diff --git a/pysmt/test/test_int.py b/pysmt/test/test_int.py
index 8929f84..7799cc1 100644
--- a/pysmt/test/test_int.py
+++ b/pysmt/test/test_int.py
@@ -20,6 +20,7 @@ from pysmt.shortcuts import (Symbol, And, Iff, Equals, LT, GT, Minus,
 from pysmt.typing import INT, REAL
 from pysmt.test import TestCase, skipIfNoSolverForLogic, main
 from pysmt.logics import QF_LIA, QF_UFLIRA
+from pysmt.exceptions import PysmtTypeError
 
 class TestLIA(TestCase):
 
@@ -40,7 +41,7 @@ class TestLIA(TestCase):
         varA = Symbol("A", REAL)
         varB = Symbol("B", INT)
 
-        with self.assertRaises(TypeError):
+        with self.assertRaises(PysmtTypeError):
             f = And(LT(varA, Plus(varA, Real(1))),
                     GT(varA, Minus(varB, Int(1))))
 
diff --git a/pysmt/test/test_regressions.py b/pysmt/test/test_regressions.py
index 6ef7eb1..6cbc103 100644
--- a/pysmt/test/test_regressions.py
+++ b/pysmt/test/test_regressions.py
@@ -29,7 +29,7 @@ from pysmt.typing import REAL, BOOL, INT, BVType, FunctionType, ArrayType
 from pysmt.test import (TestCase, skipIfSolverNotAvailable, skipIfNoSolverForLogic,
                         skipIfNoQEForLogic)
 from pysmt.test import main
-from pysmt.exceptions import ConvertExpressionError
+from pysmt.exceptions import ConvertExpressionError, PysmtValueError
 from pysmt.test.examples import get_example_formulae
 from pysmt.environment import Environment
 from pysmt.rewritings import cnf_as_set
@@ -267,7 +267,7 @@ class TestRegressions(TestCase):
         self.assertEqual(new_f, Bool(False))
 
     def test_empty_string_symbol(self):
-        with self.assertRaises(ValueError):
+        with self.assertRaises(PysmtValueError):
             Symbol("")
 
     def test_smtlib_info_quoting(self):
diff --git a/pysmt/test/test_solving.py b/pysmt/test/test_solving.py
index d520dc7..64da45c 100644
--- a/pysmt/test/test_solving.py
+++ b/pysmt/test/test_solving.py
@@ -29,7 +29,8 @@ from pysmt.test import main
 from pysmt.test.examples import get_example_formulae
 from pysmt.exceptions import (SolverReturnedUnknownResultError,
                               InternalSolverError, NoSolverAvailableError,
-                              ConvertExpressionError, UndefinedLogicError)
+                              ConvertExpressionError, UndefinedLogicError,
+                              PysmtTypeError, PysmtValueError)
 from pysmt.logics import QF_UFLIRA, QF_BOOL, QF_LRA, AUTO
 from pysmt.logics import convert_logic_from_string
 
@@ -407,7 +408,7 @@ class TestBasic(TestCase):
 
         for sname in get_env().factory.all_solvers(logic=QF_LRA):
             with Solver(name=sname) as solver:
-                with self.assertRaises(TypeError):
+                with self.assertRaises(PysmtTypeError):
                     solver.add_assertion(f1)
                 self.assertIsNone(solver.add_assertion(f2))
 
@@ -422,7 +423,7 @@ class TestBasic(TestCase):
                 solver.add_assertion(f)
                 res = solver.solve()
                 self.assertTrue(res)
-                with self.assertRaises(TypeError):
+                with self.assertRaises(PysmtTypeError):
                     solver.get_value(h)
                 self.assertIsNotNone(solver.get_value(h_0_0))
 
@@ -531,14 +532,14 @@ class TestBasic(TestCase):
         # Options are enforced at construction time
         with self.assertRaises(TypeError):
             Solver(logic=QF_BOOL, invalid_option=False)
-        with self.assertRaises(ValueError):
+        with self.assertRaises(PysmtValueError):
             Solver(logic=QF_BOOL, solver_options={'invalid': None})
 
     @skipIfNoSolverForLogic(QF_BOOL)
     def test_options_random_seed(self):
         for sname in get_env().factory.all_solvers(logic=QF_BOOL):
             if sname in ["btor", "bdd"]:
-                with self.assertRaises(ValueError):
+                with self.assertRaises(PysmtValueError):
                     Solver(name=sname, random_seed=42)
             else:
                 s = Solver(name=sname, random_seed=42)
diff --git a/pysmt/test/test_typechecker.py b/pysmt/test/test_typechecker.py
index 10d1b6f..2f23229 100644
--- a/pysmt/test/test_typechecker.py
+++ b/pysmt/test/test_typechecker.py
@@ -24,6 +24,7 @@ from pysmt.shortcuts import (Symbol, And, Plus, Minus, Times, Equals, Or, Iff,
                              LE, LT, Not, GE, GT, Ite, Bool, Int, Real, Div,
                              Function)
 from pysmt.environment import get_env
+from pysmt.exceptions import PysmtTypeError
 from pysmt.test import TestCase, main
 from pysmt.test.examples import get_example_formulae
 from pysmt.decorators import typecheck_result
@@ -74,10 +75,10 @@ class TestSimpleTypeChecker(TestCase):
         self.assertEqual(tc.walk(LE(Plus(vi, Function(f, [Real(4)])), Int(8))), BOOL)
         self.assertEqual(tc.walk(LE(Plus(vr, Function(g, [Int(4)])), Real(8))), BOOL)
 
-        with self.assertRaises(TypeError):
+        with self.assertRaises(PysmtTypeError):
             LE(Plus(vr, Function(g, [Real(4)])), Real(8))
 
-        with self.assertRaises(TypeError):
+        with self.assertRaises(PysmtTypeError):
             LE(Plus(vi, Function(f, [Int(4)])), Int(8))
 
 
@@ -151,20 +152,20 @@ class TestSimpleTypeChecker(TestCase):
 
     def test_assert_args(self):
         assert_no_boolean_in_args([self.r, self.p])
-        with self.assertRaises(TypeError):
+        with self.assertRaises(PysmtTypeError):
             assert_no_boolean_in_args([self.x, self.y])
 
         assert_boolean_args([self.x, self.y])
-        with self.assertRaises(TypeError):
+        with self.assertRaises(PysmtTypeError):
             assert_boolean_args([self.r, self.p])
 
         assert_same_type_args([self.x, self.y])
-        with self.assertRaises(TypeError):
+        with self.assertRaises(PysmtTypeError):
             assert_same_type_args([self.r, self.p])
 
         assert_args_type_in([self.x, self.p],
                             allowed_types=[INT, BOOL])
-        with self.assertRaises(TypeError):
+        with self.assertRaises(PysmtTypeError):
             assert_args_type_in([self.x, self.p],
                                 allowed_types=[REAL, BOOL])
 
@@ -184,7 +185,7 @@ class TestSimpleTypeChecker(TestCase):
 
         good_function()
 
-        with self.assertRaises(TypeError):
+        with self.assertRaises(PysmtTypeError):
             super_bad_function()
 
     def test_examples(self):
diff --git a/pysmt/test/test_walkers.py b/pysmt/test/test_walkers.py
index 445064b..0d788a1 100644
--- a/pysmt/test/test_walkers.py
+++ b/pysmt/test/test_walkers.py
@@ -27,7 +27,7 @@ from pysmt.walkers import TreeWalker, DagWalker, IdentityDagWalker
 from pysmt.test import TestCase, main
 from pysmt.formula import FormulaManager
 from pysmt.test.examples import get_example_formulae
-from pysmt.exceptions import UnsupportedOperatorError
+from pysmt.exceptions import UnsupportedOperatorError, PysmtTypeError
 from pysmt.substituter import MSSubstituter
 
 
@@ -61,7 +61,7 @@ class TestWalkers(TestCase):
         args_bad = {x:f}
 
         substitute(and_x_x, args_good)
-        with self.assertRaisesRegex(TypeError, " substitutions"):
+        with self.assertRaisesRegex(PysmtTypeError, " substitutions"):
             substitute(and_x_x, args_bad)
 
         # 2. All arguments belong to the manager of the substituter.
@@ -71,13 +71,13 @@ class TestWalkers(TestCase):
         args_1 = {x: new_x}
         args_2 = {new_x: new_x}
 
-        with self.assertRaisesRegex(TypeError, "Formula Manager" ):
+        with self.assertRaisesRegex(PysmtTypeError, "Formula Manager" ):
             substitute(and_x_x, args_1)
 
-        with self.assertRaisesRegex(TypeError, "Formula Manager."):
+        with self.assertRaisesRegex(PysmtTypeError, "Formula Manager."):
             substitute(and_x_x, args_2)
 
-        with self.assertRaisesRegex(TypeError, "substitute()"):
+        with self.assertRaisesRegex(PysmtTypeError, "substitute()"):
             substitute(f, {x:x})
 
     def test_undefined_node(self):