diff --git a/.travis.yml b/.travis.yml
index e4067cd..f3a0ee0 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -1,22 +1,250 @@
 language: python
-dist: trusty
+
+matrix:
+  include:
+  - os: linux
+    python: 3.6
+    env: PYSMT_SOLVER="all"       PYSMT_GMPY="TRUE"
+  - os: linux
+    python: 3.6
+    env: PYSMT_SOLVER="all"       PYSMT_GMPY="FALSE"
+  - os: linux
+    python: 3.6
+    env: PYSMT_SOLVER="None"      PYSMT_GMPY="FALSE"   PYSMT_CYTHON="TRUE"
+  - os: linux
+    python: 3.6
+    env: PYSMT_SOLVER="None"      PYSMT_GMPY="FALSE"   PYSMT_CYTHON="FALSE"
+  - os: linux
+    python: 3.6
+    env: PYSMT_SOLVER="msat"      PYSMT_GMPY="FALSE"
+  - os: linux
+    python: 3.6
+    env: PYSMT_SOLVER="z3"        PYSMT_GMPY="FALSE"
+  - os: linux
+    python: 3.6
+    env: PYSMT_SOLVER="cvc4"      PYSMT_GMPY="FALSE"
+  - os: linux
+    python: 3.6
+    env: PYSMT_SOLVER="yices"     PYSMT_GMPY="FALSE"
+  - os: linux
+    python: 3.6
+    env: PYSMT_SOLVER="bdd"       PYSMT_GMPY="FALSE"
+  - os: linux
+    python: 3.6
+    env: PYSMT_SOLVER="picosat"   PYSMT_GMPY="FALSE"
+  - os: linux
+    python: 3.6
+    env: PYSMT_SOLVER="btor"      PYSMT_GMPY="FALSE"
+  - os: linux
+    python: 3.6
+    env: PYSMT_SOLVER="msat_wrap" PYSMT_GMPY="FALSE"
+  - os: linux
+    python: 3.6
+    env: PYSMT_SOLVER="z3_wrap"   PYSMT_GMPY="FALSE"
+
+  - os: linux
+    python: 2.7
+    env: PYSMT_SOLVER="all"       PYSMT_GMPY="TRUE"
+  - os: linux
+    python: 2.7
+    env: PYSMT_SOLVER="all"       PYSMT_GMPY="FALSE"
+  - os: linux
+    python: 2.7
+    env: PYSMT_SOLVER="None"      PYSMT_GMPY="FALSE"   PYSMT_CYTHON="TRUE"
+  - os: linux
+    python: 2.7
+    env: PYSMT_SOLVER="None"      PYSMT_GMPY="FALSE"   PYSMT_CYTHON="FALSE"
+  - os: linux
+    python: 2.7
+    env: PYSMT_SOLVER="msat"      PYSMT_GMPY="FALSE"
+  - os: linux
+    python: 2.7
+    env: PYSMT_SOLVER="z3"        PYSMT_GMPY="FALSE"
+  - os: linux
+    python: 2.7
+    env: PYSMT_SOLVER="cvc4"      PYSMT_GMPY="FALSE"
+  - os: linux
+    python: 2.7
+    env: PYSMT_SOLVER="yices"     PYSMT_GMPY="FALSE"
+  - os: linux
+    python: 2.7
+    env: PYSMT_SOLVER="bdd"       PYSMT_GMPY="FALSE"
+  - os: linux
+    python: 2.7
+    env: PYSMT_SOLVER="picosat"   PYSMT_GMPY="FALSE"
+  - os: linux
+    python: 2.7
+    env: PYSMT_SOLVER="btor"      PYSMT_GMPY="FALSE"
+  - os: linux
+    python: 2.7
+    env: PYSMT_SOLVER="msat_wrap" PYSMT_GMPY="FALSE"
+  - os: linux
+    python: 2.7
+    env: PYSMT_SOLVER="z3_wrap"   PYSMT_GMPY="FALSE"
+
+  - os: linux
+    python: pypy
+    env: PYSMT_SOLVER="None"      PYSMT_GMPY="FALSE"   PYSMT_CYTHON="TRUE"
+  - os: linux
+    python: pypy
+    env: PYSMT_SOLVER="None"      PYSMT_GMPY="FALSE"   PYSMT_CYTHON="FALSE"
+
+
+  - os: osx
+    osx_image: xcode9.3
+    language: generic
+    python: 3.6
+    env: PYSMT_SOLVER="msat,z3,yices"       PYSMT_GMPY="TRUE"   TRAVIS_PYTHON_VERSION="3.6.5"
+  - os: osx
+    osx_image: xcode9.3
+    language: generic
+    python: 3.6
+    env: PYSMT_SOLVER="msat,z3,yices"       PYSMT_GMPY="FALSE"   TRAVIS_PYTHON_VERSION="3.6.5"
+  - os: osx
+    osx_image: xcode9
+    language: generic
+    python: 3.6
+    env: PYSMT_SOLVER="None"      PYSMT_GMPY="FALSE"   PYSMT_CYTHON="TRUE"   TRAVIS_PYTHON_VERSION="3.6.5"
+  - os: osx
+    osx_image: xcode9
+    language: generic
+    python: 3.6
+    env: PYSMT_SOLVER="None"      PYSMT_GMPY="FALSE"   PYSMT_CYTHON="FALSE"   TRAVIS_PYTHON_VERSION="3.6.5"
+  - os: osx
+    osx_image: xcode9
+    language: generic
+    python: 3.6
+    env: PYSMT_SOLVER="msat"      PYSMT_GMPY="FALSE"   TRAVIS_PYTHON_VERSION="3.6.5"
+  - os: osx
+    osx_image: xcode9.3
+    language: generic
+    python: 3.6
+    env: PYSMT_SOLVER="z3"        PYSMT_GMPY="FALSE"   TRAVIS_PYTHON_VERSION="3.6.5"
+  # - os: osx
+  #   osx_image: xcode9
+  #   language: generic
+  #   python: 3.6
+  #   env: PYSMT_SOLVER="cvc4"      PYSMT_GMPY="FALSE"   TRAVIS_PYTHON_VERSION="3.6.5"
+  - os: osx
+    osx_image: xcode9
+    language: generic
+    python: 3.6
+    env: PYSMT_SOLVER="yices"     PYSMT_GMPY="FALSE"   TRAVIS_PYTHON_VERSION="3.6.5"
+  # - os: osx
+  #   osx_image: xcode9
+  #   language: generic
+  #   python: 3.6
+  #   env: PYSMT_SOLVER="bdd"       PYSMT_GMPY="FALSE"   TRAVIS_PYTHON_VERSION="3.6.5"
+  # - os: osx
+  #   osx_image: xcode9
+  #   language: generic
+  #   python: 3.6
+  #   env: PYSMT_SOLVER="picosat"   PYSMT_GMPY="FALSE"   TRAVIS_PYTHON_VERSION="3.6.5"
+  # - os: osx
+  #   osx_image: xcode9
+  #   language: generic
+  #   python: 3.6
+  #   env: PYSMT_SOLVER="btor"      PYSMT_GMPY="FALSE"   TRAVIS_PYTHON_VERSION="3.6.5"
+  - os: osx
+    osx_image: xcode9
+    language: generic
+    python: 3.6
+    env: PYSMT_SOLVER="msat_wrap" PYSMT_GMPY="FALSE"   TRAVIS_PYTHON_VERSION="3.6.5"
+  - os: osx
+    osx_image: xcode9.3
+    language: generic
+    python: 3.6
+    env: PYSMT_SOLVER="z3_wrap"   PYSMT_GMPY="FALSE"   TRAVIS_PYTHON_VERSION="3.6.5"
+
+  - os: osx
+    osx_image: xcode9.3
+    language: generic
+    python: 2.7
+    env: PYSMT_SOLVER="msat,z3,yices"       PYSMT_GMPY="TRUE"   TRAVIS_PYTHON_VERSION="2.7.15"
+  - os: osx
+    osx_image: xcode9.3
+    language: generic
+    python: 2.7
+    env: PYSMT_SOLVER="msat,z3,yices"       PYSMT_GMPY="FALSE"   TRAVIS_PYTHON_VERSION="2.7.15"
+  - os: osx
+    osx_image: xcode9
+    language: generic
+    python: 2.7
+    env: PYSMT_SOLVER="None"      PYSMT_GMPY="FALSE"   PYSMT_CYTHON="TRUE"   TRAVIS_PYTHON_VERSION="2.7.15"
+  - os: osx
+    osx_image: xcode9
+    language: generic
+    python: 2.7
+    env: PYSMT_SOLVER="None"      PYSMT_GMPY="FALSE"   PYSMT_CYTHON="FALSE"   TRAVIS_PYTHON_VERSION="2.7.15"
+  - os: osx
+    osx_image: xcode9
+    language: generic
+    python: 2.7
+    env: PYSMT_SOLVER="msat"      PYSMT_GMPY="FALSE"   TRAVIS_PYTHON_VERSION="2.7.15"
+  - os: osx
+    osx_image: xcode9.3
+    language: generic
+    python: 2.7
+    env: PYSMT_SOLVER="z3"        PYSMT_GMPY="FALSE"   TRAVIS_PYTHON_VERSION="2.7.15"
+  # - os: osx
+  #   osx_image: xcode9
+  #   language: generic
+  #   python: 2.7
+  #   env: PYSMT_SOLVER="cvc4"      PYSMT_GMPY="FALSE"   TRAVIS_PYTHON_VERSION="2.7.15"
+  - os: osx
+    osx_image: xcode9
+    language: generic
+    python: 2.7
+    env: PYSMT_SOLVER="yices"     PYSMT_GMPY="FALSE"   TRAVIS_PYTHON_VERSION="2.7.15"
+  # - os: osx
+  #   osx_image: xcode9
+  #   language: generic
+  #   python: 2.7
+  #   env: PYSMT_SOLVER="bdd"       PYSMT_GMPY="FALSE"   TRAVIS_PYTHON_VERSION="2.7.15"
+  # - os: osx
+  #   osx_image: xcode9
+  #   language: generic
+  #   python: 2.7
+  #   env: PYSMT_SOLVER="picosat"   PYSMT_GMPY="FALSE"   TRAVIS_PYTHON_VERSION="2.7.15"
+  # - os: osx
+  #   osx_image: xcode9
+  #   language: generic
+  #   python: 2.7
+  #   env: PYSMT_SOLVER="btor"      PYSMT_GMPY="FALSE"   TRAVIS_PYTHON_VERSION="2.7.15"
+  - os: osx
+    osx_image: xcode9
+    language: generic
+    python: 2.7
+    env: PYSMT_SOLVER="msat_wrap" PYSMT_GMPY="FALSE"   TRAVIS_PYTHON_VERSION="2.7.15"
+  - os: osx
+    osx_image: xcode9.3
+    language: generic
+    python: 2.7
+    env: PYSMT_SOLVER="z3_wrap"   PYSMT_GMPY="FALSE"   TRAVIS_PYTHON_VERSION="2.7.15"
+
+  - os: osx
+    osx_image: xcode9
+    language: generic
+    python: pypy
+    env: PYSMT_SOLVER="None"      PYSMT_GMPY="FALSE"   PYSMT_CYTHON="TRUE"   TRAVIS_PYTHON_VERSION="pypy2.7-6.0.0"
+  - os: osx
+    osx_image: xcode9
+    language: generic
+    python: pypy
+    env: PYSMT_SOLVER="None"      PYSMT_GMPY="FALSE"   PYSMT_CYTHON="FALSE"   TRAVIS_PYTHON_VERSION="pypy2.7-6.0.0"
+
+
 git:
   depth: 10
 
