Update documentation

diff --git a/docs/examples/quickstart/memory.sby b/docs/examples/quickstart/memory.sby
index 055d8daee98d2a037f5c74b1044642c3e63c178e..066c0231a913869a3ff507904b7f4c645920be8e 100644 (file)
--- a/docs/examples/quickstart/memory.sby
+++ b/docs/examples/quickstart/memory.sby
@@ -4,7 +4,7 @@ depth 10
 expect fail
 
 [engines]
-smtbmc -s boolector
+smtbmc boolector
 
 [script]
 read_verilog -formal memory.v

diff --git a/docs/source/quickstart.rst b/docs/source/quickstart.rst
index cec67d7ebbefca4e41e2c17066bcfdfecd2a9223..c7c723224aa58ff30ac6d3c5a4f9391a8f596d39 100644 (file)
--- a/docs/source/quickstart.rst
+++ b/docs/source/quickstart.rst
@@ -102,15 +102,15 @@ 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 -s boolector`` uses boolector as SMT solver. Note that boolector is
-only free-to-use for noncommercial purposes. Use ``smtbmc -s z3`` to use 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
-``-s`` option is used with ``smtbmc``.)
+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
 and address logic. How does the performance of this project change if
-``abc bmc3`` is used as engine instead of ``smtbmc -s boolector``? How fast
+``abc bmc3`` is used as engine instead of ``smtbmc boolector``? How fast
 can either engine verify the design when the bug has been fixed?
 
 Beyond bounded model checks