Repository: pysmt/pysmt
Pull request #284 (2016-07-24 19:54:19)

Portfolio Solver
- Created Portfolio class that uses multiprocessing to solve the problem
  using multiple solvers.
- The solver provides a naive incremental interface by using
  IncrementalTrackingSolver Interface
- get_value and get_model work after a SAT query. Other
  artifacts (unsat-core, interpolants) are not supported.
- Extend Factory.is_\* to include `portfolio` key-word, and exported as
  is_\* shortcuts. The syntax becomes:
  
  ```
   is_sat(f, portfolio=["s1", "s2"])
  ```

Exceptions are currently not handled internally. Similarly, logic testing is done only when the solvers are started (i.e., during solve()).  If at least one solver terminates, this might not be a problem, but it is not nice.


marcogario: @mikand: This is not ready to be merged, but I'd like some feedback. An open point that I am not sure how to manage is multiple instances of the same solver with different options. I cannot figure out a syntax that I like.
marcogario: Done with the exception handling (as discussed). Missing is the handling of options for solvers, including multiple instance of the same solver with different options (btw, we should find a meaningful example for this).

Patch:
diff --git a/pysmt/factory.py b/pysmt/factory.py
index f9e6878..292fb8b 100644
--- a/pysmt/factory.py
+++ b/pysmt/factory.py
@@ -35,6 +35,8 @@ from pysmt.logics import most_generic_logic, get_closer_logic
 from pysmt.logics import convert_logic_from_string
 from pysmt.oracles import get_logic
 from pysmt.solvers.qelim import ShannonQuantifierEliminator
+from pysmt.solvers.solver import SolverOptions
+from pysmt.solvers.portfolio import Portfolio
 
 DEFAULT_SOLVER_PREFERENCE_LIST = ['msat', 'z3', 'cvc4', 'yices', 'btor',
                                   'picosat', 'bdd']
@@ -463,19 +465,24 @@ class Factory(object):
                                           logic=logic,
                                           unsat_cores_mode=unsat_cores_mode)
 
-
     def QuantifierEliminator(self, name=None, logic=None):
         return self.get_quantifier_eliminator(name=name, logic=logic)
 
     def Interpolator(self, name=None, logic=None):
         return self.get_interpolator(name=name, logic=logic)
 
-    def is_sat(self, formula, solver_name=None, logic=None):
+    def is_sat(self, formula, solver_name=None, logic=None, portfolio=None):
         if logic is None or logic == AUTO_LOGIC:
             logic = get_logic(formula, self.environment)
-        with self.Solver(name=solver_name, logic=logic,
-                         generate_models=False, incremental=False) \
-             as solver:
+        if portfolio is not None:
+            solver = Portfolio(solvers_set=portfolio,
+                               environment=self.environment,
+                               logic=logic,
+                               generate_models=False, incremental=False)
+        else:
+            solver = self.Solver(name=solver_name, logic=logic,
+                                 generate_models=False, incremental=False)
+        with solver:
             return solver.is_sat(formula)
 
     def get_model(self, formula, solver_name=None, logic=None):
@@ -530,20 +537,30 @@ class Factory(object):
 
             return solver.get_unsat_core()
 
-    def is_valid(self, formula, solver_name=None, logic=None):
+    def is_valid(self, formula, solver_name=None, logic=None, portfolio=None):
         if logic is None or logic == AUTO_LOGIC:
             logic = get_logic(formula, self.environment)
-        with self.Solver(name=solver_name, logic=logic,
-                         generate_models=False,
-                         incremental=False) as solver:
+        if portfolio is not None:
+            solver = Portfolio(solvers_set=portfolio,
+                               environment=self.environment,
+                               logic=logic,
+                               generate_models=False, incremental=False)
+        else:
+            solver = self.Solver(name=solver_name, logic=logic,
+                                 generate_models=False, incremental=False)
+        with solver:
             return solver.is_valid(formula)
 
-    def is_unsat(self, formula, solver_name=None, logic=None):
-        if logic is None or logic == AUTO_LOGIC:
-            logic = get_logic(formula, self.environment)
-        with self.Solver(name=solver_name, logic=logic,
-                         generate_models=False,
-                         incremental=False) as solver:
+    def is_unsat(self, formula, solver_name=None, logic=None, portfolio=None):
+        if portfolio is not None:
+            solver = Portfolio(solvers_set=portfolio,
+                               environment=self.environment,
+                               logic=logic,
+                               generate_models=False, incremental=False)
+        else:
+            solver = self.Solver(name=solver_name, logic=logic,
+                                 generate_models=False, incremental=False)
+        with solver:
             return solver.is_unsat(formula)
 
     def qelim(self, formula, solver_name=None, logic=None):
diff --git a/pysmt/shortcuts.py b/pysmt/shortcuts.py
index cc15ba7..940b7ca 100644
--- a/pysmt/shortcuts.py
+++ b/pysmt/shortcuts.py
@@ -71,6 +71,7 @@ def get_type(formula):
     """
     return get_env().stc.get_type(formula)
 
+
 def simplify(formula):
     """Returns the simplified version of the formula.
 
@@ -81,6 +82,7 @@ def simplify(formula):
     """
     return get_env().simplifier.simplify(formula)
 
+
 def substitute(formula, subs):
     """Applies the substitutions defined in the dictionary to the formula.
 
@@ -93,6 +95,7 @@ def substitute(formula, subs):
     """
     return get_env().substituter.substitute(formula, subs)
 
+
 def serialize(formula, threshold=None):
     """Provides a string representing the formula.
 
@@ -115,6 +118,7 @@ def get_free_variables(formula):
     """
     return get_env().fvo.get_free_variables(formula)
 
+
 def get_atoms(formula):
     """Returns the set of atoms of the formula.
 
@@ -124,6 +128,7 @@ def get_atoms(formula):
     """
     return get_env().ao.get_atoms(formula)
 
+
 def get_formula_size(formula, measure=None):
     """Returns the size of the formula as measured by the given counting type.
 
@@ -143,66 +148,82 @@ def ForAll(variables, formula):
     r""".. math:: \forall v_1, \cdots, v_n . \varphi(v_1, \cdots, v_n)"""
     return get_env().formula_manager.ForAll(variables, formula)
 
+
 def Exists(variables, formula):
     r""".. math:: \exists v_1, \cdots, v_n . \varphi(v_1, \cdots, v_n)"""
     return get_env().formula_manager.Exists(variables, formula)
 
+
 def Function(vname, params):
     r""".. math:: vname(p_1, \cdots, p_n)"""
     return get_env().formula_manager.Function(vname, params)
 
