nonterminal_positions = [
                     i for i, x in enumerate(matching_expansion) if x == next_nonterminal
                 ]
                 for nonterminal_position in nonterminal_positions:
                     next_children = [
-                        DerivationTree(nonterm, [])
-                        if idx != nonterminal_position
-                        else DerivationTree(nonterm, None)
+                        (
+                            DerivationTree(nonterm, [])
+                            if idx != nonterminal_position
+                            else DerivationTree(nonterm, None)
+                        )
                         for idx, nonterm in enumerate(matching_expansion)
                     ]
 
                     new_candidate = candidate.replace_path(
                         leaf_path, DerivationTree(leaf_node, next_children)

 
     assert isinstance(start_node, NonterminalNode)
 
     prefixes: List[Tuple[Set[Node], List[Node]]] = [
         (
-            set()
-            if start_node == dest_node and graph.reachable(start_node, start_node)
-            else {start_node},
+            (
+                set()
+                if start_node == dest_node and graph.reachable(start_node, start_node)
+                else {start_node}
+            ),
             [start_node],
         )
     ]
     result: OrderedSet[Tuple[str, ...]] = OrderedSet([])
 

         return 1 + max(child.depth() for child in self.children)
 
     def new_ids(self) -> "DerivationTree":
         return DerivationTree(
             self.value,
-            None
-            if self.children is None
-            else [child.new_ids() for child in self.children],
+            (
+                None
+                if self.children is None
+                else [child.new_ids() for child in self.children]
+            ),
         )
 
     def __len__(self):
         if self.__len is None:
             self.__len = len(self.paths())

         }
 
         if not nonterminal_expansions:
             return []
 
