Z3-Solver (z3.z3types.Z3Exception: Z3 invalid substitution, expression pairs expected.)

I have a relative complex Z3 boolean formula and when trying to set the values of a particular variable , I get the following error :
raise Z3Exception(msg) z3.z3types.Z3Exception: Z3 invalid substitution, expression pairs expected.

I tried the following :

def create_z3_formula_bdd(dimacs_file):
    variable_names = {
        1: 'inflow1', 2: "inflow1'",
        3: 'inflow2', 4: "inflow2'",
        5: 'level@0.3.107', 6: "level@0.3.107'",
        7: 'level@1', 8: "level@1'",
        9: 'level@2', 10: "level@2'",
        11: 'level@3', 12: "level@3'",
        13: 'level@4', 14: "level@4'",
        15: 'level@5', 16: "level@5'",
        17: 'level@6', 18: "level@6'",
        19: 'outflow', 20: "outflow'",
        21: '_jx_b0'
    }
    with open(dimacs_file, 'r') as f:
        dimacs_lines = f.readlines()

    # Parse variables and clauses
    variables = set()
    clauses = []
    for line in dimacs_lines:
        tokens = line.split()
        if tokens[0] == 'p':
            num_vars = int(tokens[2])
        elif tokens[0] != 'c' and tokens[0] != '0':
            clause = [int(var) for var in tokens[:-1]]
            variables.update(map(abs, clause))
            clauses.append(clause)

    z3_variables = {var: Bool(variable_names[abs(var)]) for var in variables}

    # Create Z3 clauses
    z3_clauses = [Or([z3_variables[abs(literal)] if literal > 0 else Not(z3_variables[abs(literal)]) for literal in clause]) for clause in clauses]

    return And(z3_clauses)

 formula_bdd = create_z3_formula_bdd('neg_water_reservoir.cnf')
 substitution_map = {variable_names[1]: False}
 formula_with_substitution = substitute(formula_bdd, substitution_map)

You need to post a minimal-reproducible example; i.e., an example that readers of your question can run independently on their own. Please see: https://stackoverflow.com/help/minimal-reproducible-example

Having said that, z3's substitute method expects a pair of values: https://z3prover.github.io/api/html/namespacez3py.html#ae8f9a59a4fcabbb12636c128178c5235

So, you might start by turning your substitution_map's from a python dictionary to a list of pairs. Hopefully that'll get you going. If not, please post a minimal code segment that we can run independently.