Yices 2 is the new default solver for yosys-smtbmc

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

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.    |

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]

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"
 

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"