-        possible_expansions: List[
-            Dict[Path, List[DerivationTree]]
-        ] = dict_of_lists_to_list_of_dicts(nonterminal_expansions)
+        possible_expansions: List[Dict[Path, List[DerivationTree]]] = (
+            dict_of_lists_to_list_of_dicts(nonterminal_expansions)
+        )
 
         assert (
             len(possible_expansions) > 1
             or len(possible_expansions) == 1
             and possible_expansions[0]

     assert isinstance(reference_tree, DerivationTree)
     subtrees_trie = reference_tree.trie() if subtrees_trie is None else subtrees_trie
     graph = gg.GrammarGraph.from_grammar(grammar) if graph is None else graph
 
     formula = instantiate_top_level_constant(
-        parse_isla(formula, grammar, structural_predicates, semantic_predicates)
-        if isinstance(formula, str)
-        else formula,
+        (
+            parse_isla(formula, grammar, structural_predicates, semantic_predicates)
+            if isinstance(formula, str)
+            else formula
+        ),
         reference_tree,
     )
 
     # NOTE: Deactivated, might be too strict for evaluation (though maybe
     #       necessary for solving). See comment in well_formed.

 ) -> Maybe[ThreeValuedTruth]:
     if not isinstance(formula, StructuralPredicateFormula):
         return Nothing
 
     arg_insts = [
-        arg
-        if isinstance(arg, str)
-        else next(
-            path for path, subtree in reference_tree.paths() if subtree.id == arg.id
-        )
-        if isinstance(arg, DerivationTree)
-        else assignments[arg][0]
+        (
+            arg
+            if isinstance(arg, str)
+            else (
+                next(
+                    path
+                    for path, subtree in reference_tree.paths()
+                    if subtree.id == arg.id
+                )
+                if isinstance(arg, DerivationTree)
+                else assignments[arg][0]
+            )
+        )
         for arg in formula.args
     ]
     return Some(
         ThreeValuedTruth.from_bool(
             formula.predicate.evaluate(reference_tree, *arg_insts)

 ) -> Maybe[ThreeValuedTruth]:
     if not isinstance(formula, SemanticPredicateFormula):
         return Nothing
 
     arg_insts = [
-        arg
-        if isinstance(arg, DerivationTree) or arg not in assignments
-        else assignments[arg][1]
+        (
+            arg
+            if isinstance(arg, DerivationTree) or arg not in assignments
+            else assignments[arg][1]
+        )
         for arg in formula.args
     ]
     eval_res = formula.predicate.evaluate(graph, *arg_insts)
 
     if eval_res.true():

     common_nonterminal_prefixes: List[Path] = [tuple()]
     for idx in range(min(len(path_1), len(path_2))):
         if path_1[idx] != path_2[idx]:
             break
 
-        prefix = path_1[:idx + 1]  # should consider a prefix up to and including the current index
+        prefix = path_1[
+            : idx + 1
+        ]  # should consider a prefix up to and including the current index
         if context_tree.get_subtree(prefix).value == nonterminal:
             common_nonterminal_prefixes.append(prefix)
 
     for prefix in common_nonterminal_prefixes:
         nonterminal_occs_1, nonterminal_occs_2 = [

             print("ERROR: timeout value must be an integer.", file=sys.stderr)
             print_help()
             exit(1)
 
         self.jobs_and_generators = {
-            f"{jobname_prefix} {job}": generator
-            if isinstance(generator, dict)
-            else generator(self.timeout)
+            f"{jobname_prefix} {job}": (
+                generator if isinstance(generator, dict) else generator(self.timeout)
+            )
             for job, generator in zip(jobnames, generators)
             if job in chosen_jobs
         }
 
         try:

                         store_inputs(jobname, self.timeout, inputs, self.db_file)
                 continue
 
             with pmp.Pool(processes=pmp.cpu_count()) as pool:
                 pool.starmap(
-                    lambda jobname, generator: generate_inputs(
-                        generator, self.timeout, jobname
-                    )
-                    if self.dry_run
-                    else store_inputs(
-                        jobname,
-                        self.timeout,
-                        generate_inputs(generator, self.timeout, jobname),
-                        self.db_file,
+                    lambda jobname, generator: (
+                        generate_inputs(generator, self.timeout, jobname)
+                        if self.dry_run
+                        else store_inputs(
+                            jobname,
+                            self.timeout,
+                            generate_inputs(generator, self.timeout, jobname),
+                            self.db_file,
+                        )
                     ),
                     list(self.jobs_and_generators.items()),
                 )
 
     def evaluate_validity(self) -> None:

         ] = [
             (
                 [jobname],
                 [self.validator],
                 [self.db_file],
-                sids[jobname]
-                if self.num_sessions < 0
-                else sids[jobname][len(sids[jobname]) - self.num_sessions :],
+                (
+                    sids[jobname]
+                    if self.num_sessions < 0
+                    else sids[jobname][len(sids[jobname]) - self.num_sessions :]
+                ),
             )
             for jobname in self.jobs_and_generators
         ]
 
         args: List[

             (
                 [jobname],
                 [self.graph],
                 [k],
                 [self.db_file],
-                sids[jobname]
-                if self.num_sessions < 0
-                else sids[jobname][len(sids[jobname]) - self.num_sessions :],
+                (
+                    sids[jobname]
+                    if self.num_sessions < 0
+                    else sids[jobname][len(sids[jobname]) - self.num_sessions :]
+                ),
             )
             for jobname in self.jobs_and_generators
             for k in self.kvalues
         ]
 

 def strtime() -> str:
     return datetime.now().strftime("%H:%M:%S")
 
 
 def generate_inputs(
-    generator: Generator[isla.derivation_tree.DerivationTree, None, None]
-    | ISLaSolver
-    | Grammar,
+    generator: (
+        Generator[isla.derivation_tree.DerivationTree, None, None]
+        | ISLaSolver
+        | Grammar
+    ),
     timeout_seconds: int = 60,
     jobname: Optional[str] = None,
 ) -> Dict[float, isla.derivation_tree.DerivationTree]:
     start_time = time.time()
     result: Dict[float, isla.derivation_tree.DerivationTree] = {}

 
     return result
 
 
 def make_input_generator(
-    generator: Generator[isla.derivation_tree.DerivationTree, None, None]
-    | ISLaSolver
-    | Grammar
+    generator: (
+        Generator[isla.derivation_tree.DerivationTree, None, None]
+        | ISLaSolver
+        | Grammar
+    )
 ) -> Generator[isla.derivation_tree.DerivationTree, None, None]:
     if isinstance(generator, ISLaSolver):
 
         def gen():
             while True:

 ) -> Union[bool, str]:
     contents = "int main() {\n"
     contents += "\n" + str(tree).replace("\n", "    \t")
     contents += "\n" + "}"
 
-    with tempfile.NamedTemporaryFile(suffix=".c") as tmp, tempfile.NamedTemporaryFile(
-        suffix=".o"
-    ) as outfile:
+    with (
+        tempfile.NamedTemporaryFile(suffix=".c") as tmp,
+        tempfile.NamedTemporaryFile(suffix=".o") as outfile,
+    ):
         tmp.write(contents.encode())
         tmp.flush()
         cmd = ["clang", tmp.name, "-o", outfile.name]
         process = subprocess.Popen(cmd, stderr=PIPE)
         (stdout, stderr) = process.communicate()

         return merge_intervals(
             *map(
                 lambda option_or_union: numeric_intervals_from_regex(
                     z3.Concat(option_or_union, *children[1:])
                 ),
-                first_child.children()
-                if first_child.decl().kind() == z3.Z3_OP_RE_UNION
-                else [z3.Re("+"), z3.Re("-")],
+                (
+                    first_child.children()
+                    if first_child.decl().kind() == z3.Z3_OP_RE_UNION
+                    else [z3.Re("+"), z3.Re("-")]
+                ),
             )
         )
     elif first_child in [z3.Re("+"), z3.Option(z3.Re("+"))]:
         return numeric_intervals_from_regex(
             children[1] if len(children) == 2 else z3.Concat(*children[1:])

 
 
 @dataclass(frozen=True)
 class SolverDefaults:
     formula: Optional[language.Formula | str] = None
-    structural_predicates: frozenset[
-        language.StructuralPredicate
-    ] = STANDARD_STRUCTURAL_PREDICATES
-    semantic_predicates: frozenset[
-        language.SemanticPredicate
-    ] = STANDARD_SEMANTIC_PREDICATES
+    structural_predicates: frozenset[language.StructuralPredicate] = (
+        STANDARD_STRUCTURAL_PREDICATES
+    )
+    semantic_predicates: frozenset[language.SemanticPredicate] = (
+        STANDARD_SEMANTIC_PREDICATES
+    )
     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

     timeout_seconds: Optional[int] = None
     global_fuzzer: bool = False
     predicates_unique_in_int_arg: Tuple[language.SemanticPredicate, ...] = (
         COUNT_PREDICATE,
     )
-    fuzzer_factory: Callable[
-        [Grammar], GrammarFuzzer
-    ] = lambda grammar: GrammarCoverageFuzzer(grammar)
+    fuzzer_factory: Callable[[Grammar], GrammarFuzzer] = (
+        lambda grammar: GrammarCoverageFuzzer(grammar)
+    )
     tree_insertion_methods: Optional[int] = None
     activate_unsat_support: bool = False
     grammar_unwinding_threshold: int = 4
     initial_tree: Maybe[DerivationTree] = Nothing
     enable_optimized_z3_queries: bool = True

 
         self.solutions: List[DerivationTree] = []
 
         # Debugging stuff
         self.debug = debug
-        self.state_tree: Dict[
-            SolutionState, List[SolutionState]
-        ] = {}  # is only filled if self.debug
+        self.state_tree: Dict[SolutionState, List[SolutionState]] = (
+            {}
+        )  # is only filled if self.debug
         self.state_tree_root = None
         self.current_state = None
         self.costs: Dict[SolutionState, float] = {}
 
         if self.debug:

             for abstracted_tree in generate_abstracted_trees(inp, participating_paths):
                 match (
                     safe(lambda: self.check(abstracted_tree))()
                     .bind(lambda _: Nothing)
                     .lash(
-                        lambda exc: Some(abstracted_tree)
-                        if isinstance(exc, UnknownResultError)
-                        else Nothing
+                        lambda exc: (
+                            Some(abstracted_tree)
+                            if isinstance(exc, UnknownResultError)
+                            else Nothing
+                        )
                     )
                     .bind(do_complete)
                 ):
                     case Some(completed):
                         return Some(completed)

                 # We also try to falsify (negated) semantic predicate formulas, if present,
                 # if there exist any remaining disjuncts.
                 semantic_predicate_formulas: List[
                     Tuple[language.SemanticPredicateFormula, bool]
                 ] = [
-                    (pred_formula, False)
-                    if isinstance(pred_formula, language.SemanticPredicateFormula)
-                    else (cast(language.NegatedFormula, pred_formula).args[0], True)
+                    (
+                        (pred_formula, False)
+                        if isinstance(pred_formula, language.SemanticPredicateFormula)
+                        else (cast(language.NegatedFormula, pred_formula).args[0], True)
+                    )
                     for pred_formula in language.FilterVisitor(
                         lambda f: (
                             constant in f.free_variables()
                             and (
                                 isinstance(f, language.SemanticPredicateFormula)

         )
         existential_formula = cast(
             language.ExistsFormula, conjuncts[existential_formula_idx]
         )
 
-        matches: List[
-            Dict[language.Variable, Tuple[Path, DerivationTree]]
-        ] = matches_for_quantified_formula(existential_formula, self.grammar)
+        matches: List[Dict[language.Variable, Tuple[Path, DerivationTree]]] = (
+            matches_for_quantified_formula(existential_formula, self.grammar)
+        )
 
         for match in matches:
             inst_formula = existential_formula.inner_formula.substitute_expressions(
                 {variable: match_tree for variable, (_, match_tree) in match.items()}
             )

                 tap(
                     lambda intervals: formulas.append(
                         z3_or(
                             [
                                 z3.And(
-                                    repl_var >= z3.IntVal(interval[0])
-                                    if interval[0] > -sys.maxsize
-                                    else z3.BoolVal(True),
-                                    repl_var <= z3.IntVal(interval[1])
-                                    if interval[1] < sys.maxsize
-                                    else z3.BoolVal(True),
+                                    (
+                                        repl_var >= z3.IntVal(interval[0])
+                                        if interval[0] > -sys.maxsize
+                                        else z3.BoolVal(True)
+                                    ),
+                                    (
+                                        repl_var <= z3.IntVal(interval[1])
+                                        if interval[1] < sys.maxsize
+                                        else z3.BoolVal(True)
+                                    ),
                                 )
                                 for interval in intervals
                             ]
                         )
                     )

                     z3.Concat(z3.Range("1", "9"), z3.Star(z3.Range("0", "9"))),
                 )
             elif constant in tree_substitutions:
                 # We have a more concrete shape of the desired instantiation available
                 regexes = [
-                    self.extract_regular_expression(t)
-                    if is_nonterminal(t)
-                    else z3.Re(t)
+                    (
+                        self.extract_regular_expression(t)
+                        if is_nonterminal(t)
+                        else z3.Re(t)
+                    )
                     for t in split_str_with_nonterminals(
                         str(tree_substitutions[constant])
                     )
                 ]
                 assert regexes

                 and not self.graph.reachable(elem, nonterminal)
                 for elem in canonical_expansions[0]
             )
         ):
             result_elements: List[z3.ReRef] = [
-                z3.Re(elem)
-                if not is_nonterminal(elem)
-                else self.extract_regular_expression(elem)
+                (
+                    z3.Re(elem)
+                    if not is_nonterminal(elem)
+                    else self.extract_regular_expression(elem)
+                )
                 for elem in canonical_expansions[0]
             ]
             return self.regex_cache.setdefault(nonterminal, z3.Concat(*result_elements))
 
         regex_conv = RegexConverter(