+
 def Not(formula):
     r""".. math:: \lnot \varphi"""
     return get_env().formula_manager.Not(formula)
 
+
 def Implies(left, right):
     r""".. math:: l \rightarrow r"""
     return get_env().formula_manager.Implies(left, right)
 
+
 def Iff(left, right):
     r""".. math:: l \leftrightarrow r """
     return get_env().formula_manager.Iff(left, right)
 
+
 def GE(left, right):
     r""".. math:: l \ge r"""
     return get_env().formula_manager.GE(left, right)
 
+
 def Minus(left, right):
     r""".. math:: l - r """
     return get_env().formula_manager.Minus(left, right)
 
+
 def Times(*args):
     r""".. math:: x_1 \times x_2 \cdots \times x_n"""
     return get_env().formula_manager.Times(*args)
 
+
 def Pow(left, right):
     r""".. math:: l ^ r"""
     return get_env().formula_manager.Pow(left, right)
 
+
 def Div(left, right):
     r""".. math:: \frac{l}{r}"""
     return get_env().formula_manager.Div(left, right)
 
+
 def Equals(left, right):
     r""".. math:: l = r"""
     return get_env().formula_manager.Equals(left, right)
 
+
 def GT(left, right):
     r""".. math:: l > r"""
     return get_env().formula_manager.GT(left, right)
 
+
 def LE(left, right):
     r""".. math:: l \le r"""
     return get_env().formula_manager.LE(left, right)
 
+
 def LT(left, right):
     r""".. math:: l < r"""
     return get_env().formula_manager.LT(left, right)
 
+
 def Ite(iff, left, right):
     r""".. math:: \text{ If } i \text{ Then } l \text{ Else } r"""
     return get_env().formula_manager.Ite(iff, left, right)
 
+
 def Symbol(name, typename=types.BOOL):
     """Returns a symbol with the given name and type.
 
@@ -212,6 +233,7 @@ def Symbol(name, typename=types.BOOL):
     """
     return get_env().formula_manager.Symbol(name, typename)
 
+
 def FreshSymbol(typename=types.BOOL, template=None):
     """Returns a symbol with a fresh name and given type.
 
@@ -221,6 +243,7 @@ def FreshSymbol(typename=types.BOOL, template=None):
     """
     return get_env().formula_manager.FreshSymbol(typename, template)
 
+
 def Int(value):
     """Returns an Integer constant with the given value.
 
@@ -229,6 +252,7 @@ def Int(value):
     """
     return get_env().formula_manager.Int(value)
 
+
 def Bool(value):
     """Returns a Boolean constant with the given value.
 
@@ -237,6 +261,7 @@ def Bool(value):
     """
     return get_env().formula_manager.Bool(value)
 
+
 def Real(value):
     """Returns a Real constant with the given value.
 
@@ -245,6 +270,7 @@ def Real(value):
     """
     return get_env().formula_manager.Real(value)
 
+
 def TRUE():
     """Returns the Boolean constant TRUE.
 
@@ -252,6 +278,7 @@ def TRUE():
     """
     return get_env().formula_manager.TRUE()
 
+
 def FALSE():
     """Returns the Boolean constant FALSE.
 
@@ -259,22 +286,27 @@ def FALSE():
     """
     return get_env().formula_manager.FALSE()
 
+
 def And(*args):
     r""".. math:: \varphi_0 \land \cdots \land \varphi_n """
     return get_env().formula_manager.And(*args)
 
+
 def Or(*args):
     r""".. math:: \varphi_0 \lor \cdots \lor \varphi_n """
     return get_env().formula_manager.Or(*args)
 
+
 def Plus(*args):
     r""".. math:: \varphi_0 + \cdots + \varphi_n """
     return get_env().formula_manager.Plus(*args)
 
+
 def ToReal(formula):
     """Explicit cast of a term into a Real term."""
     return get_env().formula_manager.ToReal(formula)
 
+
 def AtMostOne(*args):
     """At most one can be true at anytime.
 
@@ -282,16 +314,19 @@ def AtMostOne(*args):
     """
     return get_env().formula_manager.AtMostOne(*args)
 
+
 def ExactlyOne(*args):
     """Given a set of boolean expressions requires that exactly one holds."""
     return get_env().formula_manager.ExactlyOne(*args)
 
+
 def AllDifferent(*args):
     """Given a set of non-boolean expressions, requires that each of them
     has value different from all the others
     """
     return get_env().formula_manager.AllDifferent(*args)
 
+
 def Xor(left, right):
     """Returns the XOR of left and right
 
@@ -303,14 +338,17 @@ def Xor(left, right):
     """
     return get_env().formula_manager.Xor(left, right)
 
+
 def Min(*args):
     """Minimum over a set of real or integer terms."""
     return get_env().formula_manager.Min(*args)
 
+
 def Max(*args):
     """Maximum over a set of real or integer terms"""
     return get_env().formula_manager.Max(*args)
 
+
 def EqualsOrIff(left, right):
     """Returns Equals() or Iff() depending on the type of the arguments.
 
@@ -319,6 +357,7 @@ def EqualsOrIff(left, right):
     """
     return get_env().formula_manager.EqualsOrIff(left, right)
 
+
 #
 # Bit Vectors
 #
@@ -340,6 +379,7 @@ def BV(value, width=None):
     """
     return get_env().formula_manager.BV(value, width)
 
+
 def SBV(value, width=None):
     """Returns a constant of type BitVector interpreting the sign.
 
@@ -354,6 +394,7 @@ def SBV(value, width=None):
     """
     return get_env().formula_manager.SBV(value, width)
 
+
 def BVOne(width=None):
     """Returns the unsigned one constant BitVector.
 
@@ -363,6 +404,7 @@ def BVOne(width=None):
     """
     return get_env().formula_manager.BVOne(width)
 
+
 def BVZero(width=None):
     """Returns the zero constant BitVector.
 
@@ -372,6 +414,7 @@ def BVZero(width=None):
     """
     return get_env().formula_manager.BVZero(width)
 
+
 def BVNot(formula):
     """Returns the bitwise negation of the bitvector
 
@@ -381,6 +424,7 @@ def BVNot(formula):
     """
     return get_env().formula_manager.BVNot(formula)
 
+
 def BVAnd(left, right):
     """Returns the Bit-wise AND of two bitvectors of the same size.
 
@@ -391,6 +435,7 @@ def BVAnd(left, right):
     """
     return get_env().formula_manager.BVAnd(left, right)
 
+
 def BVOr(left, right):
     """Returns the Bit-wise OR of two bitvectors of the same size.
 