+
 cache:
   apt: true
   directories:
-  - ${HOME}/.smt_solvers/btor
-  - ${HOME}/.smt_solvers/bdd
   - ${HOME}/.cache/pip
-  - ${HOME}/python_bindings/all
-  - ${HOME}/python_bindings/msat
-  - ${HOME}/python_bindings/z3
-  - ${HOME}/python_bindings/cvc4
-  - ${HOME}/python_bindings/yices
-  - ${HOME}/python_bindings/bdd
-  - ${HOME}/python_bindings/picosat
-  - ${HOME}/python_bindings/btor
+  - ${HOME}/Library/Caches/Homebrew # For MacOSX
+  - ${HOME}/python_bindings
+
 
 addons:
   apt:
@@ -37,68 +265,18 @@ addons:
     - python3-all-dev
     - libmpc-dev
 
-python:
-  - 3.6
-  - 2.7
-  - pypy
-
-
-# Multiple envs will cause multiple build across multiple python versions.
-# We test the following:
-# 1. PySMT w/o solvers
-# 2. PySMT with one solver at the time
-#
-env:
-  matrix:
-    - PYSMT_SOLVER="all"   PYSMT_GMPY="TRUE"
-    - PYSMT_SOLVER="all"   PYSMT_GMPY="FALSE"
-    - PYSMT_SOLVER="None"  PYSMT_GMPY="FALSE"   PYSMT_CYTHON="TRUE"
-    - PYSMT_SOLVER="None"  PYSMT_GMPY="FALSE"   PYSMT_CYTHON="FALSE"
-    - PYSMT_SOLVER="msat"  PYSMT_GMPY="FALSE"
-    - PYSMT_SOLVER="z3"    PYSMT_GMPY="FALSE"
-    - PYSMT_SOLVER="cvc4"  PYSMT_GMPY="FALSE"
-    - PYSMT_SOLVER="yices" PYSMT_GMPY="FALSE"
-    - PYSMT_SOLVER="bdd"   PYSMT_GMPY="FALSE"
-    - PYSMT_SOLVER="picosat" PYSMT_GMPY="FALSE"
-    - PYSMT_SOLVER="btor"  PYSMT_GMPY="FALSE"
-    - PYSMT_SOLVER="msat_wrap" PYSMT_GMPY="FALSE"
-    - PYSMT_SOLVER="z3_wrap"   PYSMT_GMPY="FALSE"
 
