Merge pull request Z3Prover#5 from taxic/master

docs(string): typo

programmingz3/programmingz3.mdk

@@ -943,8 +943,8 @@ prove(Concat(s, Unit(IntVal(2))) != Concat(Unit(IntVal(1)), s))
 There are two solvers available in Z3 for strings. They can be exchanged
 by setting the parameter 
 
-* `s.set("smt.string.solver","seq")` with contributions by Thai Trinh, or
-* `s.set("smt.string.solver","z3str3")` by Murphy Berzish.
+* `s.set("smt.string_solver","seq")` with contributions by Thai Trinh, or
+* `s.set("smt.string_solver","z3str3")` by Murphy Berzish.
 
 ## Special Relations
 In some cases it is possible to use first-order axioms to capture all required

programmingz3/save/programmingz3.html

@@ -1164,9 +1164,9 @@ <h4 id="sec-floating-point-arithmetic" class="h3" data-line="817" data-heading-d
 by setting the parameter 
 </p>
 <ul class="ul list-star compact" data-line="886">
-<li class="li ul-li list-star-li compact-li" data-line="886"><span data-line="886"></span><code class="code code1">s.set(&quot;smt.string.solver&quot;,&quot;seq&quot;)</code><span data-line="886"></span> or
+<li class="li ul-li list-star-li compact-li" data-line="886"><span data-line="886"></span><code class="code code1">s.set(&quot;smt.string_solver&quot;,&quot;seq&quot;)</code><span data-line="886"></span> or
 </li>
-<li class="li ul-li list-star-li compact-li" data-line="887"><span data-line="887"></span><code class="code code1">s.set(&quot;smt.string.solver&quot;,&quot;z3str3&quot;)</code><span data-line="887"></span>.
+<li class="li ul-li list-star-li compact-li" data-line="887"><span data-line="887"></span><code class="code code1">s.set(&quot;smt.string_solver&quot;,&quot;z3str3&quot;)</code><span data-line="887"></span>.
 </li></ul>
 <h2 id="sec-solver-interfacing" class="h1" data-line="890" data-heading-depth="1" style="display:block"><span data-line="890"></span><span class="heading-before"><span class="heading-label">4</span>.&#8194;</span><span data-line="890"></span>Interfacing with Solvers</h2>
 <p class="p noindent" data-line="892"><span data-line="892"></span>Solvers maintain a set of formulas and supports satisfiability checking,