@@ -401,6 +446,7 @@ def BVOr(left, right):
     """
     return get_env().formula_manager.BVOr(left, right)
 
+
 def BVXor(left, right):
     """Returns the Bit-wise XOR of two bitvectors of the same size.
 
@@ -411,6 +457,7 @@ def BVXor(left, right):
     """
     return get_env().formula_manager.BVXor(left, right)
 
+
 def BVConcat(left, right):
     """Returns the Concatenation of the two BVs
 
@@ -421,6 +468,7 @@ def BVConcat(left, right):
     """
     return get_env().formula_manager.BVConcat(left, right)
 
+
 def BVExtract(formula, start=0, end=None):
     """Returns the slice of formula from start to end (inclusive).
 
@@ -432,6 +480,7 @@ def BVExtract(formula, start=0, end=None):
     """
     return get_env().formula_manager.BVExtract(formula, start=start, end=end)
 
+
 def BVULT(left, right):
     """Returns the Unsigned Less-Than comparison of the two BVs.
 
@@ -442,6 +491,7 @@ def BVULT(left, right):
     """
     return get_env().formula_manager.BVULT(left, right)
 
+
 def BVUGT(left, right):
     """Returns the Unsigned Greater-Than comparison of the two BVs.
 
@@ -452,6 +502,7 @@ def BVUGT(left, right):
     """
     return get_env().formula_manager.BVUGT(left, right)
 
+
 def BVULE(left, right):
     """Returns the Unsigned Less-Equal comparison of the two BVs.
 
@@ -462,6 +513,7 @@ def BVULE(left, right):
     """
     return get_env().formula_manager.BVULE(left, right)
 
+
 def BVUGE(left, right):
     """Returns the Unsigned Greater-Equal comparison of the two BVs.
 
@@ -472,6 +524,7 @@ def BVUGE(left, right):
     """
     return get_env().formula_manager.BVUGE(left, right)
 
+
 def BVNeg(formula):
     """Returns the arithmetic negation of the BV.
 
@@ -481,6 +534,7 @@ def BVNeg(formula):
     """
     return get_env().formula_manager.BVNeg(formula)
 
+
 def BVAdd(left, right):
     """Returns the sum of two BV.
 
@@ -491,6 +545,7 @@ def BVAdd(left, right):
     """
     return get_env().formula_manager.BVAdd(left, right)
 
+
 def BVSub(left, right):
     """Returns the difference of two BV.
 
@@ -501,6 +556,7 @@ def BVSub(left, right):
     """
     return get_env().formula_manager.BVSub(left, right)
 
+
 def BVMul(left, right):
     """Returns the product of two BV.
 
@@ -511,6 +567,7 @@ def BVMul(left, right):
     """
     return get_env().formula_manager.BVMul(left, right)
 
+
 def BVUDiv(left, right):
     """Returns the Unsigned division of the two BV.
 
@@ -521,6 +578,7 @@ def BVUDiv(left, right):
     """
     return get_env().formula_manager.BVUDiv(left, right)
 
+
 def BVURem(left, right):
     """Returns the Unsigned remainder of the two BV.
 
@@ -531,6 +589,7 @@ def BVURem(left, right):
     """
     return get_env().formula_manager.BVURem(left, right)
 
+
 def BVLShl(left, right):
     """Returns the logical left shift the BV.
 
@@ -541,6 +600,7 @@ def BVLShl(left, right):
     """
     return get_env().formula_manager.BVLShl(left, right)
 
+
 def BVLShr(left, right):
     """Returns the logical right shift the BV.
 
@@ -551,6 +611,7 @@ def BVLShr(left, right):
     """
     return get_env().formula_manager.BVLShr(left, right)
 
+
 def BVAShr(left, right):
     """Returns the RIGHT arithmetic rotation of the left BV by the number
         of steps specified by the right BV.
@@ -563,6 +624,7 @@ def BVAShr(left, right):
     """
     return get_env().formula_manager.BVAShr(left, right)
 
+
 def BVRol(formula, steps):
     """Returns the LEFT rotation of the BV by the number of steps.
 
@@ -573,6 +635,7 @@ def BVRol(formula, steps):
     """
     return get_env().formula_manager.BVRol(formula, steps)
 
+
 def BVRor(formula, steps):
     """Returns the RIGHT rotation of the BV by the number of steps.
 
@@ -583,6 +646,7 @@ def BVRor(formula, steps):
     """
     return get_env().formula_manager.BVRor(formula, steps)
 
+
 def BVZExt(formula, increase):
     """Returns the zero-extension of the BV.
 
@@ -595,6 +659,7 @@ def BVZExt(formula, increase):
     """
     return get_env().formula_manager.BVZExt(formula, increase)
 
+
 def BVSExt(formula, increase):
     """Returns the signed-extension of the BV.
 
@@ -607,6 +672,7 @@ def BVSExt(formula, increase):
     """
     return get_env().formula_manager.BVSExt(formula, increase)
 
+
 def BVSLT(left, right):
     """Returns the Signed Less-Than comparison of the two BVs.
 
@@ -617,6 +683,7 @@ def BVSLT(left, right):
     """
     return get_env().formula_manager.BVSLT(left, right)
 
+
 def BVSLE(left, right):
     """Returns the Signed Less-Equal comparison of the two BVs.
 
@@ -627,6 +694,7 @@ def BVSLE(left, right):
     """
     return get_env().formula_manager.BVSLE(left, right)
 
+
 def BVSGT(left, right):
     """Returns the Signed Greater-Than comparison of the two BVs.
 
@@ -637,6 +705,7 @@ def BVSGT(left, right):
     """
     return get_env().formula_manager.BVSGT(left, right)
 
+
 def BVSGE(left, right):
     """Returns the Signed Greater-Equal comparison of the two BVs.
 
@@ -647,6 +716,7 @@ def BVSGE(left, right):
     """
     return get_env().formula_manager.BVSGE(left, right)
 
+
 def BVSDiv(left, right):
     """Returns the Signed division of the two BVs.
 
@@ -657,6 +727,7 @@ def BVSDiv(left, right):
     """
     return get_env().formula_manager.BVSDiv(left, right)
 
+
 def BVSRem(left, right):
     """Returns the Signed remainder of the two BVs
 
@@ -667,6 +738,7 @@ def BVSRem(left, right):
     """
     return get_env().formula_manager.BVSRem(left, right)
 
+
 def BVComp(left, right):
     """Returns a BV of size 1 equal to 0 if left is equal to right,
         otherwise equal to 1.