-matrix:
-  fast_finish: true
-
-  exclude:
-    - python: pypy
-      env: PYSMT_SOLVER="all"   PYSMT_GMPY="TRUE"
-    - python: pypy
-      env: PYSMT_SOLVER="all"   PYSMT_GMPY="FALSE"
-    - python: pypy
-      env: PYSMT_SOLVER="None"  PYSMT_GMPY="FALSE"
-    - python: pypy
-      env: PYSMT_SOLVER="msat"  PYSMT_GMPY="FALSE"
-    - python: pypy
-      env: PYSMT_SOLVER="z3"    PYSMT_GMPY="FALSE"
-    - python: pypy
-      env: PYSMT_SOLVER="cvc4"  PYSMT_GMPY="FALSE"
-    - python: pypy
-      env: PYSMT_SOLVER="yices" PYSMT_GMPY="FALSE"
-    - python: pypy
-      env: PYSMT_SOLVER="bdd"   PYSMT_GMPY="FALSE"
-    - python: pypy
-      env: PYSMT_SOLVER="picosat" PYSMT_GMPY="FALSE"
-    - python: pypy
-      env: PYSMT_SOLVER="btor"  PYSMT_GMPY="FALSE"
-    - python: pypy
-      env: PYSMT_SOLVER="msat_wrap" PYSMT_GMPY="FALSE"
-    - python: pypy
-      env: PYSMT_SOLVER="z3_wrap"   PYSMT_GMPY="FALSE"
+before_install:
+  - "./ci/travis_before_install.sh"
+
 
 install:
   - "./ci/travis_install.sh"
 
+
 script:
   - "./ci/travis_script.sh"
 
+
 after_success:
