Portfolio of parallel solvers (#2420)

* First attempt to have parallel solvers * busy waiting * fix * fixes * linted * fixed mypy types * fixed tests * fixes * linted * fixed mypy types * adjusted the number of workers * randomize solvers * simplified code * fix * fixes * use portfolio by default * use the portfolio solver by default in the detectors (and reverted last commit) * rewrote the recv function * fixes * fixes * use the portfolio solver by default in the general evm tests * fix * more fixes * fixes * fix * fix * fix * fix * fixes * fix * code refactoring * mypy fix * linted code Co-authored-by: Eric Hennenfent <[email protected]>
2026-10-12 02:23:44 +00:00 · 2021-06-10 12:09:33 -07:00
parent 2380d5ebc4
commit 5e4d358408
6 changed files with 348 additions and 101 deletions
@@ -49,7 +49,11 @@ consts.add(
    default=False,
    description="If True enables to run workers over the network UNIMPLEMENTED",
 )
-consts.add("procs", default=10, description="Number of parallel processes to spawn")
+consts.add(
+    "procs",
+    default=12,
+    description="Number of parallel processes to spawn in order to run every task, including solvers",
+)

 proc_type = MProcessingType.threading
 if sys.platform != "linux":
@@ -380,8 +384,9 @@ class ManticoreBase(Eventful):
            raise TypeError(f"Invalid initial_state type: {type(initial_state).__name__}")
        self._put_state(initial_state)

+        nworkers = max(consts.procs // initial_state._solver.ncores, 1)
        # Workers will use manticore __dict__ So lets spawn them last
-        self._workers = [self._worker_type(id=i, manticore=self) for i in range(consts.procs)]
+        self._workers = [self._worker_type(id=i, manticore=self) for i in range(nworkers)]

        # Create log capture worker. We won't create the rest of the daemons until .run() is called
        self._daemon_threads: typing.Dict[int, DaemonThread] = {
@@ -15,15 +15,18 @@
 # You can add new constraints. A new constraint may change the state from {None, sat} to {sat, unsat, unknown}

 import os
+import fcntl
 import shutil
 import threading
 from queue import Queue
 import collections
 import shlex
 import time
+from abc import abstractmethod
 from functools import lru_cache
 from typing import Any, Dict, Tuple, Sequence, Optional, List
 from subprocess import PIPE, Popen, check_output
+from random import shuffle
 import re
 from . import operators as Operators
 from .constraints import *
@@ -32,17 +35,6 @@ from ...exceptions import Z3NotFoundError, SolverError, SolverUnknown, TooManySo
 from ...utils import config
 from . import issymbolic

-
-class SolverType(config.ConfigEnum):
-    """Used as configuration constant for choosing solver flavor"""
-
-    z3 = "z3"
-    cvc4 = "cvc4"
-    yices = "yices"
-    auto = "auto"
-    boolector = "boolector"
-
-
 logger = logging.getLogger(__name__)
 consts = config.get_group("smt")
 consts.add("timeout", default=120, description="Timeout, in seconds, for each Z3 invocation")
@@ -63,12 +55,6 @@ consts.add(
    "optimize", default=True, description="Use smtlib command optimize to find min/max if available"
 )

-consts.add(
-    "solver",
-    default=SolverType.auto,
-    description="Choose default smtlib2 solver (z3, yices, cvc4, boolector, auto)",
-)
-
 # Regular expressions used by the solver
 RE_GET_EXPR_VALUE_ALL = re.compile(
    "\(([a-zA-Z0-9_]*)[ \\n\\s]*(#b[0-1]*|#x[0-9a-fA-F]*|[\(]?_ bv[0-9]* [0-9]*|true|false)\\)"
@@ -84,6 +70,24 @@ RE_MIN_MAX_OBJECTIVE_EXPR_VALUE = re.compile(r"(?P<expr>.*?)\s+\|->\s+(?P<value>
 SOLVER_STATS = {"unknown": 0, "timeout": 0}


+class SolverType(config.ConfigEnum):
+    """Used as configuration constant for choosing solver flavor"""
+
+    z3 = "z3"
+    cvc4 = "cvc4"
+    yices = "yices"
+    auto = "auto"
+    portfolio = "portfolio"
+    boolector = "boolector"
+
+
+consts.add(
+    "solver",
+    default=SolverType.auto,
+    description="Choose default smtlib2 solver (z3, yices, cvc4, boolector, portfolio, auto)",
+)
+
+
 def _convert(v):
    r = None
    if v == "true":
@@ -203,6 +207,7 @@ class SmtlibProc:
        self._proc: Optional[Popen] = None
        self._command = command
        self._debug = debug
+        self._last_buf = ""

    def start(self):
        """Spawns POpen solver process"""
@@ -217,6 +222,11 @@ class SmtlibProc:
            close_fds=True,
        )

+        # stdout should be non-blocking
+        fl = fcntl.fcntl(self._proc.stdout, fcntl.F_GETFL)
+        fcntl.fcntl(self._proc.stdout, fcntl.F_SETFL, fl | os.O_NONBLOCK)
+        self._last_buf = ""
+
    def stop(self):
        """
        Stops the solver process by:
@@ -236,18 +246,6 @@ class SmtlibProc:
            # No need to wait for termination, zombies avoided.
        self._proc = None

-    def __readline_and_count(self):
-        assert self._proc
-        assert self._proc.stdout
-        buf = self._proc.stdout.readline()  # No timeout enforced here
-        # If debug is enabled check if the solver reports a syntax error
-        # Error messages may contain an unbalanced parenthesis situation
-        if self._debug:
-            if "(error" in buf:
-                raise SolverException(f"Error in smtlib: {buf}")
-        lparen, rparen = map(sum, zip(*((c == "(", c == ")") for c in buf)))
-        return buf, lparen, rparen
-
    def send(self, cmd: str) -> None:
        """
        Send a string to the solver.
@@ -259,17 +257,50 @@ class SmtlibProc:
        self._proc.stdout.flush()  # type: ignore
        self._proc.stdin.write(f"{cmd}\n")  # type: ignore

-    def recv(self) -> str:
-        """Reads the response from the smtlib solver"""
-        buf, left, right = self.__readline_and_count()
-        bufl = [buf]
-        while left != right:
-            buf, l, r = self.__readline_and_count()
-            bufl.append(buf)
-            left += l
-            right += r
+    def recv(self, wait=True) -> Optional[str]:
+        """Reads the response from the smtlib solver

-        buf = "".join(bufl).strip()
+        :param wait: a boolean that indicate to wait with a blocking call
+        until the results are available. Otherwise, it returns None if the solver
+        does not respond.
+
+        """
+        tries = 0
+        timeout = 0.0
+
+        buf = ""
+        if self._last_buf != "":  # we got a partial response last time, let's use it
+            buf = buf + self._last_buf
+
+        while True:
+            try:
+                buf = buf + self._proc.stdout.read()  # type: ignore
+                buf = buf.strip()
+            except TypeError:
+                if not wait:
+                    if buf != "":  # we got an error, but something was returned, let's save it
+                        self._last_buf = buf
+                    return None
+                else:
+                    tries += 1
+
+            if buf == "":
+                continue
+
+            # this verifies if the response from the solver is complete (it has balanced brackets)
+            lparen, rparen = map(sum, zip(*((c == "(", c == ")") for c in buf)))
+            if lparen == rparen and buf != "":
+                break
+
+            if tries > 3:
+                time.sleep(timeout)
+                timeout += 0.1
+
+        buf = buf.strip()
+        self._last_buf = ""
+
+        if "(error" in buf:
+            raise SolverException(f"Error in smtlib: {buf}")

        if self._debug:
            logger.debug("<%s", buf)
@@ -286,8 +317,19 @@ class SmtlibProc:


 class SMTLIBSolver(Solver):
+    ncores: Optional[int] = None
    sname: Optional[str] = None

+    @classmethod
+    @abstractmethod
+    def command(self) -> str:
+        raise NotImplementedError()
+
+    @classmethod
+    @abstractmethod
+    def inits(self) -> List[str]:
+        raise NotImplementedError()
+
    def __init__(
        self,
        command: str,
@@ -352,7 +394,11 @@ class SMTLIBSolver(Solver):
        start = time.time()
        self._smtlib.send("(check-sat)")
        status = self._smtlib.recv()
+        assert status is not None
        logger.debug("Check took %s seconds (%s)", time.time() - start, status)
+        if "ALARM TRIGGERED" in status:
+            return False
+
        if status not in ("sat", "unsat", "unknown"):
            raise SolverError(status)
        if consts.defaultunsat:
@@ -380,6 +426,7 @@ class SMTLIBSolver(Solver):
    def __getvalue_bv(self, expression_str: str) -> int:
        self._smtlib.send(f"(get-value ({expression_str}))")
        t = self._smtlib.recv()
+        assert t is not None
        base = 2
        m = RE_GET_EXPR_VALUE_FMT_BIN.match(t)
        if m is None:
@@ -399,14 +446,13 @@ class SMTLIBSolver(Solver):
        ret = self._smtlib.recv()
        return {"true": True, "false": False, "#b0": False, "#b1": True}[ret[2:-2].split(" ")[1]]

-    def __getvalue_all(
-        self, expressions_str: List[str], is_bv: List[bool]
-    ) -> Tuple[Dict[str, int], str]:
+    def __getvalue_all(self, expressions_str: List[str], is_bv: List[bool]) -> Dict[str, int]:
        all_expressions_str = " ".join(expressions_str)
        self._smtlib.send(f"(get-value ({all_expressions_str}))")
-        ret_solver = self._smtlib.recv()
+        ret_solver: Optional[str] = self._smtlib.recv()
+        assert ret_solver is not None
        return_values = re.findall(RE_GET_EXPR_VALUE_ALL, ret_solver)
-        return {value[0]: _convert(value[1]) for value in return_values}, ret_solver
+        return {value[0]: _convert(value[1]) for value in return_values}

    def _getvalue(self, expression) -> Union[int, bool, bytes]:
        """
@@ -708,7 +754,7 @@ class SMTLIBSolver(Solver):
            if values_to_ask == []:
                return values

-            values_returned, sol = self.__getvalue_all(values_to_ask, is_bv)
+            values_returned = self.__getvalue_all(values_to_ask, is_bv)
            for idx, expression in enumerate(expressions):
                if not issymbolic(expression):
                    continue
@@ -738,13 +784,26 @@ class SMTLIBSolver(Solver):
 class Z3Solver(SMTLIBSolver):
    sname = "z3"

+    @classmethod
+    def command(self) -> str:
+        return f"{consts.z3_bin} -t:{consts.timeout * 1000} -memory:{consts.memory} -smt2 -in"
+
+    @classmethod
+    def inits(self) -> List[str]:
+        return [
+            "(set-logic QF_AUFBV)",
+            "(set-option :global-decls false)",
+            "(set-option :tactic.solve_eqs.context_solve false)",
+        ]
+
    def __init__(self):
        """
        Build a Z3 solver instance.
        This is implemented using an external z3 solver (via a subprocess).
        See https://github.com/Z3Prover/z3
        """
-        command = f"{consts.z3_bin} -t:{consts.timeout * 1000} -memory:{consts.memory} -smt2 -in"
+        command = self.command()
+        self.ncores = 1

        init, support_minmax, support_reset, multiple_check = self.__autoconfig()
        super().__init__(
@@ -758,26 +817,12 @@ class Z3Solver(SMTLIBSolver):
        )

    def __autoconfig(self):
-        init = [
-            # http://smtlib.cs.uiowa.edu/logics-all.shtml#QF_AUFBV
-            # Closed quantifier-free formulas over the theory of bitvectors and bitvector arrays extended with
-            # free sort and function symbols.
-            "(set-logic QF_AUFBV)",
-            # The declarations and definitions will be scoped
-            "(set-option :global-decls false)",
-        ]
+        init = self.inits()

        # To cache what get-info returned; can be directly set when writing tests
        self.version = self._solver_version()
        support_reset = True

-        if self.version > Version(4, 8, 4):
-            # sam.moelius: Option "tactic.solve_eqs.context_solve" was turned on by this commit in z3:
-            #   https://github.com/Z3Prover/z3/commit/3e53b6f2dbbd09380cd11706cabbc7e14b0cc6a2
-            # Turning it off greatly improves Manticore's performance on test_integer_overflow_storageinvariant
-            # in test_consensys_benchmark.py.
-            init.append("(set-option :tactic.solve_eqs.context_solve false)")
-
        support_minmax = self.version >= Version(4, 4, 1)

        # Certain version of Z3 fails to handle multiple check-sat
@@ -814,9 +859,18 @@ class Z3Solver(SMTLIBSolver):
 class YicesSolver(SMTLIBSolver):
    sname = "yices"

+    @classmethod
+    def command(self) -> str:
+        return f"{consts.yices_bin} --timeout={consts.timeout}  --incremental"
+
+    @classmethod
+    def inits(self) -> List[str]:
+        return ["(set-logic QF_AUFBV)"]
+
    def __init__(self):
-        init = ["(set-logic QF_AUFBV)"]
-        command = f"{consts.yices_bin} --timeout={consts.timeout}  --incremental"
+        init = self.inits()
+        command = self.command()
+        self.ncores = 1
        super().__init__(
            command=command,
            init=init,
@@ -829,21 +883,198 @@ class YicesSolver(SMTLIBSolver):
 class CVC4Solver(SMTLIBSolver):
    sname = "cvc4"

+    @classmethod
+    def command(self) -> str:
+        return f"{consts.cvc4_bin} --tlimit={consts.timeout * 1000} --lang=smt2 --incremental"
+
+    @classmethod
+    def inits(self) -> List[str]:
+        return ["(set-logic QF_AUFBV)", "(set-option :produce-models true)"]
+
    def __init__(self):
-        init = ["(set-logic QF_AUFBV)", "(set-option :produce-models true)"]
-        command = f"{consts.cvc4_bin} --tlimit={consts.timeout * 1000} --lang=smt2 --incremental"
+        init = self.inits()
+        command = self.command()
+        self.ncores = 1
        super().__init__(command=command, init=init)


 class BoolectorSolver(SMTLIBSolver):
    sname = "boolector"

-    def __init__(self):
-        init = ["(set-logic QF_AUFBV)", "(set-option :produce-models true)"]
-        command = f"{consts.boolector_bin} --time={consts.timeout} -i"
+    @classmethod
+    def command(self) -> str:
+        return f"{consts.boolector_bin} --time={consts.timeout} -i"
+
+    @classmethod
+    def inits(self) -> List[str]:
+        return ["(set-logic QF_AUFBV)", "(set-option :produce-models true)"]
+
+    def __init__(self, args: List[str] = []):
+        init = self.inits()
+        command = self.command()
+        self.ncores = 1
        super().__init__(command=command, init=init)


+class SmtlibPortfolio:
+    def __init__(self, solvers: List[str], debug: bool = False):
+        """Single smtlib interactive process
+
+        :param command: the shell command to execute
+        :param debug: log all messaging
+        """
+        self._procs: Dict[str, SmtlibProc] = {}
+        self._solvers: List[str] = solvers
+        self._debug = debug
+
+    def start(self):
+        if len(self._procs) == 0:
+            for solver in self._solvers:
+                self._procs[solver] = SmtlibProc(solver_selector[solver].command(), self._debug)
+
+        for _, proc in self._procs.items():
+            proc.start()
+
+    def stop(self):
+        """
+        Stops the solver process by:
+        - sending a SIGKILL signal,
+        - waiting till the process terminates (so we don't leave a zombie process)
+        """
+        for solver, proc in self._procs.items():
+            proc.stop()
+
+    def send(self, cmd: str) -> None:
+        """
+        Send a string to the solver.
+
+        :param cmd: a SMTLIBv2 command (ex. (check-sat))
+        """
+        assert len(self._procs) > 0
+        inds = list(range(len(self._procs)))
+        shuffle(inds)
+
+        for i in inds:
+            solver = self._solvers[i]
+            proc = self._procs[solver]
+            if not proc.is_started():
+                continue
+
+            proc.send(cmd)
+
+    def recv(self) -> str:
+        """Reads the response from the smtlib solver"""
+        tries = 0
+        timeout = 0.0
+        inds = list(range(len(self._procs)))
+        # print(self._solvers)
+        while True:
+            shuffle(inds)
+            for i in inds:
+
+                solver = self._solvers[i]
+                proc = self._procs[solver]
+
+                if not proc.is_started():
+                    continue
+
+                buf = proc.recv(wait=False)
+                if buf is not None:
+
+                    for osolver in self._solvers:  # iterate on all the solvers
+                        if osolver != solver:  # check for the other ones
+                            self._procs[osolver].stop()  # stop them
+
+                    return buf
+                else:
+                    tries += 1
+
+            if tries > 10 * len(self._procs):
+                time.sleep(timeout)
+                timeout += 0.1
+
+    def _restart(self) -> None:
+        """Auxiliary to start or restart the external solver"""
+        self.stop()
+        self.start()
+
+    def is_started(self):
+        return len(self._procs) > 0
+
+    def init(self):
+        assert len(self._solvers) == len(self._procs)
+        for solver, proc in self._procs.items():
+            for cfg in solver_selector[solver].inits():
+                proc.send(cfg)
+
+
+class PortfolioSolver(SMTLIBSolver):
+    sname = "portfolio"
+
+    def __init__(self):
+        solvers = []
+        if shutil.which(consts.yices_bin):
+            solvers.append(consts.solver.yices.name)
+        # not sure we want z3 here, since it tends to be slower
+        # if shutil.which(consts.z3_bin):
+        #    solvers.append(consts.solver.z3.name)
+        if shutil.which(consts.cvc4_bin):
+            solvers.append(consts.solver.cvc4.name)
+        if shutil.which(consts.boolector_bin):
+            solvers.append(consts.solver.boolector.name)
+        if solvers == []:
+            raise SolverException(
+                f"No Solver not found. Install one ({consts.yices_bin}, {consts.z3_bin}, {consts.cvc4_bin}, {consts.boolector_bin})."
+            )
+
+        logger.info("Creating portfolio with solvers: " + ",".join(solvers))
+        assert len(solvers) > 0
+        support_reset: bool = False
+        support_minmax: bool = False
+        support_pushpop: bool = False
+        multiple_check: bool = True
+        debug: bool = False
+
+        self._smtlib: SmtlibPortfolio = SmtlibPortfolio(solvers, debug)
+        self._support_minmax = support_minmax
+        self._support_reset = support_reset
+        self._support_pushpop = support_pushpop
+        self._multiple_check = multiple_check
+
+        if not self._support_pushpop:
+            setattr(self, "_push", None)
+            setattr(self, "_pop", None)
+
+        if self._support_minmax and consts.optimize:
+            setattr(self, "optimize", self._optimize_fancy)
+        else:
+            setattr(self, "optimize", self._optimize_generic)
+        self.ncores = len(solvers)
+
+    def _reset(self, constraints: Optional[str] = None) -> None:
+        """Auxiliary method to reset the smtlib external solver to initial defaults"""
+        if self._support_reset:
+            self._smtlib.start()  # does not do anything if already started
+            self._smtlib.send("(reset)")
+        else:
+            self._smtlib.stop()  # does not do anything if already stopped
+            self._smtlib.start()
+
+        self._smtlib.init()
+
+        if constraints is not None:
+            self._smtlib.send(constraints)
+
+
+solver_selector = {
+    "cvc4": CVC4Solver,
+    "boolector": BoolectorSolver,
+    "yices": YicesSolver,
+    "z3": Z3Solver,
+    "portfolio": PortfolioSolver,
+}
+
+
 class SelectedSolver:
    choice = None

@@ -863,13 +1094,9 @@ class SelectedSolver:
                    raise SolverException(
                        f"No Solver not found. Install one ({consts.yices_bin}, {consts.z3_bin}, {consts.cvc4_bin}, {consts.boolector_bin})."
                    )
+
        else:
            cls.choice = consts.solver

-        SelectedSolver = {
-            "cvc4": CVC4Solver,
-            "boolector": BoolectorSolver,
-            "yices": YicesSolver,
-            "z3": Z3Solver,
-        }[cls.choice.name]
+        SelectedSolver = solver_selector[cls.choice.name]
        return SelectedSolver.instance()
@@ -103,7 +103,7 @@ run_truffle_tests(){
    mkdir truffle_tests
    cd truffle_tests
    truffle unbox metacoin
-    coverage run -m manticore . --contract MetaCoin --workspace output --exclude-all --thorough-mode --evm.oog ignore --evm.txfail optimistic
+    coverage run -m manticore . --contract MetaCoin --workspace output --exclude-all --thorough-mode --evm.oog ignore --evm.txfail optimistic --smt.solver portfolio
    # Truffle smoke test. We test if manticore is able to generate states
    # from a truffle project.
    count=$(find output/ -name '*tx' -type f | wc -l)
@@ -9,7 +9,7 @@ import os
 import shutil
 from manticore.platforms.evm import EVMWorld

-from manticore.core.smtlib import operators, ConstraintSet
+from manticore.core.smtlib import operators, ConstraintSet, SolverType
 from manticore.ethereum import (
    DetectDelegatecall,
    DetectEnvInstruction,
@@ -32,6 +32,9 @@ from typing import Tuple, Type
 consts = config.get_group("core")
 consts.mprocessing = consts.mprocessing.single

+consts = config.get_group("smt")
+consts.solver = SolverType.portfolio
+
 THIS_DIR = os.path.dirname(os.path.abspath(__file__))


@@ -14,8 +14,7 @@ import tempfile

 from manticore import ManticoreError
 from manticore.core.plugin import Plugin
-from manticore.core.smtlib import ConstraintSet, operators
-from manticore.core.smtlib import Z3Solver
+from manticore.core.smtlib import ConstraintSet, operators, PortfolioSolver, SolverType
 from manticore.core.smtlib.expression import BitVec, BitVecVariable
 from manticore.core.smtlib.visitors import to_constant
 from manticore.core.state import TerminateState
@@ -41,7 +40,9 @@ import io
 import contextlib


-solver = Z3Solver.instance()
+solver = PortfolioSolver.instance()
+consts = config.get_group("smt")
+consts.solver = SolverType.portfolio

 THIS_DIR = os.path.dirname(os.path.abspath(__file__))

@@ -73,7 +74,7 @@ class EthVerifierIntegrationTest(unittest.TestCase):
    def test_propverif(self):
        smtcfg = config.get_group("smt")
        with smtcfg.temp_vals():
-            smtcfg.solver = smtcfg.solver.yices
+            smtcfg.solver = smtcfg.solver.portfolio

            filename = os.path.join(THIS_DIR, "contracts/prop_verifier.sol")
            f = io.StringIO()
@@ -16,7 +16,13 @@ from manticore.core.smtlib import (
    replace,
    BitVecConstant,
 )
-from manticore.core.smtlib.solver import Z3Solver, YicesSolver, CVC4Solver, BoolectorSolver
+from manticore.core.smtlib.solver import (
+    Z3Solver,
+    YicesSolver,
+    CVC4Solver,
+    BoolectorSolver,
+    PortfolioSolver,
+)
 from manticore.core.smtlib.expression import *
 from manticore.utils.helpers import pickle_dumps
 from manticore import config
@@ -700,7 +706,7 @@ class ExpressionTest(unittest.TestCase):
        self.assertFalse(BoolConstant(value=False).__bool__())

    def test_visitors(self):
-        solver = Z3Solver.instance()
+        solver = self.solver
        cs = ConstraintSet()
        arr = cs.new_array(name="MEM")
        a = cs.new_bitvec(32, name="VAR")
@@ -853,7 +859,7 @@ class ExpressionTest(unittest.TestCase):
        self.assertEqual(translate_to_smtlib(x), "(bvadd #x00000064 VAR2)")

    def testBasicMigration(self):
-        solver = Z3Solver.instance()
+        solver = self.solver
        cs1 = ConstraintSet()
        cs2 = ConstraintSet()
        var1 = cs1.new_bitvec(32, "var")
@@ -875,7 +881,7 @@ class ExpressionTest(unittest.TestCase):
        self.assertItemsEqual(solver.get_all_values(cs1, var1), [2])  # should only be [2]

    def test_SAR(self):
-        solver = Z3Solver.instance()
+        solver = self.solver
        A = 0xBADF00D
        for B in range(32):
            cs = ConstraintSet()
@@ -891,7 +897,7 @@ class ExpressionTest(unittest.TestCase):
            self.assertEqual(solver.get_value(cs, c), Operators.SAR(32, A, B))

    def test_ConstraintsForking(self):
-        solver = Z3Solver.instance()
+        solver = self.solver
        import pickle

        cs = ConstraintSet()
@@ -993,7 +999,7 @@ class ExpressionTest(unittest.TestCase):
            self.assertItemsEqual(solver.get_all_values(cs_down_left, y), range(0x00, 0x80))

    def test_ORD(self):
-        solver = Z3Solver.instance()
+        solver = self.solver
        cs = ConstraintSet()
        a = cs.new_bitvec(8)
        cs.add(Operators.ORD(a) == Operators.ORD("Z"))
@@ -1002,7 +1008,7 @@ class ExpressionTest(unittest.TestCase):
        self.assertEqual(solver.get_value(cs, a), ord("Z"))

    def test_ORD_proper_extract(self):
-        solver = Z3Solver.instance()
+        solver = self.solver
        cs = ConstraintSet()
        a = cs.new_bitvec(32)
        cs.add(Operators.ORD(a) == Operators.ORD("\xff"))
@@ -1011,7 +1017,7 @@ class ExpressionTest(unittest.TestCase):
        self.assertEqual(solver.get_value(cs, a), ord("\xff"))

    def test_CHR(self):
-        solver = Z3Solver.instance()
+        solver = self.solver
        cs = ConstraintSet()
        a = cs.new_bitvec(8)
        cs.add(Operators.CHR(a) == Operators.CHR(0x41))
@@ -1020,7 +1026,7 @@ class ExpressionTest(unittest.TestCase):
        self.assertEqual(solver.get_value(cs, a), 0x41)

    def test_CONCAT(self):
-        solver = Z3Solver.instance()
+        solver = self.solver
        cs = ConstraintSet()
        a = cs.new_bitvec(16)
        b = cs.new_bitvec(8)
@@ -1034,7 +1040,7 @@ class ExpressionTest(unittest.TestCase):
        self.assertEqual(solver.get_value(cs, a), Operators.CONCAT(a.size, 0x41, 0x42))

    def test_ITEBV_1(self):
-        solver = Z3Solver.instance()
+        solver = self.solver
        cs = ConstraintSet()
        a = cs.new_bitvec(8)
        b = cs.new_bitvec(8)
@@ -1048,7 +1054,7 @@ class ExpressionTest(unittest.TestCase):
        self.assertEqual(solver.get_value(cs, a), 0x42)

    def test_ITEBV_2(self):
-        solver = Z3Solver.instance()
+        solver = self.solver
        cs = ConstraintSet()
        a = cs.new_bitvec(8)
        b = cs.new_bitvec(8)
@@ -1062,7 +1068,7 @@ class ExpressionTest(unittest.TestCase):
        self.assertEqual(solver.get_value(cs, a), 0x44)

    def test_ITE(self):
-        solver = Z3Solver.instance()
+        solver = self.solver
        cs = ConstraintSet()
        a = cs.new_bool()
        b = cs.new_bool()
@@ -1076,7 +1082,7 @@ class ExpressionTest(unittest.TestCase):
        self.assertEqual(solver.get_value(cs, a), False)

    def test_UREM(self):
-        solver = Z3Solver.instance()
+        solver = self.solver
        cs = ConstraintSet()
        a = cs.new_bitvec(8)
        b = cs.new_bitvec(8)
@@ -1093,7 +1099,7 @@ class ExpressionTest(unittest.TestCase):
        self.assertEqual(solver.get_value(cs, a), 0xF)

    def test_SREM(self):
-        solver = Z3Solver.instance()
+        solver = self.solver
        cs = ConstraintSet()
        a = cs.new_bitvec(8)
        b = cs.new_bitvec(8)
@@ -1110,7 +1116,7 @@ class ExpressionTest(unittest.TestCase):
        self.assertEqual(solver.get_value(cs, a), -3 & 0xFF)

    def test_UDIV(self):
-        solver = Z3Solver.instance()
+        solver = self.solver
        cs = ConstraintSet()
        a = cs.new_bitvec(8)
        b = cs.new_bitvec(8)
@@ -1127,7 +1133,7 @@ class ExpressionTest(unittest.TestCase):
        self.assertEqual(solver.get_value(cs, a), 7)

    def test_SDIV(self):
-        solver = Z3Solver.instance()
+        solver = self.solver
        cs = ConstraintSet()
        a = cs.new_bitvec(8)
        b = cs.new_bitvec(8)
@@ -1143,7 +1149,7 @@ class ExpressionTest(unittest.TestCase):
        self.assertEqual(solver.get_value(cs, a), -7 & 0xFF)

    def test_ULE(self):
-        solver = Z3Solver.instance()
+        solver = self.solver
        cs = ConstraintSet()
        a = cs.new_bitvec(8)
        b = cs.new_bitvec(8)
@@ -1165,7 +1171,7 @@ class ExpressionTest(unittest.TestCase):
        self.assertTrue(solver.must_be_true(cs, Operators.ULE(0x10, c)))

    def test_ULT(self):
-        solver = Z3Solver.instance()
+        solver = self.solver
        cs = ConstraintSet()
        a = cs.new_bitvec(8)
        b = cs.new_bitvec(8)
@@ -1187,7 +1193,7 @@ class ExpressionTest(unittest.TestCase):
        self.assertTrue(solver.must_be_true(cs, Operators.ULT(0x10, c)))

    def test_NOT(self):
-        solver = Z3Solver.instance()
+        solver = self.solver
        cs = ConstraintSet()
        a = cs.new_bitvec(8)
        b = cs.new_bitvec(8)
@@ -1295,5 +1301,10 @@ class ExpressionTestBoolector(ExpressionTest):
        self.solver = BoolectorSolver.instance()


+class ExpressionTestPortfolio(ExpressionTest):
+    def setUp(self):
+        self.solver = PortfolioSolver.instance()
+
+
 if __name__ == "__main__":
    unittest.main()