From: Clifford Wolf Date: Tue, 23 Jul 2019 13:24:04 +0000 (+0200) Subject: Documentation update: Boolector is using the MIT license now X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ddbad8fd714a228343597cc43ca59bf3ba7d7272;p=SymbiYosys.git Documentation update: Boolector is using the MIT license now Signed-off-by: Clifford Wolf --- diff --git a/docs/source/quickstart.rst b/docs/source/quickstart.rst index 55a1a81..c711269 100644 --- a/docs/source/quickstart.rst +++ b/docs/source/quickstart.rst @@ -207,10 +207,8 @@ proof. This engine uses the array-theories provided by those solvers to efficiently model memories. Since this example uses large memories, the ``smtbmc`` engine is a good match. -(``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, or use ``smtbmc yices`` to use the -copyleft licensed solver Yices 2 intead. Yices 2 is the default solver when +(``smtbmc boolector`` selects Boolector as SMT solver, ``smtbmc z3`` selects +Z3, and ``smtbmc yices`` selects Yices 2. Yices 2 is the default solver when no argument is used with ``smtbmc``.) Exercise: The engine ``abc bmc3`` does not provide abstract memory models.