-  - coveralls
-#
+  - "./ci/travis_after_success.sh"
\ No newline at end of file
diff --git a/ci/travis_after_success.sh b/ci/travis_after_success.sh
new file mode 100755
index 0000000..aca53eb
--- /dev/null
+++ b/ci/travis_after_success.sh
@@ -0,0 +1,3 @@
+if [ "${TRAVIS_OS_NAME}" == "linux" ]; then
+    coveralls
+fi
diff --git a/ci/travis_before_install.sh b/ci/travis_before_install.sh
new file mode 100755
index 0000000..66a57ec
--- /dev/null
+++ b/ci/travis_before_install.sh
@@ -0,0 +1,52 @@
+#!/bin/bash
+set -ev
+
+#
+# Skip Install if Python 2.7 or PyPy and not a PR
+#
+if [ "${TRAVIS_PULL_REQUEST}" == "false" ] && [ "${TRAVIS_BRANCH}" != "master" ]; then
+    echo "Regular Push (not PR) on non-master branch:"
+    if [ "${TRAVIS_PYTHON_VERSION}" == "2.7" ]; then
+        echo "Skipping Python 2.7"
+        exit 0
+    fi
+    if [ "${TRAVIS_PYTHON_VERSION}" == "pypy" ]; then
+        echo "Skipping Python PyPy"
+        exit 0
+    fi
+    if [ "${PYSMT_SOLVER}" == "all" ]; then
+        echo "Skipping 'all' configuration"
+        exit 0
+    fi
+    if [ "${TRAVIS_OS_NAME}" == "osx" ]; then
+        echo "Skipping MacOSX build"
+        exit 0
+    fi
+fi
+
+function brew_install_or_upgrade {
+    brew install "$1" || (brew upgrade "$1" && brew cleanup "$1")
+}
+
+if [ "${TRAVIS_OS_NAME}" == "osx" ]; then
+    brew update
+    brew_install_or_upgrade openssl
+    brew_install_or_upgrade readline
+    brew_install_or_upgrade swig
+    brew_install_or_upgrade gperf
+
+    brew_install_or_upgrade mpfr
+    brew_install_or_upgrade libmpc
+    brew_install_or_upgrade gmp
+
+    brew_install_or_upgrade pyenv
+    brew_install_or_upgrade pyenv-virtualenv
+
+
+    pyenv install ${TRAVIS_PYTHON_VERSION}
+
+    pyenv virtualenv ${TRAVIS_PYTHON_VERSION} venv
+
+    # Check that the correct version of Python is running.
+    python --version
+fi
diff --git a/ci/travis_install.sh b/ci/travis_install.sh
index 94fb6ce..f8691db 100755
--- a/ci/travis_install.sh
+++ b/ci/travis_install.sh
@@ -18,19 +18,31 @@ if [ "${TRAVIS_PULL_REQUEST}" == "false" ] && [ "${TRAVIS_BRANCH}" != "master" ]
         echo "Skipping 'all' configuration"
         exit 0
     fi
+    if [ "${TRAVIS_OS_NAME}" == "osx" ]; then
+        echo "Skipping MacOSX build"
+        exit 0
+    fi
+fi
+
+PIP_INSTALL="python -m pip install --upgrade"
+if [ "${TRAVIS_OS_NAME}" == "osx" ]; then
+    # On OSX we need to upgrade pip as the image version is too old ...
+    curl https://bootstrap.pypa.io/get-pip.py | sudo python
+    PIP_INSTALL="python -m pip install --user --upgrade"
 fi
 
-pip install six
-pip install cython;
+$PIP_INSTALL configparser
+$PIP_INSTALL six
+$PIP_INSTALL cython;
 
-if [ "${PYSMT_SOLVER}" == "all" ] || [ "${PYSMT_SOLVER}" == "btor" ];
+if [ "${PYSMT_SOLVER}" == "all" ] || [ "${PYSMT_SOLVER}" == *"btor"* ];
 then
-    pip install python-coveralls;
+    $PIP_INSTALL python-coveralls;
 fi
 
 if [ "${PYSMT_GMPY}" == "TRUE" ];
 then
-    pip install gmpy2;
+    $PIP_INSTALL gmpy2;
 fi
 
 # Adding Python 3.6 library path to GCC search
@@ -43,21 +55,30 @@ fi
 #
 # Install Solvers
 #
-export BINDINGS_FOLDER=${HOME}/python_bindings/${PYSMT_SOLVER}
+PYSMT_SOLVER_FOLDER="${PYSMT_SOLVER}_${TRAVIS_OS_NAME}"
+PYSMT_SOLVER_FOLDER="${PYSMT_SOLVER_FOLDER//,/$'_'}"
+export BINDINGS_FOLDER=${HOME}/python_bindings/${PYSMT_SOLVER_FOLDER}
+
 mkdir -p ${BINDINGS_FOLDER}
 python install.py --confirm-agreement --bindings-path ${BINDINGS_FOLDER}
 eval `python install.py --env --bindings-path ${BINDINGS_FOLDER}`
 
-if [ "${PYSMT_SOLVER}" == "all" ] || [ "${PYSMT_SOLVER}" == "z3_wrap" ]; then
+if [ "${PYSMT_SOLVER}" == "all" ] || [ "${PYSMT_SOLVER}" == *"z3_wrap"* ]; then
     python install.py --z3 --conf --force;
     cp -v $(find ~/.smt_solvers/ -name z3 -type f) pysmt/test/smtlib/bin/z3;
     chmod +x pysmt/test/smtlib/bin/z3;
     mv pysmt/test/smtlib/bin/z3.solver.sh.template pysmt/test/smtlib/bin/z3.solver.sh ;
 fi
 
