From a2c1dd3f91fda8b8fbcc7065f79f3052c98b4c0e Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Sat, 27 May 2017 12:04:43 +0200
Subject: [PATCH] Yices 2 is the new default solver for yosys-smtbmc

---
 docs/source/quickstart.rst | 18 +++++++++++++++---
 docs/source/reference.rst  |  2 +-
 sbysrc/sby_mode_bmc.py     |  2 +-
 sbysrc/sby_mode_live.py    |  2 +-
 sbysrc/sby_mode_prove.py   |  2 +-
 5 files changed, 19 insertions(+), 7 deletions(-)

diff --git a/docs/source/quickstart.rst b/docs/source/quickstart.rst
index c1731e3..9e74bf1 100644
--- 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 5195c39..dc8c08e 100644
--- 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 86f114a..203a224 100644
--- 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 dd81ffa..6b22487 100644
--- 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 e745666..f1fee35 100644
--- 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"
 
-- 
2.30.2