@@ -679,6 +751,7 @@ def BVComp(left, right):
     """
     return get_env().formula_manager.BVComp(left, right)
 
+
 #
 # Arrays
 #
@@ -692,6 +765,7 @@ def Select(array, index):
     """
     return get_env().formula_manager.Select(array, index)
 
+
 def Store(array, index, value):
     """Returns a STORE application with given value on array at the given index
 
@@ -702,6 +776,7 @@ def Store(array, index, value):
     """
     return get_env().formula_manager.Store(array, index, value)
 
+
 def Array(idx_type, default, assigned_values=None):
     """Returns an Array with the given index type and initialization.
 
@@ -721,6 +796,7 @@ def Array(idx_type, default, assigned_values=None):
     """
     return get_env().formula_manager.Array(idx_type, default, assigned_values)
 
+
 ##
 ## Shortcuts for Solvers Factory
 ##
@@ -738,6 +814,7 @@ def Solver(quantified=False, name=None, logic=None, **kwargs):
                                     logic=logic,
                                     **kwargs)
 
+
 def UnsatCoreSolver(quantified=False, name=None, logic=None,
                     unsat_cores_mode="all"):
     """Returns a solver supporting unsat core extraction.
@@ -754,6 +831,7 @@ def UnsatCoreSolver(quantified=False, name=None, logic=None,
                                              logic=logic,
                                              unsat_cores_mode=unsat_cores_mode)
 
+
 def QuantifierEliminator(name=None, logic=None):
     """Returns a quantifier eliminator.
 
@@ -765,6 +843,7 @@ def QuantifierEliminator(name=None, logic=None):
     """
     return get_env().factory.QuantifierEliminator(name=name, logic=logic)
 
+
 def Interpolator(name=None, logic=None):
     """Returns an interpolator
 
@@ -775,14 +854,18 @@ def Interpolator(name=None, logic=None):
     """
     return get_env().factory.Interpolator(name=name, logic=logic)
 
-def is_sat(formula, solver_name=None, logic=None):
+
+def is_sat(formula, solver_name=None, logic=None, portfolio=None):
     """ Returns whether a formula is satisfiable.
 
     :param formula: The formula to check satisfiability
     :type  formula: FNode
     :param solver_name: Specify the name of the solver to be used
+    :type  solver_name: string
     :param logic: Specify the logic that is going to be used
-    :returns: Whether the formula is SAT or UNSAT
+    :param portfolio: A list of solver names to perform portfolio solving.
+    :type  portfolio: An iterable of solver names
+    :returns: Whether the formula is SAT or UNSAT.
     :rtype: bool
     """
     env = get_env()
@@ -792,7 +875,9 @@ def is_sat(formula, solver_name=None, logic=None):
 
     return env.factory.is_sat(formula,
                               solver_name=solver_name,
-                              logic=logic)
+                              logic=logic,
+                              portfolio=portfolio)
+
 
 def get_model(formula, solver_name=None, logic=None):
     """ Similar to :py:func:`is_sat` but returns a model if the formula is
@@ -813,6 +898,7 @@ def get_model(formula, solver_name=None, logic=None):
                                  solver_name=solver_name,
                                  logic=logic)
 
+
 def get_implicant(formula, solver_name=None, logic=None):
     """Returns a formula f_i such that Implies(f_i, formula) is valid or None
     if formula is unsatisfiable.
@@ -835,6 +921,7 @@ def get_implicant(formula, solver_name=None, logic=None):
                                      solver_name=solver_name,
                                      logic=logic)
 
+
 def get_unsat_core(clauses, solver_name=None, logic=None):
     """Similar to :py:func:`get_model` but returns the unsat core of the
     conjunction of the input clauses
@@ -854,13 +941,15 @@ def get_unsat_core(clauses, solver_name=None, logic=None):
                                       solver_name=solver_name,
                                       logic=logic)
 
-def is_valid(formula, solver_name=None, logic=None):
+
+def is_valid(formula, solver_name=None, logic=None, portfolio=None):
     """Similar to :py:func:`is_sat` but checks validity.
 
     :param formula: The target formula
     :type  formula: FNode
     :param solver_name: Specify the name of the solver to be used
     :param logic: Specify the logic that is going to be used
+    :param portfolio: A list of solver names to perform portfolio solving.
     :returns: Whether the formula is SAT or UNSAT but checks validity
     :rtype: bool
     """
@@ -871,15 +960,18 @@ def is_valid(formula, solver_name=None, logic=None):
 
     return env.factory.is_valid(formula,
                                 solver_name=solver_name,
-                                logic=logic)
+                                logic=logic,
+                                portfolio=portfolio)
 
-def is_unsat(formula, solver_name=None, logic=None):
+
+def is_unsat(formula, solver_name=None, logic=None, portfolio=None):
     """Similar to :py:func:`is_sat` but checks unsatisfiability.
 
     :param formula: The target formula
     :type  formula: FNode
     :param solver_name: Specify the name of the solver to be used
     :param logic: Specify the logic that is going to be used
+    :param portfolio: A list of solver names to perform portfolio solving.
     :returns: Whether the formula is UNSAT or not
     :rtype: bool
     """
@@ -890,7 +982,9 @@ def is_unsat(formula, solver_name=None, logic=None):
 
     return env.factory.is_unsat(formula,
                                 solver_name=solver_name,
-                                logic=logic)
+                                logic=logic,
+                                portfolio=portfolio)
+
 
 def qelim(formula, solver_name=None, logic=None):
     """Performs quantifier elimination of the given formula.
@@ -910,6 +1004,7 @@ def qelim(formula, solver_name=None, logic=None):
                              solver_name=solver_name,
                              logic=logic)
 
+
 def binary_interpolant(formula_a, formula_b, solver_name=None, logic=None):
     """Computes an interpolant of (formula_a, formula_b).
 
@@ -935,6 +1030,7 @@ def binary_interpolant(formula_a, formula_b, solver_name=None, logic=None):
                                           solver_name=solver_name,
                                           logic=logic)
 
+
 def sequence_interpolant(formulas, solver_name=None, logic=None):
     """Computes a sequence interpolant of the formulas.
 
@@ -959,6 +1055,7 @@ def sequence_interpolant(formulas, solver_name=None, logic=None):
                                             solver_name=solver_name,
                                             logic=logic)
 
+
 def read_configuration(config_filename, environment=None):
     """Reads the pysmt configuration of the given file path and applies
     it on the specified environment. If no environment is specified,
@@ -971,6 +1068,7 @@ def read_configuration(config_filename, environment=None):
         environment = get_env()
     config.configure_environment(config_filename, environment)
 