-if [ "${PYSMT_SOLVER}" == "all" ] || [ "${PYSMT_SOLVER}" == "msat_wrap" ];
+if [ "${PYSMT_SOLVER}" == "all" ] || [ "${PYSMT_SOLVER}" == *"msat_wrap"* ];
 then
     python install.py --msat --conf --force;
     cp -v $(find ~/.smt_solvers/ -name mathsat -type f) pysmt/test/smtlib/bin/mathsat;
     mv pysmt/test/smtlib/bin/mathsat.solver.sh.template pysmt/test/smtlib/bin/mathsat.solver.sh ;
 fi
+
+
+# On OSX install nosetest
+if [ "${TRAVIS_OS_NAME}" == "osx" ]; then
+    $PIP_INSTALL nose
+fi
diff --git a/ci/travis_script.sh b/ci/travis_script.sh
index a101c7c..bca9867 100755
--- a/ci/travis_script.sh
+++ b/ci/travis_script.sh
@@ -21,9 +21,16 @@ if [ "${TRAVIS_PULL_REQUEST}" == "false" ] && [ "${TRAVIS_BRANCH}" != "master" ]
         echo "Skipping 'all' configuration"
         exit 0
     fi
+    if [ "${TRAVIS_OS_NAME}" == "osx" ]; then
+        echo "Skipping MacOSX build"
+        exit 0
+    fi
 fi
 
-export BINDINGS_FOLDER=${HOME}/python_bindings/${PYSMT_SOLVER}
+PYSMT_SOLVER_FOLDER="${PYSMT_SOLVER}_${TRAVIS_OS_NAME}"
+PYSMT_SOLVER_FOLDER="${PYSMT_SOLVER_FOLDER//,/$'_'}"
+export BINDINGS_FOLDER=${HOME}/python_bindings/${PYSMT_SOLVER_FOLDER}
+
 eval `python install.py --env --bindings-path ${BINDINGS_FOLDER}`
 echo ${PYTHONPATH}
 python install.py --check
@@ -33,9 +40,9 @@ python install.py --check
 #  * Coverage is enabled only on master / all
 if [ "${TRAVIS_BRANCH}" == "master" ] && [ "${PYSMT_SOLVER}" == "all" ];
 then
-  nosetests pysmt -v # --with-coverage --cover-package=pysmt
+    python -m nose pysmt -v # --with-coverage --cover-package=pysmt
 else
-  nosetests pysmt -v
+    python -m nose pysmt -v
 fi
 
 #
diff --git a/pysmt/cmd/install.py b/pysmt/cmd/install.py
index 29a964e..eb47caa 100755
--- a/pysmt/cmd/install.py
+++ b/pysmt/cmd/install.py
@@ -230,6 +230,7 @@ def main():
         else:
             print("export PYTHONPATH=\"" + bindings_dir + ":${PYTHONPATH}\"")
 
+
     else:
         if len(solvers_to_install) == 0:
             print("Nothing to do.\nTry with '%s --help'" % sys.argv[0])
diff --git a/pysmt/cmd/installers/base.py b/pysmt/cmd/installers/base.py
index d837dbe..81f4a72 100644
--- a/pysmt/cmd/installers/base.py
+++ b/pysmt/cmd/installers/base.py
@@ -109,10 +109,11 @@ class SolverInstaller(object):
                         if e.code != 404:
                             raise
                         print("HTTP 404 while trying to get the archive using link" \
-                              " #%d (trial %d/%d)" % (i, turn+1, self.trials_404))
+                              " '%s' (trial %d/%d)" % (link, turn+1, self.trials_404))
                     except URLError as e:
                         print("Error while trying to get the archive using link" \
-                              " #%d (trial %d/%d)" % (i, turn+1, self.trials_404))
+                              " '%s' (trial %d/%d)" % (link, turn+1, self.trials_404))
+                        raise e
 
     def unpack(self):
         """Unpacks the archive"""
@@ -203,18 +204,31 @@ class SolverInstaller(object):
                                    get_output=get_output)
 
     @staticmethod
-    def run(program, directory=None, env_variables=None, get_output=False):
+    def run(program, directory=None, env_variables=None, get_output=False,
+            suppress_stderr=False):
         """Executes an arbitrary program"""
         environment = os.environ.copy()
         if env_variables is not None:
             for k,v in six.iteritems(env_variables):
                 environment[k] = v
 
+        stderr = None
+        if suppress_stderr:
+            stderr = open(os.devnull, 'w')
         if get_output:
-            output = subprocess.check_output(program.split(), env=environment, cwd=directory)
+            output = subprocess.check_output(program.split(),
+                                             env=environment,
+                                             cwd=directory,
+                                             stderr=stderr)
+            if suppress_stderr:
+                stderr.close()
             return output.decode("ascii")
         else:
-            subprocess.check_call(program.split(), env=environment, cwd=directory)
+            subprocess.check_call(program.split(), env=environment,
+                                  cwd=directory, stderr=stderr)
+            if suppress_stderr:
+                stderr.close()
+
 
     @staticmethod
     def clean_dir(path):
