diff --git a/notebooks/PICS/PythonFuzzer-synopsis-2.png b/notebooks/PICS/PythonFuzzer-synopsis-2.png
new file mode 100644
index 000000000..3a4138e90
Binary files /dev/null and b/notebooks/PICS/PythonFuzzer-synopsis-2.png differ
diff --git a/notebooks/PICS/PythonFuzzer-synopsis-2.svg b/notebooks/PICS/PythonFuzzer-synopsis-2.svg
new file mode 100644
index 000000000..6f8635868
--- /dev/null
+++ b/notebooks/PICS/PythonFuzzer-synopsis-2.svg
@@ -0,0 +1,71 @@
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN"
+ "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd">
+<!-- Generated by graphviz version 9.0.0 (20230911.1827)
+ -->
+<!-- Pages: 1 -->
+<svg width="248pt" height="148pt"
+ viewBox="0.00 0.00 248.12 147.75" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink">
+<g id="graph0" class="graph" transform="scale(1 1) rotate(0) translate(4 143.75)">
+<g id="a_graph0"><a xlink:title="PythonFuzzer class hierarchy">
+<polygon fill="white" stroke="none" points="-4,4 -4,-143.75 244.12,-143.75 244.12,4 -4,4"/>
+</a>
+</g>
+<!-- PythonFuzzer -->
+<g id="node1" class="node">
+<title>PythonFuzzer</title>
+<g id="a_node1"><a xlink:href="#" xlink:title="class PythonFuzzer:&#10;Produce Python code.">
+<polygon fill="none" stroke="black" points="0,-0.5 0,-57 103,-57 103,-0.5 0,-0.5"/>
+<text text-anchor="start" x="8" y="-40.7" font-family="Patua One, Helvetica, sans-serif" font-weight="bold" font-size="14.00" fill="#b03a2e">PythonFuzzer</text>
+<polyline fill="none" stroke="black" points="0,-31 103,-31"/>
+<g id="a_node1_0"><a xlink:href="#" xlink:title="PythonFuzzer">
+<g id="a_node1_1"><a xlink:href="#" xlink:title="__init__(self, start_symbol: Optional[str] = None, *, grammar: Optional[Dict[str, List[Union[str, Tuple[str, Dict[str, Any]]]]]] = None, constraint: Optional[str] = None, **kw_params) &#45;&gt; None:&#10;Produce Python code. Parameters are:&#10;&#10;* `start_symbol`: The grammatical entity to be generated (default: `&lt;FunctionDef&gt;`)&#10;* `grammar`: The EBNF grammar to be used (default: `PYTHON__AST_GRAMMAR`); and&#10;* `constraint` an ISLa constraint (if any).&#10;&#10;Additional keyword parameters are passed to the `ISLaSolver` superclass.">
+<text text-anchor="start" x="21.5" y="-18.5" font-family="'Fira Mono', 'Source Code Pro', 'Courier', monospace" font-weight="bold" font-style="italic" font-size="10.00">__init__()</text>
+</a>
+</g>
+<g id="a_node1_2"><a xlink:href="#" xlink:title="fuzz(self) &#45;&gt; str:&#10;Produce a Python code string.">
+<text text-anchor="start" x="21.5" y="-7.25" font-family="'Fira Mono', 'Source Code Pro', 'Courier', monospace" font-weight="bold" font-size="10.00">fuzz()</text>
+</a>
+</g>
+</a>
+</g>
+</a>
+</g>
+</g>
+<!-- ISLaSolver -->
+<g id="node2" class="node">
+<title>ISLaSolver</title>
+<g id="a_node2"><a xlink:href="isla.solver.ipynb" xlink:title="class ISLaSolver:&#10;The solver class for ISLa formulas/constraints. Its top&#45;level methods are&#10;&#10;:meth:`~isla.solver.ISLaSolver.solve`&#10;Use to generate solutions for an ISLa constraint.&#10;&#10;:meth:`~isla.solver.ISLaSolver.check`&#10;Use to check if an ISLa constraint is satisfied for a given input.&#10;&#10;:meth:`~isla.solver.ISLaSolver.parse`&#10;Use to parse and validate an input.&#10;&#10;:meth:`~isla.solver.ISLaSolver.repair`&#10;Use to repair an input such that it satisfies a constraint.&#10;&#10;:meth:`~isla.solver.ISLaSolver.mutate`&#10;Use to mutate an input such that the result satisfies a constraint.">
+<polygon fill="none" stroke="black" points="10.88,-94 10.88,-139.25 92.12,-139.25 92.12,-94 10.88,-94"/>
+<text text-anchor="start" x="18.88" y="-122.95" font-family="Patua One, Helvetica, sans-serif" font-weight="bold" font-size="14.00" fill="#b03a2e">ISLaSolver</text>
+<polyline fill="none" stroke="black" points="10.88,-113.25 92.12,-113.25"/>
+<g id="a_node2_3"><a xlink:href="#" xlink:title="ISLaSolver">
+<g id="a_node2_4"><a xlink:href="isla.solver.ipynb" xlink:title="__init__(self, grammar: Union[Dict[str, List[str]], str], formula: Union[isla.language.Formula, str, NoneType] = None, structural_predicates: Set[isla.language.StructuralPredicate] = frozenset({StructuralPredicate(name=&#39;same_position&#39;, arity=2, eval_fun=&lt;function is_same_position&gt;), StructuralPredicate(name=&#39;nth&#39;, arity=3, eval_fun=&lt;function is_nth&gt;), StructuralPredicate(name=&#39;direct_child&#39;, arity=2, eval_fun=&lt;function is_direct_child&gt;), StructuralPredicate(name=&#39;before&#39;, arity=2, eval_fun=&lt;function is_before&gt;), StructuralPredicate(name=&#39;consecutive&#39;, arity=2, eval_fun=&lt;function consecutive&gt;), StructuralPredicate(name=&#39;level&#39;, arity=4, eval_fun=&lt;function level_check&gt;), StructuralPredicate(name=&#39;inside&#39;, arity=2, eval_fun=&lt;function in_tree&gt;), StructuralPredicate(name=&#39;after&#39;, arity=2, eval_fun=&lt;function is_after&gt;), StructuralPredicate(name=&#39;different_position&#39;, arity=2, eval_fun=&lt;function is_different_position&gt;)}), semantic_predicates: Set[isla.language.SemanticPredicate] = frozenset({SemanticPredicate(count, 3)}), max_number_free_instantiations: int = 10, max_number_smt_instantiations: int = 10, max_number_tree_insertion_results: int = 5, enforce_unique_trees_in_queue: bool = False, debug: bool = False, cost_computer: Optional[ForwardRef(&#39;CostComputer&#39;)] = None, timeout_seconds: Optional[int] = None, global_fuzzer: bool = False, predicates_unique_in_int_arg: Tuple[isla.language.SemanticPredicate, ...] = (SemanticPredicate(count, 3),), fuzzer_factory: Callable[[Dict[str, List[str]]], isla.fuzzer.GrammarFuzzer] = &lt;function SolverDefaults.&lt;lambda&gt;&gt;, tree_insertion_methods: Optional[int] = None, activate_unsat_support: bool = False, grammar_unwinding_threshold: int = 4, initial_tree: isla.helpers.Maybe[isla.derivation_tree.DerivationTree] = Maybe(a=None), enable_optimized_z3_queries: bool = True, start_symbol: Optional[str] = None):&#10;The constructor of :class:`~isla.solver.ISLaSolver` accepts a large number of&#10;parameters. However, all but the first one, :code:`grammar`, are *optional.*&#10;&#10;The simplest way to construct an ISLa solver is by only providing it with a&#10;grammar only; it then works like a grammar fuzzer.&#10;&#10;&gt;&gt;&gt; import random&#10;&gt;&gt;&gt; random.seed(1)&#10;&#10;&gt;&gt;&gt; import string&#10;&gt;&gt;&gt; LANG_GRAMMAR = {&#10;... &#160;&#160;&#160;&#160;&quot;&lt;start&gt;&quot;:&#10;... &#160;&#160;&#160;&#160;&#160;&#160;&#160;&#160;[&quot;&lt;stmt&gt;&quot;],&#10;... &#160;&#160;&#160;&#160;&quot;&lt;stmt&gt;&quot;:&#10;... &#160;&#160;&#160;&#160;&#160;&#160;&#160;&#160;[&quot;&lt;assgn&gt; ; &lt;stmt&gt;&quot;, &quot;&lt;assgn&gt;&quot;],&#10;... &#160;&#160;&#160;&#160;&quot;&lt;assgn&gt;&quot;:&#10;... &#160;&#160;&#160;&#160;&#160;&#160;&#160;&#160;[&quot;&lt;var&gt; := &lt;rhs&gt;&quot;],&#10;... &#160;&#160;&#160;&#160;&quot;&lt;rhs&gt;&quot;:&#10;... &#160;&#160;&#160;&#160;&#160;&#160;&#160;&#160;[&quot;&lt;var&gt;&quot;, &quot;&lt;digit&gt;&quot;],&#10;... &#160;&#160;&#160;&#160;&quot;&lt;var&gt;&quot;: list(string.ascii_lowercase),&#10;... &#160;&#160;&#160;&#160;&quot;&lt;digit&gt;&quot;: list(string.digits)&#10;... }&#10;&gt;&gt;&gt;&#10;&gt;&gt;&gt; from isla.solver import ISLaSolver&#10;&gt;&gt;&gt; solver = ISLaSolver(LANG_GRAMMAR)&#10;&gt;&gt;&gt;&#10;&gt;&gt;&gt; str(solver.solve())&#10;&#39;d := 9&#39;&#10;&gt;&gt;&gt; str(solver.solve())&#10;&#39;v := n ; s := r&#39;&#10;&#10;:param grammar: The underlying grammar; either, as a &quot;Fuzzing Book&quot; dictionary&#10;or in BNF syntax.&#10;:param formula: The formula to solve; either a string or a readily parsed&#10;formula. If no formula is given, a default `true` constraint is assumed, and&#10;the solver falls back to a grammar fuzzer. The number of produced solutions&#10;will then be bound by `max_number_free_instantiations`.&#10;:param structural_predicates: Structural predicates to use when parsing a&#10;formula.&#10;:param semantic_predicates: Semantic predicates to use when parsing a formula.&#10;:param max_number_free_instantiations: Number of times that nonterminals that&#10;are not bound by any formula should be expanded by a coverage&#45;based fuzzer.&#10;:param max_number_smt_instantiations: Number of solutions of SMT formulas that&#10;should be produced.&#10;:param max_number_tree_insertion_results: The maximum number of results when&#10;solving existential quantifiers by tree insertion.&#10;:param enforce_unique_trees_in_queue: If true, states with the same tree as an&#10;already existing tree in the queue are discarded, irrespectively of the&#10;constraint.&#10;:param debug: If true, debug information about the evolution of states is&#10;collected, notably in the field state_tree. The root of the tree is in the&#10;field state_tree_root. The field costs stores the computed cost values for&#10;all new nodes.&#10;:param cost_computer: The `CostComputer` class for computing the cost relevant&#10;to placing states in ISLa&#39;s queue.&#10;:param timeout_seconds: Number of seconds after which the solver will terminate.&#10;:param global_fuzzer: If set to True, only one coverage&#45;guided grammar fuzzer&#10;object is used to finish off unconstrained open derivation trees throughout&#10;the whole generation time. This may be beneficial for some targets; e.g., we&#10;experienced that CSV works significantly faster. However, the achieved k&#45;path&#10;coverage can be lower with that setting.&#10;:param predicates_unique_in_int_arg: This is needed in certain cases for&#10;instantiating universal integer quantifiers. The supplied predicates should&#10;have exactly one integer argument, and hold for exactly one integer value&#10;once all other parameters are fixed.&#10;:param fuzzer_factory: Constructor of the fuzzer to use for instantiating&#10;&quot;free&quot; nonterminals.&#10;:param tree_insertion_methods: Combination of methods to use for existential&#10;quantifier elimination by tree insertion. Full selection: `DIRECT_EMBEDDING &amp;&#10;SELF_EMBEDDING &amp; CONTEXT_ADDITION`.&#10;:param activate_unsat_support: Set to True if you assume that a formula might&#10;be unsatisfiable. This triggers additional tests for unsatisfiability that&#10;reduce input generation performance, but might ensure termination (with a&#10;negative solver result) for unsatisfiable problems for which the solver could&#10;otherwise diverge.&#10;:param grammar_unwinding_threshold: When querying the SMT solver, ISLa passes a&#10;regular expression for the syntax of the involved nonterminals. If this&#10;syntax is not regular, we unwind the respective part in the reference grammar&#10;up to a depth of `grammar_unwinding_threshold`. If this is too shallow, it can&#10;happen that an equation etc. cannot be solved; if it is too deep, it can&#10;negatively impact performance (and quite tremendously so).&#10;:param initial_tree: An initial input tree for the queue, if the solver shall&#10;not start from the tree `(&lt;start&gt;, None)`.&#10;:param enable_optimized_z3_queries: Enables preprocessing of Z3 queries (mainly&#10;numeric problems concerning things like length). This can improve performance&#10;significantly; however, it might happen that certain problems cannot be solved&#10;anymore. In that case, this option can/should be deactivated.&#10;:param start_symbol: This is an alternative to `initial_tree` for starting with&#10;a start symbol different form `&lt;start&gt;`. If `start_symbol` is provided, a tree&#10;consisting of a single root node with the value of `start_symbol` is chosen as&#10;initial tree.">
+<text text-anchor="start" x="21.5" y="-100.75" font-family="'Fira Mono', 'Source Code Pro', 'Courier', monospace" font-weight="bold" font-style="italic" font-size="10.00">__init__()</text>
+</a>
+</g>
+</a>
+</g>
+</a>
+</g>
+</g>
+<!-- PythonFuzzer&#45;&gt;ISLaSolver -->
+<g id="edge1" class="edge">
+<title>PythonFuzzer&#45;&gt;ISLaSolver</title>
+<path fill="none" stroke="black" d="M51.5,-57.39C51.5,-65.39 51.5,-74.2 51.5,-82.5"/>
+<polygon fill="none" stroke="black" points="48,-82.23 51.5,-92.23 55,-82.23 48,-82.23"/>
+</g>
+<!-- Legend -->
+<g id="node3" class="node">
+<title>Legend</title>
+<text text-anchor="start" x="120.88" y="-44.75" font-family="Patua One, Helvetica, sans-serif" font-weight="bold" font-size="10.00" fill="#b03a2e">Legend</text>
+<text text-anchor="start" x="120.88" y="-34.75" font-family="Patua One, Helvetica, sans-serif" font-size="10.00">• </text>
+<text text-anchor="start" x="126.88" y="-34.75" font-family="'Fira Mono', 'Source Code Pro', 'Courier', monospace" font-weight="bold" font-size="8.00">public_method()</text>
+<text text-anchor="start" x="120.88" y="-24.75" font-family="Patua One, Helvetica, sans-serif" font-size="10.00">• </text>
+<text text-anchor="start" x="126.88" y="-24.75" font-family="'Fira Mono', 'Source Code Pro', 'Courier', monospace" font-size="8.00">private_method()</text>
+<text text-anchor="start" x="120.88" y="-14.75" font-family="Patua One, Helvetica, sans-serif" font-size="10.00">• </text>
+<text text-anchor="start" x="126.88" y="-14.75" font-family="'Fira Mono', 'Source Code Pro', 'Courier', monospace" font-style="italic" font-size="8.00">overloaded_method()</text>
+<text text-anchor="start" x="120.88" y="-5.7" font-family="Helvetica,sans-Serif" font-size="9.00">Hover over names to see doc</text>
+</g>
+</g>
+</svg>