+
 def write_configuration(config_filename, environment=None):
     """Dumps the current pysmt configuration to the specified file path
 
@@ -981,6 +1079,7 @@ def write_configuration(config_filename, environment=None):
         environment = get_env()
     config.write_environment_configuration(config_filename, environment)
 
+
 def read_smtlib(fname):
     """Reads the SMT formula from the given file.
 
@@ -992,6 +1091,7 @@ def read_smtlib(fname):
     """
     return pysmt.smtlib.parser.get_formula_fname(fname)
 
+
 def write_smtlib(formula, fname):
     """Reads the SMT formula from the given file.
 
diff --git a/pysmt/solvers/btor.py b/pysmt/solvers/btor.py
index 2973547..757ede3 100644
--- a/pysmt/solvers/btor.py
+++ b/pysmt/solvers/btor.py
@@ -90,6 +90,10 @@ class BoolectorSolver(IncrementalTrackingSolver,
         self.declarations = {}
         return
 
+# EOC BoolectorOptions
+
+        pass
+
     @clear_pending_pop
     def _reset_assertions(self):
         raise NotImplementedError
diff --git a/pysmt/solvers/eager.py b/pysmt/solvers/eager.py
index 89b767b..d207b33 100644
--- a/pysmt/solvers/eager.py
+++ b/pysmt/solvers/eager.py
@@ -51,7 +51,6 @@ class EagerModel(Model):
             raise PysmtTypeError("Was expecting a constant but got %s" % res)
         return res
 
-
     def _complete_model(self, symbols):
         undefined_symbols = (s for s in symbols
                              if s not in self.completed_assignment)
diff --git a/pysmt/solvers/msat.py b/pysmt/solvers/msat.py
index 641fd5c..2d073b0 100644
--- a/pysmt/solvers/msat.py
+++ b/pysmt/solvers/msat.py
@@ -1356,3 +1356,5 @@ class MSatBoolUFRewriter(IdentityDagWalker):
             stack = tmp
         res = stack[0]
         return res
+
+# EOC MSatBoolUFRewriter
diff --git a/pysmt/solvers/options.py b/pysmt/solvers/options.py
new file mode 100644
index 0000000..b8b03da
--- /dev/null
+++ b/pysmt/solvers/options.py
@@ -0,0 +1,111 @@
+#
+# This file is part of pySMT.
+#
+#   Copyright 2014 Andrea Micheli and Marco Gario
+#
+#   Licensed under the Apache License, Version 2.0 (the "License");
+#   you may not use this file except in compliance with the License.
+#   You may obtain a copy of the License at
+#
+#       http://www.apache.org/licenses/LICENSE-2.0
+#
+#   Unless required by applicable law or agreed to in writing, software
+#   distributed under the License is distributed on an "AS IS" BASIS,
+#   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+#   See the License for the specific language governing permissions and
+#   limitations under the License.
+#
+"""A SolverOptions class is associated to each Solver to handle its
+configuration. We consider two types of options. The first type is
+available in most solvers, while the second type is solver-specific.
+
+The first type is handled and documented in the base class
+SolverOptions: generate_models, incremental etc.
+The second type is handled within the dictionary "solver_options".
+
+To use the Options it is necessary to:
+
+* Define the class attribute OptionsClass within the Solver Class
+* Validate the options during in SolverOptions.__init__
+* Implement the method SolverOptions.__call__
+* During Solver.__init__ the solver must call the option class::
+
+    self.options(self)
+
+"""
+
+import abc
+
+class SolverOptions(object):
+    """Solver Options shared by most solvers.
+
+    * generate_models : True, False
+      Enable model generation. Needed for get_value, get_model etc.
+
+    * incremental: True, False
+      Enable incremental interface (push, pop)
+
+    * unsat_cores_mode: None, "named", "all"
+      Enable UNSAT core extraction using "named" or "all" strategy.
+
+    * random_seed: None, integer
+      Sets the random seed for the solver
+
+    * solver_options: dictionary
+      Provides solver specific options
+
+    """
+    __metaclass__ = abc.ABCMeta
+
+    def __init__(self, generate_models=True, incremental=True,
+                 unsat_cores_mode=None, random_seed=None,
+                 solver_options=None):
+
+        if generate_models not in (True, False):
+            raise ValueError("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)
+        self.incremental = incremental
+
+        if unsat_cores_mode not in (None, "named", "all"):
+            raise ValueError("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)
+        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)
+        else:
+            solver_options = dict()
+        self.solver_options = solver_options
+
+    @abc.abstractmethod
+    def __call__(self, solver):
+        """Handle the setting options within solver"""
+        raise NotImplementedError
+
+    def as_kwargs(self):
+        """Construct a dictionary object that can be used as **kwargs.
+
+        This can be used to duplicate the options.
+        """
+        kwargs = {}
+        for k in ("generate_models", "incremental", "unsat_cores_mode",
+                  "random_seed", "solver_options"):
+            v = getattr(self, k)
+            kwargs[k] = v
+        return kwargs
+
+# EOC SolverOptions
diff --git a/pysmt/solvers/portfolio.py b/pysmt/solvers/portfolio.py
new file mode 100644
index 0000000..514afb7
--- /dev/null
+++ b/pysmt/solvers/portfolio.py
@@ -0,0 +1,255 @@
+#
+# This file is part of pySMT.
+#
+#   Copyright 2014 Andrea Micheli and Marco Gario
+#
+#   Licensed under the Apache License, Version 2.0 (the "License");
+#   you may not use this file except in compliance with the License.
+#   You may obtain a copy of the License at
+#
+#       http://www.apache.org/licenses/LICENSE-2.0
+#
+#   Unless required by applicable law or agreed to in writing, software
+#   distributed under the License is distributed on an "AS IS" BASIS,
+#   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+#   See the License for the specific language governing permissions and
+#   limitations under the License.
+#
+import logging
+from multiprocessing import Process, Queue, Pipe
+
+from pysmt.solvers.solver import IncrementalTrackingSolver, SolverOptions
+from pysmt.decorators import clear_pending_pop
+
+
+LOGGER = logging.getLogger(__name__)
+_debug = LOGGER.debug
+
+
+class PortfolioOptions(SolverOptions):
+
+    def __init__(self, **base_options):
+        SolverOptions.__init__(self, **base_options)
+        self.exit_on_exception = False
+        for k,v in self.solver_options.items():
+            if k == "exit_on_exception":
+                if v not in (True, False):
+                    raise ValueError("Invalid value for %s: %s" % \
+                                     (str(k),str(v)))
+            else:
+                raise ValueError("Unrecognized option '%s'." % k)
+            # Store option
+            setattr(self, k, v)
+
+    def __call__(self, solver):
+        pass
+
+# EOC PortfolioOptions
+
+
+class Portfolio(IncrementalTrackingSolver):
+    """Create a portfolio instance of multiple Solvers."""
+    OptionsClass = PortfolioOptions
+
+    def __init__(self, solvers_set, environment, logic, **options):
+        """Creates a portfolio using the specified solvers.
+
+        Solver_set is an iterable. Elements of solver_set can be
+         1) a name of a solver
+         2) a tuple containing a name of a solver and dict of options
+
+        E.g.,
+           Portfolio(["msat", "z3"], incremental=True)
+              or
+           Porfolio([("msat", {"random_seed": 1}), ("msat", {"random_seed": 2})],
+                     incremental=True)
+
+        Options specified in the Portfolio are shared among all
+        solvers, e.g., in the first example all solvers will receive
+        the option 'incremental=True'.
+
+        One process will be used for each of the solvers.
+        """
+        IncrementalTrackingSolver.__init__(self,
+                                           environment=environment,
+                                           logic=logic,
+                                           **options)
+        self.solvers = []
+        self._process_solver_set(solvers_set)
+        # Check that the names are valid ?
+        all_solvers = set(self.environment.factory.all_solvers())
+        not_found = set(s for s,_ in self.solvers) - all_solvers
+        if len(not_found) != 0:
+            raise ValueError("Cannot find solvers %s" % not_found)
+
+        # After Solving, we only keep the solver that finished first.
+        # We can extract models from the solver, unsat cores, etc
+        self._ext_solver = None # Existing solver Process
+        self._ctrl_pipe = None  # Ctrl Pipe to the existing solver
+
+    def _process_solver_set(self, sset):
+        """The sset can contain both solver names and pairs name options."""
+        global_opts = self.options.as_kwargs()
+        # Remove solver_options from global_opts. These are the
+        # Portfolio specific options and might not make sense for the
+        # solvers.
+        del global_opts["solver_options"]
+        for elem in sset:
+            if type(elem) is str:
+                sname = elem
+                opts = global_opts
+            else:
+                sname, local_opts = elem
+                opts = dict(global_opts)
+                for k,v in local_opts.items():
+                    # local_opts has priority over global_opts
+                    opts[k] = v
+            self.solvers.append((sname, opts))
+
+    def _reset_assertions(self):
+        pass
+
+    @clear_pending_pop
+    def _add_assertion(self, formula, named=None):
+        return formula
+
+    @clear_pending_pop
+    def _push(self, levels=1):
+        pass
+
+    @clear_pending_pop
+    def _pop(self, levels=1):
+        pass
+
+    @clear_pending_pop
+    def _solve(self, assumptions=None):
+        # We destroy the last solver before solving again. Note: We
+        # might be able to do something smarter by keeping track of
+        # the state of the solver. This, however, requires more
+        # booking (e.g., we need to assert expressions incrementaly,
+        # instead of in one shot!)
+        self._close_existing()
+
+        formula = self.environment.formula_manager.And(self.assertions)
+        _debug("Creating Queue and Pipe")
+        signaling_queue = Queue()
+        child_ctrl_pipe, my_ctrl_pipe = Pipe()
+        self._ctrl_pipe = my_ctrl_pipe
+
+        processes = []
+        for idx, (sname, opts) in enumerate(self.solvers):
+            _debug("Creating instance of %s", sname)
+            options = opts
+            _p = Process(name="%d (%s)" % (idx, sname),
+                         target=_run_solver,
+                         args=("%d (%s)" % (idx, sname),
+                               sname, options, formula,
+                               signaling_queue, child_ctrl_pipe))
+            processes.append(_p)
+            _p.start()
+            _debug("Started instance of %s", sname)
+
+        while True:
+            (sname, res) = signaling_queue.get(block=True)
+            if isinstance(res, BaseException):
+                if self.options.exit_on_exception:
+                    # Close all solvers and raise exception
+                    for p in processes:
+                        p.terminate()
+                    raise res
+                else:
+                    continue
+            else:
+                assert type(res) is bool, type(res)
+                break
+        _debug("Solver %s finished first saying %s", sname, res)
+        # Kill all processes, except for the "winner"
+        for p in processes:
+            if p.name == sname:
+                self._ext_solver = p
+            else:
+                p.terminate()
+
+        return res
+
+    def get_value(self, formula):
+        if not self._ext_solver:
+            raise ValueError("No SAT model")
+
+        self._ctrl_pipe.send(("get_value", formula))
+        res = self._ctrl_pipe.recv()
+        return self.environment.formula_manager.normalize(res)
+
+    def get_model(self):
+        from pysmt.solvers.eager import EagerModel
+
+        if not self._ext_solver:
+            raise ValueError("No SAT model")
+
+        self._ctrl_pipe.send("get_model")
+        # Contextualize the result within the calling process
+        _normalize = self.environment.formula_manager.normalize
+        model_list = self._ctrl_pipe.recv()
+        model = {}
+        for k,v in model_list:
+            _k, _v = _normalize(k), _normalize(v)
+            model[_k] = _v
+
+        return EagerModel(model)
+
+    def _close_existing(self):
+        _debug("Closing resources..")
+        if self._ctrl_pipe :
+            self._ctrl_pipe.send("exit")
+            self._ctrl_pipe = None
+        if self._ext_solver and self._ext_solver.is_alive():
+            self._ext_solver.terminate()
+            _debug("Previous solver killed")
+
+    def _exit(self):
+        self._close_existing()
+
+# EOC Portfolio
+
+# Function to pass to the solver
+def _run_solver(idx, solver, options, formula, signaling_queue, ctrl_pipe):
+    """Function used by the child Process to handle Portfolio requests.
+
+    solver  : name of the solver
+    options : options for the solver
+    formula : formula to assert
+    signaling_queue: queue in which to write to indicate completion of solve
+    ctrl_pipe: Pipe to communicate with parent process *after* solve
+    """
+    from pysmt.environment import get_env
+
+    Solver = get_env().factory.Solver
+    with Solver(name=solver, **options) as s:
+        s.add_assertion(formula)
+        try:
+            local_res = s.solve()
+        except Exception as ex:
+            signaling_queue.put((solver, ex))
+            return
+
+        signaling_queue.put((idx, local_res))
+        _exit = False
+        while not _exit:
+            try:
+                cmd = ctrl_pipe.recv()
+            except EOFError:
+                break
+            if type(cmd) == tuple:
+                cmd, args = cmd
+            if cmd == "exit":
+                _exit = True
+            elif cmd == "get_model":
+                # MG: Can we pickle the EagerModel directly?
+                # Note: contextualization happens on the receiver side
+                model = list(s.get_model())
+                ctrl_pipe.send(model)
+            elif cmd == "get_value":
+                args = get_env().formula_manager.normalize(args)
+                ctrl_pipe.send(s.get_value(args))
+            else:
+                raise ValueError("Unknown command '%s'" % cmd)
diff --git a/pysmt/solvers/solver.py b/pysmt/solvers/solver.py
index 809f65b..1253f21 100644
--- a/pysmt/solvers/solver.py
+++ b/pysmt/solvers/solver.py
@@ -15,75 +15,12 @@
 #   See the License for the specific language governing permissions and
 #   limitations under the License.
 #
-import abc
+from six.moves import xrange
 
 from pysmt.typing import BOOL
+from pysmt.solvers.options import SolverOptions
 from pysmt.exceptions import (SolverReturnedUnknownResultError, PysmtValueError,
                               PysmtTypeError, SolverStatusError)
-from six.moves import xrange
-
-
-class SolverOptions(object):
-    """Solver Options shared by most solvers.
-
-    * generate_models : True, False
-      Enable model generation. Needed for get_value, get_model etc.
-
-    * incremental: True, False
-      Enable incremental interface (push, pop)
-
-    * unsat_cores_mode: None, "named", "all"
-      Enable UNSAT core extraction using "named" or "all" strategy.
-
-    * random_seed: None, integer
-      Sets the random seed for the solver
-
-    * solver_options: dictionary
-      Provides solver specific options
-
-    """
-    __metaclass__ = abc.ABCMeta
-
-    def __init__(self, generate_models=True, incremental=True,
-                 unsat_cores_mode=None, random_seed=None,
-                 solver_options=None):
-
-        if generate_models not in (True, False):
-            raise PysmtValueError("Invalid value %s for 'generate_models'" \
-                                  % generate_models)
-        self.generate_models = generate_models
-
-        if incremental not in (True, False):
-            raise PysmtValueError("Invalid value %s for 'incremental'" \
-                                  % incremental)
-        self.incremental = incremental
-
-        if unsat_cores_mode not in (None, "named", "all"):
-            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 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 PysmtValueError("Invalid value %s for 'solver_options'" \
-                                      % solver_options)
-        else:
-            solver_options = dict()
-        self.solver_options = solver_options
-
-    @abc.abstractmethod
-    def __call__(self, solver):
-        """Handle the setting options within solver"""
-        raise NotImplementedError
-
-# EOC SolverOptions
 
 
 class Solver(object):
@@ -263,6 +200,26 @@ class Solver(object):
         """Add assertion to the solver."""
         raise NotImplementedError
 
+    def solve(self, assumptions=None):
+        """Returns the satisfiability value of the asserted formulas.
+
+        Assumptions is a list of Boolean variables or negations of
+        boolean variables. If assumptions is specified, the
+        satisfiability result is computed assuming that all the
+        specified literals are True.
+
+        A call to solve([a1, ..., an]) is functionally equivalent to:
+
+        push()
+        add_assertion(And(a1, ..., an))
+        res = solve()
+        pop()
+        return res
+
+        but is in general more efficient.
+        """
+        raise NotImplementedError
+
     def print_model(self, name_filter=None):
         """Prints the model (if one exists).
 


Test patch:
diff --git a/pysmt/test/test_models.py b/pysmt/test/test_models.py
index 4f5a207..149de8a 100644
--- a/pysmt/test/test_models.py
+++ b/pysmt/test/test_models.py
@@ -22,7 +22,6 @@ from pysmt.test import TestCase, skipIfNoSolverForLogic, main
 from pysmt.logics import QF_UFLIRA, QF_LRA, QF_BOOL
 from pysmt.solvers.eager import EagerModel
 
-
 class TestModels(TestCase):
 
     @skipIfNoSolverForLogic(QF_LRA)
@@ -71,7 +70,16 @@ class TestModels(TestCase):
         for (k,_) in m:
             self.assertFalse(k == z)
 
+    @skipIfNoSolverForLogic(QF_BOOL)
+    def test_pickle_eager_model(self):
+        import pickle
 
+        x, y = Symbol("x"), Symbol("y")
+        with Solver(logic=QF_BOOL) as s:
+            s.add_assertion(And(x,y))
+            assert s.solve()
+            model = list(s.get_model())
+            self.assertIsNotNone(pickle.dumps(model, -1))
 
 if __name__ == '__main__':
     main()
diff --git a/pysmt/test/test_portfolio.py b/pysmt/test/test_portfolio.py
new file mode 100644
index 0000000..d602368
--- /dev/null
+++ b/pysmt/test/test_portfolio.py
@@ -0,0 +1,173 @@
+#
+# This file is part of pySMT.
+#
+#   Copyright 2014 Andrea Micheli and Marco Gario
+#
+#   Licensed under the Apache License, Version 2.0 (the "License");
+#   you may not use this file except in compliance with the License.
+#   You may obtain a copy of the License at
+#
+#       http://www.apache.org/licenses/LICENSE-2.0
+#
+#   Unless required by applicable law or agreed to in writing, software
+#   distributed under the License is distributed on an "AS IS" BASIS,
+#   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+#   See the License for the specific language governing permissions and
+#   limitations under the License.
+#
+import os
+
+from pysmt.test import TestCase
+from pysmt.test import skipIfSolverNotAvailable
+from pysmt.test.examples import get_example_formulae
+from pysmt.logics import QF_LRA, QF_UFLIRA, QF_BOOL
+from pysmt.solvers.portfolio import Portfolio
+from pysmt.smtlib.parser import get_formula_fname
+from pysmt.shortcuts import TRUE, Implies, Equals, Symbol, FALSE
+from pysmt.shortcuts import reset_env, is_sat
+from pysmt.typing import REAL
+
+
+class PortfolioTestCase(TestCase):
+
+    @skipIfSolverNotAvailable("z3")
+    @skipIfSolverNotAvailable("msat")
+    @skipIfSolverNotAvailable("cvc4")
+    def test_basic(self):
+        with Portfolio(["z3", "msat", "cvc4"],
+                       environment=self.env,
+                       logic="QF_LRA") as p:
+            for example in get_example_formulae():
+                if not example.logic <= QF_LRA: continue
+                res = p.is_sat(example.expr)
+                self.assertEqual(res, example.is_sat, example.expr)
+                if res:
+                    self.assertTrue(p.get_model().get_value(example.expr).is_true())
+
+    @skipIfSolverNotAvailable("msat")
+    @skipIfSolverNotAvailable("cvc4")
+    @skipIfSolverNotAvailable("yices")
+    def test_smtlib(self):
+        from pysmt.test.smtlib.parser_utils import SMTLIB_TEST_FILES, SMTLIB_DIR
+
+        for (logic, f, expected_result) in SMTLIB_TEST_FILES:
+            smtfile = os.path.join(SMTLIB_DIR, f)
+            if logic <= QF_UFLIRA:
+                self.run_smtlib(smtfile, logic, expected_result)
+
+    @skipIfSolverNotAvailable("msat")
+    def test_smtlib_multi_msat(self):
+        from pysmt.test.smtlib.parser_utils import SMTLIB_TEST_FILES, SMTLIB_DIR
+
+        for (logic, f, expected_result) in SMTLIB_TEST_FILES:
+            smtfile = os.path.join(SMTLIB_DIR, f)
+            if logic <= QF_UFLIRA:
+                env = reset_env()
+                formula = get_formula_fname(smtfile, env)
+                with Portfolio([("msat", {"random_seed": 1}),
+                                ("msat", {"random_seed": 17}),
+                                ("msat", {"random_seed": 42})],
+                               logic=logic,
+                               environment=env,
+                               incremental=False,
+                               generate_models=False) as s:
+                    res = s.is_sat(formula)
+                    result = "sat" if res else "unsat"
+                    self.assertEqual(expected_result, result, smtfile)
+
+    def run_smtlib(self, smtfile, logic, expected_result):
+        env = reset_env()
+        formula = get_formula_fname(smtfile, env)
+        with Portfolio(["cvc4", "msat", "yices"],
+                       logic=logic,
+                       environment=env,
+                       incremental=False,
+                       generate_models=False) as s:
+            res = s.is_sat(formula)
+            result = "sat" if res else "unsat"
+            self.assertEqual(expected_result, result, smtfile)
+
+    @skipIfSolverNotAvailable("msat")
+    @skipIfSolverNotAvailable("cvc4")
+    @skipIfSolverNotAvailable("z3")
+    def test_shortcuts(self):
+        for (expr, _, sat_res, logic) in get_example_formulae():
+            if not logic <= QF_UFLIRA: continue
+            res = is_sat(expr, portfolio=["z3", "cvc4", "msat"])
+            self.assertEqual(res, sat_res, expr)
+
+        with self.assertRaises(ValueError):
+            is_sat(TRUE(), portfolio=["supersolver"])
+
+    @skipIfSolverNotAvailable("msat")
+    @skipIfSolverNotAvailable("picosat")
+    @skipIfSolverNotAvailable("btor")
+    @skipIfSolverNotAvailable("bdd")
+    def test_get_value(self):
+        with Portfolio(["msat", "picosat", "btor", "bdd"],
+                       logic=QF_UFLIRA,
+                       environment=self.env,
+                       incremental=False,
+                       generate_models=True) as s:
+            x, y = Symbol("x"), Symbol("y")
+            s.add_assertion(Implies(x, y))
+            s.add_assertion(x)
+            res = s.solve()
+            self.assertTrue(res)
+            v = s.get_value(x)
+            self.assertTrue(v, TRUE())
+
+    @skipIfSolverNotAvailable("msat")
+    @skipIfSolverNotAvailable("cvc4")
+    @skipIfSolverNotAvailable("yices")
+    def test_incrementality(self):
+        with Portfolio(["cvc4", "msat", "yices"],
+                       logic=QF_UFLIRA,
+                       environment=self.env,
+                       incremental=True,
+                       generate_models=True) as s:
+            x, y = Symbol("x"), Symbol("y")
+            s.add_assertion(Implies(x, y))
+            s.push()
+            s.add_assertion(x)
+            res = s.solve()
+            self.assertTrue(res)
+            v = s.get_value(y)
+            self.assertTrue(v, TRUE())
+            s.pop()
+            s.add_assertion(x)
+            res = s.solve()
+            self.assertTrue(res)
+            v = s.get_value(x)
+            self.assertTrue(v, FALSE())
+
+    @skipIfSolverNotAvailable("z3")
+    @skipIfSolverNotAvailable("bdd")
+    def test_exceptions(self):
+        with Portfolio(["bdd", "z3"],
+                       logic=QF_BOOL,
+                       environment=self.env,
+                       incremental=True,
+                       generate_models=True,
+                       solver_options={"exit_on_exception":False}) as s:
+            s.add_assertion(Equals(Symbol("r", REAL), Symbol("r", REAL)))
+            res = s.solve()
+            self.assertTrue(res)
+
+            # TODO: How can we make this test more robust?
+            # It assumes that bdd will raise an error before z3.
+            # It should be so, but this is non-deterministic by nature
+            with Portfolio(["bdd", "z3"],
+                           logic=QF_BOOL,
+                           environment=self.env,
+                           incremental=True,
+                           generate_models=True,
+                           solver_options={"exit_on_exception":True}) as s:
+                s.add_assertion(Equals(Symbol("r", REAL), Symbol("r", REAL)))
+                with self.assertRaises(Exception):
+                    s.solve()
+
+
+if __name__ == "__main__":
+    import unittest
+    unittest.main()
diff --git a/pysmt/test/test_solving.py b/pysmt/test/test_solving.py
index 64da45c..84d32f0 100644
--- a/pysmt/test/test_solving.py
+++ b/pysmt/test/test_solving.py
@@ -31,9 +31,10 @@ from pysmt.exceptions import (SolverReturnedUnknownResultError,
                               InternalSolverError, NoSolverAvailableError,
                               ConvertExpressionError, UndefinedLogicError,
                               PysmtTypeError, PysmtValueError)
-from pysmt.logics import QF_UFLIRA, QF_BOOL, QF_LRA, AUTO
+from pysmt.logics import QF_UFLIRA, QF_BOOL, QF_LRA, AUTO, QF_BV
 from pysmt.logics import convert_logic_from_string
 
+
 class TestBasic(TestCase):
 
     @skipIfNoSolverForLogic(QF_BOOL)
@@ -573,5 +574,17 @@ class TestBasic(TestCase):
                 s.is_sat(Not(Symbol("x")))
 
 
+    @skipIfSolverNotAvailable("btor")
+    def test_btor_options(self):
+        for (f, _, sat, logic) in get_example_formulae():
+            if logic == QF_BV:
+                solver = Solver(name="btor",
+                                solver_options={"rewrite_level":0,
+                                                "dual_prop":1,
+                                                "eliminate_slices":1})
+                solver.add_assertion(f)
+                res = solver.solve()
+                self.assertTrue(res == sat)
+
 if __name__ == '__main__':
     main()