diff --git a/pysmt/cmd/installers/yices.py b/pysmt/cmd/installers/yices.py
index 3834229..1215632 100644
--- a/pysmt/cmd/installers/yices.py
+++ b/pysmt/cmd/installers/yices.py
@@ -24,9 +24,16 @@ class YicesInstaller(SolverInstaller):
 
     def __init__(self, install_dir, bindings_dir, solver_version,
                  mirror_link=None, yicespy_version='HEAD'):
-        
-        if self.os_name == "darwin":
-            pack = "x86_64-apple-darwin16.7.0-static-gmp"
+
+        self.needs_compilation = False
+        if self.os_name == "darwin" or self.needs_compilation:
+            sysctl = self.run("sysctl -a", get_output=True, suppress_stderr=True)
+            if 'hw.optional.avx2_0: 1' in sysctl:
+                # No need to compile, see http://yices.csl.sri.com/faq.html
+                pack = "x86_64-apple-darwin16.7.0-static-gmp"
+            else:
+                self.needs_compilation = True
+                pack = "src"
         else:
             pack = "x86_64-pc-linux-gnu-static-gmp"
 
@@ -67,8 +74,14 @@ class YicesInstaller(SolverInstaller):
         # Prepare an empty folder for installing yices
         SolverInstaller.clean_dir(self.yices_path)
 
-        SolverInstaller.run("bash ./install-yices %s" % self.yices_path,
-                            directory=self.extract_path)
+        if self.needs_compilation:
+            SolverInstaller.run("bash configure --prefix %s" % self.yices_path,
+                                directory=self.extract_path)
+            SolverInstaller.run("make", directory=self.extract_path)
+            SolverInstaller.run("make install", directory=self.extract_path)
+        else:
+            SolverInstaller.run("bash ./install-yices %s" % self.yices_path,
+                                directory=self.extract_path)
 
         self.install_yicespy()
 
diff --git a/pysmt/shortcuts.py b/pysmt/shortcuts.py
index 538c3e0..a3b3c9e 100644
--- a/pysmt/shortcuts.py
+++ b/pysmt/shortcuts.py
@@ -627,12 +627,12 @@ def BVLShr(left, right):
 
 
 def BVAShr(left, right):
-    """Returns the RIGHT arithmetic rotation of the left BV by the number
+    """Returns the RIGHT arithmetic shift of the left BV by the number
         of steps specified by the right BV.
 
     :param left: Specify the left bitvector
     :param right: Specify the right bitvector
