Repository: pysmt/pysmt
Pull request #635 (2020-04-13 09:12:17)

RC: 0.9.0
0.9.0: 2020-04-1X -- PySMT as module
------------------------------------

General:

* PySMT as module (PR #573): It is now possible to do
    python -m pysmt install

  and

    python -m pysmt shell

  while the tool pystm-install is still available, using the module syntax makes it easier to understand which version of python will be used, in case multiple interpreters co-exist.

* Added functions to obtain the symbols in SMTLIB script (PR #583)

* Python 2 is not supported anymore. While it might still work, we will not actively test for it anymore.

Solvers:

* Boolector: Incremental and Unsat cores support (PR #591, #567). Thanks **Makai Mann** for providing the patch.

* Picosat: Fixed a bug related to solver reset (PR #567)

* Boolector: Upgrade to 3.2.1

* MathSAT: Upgrade to 5.6.1

* Yices: Upgrade to 2.6.2

Bugfix:

* Collections.abc: fix deprecation warning (PR #574, PR #562). Thanks to **Liana Hadarean** and **Caleb Donovick**.

* PysmtSyntaxError: Fix missing message constructor (PR #576). Thanks to **Liana Hadarean** for providing a fix.

* Version: Static version in make_distrib.sh (PR #575)

* Fix simplifier StrIndexOf capitalization (PR #563). Thanks to **Makai Mann** for providing the patch.

* Sort the arguments of Times while simplifying (PR #561). Thanks to **Ahmed Irfan** for providing the patch.

* Fix bug in deque pop in smtlib/parser (PR #558). Thanks to **Sebastiano Mariani** for providing the patch.

* Function names quoted with `'` instead of `|` when seraializing to smt2 (PR #584). Thanks **Kevin Laeufer** for reporting this.

* Fix assertion tracking for boolector (PR #589). Thanks **Makai Mann** for providing the patch.

* Handle one-bit shifts in btor (PR #592) Thanks **Makai Mann** for providing the patch.

* Fix issue with bv conversion in Yices (PR #597). Thanks to `@nano-o` for reporting this.

* Fix Mathsat signature for BV_CONCAT (PR #598). Thanks **Makai Mann** for providing the patch.

* Support n-ary BVConcat (PR #621). Thanks to **Ridwan Shariffdeen** for reporting this.

* Fix a correctness issue when reading from SMT-LIB interface (Issue #616, #615, PR #619). Thanks to **Sergio Mover** for reporting this.

* Clear pending assertions in IncrementalTrackingSolver.assertions (PR #627). Thanks to **Enrico Magnago** for reporting this.

* Various documentation fixes. Thanks to **Matthew Fernandez**, **Guillem Francès**, and **Gianluca Redondi**.

* Disable multiprocessing in run_tests.sh script (PR #637). Thanks **Patrick Trentin** for reporting this.


marcogario: - [ ] Simplify CI by removing python 2.7 builds.
- [] `WARNING: unknown parameter 'model_compress'
- [] Z3 - 4.8.7
  - Zero division error on model
- [ ] Yices - 2.6.2
  - Error installing in CI
- [ ] CVC4 - 1.7
  - Detection of python version might find systems version before current python.
marcogario: @mikand can you review and approve, if this content is ok for a release? I could not update Yices and CVC4, so I would keep the current version and try to work out an upgrade after the release.

This already includes the changes from #636 , but I would like to get that in master first. Here I just wanted to show that it works with the new version of Z3.

I will merge when making the release.
mikand: This looks ok to me. Two points:
1. I am not sure you pushed the roll-back to CVC4 1.7-pre: tests are still faining
2. Have a look on #636 : Maybe we can leave the Div(x, Real(0)) instead of having an artificial UF (with the risk of name clashing)...  
marcogario: Yices - 2.6.2 , since SRI-CSL/yices2#192 was fixed

Patch:
diff --git a/azure-pipelines.yml b/azure-pipelines.yml
index b9127dd..05c2778 100644
--- a/azure-pipelines.yml
+++ b/azure-pipelines.yml
@@ -53,33 +53,33 @@ jobs:
     vmImage: 'Ubuntu-16.04'
   strategy:
     matrix:
-      Py27All:
-        PYTHON_VERSION: '2.7'
-        PYSMT_SOLVER: "all"
+      # Py27All:
+        # PYTHON_VERSION: '2.7'
+        # PYSMT_SOLVER: "all"
       Py37All:
         PYTHON_VERSION: '3.7'
         PYSMT_SOLVER: "all"
-      Py27Cython:
-        PYTHON_VERSION: '2.7'
-        PYSMT_SOLVER: "None"
-        PYSMT_CYTHON: "TRUE"
+      # Py27Cython:
+      #   PYTHON_VERSION: '2.7'
+      #   PYSMT_SOLVER: "None"
+      #   PYSMT_CYTHON: "TRUE"
       Py37Cython:
         PYTHON_VERSION: '3.7'
         PYSMT_SOLVER: "None"
         PYSMT_CYTHON: "TRUE"
-      Py27GMPy:
-        PYTHON_VERSION: '2.7'
-        PYSMT_SOLVER: "None"
-        PYSMT_GMPY: "TRUE"
+      # Py27GMPy:
+      #   PYTHON_VERSION: '2.7'
+      #   PYSMT_SOLVER: "None"
+      #   PYSMT_GMPY: "TRUE"
       Py37GMPy:
         PYTHON_VERSION: '3.7'
         PYSMT_SOLVER: "None"
         PYSMT_GMPY: "TRUE"
-      Py27CythonGMPy:
-        PYTHON_VERSION: '2.7'
-        PYSMT_SOLVER: "None"
-        PYSMT_CYTHON: "TRUE"
-        PYSMT_GMPY: "TRUE"
+      # Py27CythonGMPy:
+      #   PYTHON_VERSION: '2.7'
+      #   PYSMT_SOLVER: "None"
+      #   PYSMT_CYTHON: "TRUE"
+      #   PYSMT_GMPY: "TRUE"
       Py37CythonGMPy:
         PYTHON_VERSION: '3.7'
         PYSMT_SOLVER: "None"
@@ -97,51 +97,51 @@ jobs:
 
 
 
-- job: 'Ubuntu16Py27'
-  condition: or(eq(variables['build.sourceBranch'], 'refs/heads/master'), eq(variables['Build.Reason'], 'PullRequest'))
-  pool:
-    vmImage: 'Ubuntu-16.04'
-  strategy:
-    matrix:
-      Py27NoSolver:
-        PYTHON_VERSION: '2.7'
-        PYSMT_SOLVER: "None"
-      Py27Msat:
-        PYTHON_VERSION: '2.7'
-        PYSMT_SOLVER: "msat"
-      Py27Z3:
-        PYTHON_VERSION: '2.7'
-        PYSMT_SOLVER: "z3"
-      Py27Yices:
-        PYTHON_VERSION: '2.7'
-        PYSMT_SOLVER: "yices"
-      Py27CVC4:
-        PYTHON_VERSION: '2.7'
-        PYSMT_SOLVER: "cvc4"
-      Py27Btor:
-        PYTHON_VERSION: '2.7'
-        PYSMT_SOLVER: "btor"
-      Py27Picosat:
-        PYTHON_VERSION: '2.7'
-        PYSMT_SOLVER: "picosat"
-      Py27Bdd:
-        PYTHON_VERSION: '2.7'
-        PYSMT_SOLVER: "bdd"
-      Py27MsatWrap:
-        PYTHON_VERSION: '2.7'
-        PYSMT_SOLVER: "msat_wrap"
-      Py27Z3Wrap:
-        PYTHON_VERSION: '2.7'
-        PYSMT_SOLVER: "z3_wrap"
-  steps:
-  - task: UsePythonVersion@0
-    inputs:
-      versionSpec: '$(PYTHON_VERSION)'
-      architecture: 'x64'
-  - bash: ci/install_unix.sh
-    displayName: 'Prepare System'
-  - bash: ci/run_unix.sh
-    displayName: 'Testing'
+# - job: 'Ubuntu16Py27'
+#   condition: or(eq(variables['build.sourceBranch'], 'refs/heads/master'), eq(variables['Build.Reason'], 'PullRequest'))
+#   pool:
+#     vmImage: 'Ubuntu-16.04'
+#   strategy:
+#     matrix:
+#       Py27NoSolver:
+#         PYTHON_VERSION: '2.7'
+#         PYSMT_SOLVER: "None"
+#       Py27Msat:
+#         PYTHON_VERSION: '2.7'
+#         PYSMT_SOLVER: "msat"
+#       Py27Z3:
+#         PYTHON_VERSION: '2.7'
+#         PYSMT_SOLVER: "z3"
+#       Py27Yices:
+#         PYTHON_VERSION: '2.7'
+#         PYSMT_SOLVER: "yices"
+#       Py27CVC4:
+#         PYTHON_VERSION: '2.7'
+#         PYSMT_SOLVER: "cvc4"
+#       Py27Btor:
+#         PYTHON_VERSION: '2.7'
+#         PYSMT_SOLVER: "btor"
+#       Py27Picosat:
+#         PYTHON_VERSION: '2.7'
+#         PYSMT_SOLVER: "picosat"
+#       Py27Bdd:
+#         PYTHON_VERSION: '2.7'
+#         PYSMT_SOLVER: "bdd"
+#       Py27MsatWrap:
+#         PYTHON_VERSION: '2.7'
+#         PYSMT_SOLVER: "msat_wrap"
+#       Py27Z3Wrap:
+#         PYTHON_VERSION: '2.7'
+#         PYSMT_SOLVER: "z3_wrap"
+#   steps:
+#   - task: UsePythonVersion@0
+#     inputs:
+#       versionSpec: '$(PYTHON_VERSION)'
+#       architecture: 'x64'
+#   - bash: ci/install_unix.sh
+#     displayName: 'Prepare System'
+#   - bash: ci/run_unix.sh
+#     displayName: 'Testing'
 
 
 
@@ -241,27 +241,27 @@ jobs:
     vmImage: 'macOS-10.14'
   strategy:
     matrix:
-      Py27NoSolver:
-        PYTHON_VERSION: '2.7'
-        PYSMT_SOLVER: "None"
+      # Py27NoSolver:
+      #   PYTHON_VERSION: '2.7'
+      #   PYSMT_SOLVER: "None"
       Py37NoSolver:
         PYTHON_VERSION: '3.7'
         PYSMT_SOLVER: "None"
-      Py27Msat:
-        PYTHON_VERSION: '2.7'
-        PYSMT_SOLVER: "msat"
+      # Py27Msat:
+      #   PYTHON_VERSION: '2.7'
+      #   PYSMT_SOLVER: "msat"
       Py37Msat:
         PYTHON_VERSION: '3.7'
         PYSMT_SOLVER: "msat"
-      Py27Z3:
-        PYTHON_VERSION: '2.7'
-        PYSMT_SOLVER: "z3"
+      # Py27Z3:
+      #   PYTHON_VERSION: '2.7'
+      #   PYSMT_SOLVER: "z3"
       Py37Z3:
         PYTHON_VERSION: '3.7'
         PYSMT_SOLVER: "z3"
-      Py27Yices:
-        PYTHON_VERSION: '2.7'
-        PYSMT_SOLVER: "yices"
+      # Py27Yices:
+      #   PYTHON_VERSION: '2.7'
+      #   PYSMT_SOLVER: "yices"
       Py37Yices:
         PYTHON_VERSION: '3.7'
         PYSMT_SOLVER: "yices"
@@ -283,21 +283,21 @@ jobs:
     vmImage: 'vs2017-win2016'
   strategy:
     matrix:
-      Py27NoSolver:
-        PYTHON_VERSION: '2.7'
-        PYSMT_SOLVER: "None"
+      # Py27NoSolver:
+      #   PYTHON_VERSION: '2.7'
+      #   PYSMT_SOLVER: "None"
       Py37NoSolver:
         PYTHON_VERSION: '3.7'
         PYSMT_SOLVER: "None"
-      Py27Msat:
-        PYTHON_VERSION: '2.7'
-        PYSMT_SOLVER: "msat"
+      # Py27Msat:
+      #   PYTHON_VERSION: '2.7'
+      #   PYSMT_SOLVER: "msat"
       Py37Msat:
         PYTHON_VERSION: '3.7'
         PYSMT_SOLVER: "msat"
-      Py27Z3:
-        PYTHON_VERSION: '2.7'
-        PYSMT_SOLVER: "z3"
+      # Py27Z3:
+      #   PYTHON_VERSION: '2.7'
+      #   PYSMT_SOLVER: "z3"
       Py37Z3:
         PYTHON_VERSION: '3.7'
         PYSMT_SOLVER: "z3"
@@ -315,7 +315,7 @@ jobs:
   dependsOn:
     - 'Ubuntu16Py37'
     - 'Ubuntu16All'
-    - 'Ubuntu16Py27'
+#    - 'Ubuntu16Py27'
     - 'Ubuntu16PyPy2'
     - 'Ubuntu16PyPy3'
     - 'OSX10_13'
diff --git a/ci/install_unix.sh b/ci/install_unix.sh
index 0f045cc..825ca78 100755
--- a/ci/install_unix.sh
+++ b/ci/install_unix.sh
@@ -81,6 +81,11 @@ $PIP_INSTALL six
 $PIP_INSTALL wheel
 $PIP_INSTALL nose
 
+if [ "${PYSMT_SOLVER}" == "cvc4" ]
+then
+    $PIP_INSTALL toml
+fi
+
 # Install gmpy if needed
 if [ "${PYSMT_GMPY}" == "TRUE" ]
 then
diff --git a/docs/CHANGES.rst b/docs/CHANGES.rst
index e8cbcef..90a951a 100644
--- a/docs/CHANGES.rst
+++ b/docs/CHANGES.rst
@@ -1,6 +1,68 @@
 Change Log
 ==========
 
+0.9.0: 2020-04-26 -- PySMT as module
+------------------------------------
+
+General:
+
+* PySMT as module (PR #573): It is now possible to do
+    python -m pysmt install
+
+  and
+
+    python -m pysmt shell
+
+  while the tool pystm-install is still available, using the module syntax makes it easier to understand which version of python will be used, in case multiple interpreters co-exist.
+
+* Added functions to obtain the symbols in SMTLIB script (PR #583)
+
+* Python 2 is not supported anymore. While it might still work, we will not actively test for it anymore.
+
+Solvers:
+
+* Boolector: Incremental and Unsat cores support (PR #591, #567). Thanks **Makai Mann** for providing the patch.
+
+* Picosat: Fixed a bug related to solver reset (PR #567)
+
+* Boolector: Upgrade to 3.2.1
+
+* MathSAT: Upgrade to 5.6.1
+
+Bugfix:
+
+* Collections.abc: fix deprecation warning (PR #574, PR #562). Thanks to **Liana Hadarean** and **Caleb Donovick**.
+
+* PysmtSyntaxError: Fix missing message constructor (PR #576). Thanks to **Liana Hadarean** for providing a fix.
+
+* Version: Static version in make_distrib.sh (PR #575)
+
+* Fix simplifier StrIndexOf capitalization (PR #563). Thanks to **Makai Mann** for providing the patch.
+
+* Sort the arguments of Times while simplifying (PR #561). Thanks to **Ahmed Irfan** for providing the patch.
+
+* Fix bug in deque pop in smtlib/parser (PR #558). Thanks to **Sebastiano Mariani** for providing the patch.
+
+* Function names quoted with `'` instead of `|` when seraializing to smt2 (PR #584). Thanks **Kevin Laeufer** for reporting this.
+
+* Fix assertion tracking for boolector (PR #589). Thanks **Makai Mann** for providing the patch.
+
+* Handle one-bit shifts in btor (PR #592) Thanks **Makai Mann** for providing the patch.
+
+* Fix issue with bv conversion in Yices (PR #597). Thanks to `@nano-o` for reporting this.
+
+* Fix Mathsat signature for BV_CONCAT (PR #598). Thanks **Makai Mann** for providing the patch.
+
+* Support n-ary BVConcat (PR #621). Thanks to **Ridwan Shariffdeen** for reporting this.
+
+* Fix a correctness issue when reading from SMT-LIB interface (Issue #616, #615, PR #619). Thanks to **Sergio Mover** for reporting this.
+
+* Clear pending assertions in IncrementalTrackingSolver.assertions (PR #627). Thanks to **Enrico Magnago** for reporting this.
+
+* Various documentation fixes. Thanks to **Matthew Fernandez**, **Guillem Francès**, and **Gianluca Redondi**.
+
+* Disable multiprocessing in run_tests.sh script (PR #637). Thanks **Patrick Trentin** for reporting this.
+
 0.8.0: 2019-01-27 -- Better Install and Great Community
 -------------------------------------------------------
 
@@ -20,7 +82,7 @@ General:
   installs the solvers within the site-package directory (by
   default). This makes it possible to work with virtual environments,
   and does not require anymore to export the Python path, greatly
-  simplifying the installation process. Thanks to **Radomi
+  simplifying the installation process. Thanks to **Radomir
   Stevanovic** for contributing the patch.
 
 * Simplify shared lib usage (PR #494): Modify z3 and msat installers
diff --git a/docs/development.rst b/docs/development.rst
index 7eef940..6a0f365 100644
--- a/docs/development.rst
+++ b/docs/development.rst
@@ -199,8 +199,8 @@ Preparing a Release (Check-List)
 ================================
 
 In order to make a release, the master branch must pass all tests on
-the CI (Travis and Appveyor). The release process is broken into the
-following steps:
+the CI (Travis and Appveyor). The release process is broken down into
+the following steps:
 
  * Release branch creation
  * Changelog update
@@ -215,7 +215,7 @@ following steps:
 Release Branch Creation
 -----------------------
 
-As all other activities, also the creation of a release requires
+As all other activities, the creation of a release requires
 working on a separate branch. This makes it possible to interrupt,
 share, and resume the release creation, if bugs are discovered during
 this process. The branch must be called ``rc/a.b.c``, where a.b.c is
@@ -342,13 +342,13 @@ Avoid Infix Notation and shortcuts
 ----------------------------------
 
 Infix notation and shortcuts assume that you are operating on the
-global environment. The expression ``a & b`` needs:
+global environment. The expression ``a & b`` needs to:
 
-* Resolve the implicit operator (i.e., translate ``&`` into ``And``)
-* Access the global environment
-* Access corresponding formula manager
-* Check if the right-hand-side is already an FNode
-* Call ``FormulaManager.And`` on the two elements.
+1. Resolve the implicit operator (i.e., translate ``&`` into ``And``)
+2. Access the global environment
+3. Access the corresponding formula manager
+4. Check if the right-hand-side is already an FNode
+5. Call ``FormulaManager.And`` on the two elements.
 
 Using a shortcut is similar in complexity, although you skip step 1
 and 4. Therefore, within loop intensive code, make sure that you
@@ -375,7 +375,7 @@ calls to the type-checker are memoized, the cost of doing so can add
 up. If you are 100% sure that your expressions will be well-typed,
 then you can use the following code to create a context that disables
 temporarily the type-checker. WARNING: If you create an expression
-that is not well-typed while the type-checker is disabled,, there is no
+that is not well-typed while the type-checker is disabled, there is no
 way to detect it later on. ::
 
   class SuspendTypeChecking(object):
@@ -415,7 +415,7 @@ is spent in simple loops. A typical example is parsing, modifying, and
 dumping an SMT-LIB: this flow can significantly improve by using pypy.
 
 Some work has been done in order to use `CFFI
-<http://cffi.readthedocs.io/en/latest/>`_ in order to interface more
+<http://cffi.readthedocs.io/en/latest/>`_ to interface more
 solvers with pypy (see `mathsat-cffi
 <https://github.com/pysmt/mathsat-cffi>`_ repo). If you are interested
 in this activity, please `get in touch <https://groups.google.com/forum/#!forum/pysmt>`_.
diff --git a/pysmt/__init__.py b/pysmt/__init__.py
index b6c3d5b..50749f3 100644
--- a/pysmt/__init__.py
+++ b/pysmt/__init__.py
@@ -16,7 +16,7 @@
 #   limitations under the License.
 #
 
-VERSION = (0, 8, 1, "dev", 1)
+VERSION = (0, 9, 0)
 
 # Try to provide human-readable version of latest commit for dev versions
 # E.g. v0.5.1-4-g49a49f2-wip
diff --git a/pysmt/cmd/install.py b/pysmt/cmd/install.py
index 24b9063..af39ee4 100755
--- a/pysmt/cmd/install.py
+++ b/pysmt/cmd/install.py
@@ -34,14 +34,13 @@ from pysmt import __version__ as pysmt_version
 Installer = namedtuple("Installer",
                        ["InstallerClass", "version", "extra_params"])
 INSTALLERS = [
-    Installer(MSatInstaller,    "5.5.1", {}),
+    Installer(MSatInstaller,    "5.6.1", {}),
     Installer(CVC4Installer,    "1.7-prerelease",
               {"git_version" : "391ab9df6c3fd9a3771864900c1718534c1e4666"}),
-    Installer(Z3Installer,      "4.8.4",
-              {"osx": "10.14.1", "commit": "d6df51951f4c"}),
-    Installer(YicesInstaller,   "2.6.0",
+    Installer(Z3Installer,      "4.8.7", {"osx": "10.14.6"}),
+    Installer(YicesInstaller,   "2.6.2",
               {"yicespy_version": "f0768ffeec15ea310f830d10878971c9998454ac"}),
-    Installer(BtorInstaller,    "3.1.0", {}),
+    Installer(BtorInstaller,    "3.2.1", {}),
     Installer(PicoSATInstaller, "965",
               {"pypicosat_minor_version" : "1708010052"}),
     Installer(CuddInstaller,    "2.0.3",
diff --git a/pysmt/cmd/installers/cvc4.py b/pysmt/cmd/installers/cvc4.py
index 37fb92d..fd50a3e 100644
--- a/pysmt/cmd/installers/cvc4.py
+++ b/pysmt/cmd/installers/cvc4.py
@@ -45,8 +45,9 @@ class CVC4Installer(SolverInstaller):
 
     def compile(self):
         # Build ANTLR
-        SolverInstaller.run("bash get-antlr-3.4",
-                            directory=os.path.join(self.extract_path, "contrib"))
+
+        SolverInstaller.run("bash %s" % os.path.join("contrib", "get-antlr-3.4"),
+                            directory=self.extract_path)
 
         # Build ABC
         # SolverInstaller.run("bash get-abc",
diff --git a/pysmt/cmd/installers/z3.py b/pysmt/cmd/installers/z3.py
index 91f94d2..a72144a 100644
--- a/pysmt/cmd/installers/z3.py
+++ b/pysmt/cmd/installers/z3.py
@@ -31,7 +31,7 @@ class Z3Installer(SolverInstaller):
 
         system = self.os_name
         if system == "linux":
-            system = "ubuntu-14.04"
+            system = "ubuntu-16.04"
         elif system == "darwin":
             system = "osx-%s" % osx
         elif system == "windows":
@@ -39,7 +39,10 @@ class Z3Installer(SolverInstaller):
 
         if git_version is None:
             # Stable versions template
-            archive_name = "z3-%s.%s-%s-%s.zip" % (solver_version, commit, arch, system)
+            if commit:
+                archive_name = "z3-%s.%s-%s-%s.zip" % (solver_version, commit, arch, system)
+            else:
+                archive_name = "z3-%s-%s-%s.zip"  % (solver_version, arch, system)
             native_link = "https://github.com/Z3Prover/z3/releases/download/z3-" + solver_version + "/{archive_name}"
             # print(native_link)
         else:
diff --git a/pysmt/environment.py b/pysmt/environment.py
index c918470..6428e44 100644
--- a/pysmt/environment.py
+++ b/pysmt/environment.py
@@ -74,6 +74,7 @@ class Environment(object):
         self._factory = None
         # Configurations
         self.enable_infix_notation = False
+        self.enable_div_by_0 = True
 
         # Dynamic Walker Configuration Map
         # See: add_dynamic_walker_function
diff --git a/pysmt/fnode.py b/pysmt/fnode.py
index ce009f3..340e536 100644
--- a/pysmt/fnode.py
+++ b/pysmt/fnode.py
@@ -22,7 +22,7 @@ import pysmt.smtlib
 from pysmt.operators import (FORALL, EXISTS, AND, OR, NOT, IMPLIES, IFF,
                              SYMBOL, FUNCTION,
                              REAL_CONSTANT, BOOL_CONSTANT, INT_CONSTANT,
-                             PLUS, MINUS, TIMES,
+                             PLUS, MINUS, TIMES, DIV,
                              LE, LT, EQUALS,
                              ITE,
                              TOREAL,
@@ -299,6 +299,10 @@ class FNode(object):
         """Test whether the node is the Times operator."""
         return self.node_type() == TIMES
 
+    def is_div(self):
+        """Test whether the node is the Division operator."""
+        return self.node_type() == DIV
+
     def is_implies(self):
         """Test whether the node is the Implies operator."""
         return self.node_type() == IMPLIES
diff --git a/pysmt/formula.py b/pysmt/formula.py
index 735d0c9..5a66aa6 100644
--- a/pysmt/formula.py
+++ b/pysmt/formula.py
@@ -33,6 +33,7 @@ if sys.version_info >= (3, 3):
 else:
     from collections import Iterable
 
+import warnings
 from six.moves import xrange
 
 import pysmt.typing as types
@@ -261,7 +262,11 @@ class FormulaManager(object):
 
     def Div(self, left, right):
         """ Creates an expression of the form: left / right """
-        if right.is_constant(types.REAL):
+        if right.is_constant(types.REAL, 0) and self.env.enable_div_by_0:
+            # Allow division by 0 byt warn the user
+            # This can only happen in non-linear logics
+            warnings.warn("Warning: Division by 0")
+        elif right.is_constant(types.REAL):
             # If right is a constant we rewrite as left * 1/right
             inverse = Fraction(1) / right.constant_value()
             return self.Times(left, self.Real(inverse))
diff --git a/pysmt/oracles.py b/pysmt/oracles.py
index d3a9b40..36b8b12 100644
--- a/pysmt/oracles.py
+++ b/pysmt/oracles.py
@@ -315,6 +315,13 @@ class TheoryOracle(walkers.DagWalker):
         if len(left.get_free_variables()) != 0 and \
            len(right.get_free_variables()) != 0:
             theory_out = theory_out.set_linear(False)
+        elif formula.arg(1).is_zero():
+            # DivBy0 is non-linear
+            theory_out = theory_out.set_linear(False)
+        else:
+            theory_out = theory_out.combine(args[1])
+        return theory_out
+
         # This is  not in DL anymore
         theory_out = theory_out.set_difference_logic(False)
         return theory_out
diff --git a/pysmt/simplifier.py b/pysmt/simplifier.py
index 7c8eef0..1dcc787 100644
--- a/pysmt/simplifier.py
+++ b/pysmt/simplifier.py
@@ -975,7 +975,7 @@ class Simplifier(pysmt.walkers.DagWalker):
         sl = args[0]
         sr = args[1]
 
-        if sl.is_constant() and sr.is_constant():
+        if sl.is_constant() and sr.is_constant() and not sr.is_zero():
             l = sl.constant_value()
             r = sr.constant_value()
             if sl.is_real_constant():
diff --git a/pysmt/solvers/solver.py b/pysmt/solvers/solver.py
index 6c7d35c..1c25a50 100644
--- a/pysmt/solvers/solver.py
+++ b/pysmt/solvers/solver.py
@@ -496,6 +496,45 @@ class Model(object):
             res[f] = v
         return res
 
+    def satisfies(self, formula, solver=None):
+        """Checks whether the model satisfies the formula.
+
+        The optional solver argument is used to complete partial
+        models.
+        """
+
+        subs = self.get_values(formula.get_free_variables())
+        simp = formula.substitute(subs).simplify()
+        if simp.is_true():
+            return True
+        if simp.is_false():
+            return False
+
+        free_vars = simp.get_free_variables()
+        if  len(free_vars) > 0:
+            # Partial model
+            return False
+        
+        if self.environment.enable_div_by_0 and solver is not None:
+            # Models might not be simplified to a constant value
+            # if there is a division by zero. We find the
+            # division(s) and ask the solver for a replacement
+            # expression.
+            stack = [simp]
+            div_0 = []
+            while stack:
+                x = stack.pop()
+                if x.is_constant():
+                    pass
+                elif x.is_div() and x.arg(1).is_zero():
+                    div_0.append(x)
+                stack += x.args()
+
+            subs = self.get_values(div_0)
+            simp = simp.substitute(subs).simplify()
+            return simp.is_true()
+        return False
+
     @property
     def converter(self):
         """Get the Converter associated with the Solver."""
diff --git a/pysmt/solvers/z3.py b/pysmt/solvers/z3.py
index 1f48bc3..4e86e60 100644
--- a/pysmt/solvers/z3.py
+++ b/pysmt/solvers/z3.py
@@ -26,7 +26,7 @@ except ImportError:
 
 # Keep array models expressed as values instead of Lambdas
 # (see https://github.com/Z3Prover/z3/issues/1769)
-z3.set_param('model_compress', False)
+z3.set_param('model.compact', False)
 
 from six.moves import xrange
 


Test patch:
diff --git a/pysmt/test/test_nlira.py b/pysmt/test/test_nlira.py
index bedb1a7..615845f 100644
--- a/pysmt/test/test_nlira.py
+++ b/pysmt/test/test_nlira.py
@@ -17,11 +17,11 @@
 #
 
 from pysmt.test import TestCase, main
-from pysmt.test import skipIfSolverNotAvailable
+from pysmt.test import skipIfSolverNotAvailable, skipIfNoSolverForLogic
 
 from pysmt.oracles import get_logic
 from pysmt.shortcuts import FreshSymbol, Times, Equals, Div, Real, Int, Pow
-from pysmt.shortcuts import Solver, is_sat
+from pysmt.shortcuts import Solver, Symbol, And, Not, is_sat
 from pysmt.typing import REAL, INT
 from pysmt.exceptions import (ConvertExpressionError,
                               NonLinearError,
@@ -117,5 +117,16 @@ class TestNonLinear(TestCase):
         except SolverReturnedUnknownResultError:
             pass
 
+    @skipIfNoSolverForLogic(QF_NRA)
+    def test_div_by_0(self):
+        varA = Symbol('A', REAL)
+        varB = Symbol('B', REAL)
+
+        f = And(Equals(varA, varB),
+                Not(Equals(Div(varA, Real(0)), Div(varB, Real(0)))))
+
+        self.assertUnsat(f)
+
+
 if __name__ == "__main__":
     main()
diff --git a/pysmt/test/test_oracles.py b/pysmt/test/test_oracles.py
index ec17ed0..7402953 100644
--- a/pysmt/test/test_oracles.py
+++ b/pysmt/test/test_oracles.py
@@ -20,7 +20,7 @@ from pysmt.shortcuts import Symbol, Implies, And, Not
 from pysmt.test.examples import get_example_formulae
 from pysmt.test import TestCase, main
 from pysmt.oracles import get_logic
-from pysmt.typing import BOOL, Type, INT, FunctionType
+from pysmt.typing import BOOL, Type, INT, REAL, FunctionType
 
 
 class TestOracles(TestCase):
@@ -137,6 +137,15 @@ class TestOracles(TestCase):
         theory = self.env.theoryo.get_theory(f_1)
         self.assertEqual(theory, QF_UFIDL.theory)
 
+    def test_types_oracle_divby0(self):
+        from pysmt.logics import QF_NRA
+
+        mgr = self.env.formula_manager
+        r = mgr.Symbol("r", REAL)
+        f = mgr.Equals(mgr.Real(4),
+                       mgr.Div(r, mgr.Real(0)))
+        theory = self.env.theoryo.get_theory(f)
+        self.assertFalse(theory.linear)
 
 
 if __name__ == '__main__':
diff --git a/pysmt/test/test_solving.py b/pysmt/test/test_solving.py
index 6fd971a..c0483c9 100644
--- a/pysmt/test/test_solving.py
+++ b/pysmt/test/test_solving.py
@@ -240,6 +240,7 @@ class TestBasic(TestCase):
             self.assertEqual(satisfiability, s, f)
 
     def do_model(self, solver_name):
+
         for (f, _, satisfiability, logic) in get_example_formulae():
             if satisfiability and not logic.theory.uninterpreted and logic.quantifier_free:
                 try:
@@ -249,24 +250,9 @@ class TestBasic(TestCase):
                         check = s.solve()
                         self.assertTrue(check)
 
-                        # Ask single values to the solver
-                        subs = {}
-                        for d in f.get_free_variables():
-                            m = s.get_value(d)
-                            subs[d] = m
-
-                        simp = f.substitute(subs).simplify()
-                        self.assertEqual(simp, TRUE(), "%s -- %s :> %s" % (f, subs, simp))
-
-                        # Ask the eager model
-                        subs = {}
                         model = s.get_model()
-                        for d in f.get_free_variables():
-                            m = model.get_value(d)
-                            subs[d] = m
+                        self.assertTrue(model.satisfies(f, s))
 
-                        simp = f.substitute(subs).simplify()
-                        self.assertEqual(simp, TRUE())
                 except NoSolverAvailableError:
                     pass
 
@@ -629,5 +615,6 @@ class TestBasic(TestCase):
                 res = solver.solve()
                 self.assertTrue(res == sat)
 
+
 if __name__ == '__main__':
     main()