From ddbad8fd714a228343597cc43ca59bf3ba7d7272 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Tue, 23 Jul 2019 15:24:04 +0200 Subject: [PATCH] Documentation update: Boolector is using the MIT license now Signed-off-by: Clifford Wolf --- docs/source/quickstart.rst | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) 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. -- 2.30.2