-    :returns: The RIGHT arithmetic rotation of the left BV by the number
+    :returns: The RIGHT arithmetic shift of the left BV by the number
               of steps specified by the right BV
     :rtype: FNode
     """
diff --git a/pysmt/smtlib/parser/parser.py b/pysmt/smtlib/parser/parser.py
index bf093d6..abbca6e 100644
--- a/pysmt/smtlib/parser/parser.py
+++ b/pysmt/smtlib/parser/parser.py
@@ -876,7 +876,6 @@ class SmtLibParser(object):
                                        "command." % command,
                                        tokens.pos_info)
             res.append(current)
-
         for _ in xrange(min_size, max_size + 1):
             current = tokens.consume()
             if current == ")":
@@ -1170,16 +1169,18 @@ class SmtLibParser(object):
         var = self.parse_atom(tokens, current)
         namedparams = self.parse_named_params(tokens, current)
         rtype = self.parse_type(tokens, current)
-
+        bindings = []
         for (x,t) in namedparams:
-            v = self._get_var(x, t)
+            v = self.env.formula_manager.FreshSymbol(typename=t,
+                                                        template="__"+x+"%d")
             self.cache.bind(x, v)
-            formal.append(v)
+            formal.append(v) #remember the variable
+            bindings.append(x) #remember the name
         # Parse expression using also parameters
         ebody = self.get_expression(tokens)
-        # Discard parameters
-        for x in formal:
-            self.cache.unbind(x.symbol_name())
+        #Discard parameters
+        for x in bindings:
+            self.cache.unbind(x)
         # Finish Parsing
         self.consume_closing(tokens, current)
         self.cache.define(var, formal, ebody)
diff --git a/pysmt/smtlib/script.py b/pysmt/smtlib/script.py
index 4b00ffc..372fd3f 100644
--- a/pysmt/smtlib/script.py
+++ b/pysmt/smtlib/script.py
@@ -337,6 +337,11 @@ def evaluate_command(cmd, solver):
     elif cmd.name == smtcmd.GET_UNSAT_CORE:
         return solver.get_unsat_core()
 
+    elif cmd.name == smtcmd.DECLARE_SORT:
+        name = cmd.args[0].name
+        arity = cmd.args[0].arity
+        return solver.declare_sort(name, arity)
+
     elif cmd.name in smtcmd.ALL_COMMANDS:
         raise NotImplementedError("'%s' is a valid SMT-LIB command "\
                                   "but it is currently not supported. "\

SmtLibScript.evaluate() raises NotImplementedError for (declare-sort)
Although support for (declare-sort) seems to have been added [here](https://github.com/pysmt/pysmt/pull/411), it raises a `NotImplementedError` when evaluated through `SmtLibScript`.
To reproduce:
Run `python tmp.py`, with `tmp.py` having the following content:
```
from pysmt.smtlib.parser import SmtLibParser
from pysmt.smtlib.script import SmtLibScript
from pysmt.shortcuts import Solver
import os

def main():
    smtlib_script = '(declare-sort s 0)'
    tmp_file_name = "tmp.smt2"
    tmp_file = open(tmp_file_name, 'w')
    tmp_file.write(smtlib_script)
    tmp_file.close()
    parser = SmtLibParser()
    script = parser.get_script_fname(tmp_file_name)
    script.evaluate(Solver('z3'))
    os.remove(tmp_file_name)

if __name__ == "__main__":
    main()
```
diff --git a/pysmt/test/smtlib/test_smtlibscript.py b/pysmt/test/smtlib/test_smtlibscript.py
index 2f97538..307b803 100644
--- a/pysmt/test/smtlib/test_smtlibscript.py
+++ b/pysmt/test/smtlib/test_smtlibscript.py
@@ -55,6 +55,32 @@ class TestSmtLibScript(TestCase):
         res = script.filter_by_command_name([smtcmd.SET_LOGIC])
         self.assertEqual(len(list(res)), 1)
 
+
+    def test_declare_sort(self):
+        class SmtLibIgnore(SmtLibIgnoreMixin):
+            declare_sort_history = []
+            def declare_sort(self, name, arity):
+                self.declare_sort_history.append((name, arity))
+
+        mock = SmtLibIgnore()
+        parser = SmtLibParser()
+        smtlib_script = '\n'.join(['(declare-sort s0 0)', \
+                                   '(declare-sort s1 1)', \
+                                   '(declare-const c0 s0)', \
+                                   '(declare-const c1 (s1 Int))'])
+        outstream = cStringIO(smtlib_script)
+        script = parser.get_script(outstream)
+        script.evaluate(solver=mock)
+
+        self.assertEqual(len(mock.declare_sort_history), 2)
+        s0_name, s0_arity = mock.declare_sort_history[0]
+        s1_name, s1_arity = mock.declare_sort_history[1]
+        self.assertEqual(s0_name, "s0")
+        self.assertEqual(s0_arity, 0)
+        self.assertEqual(s1_name, "s1")
+        self.assertEqual(s1_arity, 1)
+
+
     def test_from_formula(self):
         x, y = Symbol("x"), Symbol("y")
         f = And(x, Or(y, x))
@@ -122,6 +148,19 @@ class TestSmtLibScript(TestCase):
             f = get_formula_strict(stream_in)
 
 
+    #n is defined once as an Int and once as a Real
+    def test_define_funs_same_args(self):
+        smtlib_script = "\n".join(['(define-fun f ((n Int)) Int n)', '(define-fun f ((n Real)) Real n)'])
+        stream = cStringIO(smtlib_script)
+        parser = SmtLibParser()
+        script = parser.get_script(stream)
+
+    def test_define_funs_arg_and_fun(self):
+        smtlib_script = "\n".join(['(define-fun f ((n Int)) Int n)', '(declare-fun n () Real)'])
+        stream = cStringIO(smtlib_script)
+        parser = SmtLibParser()
+        script = parser.get_script(stream)
+
     def test_evaluate_command(self):
         class SmtLibIgnore(SmtLibIgnoreMixin):
             pass
@@ -207,6 +246,12 @@ DEMO_SMTSCRIPT = [ "(declare-fun a () Bool)",
                    "(define-sort G (H) (F Int H))",
                    "(define-fun f ((a Bool)) B a)",
                    "(define-fun g ((a Bool)) B (f a))",
+                   "(define-fun h ((a Int)) Int a)",
+                   "(declare-const x Bool)",
+                   "(declare-const y Int)",
+                   "(assert (= (h y) y))",
+                   "(assert (= (f x) x))",
+                   "(check-sat)",
                    "(define-fun-rec f ((a A)) B a)",
                    "(define-fun-rec g ((a A)) B (g a))",
                    """(define-funs-rec ((h ((a A)) B) (i ((a A)) B) )
diff --git a/pysmt/test/test_regressions.py b/pysmt/test/test_regressions.py
index a33c576..da2f2b6 100644
--- a/pysmt/test/test_regressions.py
+++ b/pysmt/test/test_regressions.py
@@ -393,7 +393,7 @@ class TestRegressions(TestCase):
         s = parser.get_script(buffer_)
         for c in s:
             res = c.serialize_to_string(daggify=False)
-        self.assertEqual(res, smtlib_input)
+        self.assertEqual(res.replace('__x0', 'x'), smtlib_input)
 
     @skipIfSolverNotAvailable("z3")
     def test_z3_nary_back(self):

pip install -e .[dev]
parse_log_pytest
requirements.txt
pytest
apt-get update apt-get install -y gcc
3.9
dev-requirements.txt
pytest --no-header -rA --tb=line --color=no -p no:cacheprovider -W ignore::DeprecationWarning
exceptiongroup==1.2.2
iniconfig==2.1.0
nose==1.3.7
packaging==24.2
pluggy==1.5.0
-e git+https://github.com/pysmt/pysmt.git@b0324e68bee72c862db9620206a34f2e20c38160#egg=PySMT
pytest==8.3.5
six==1.17.0
tomli==2.2.1

name: pysmt
channels:
  - defaults
  - https://repo.anaconda.com/pkgs/main
  - https://repo.anaconda.com/pkgs/r
  - conda-forge
dependencies:
  - _libgcc_mutex=0.1=main
  - _openmp_mutex=5.1=1_gnu
  - ca-certificates=2025.2.25=h06a4308_0
  - ld_impl_linux-64=2.40=h12ee557_0
  - libffi=3.4.4=h6a678d5_1
  - libgcc-ng=11.2.0=h1234567_1
  - libgomp=11.2.0=h1234567_1
  - libstdcxx-ng=11.2.0=h1234567_1
  - ncurses=6.4=h6a678d5_0
  - openssl=3.0.16=h5eee18b_0
  - pip=25.0=py39h06a4308_0
  - python=3.9.21=he870216_1
  - readline=8.2=h5eee18b_0
  - setuptools=75.8.0=py39h06a4308_0
  - sqlite=3.45.3=h5eee18b_0
  - tk=8.6.14=h39e8969_0
  - tzdata=2025a=h04d1e81_0
  - wheel=0.45.1=py39h06a4308_0
  - xz=5.6.4=h5eee18b_1
  - zlib=1.2.13=h5eee18b_1
  - pip:
      - exceptiongroup==1.2.2
      - iniconfig==2.1.0
      - nose==1.3.7
      - packaging==24.2
      - pluggy==1.5.0
      - pytest==8.3.5
      - six==1.17.0
      - tomli==2.2.1
prefix: /opt/conda/envs/pysmt

pysmt/test/smtlib/test_smtlibscript.py::TestSmtLibScript::test_all_parsing
pysmt/test/smtlib/test_smtlibscript.py::TestSmtLibScript::test_declare_sort pysmt/test/smtlib/test_smtlibscript.py::TestSmtLibScript::test_define_funs_arg_and_fun pysmt/test/smtlib/test_smtlibscript.py::TestSmtLibScript::test_define_funs_same_args pysmt/test/smtlib/test_smtlibscript.py::TestSmtLibScript::test_get_strict_formula pysmt/test/test_regressions.py::TestRegressions::test_parse_bvconst_width pysmt/test/test_regressions.py::TestRegressions::test_parse_bvx_var pysmt/test/test_regressions.py::TestRegressions::test_parse_declare_const pysmt/test/test_regressions.py::TestRegressions::test_parse_define_fun pysmt/test/test_regressions.py::TestRegressions::test_parse_define_fun_bind pysmt/test/test_regressions.py::TestRegressions::test_smtlib_define_fun_serialization pysmt/test/test_regressions.py::TestRegressions::test_string_constant_quote_escaping_parsing
pysmt/test/smtlib/test_smtlibscript.py::TestSmtLibScript::test_basic_operations pysmt/test/smtlib/test_smtlibscript.py::TestSmtLibScript::test_evaluate_command pysmt/test/smtlib/test_smtlibscript.py::TestSmtLibScript::test_from_formula pysmt/test/smtlib/test_smtlibscript.py::TestSmtLibScript::test_smtlibignore_mixin pysmt/test/test_regressions.py::TestRegressions::test_array_initialization_printing pysmt/test/test_regressions.py::TestRegressions::test_cnf_as_set pysmt/test/test_regressions.py::TestRegressions::test_dependencies_not_includes_toreal pysmt/test/test_regressions.py::TestRegressions::test_determinism pysmt/test/test_regressions.py::TestRegressions::test_empty_string_symbol pysmt/test/test_regressions.py::TestRegressions::test_equality_typing pysmt/test/test_regressions.py::TestRegressions::test_exactly_one_unpacking pysmt/test/test_regressions.py::TestRegressions::test_exactlyone_w_generator pysmt/test/test_regressions.py::TestRegressions::test_git_version pysmt/test/test_regressions.py::TestRegressions::test_infix_notation_wrong_le pysmt/test/test_regressions.py::TestRegressions::test_is_one pysmt/test/test_regressions.py::TestRegressions::test_multiple_declaration_w_same_functiontype pysmt/test/test_regressions.py::TestRegressions::test_multiple_exit pysmt/test/test_regressions.py::TestRegressions::test_parse_exception pysmt/test/test_regressions.py::TestRegressions::test_qf_bool_smt2 pysmt/test/test_regressions.py::TestRegressions::test_simplify_times pysmt/test/test_regressions.py::TestRegressions::test_simplifying_int_plus_changes_type_of_expression pysmt/test/test_regressions.py::TestRegressions::test_smtlib_info_quoting pysmt/test/test_regressions.py::TestRegressions::test_string_constant_quote_escaping_hr_printer pysmt/test/test_regressions.py::TestRegressions::test_string_constant_quote_escaping_smtlib_printer pysmt/test/test_regressions.py::TestRegressions::test_substitute_memoization pysmt/test/test_regressions.py::TestRegressions::test_substitute_to_real
pysmt/cmd/installers/base.py pysmt/smtlib/parser/parser.py pysmt/smtlib/script.py ci/travis_script.sh .travis.yml ci/travis_before_install.sh ci/travis_after_success.sh pysmt/cmd/install.py pysmt/cmd/installers/yices.py ci/travis_install.sh pysmt/shortcuts.py
pysmt/cmd/installers/base.py pysmt/smtlib/parser/parser.py pysmt/smtlib/script.py ci/travis_script.sh .travis.yml ci/travis_before_install.sh ci/travis_after_success.sh pysmt/cmd/install.py pysmt/cmd/installers/yices.py ci/travis_install.sh pysmt/shortcuts.py