Yices 2 is the new default solver for yosys-smtbmc

diff --git a/docs/source/quickstart.rst b/docs/source/quickstart.rst
index c1731e390530b5a173fd5b6eeca7aec7c711157c..9e74bf110f6d92c4492fd627982cfa744945f30d 100644 (file)
--- a/docs/source/quickstart.rst
+++ b/docs/source/quickstart.rst
@@ -44,6 +44,18 @@ SymbiYosys
    cd SymbiYosys
    sudo make install
 
+Yices 2
+~~~~~~~
+
+.. code-block:: text
+
+   git clone https://github.com/SRI-CSL/yices2.git yices2
+   cd yices2
+   autoconf
+   ./configure
+   make -j$(nproc)
+   sudo make install
+
 Z3
 ~~
 
@@ -89,7 +101,6 @@ Other packages
 Until I find the time to write install guides for the following packages, this
 links must suffice:
 
-  * Yices2: http://yices.csl.sri.com/
   * Boolector: http://fmv.jku.at/boolector/
   * AIGER: http://fmv.jku.at/aiger/
 
@@ -175,8 +186,9 @@ efficiently model memories. Since this example uses large memories, the
 
 (``smtbmc boolector`` uses boolector as SMT solver. Note that boolector is
 only free-to-use for noncommercial purposes. Use ``smtbmc z3`` to use the
-permissively licensed solver Z3 instead. Z3 is the default solver when no
-argument is used with ``smtbmc``.)
+permissively licensed solver Z3, or use ``smtbmc yices`` to use the
+copyleft licensed solver Yices 2 intead. Yices 2 is the default solver when
+no argument is used with ``smtbmc``.)
 
 Exercise: The engine ``abc bmc3`` does not provide abstract memory models.
 Therefore SymbiYosys has to synthesize the memories in the example to FFs

diff --git a/docs/source/reference.rst b/docs/source/reference.rst
index 5195c3982ba5a3094f7b1a0c31c1b0a596c81e5b..dc8c08efa3391cc06f83d71aa591d9b94474855c 100644 (file)
--- a/docs/source/reference.rst
+++ b/docs/source/reference.rst
@@ -40,7 +40,7 @@ options are:
 |             |            | consistency. Values: ``on``, ``off``. Default: ``off``  |
 +-------------+------------+---------------------------------------------------------+
 | ``aigsmt``  |   All      | Which SMT2 solver to use for converting AIGER witnesses |
-|             |            | to counter example traces. Default: ``z3``              |
+|             |            | to counter example traces. Default: ``yices``           |
 +-------------+------------+---------------------------------------------------------+
 | ``smtc``    | ``bmc``,   | Pass this ``.smtc`` file to the smtbmc engine. All      |
 |             | ``prove``, | other engines are disabled when this option is used.    |

diff --git a/sbysrc/sby_mode_bmc.py b/sbysrc/sby_mode_bmc.py
index 86f114a4c1d73e87cab975b7371dd4de1f08133a..203a2248ffbe0e39b5563160791f0d975b0f7c09 100644 (file)
--- a/sbysrc/sby_mode_bmc.py
+++ b/sbysrc/sby_mode_bmc.py
@@ -22,7 +22,7 @@ from sby_core import SbyTask
 def run(job):
     job.handle_int_option("depth", 20)
     job.handle_int_option("append", 0)
-    job.handle_str_option("aigsmt", "z3")
+    job.handle_str_option("aigsmt", "yices")
 
     for engine_idx in range(len(job.engines)):
         engine = job.engines[engine_idx]

diff --git a/sbysrc/sby_mode_live.py b/sbysrc/sby_mode_live.py
index dd81ffa0be6e889382b56b31f7177f1f0f071f44..6b22487f121c3258eaae86b4a3da1b05cf64ade8 100644 (file)
--- a/sbysrc/sby_mode_live.py
+++ b/sbysrc/sby_mode_live.py
@@ -20,7 +20,7 @@ import re, os, getopt
 from sby_core import SbyTask
 
 def run(job):
-    job.handle_str_option("aigsmt", "z3")
+    job.handle_str_option("aigsmt", "yices")
 
     job.status = "UNKNOWN"
 

diff --git a/sbysrc/sby_mode_prove.py b/sbysrc/sby_mode_prove.py
index e745666eecc24847ae7b6e58e56f0c8faf1db5b4..f1fee351adc0cb4ebb24c8efb5b5579889f7bba1 100644 (file)
--- a/sbysrc/sby_mode_prove.py
+++ b/sbysrc/sby_mode_prove.py
@@ -22,7 +22,7 @@ from sby_core import SbyTask
 def run(job):
     job.handle_int_option("depth", 20)
     job.handle_int_option("append", 0)
-    job.handle_str_option("aigsmt", "z3")
+    job.handle_str_option("aigsmt", "yices")
 
     job.status = "UNKNOWN"