def effect(start, idx, local_list, rule_list, conf_symbol, trans_symbol):
    """
    Returns SMT constrains that relate a transition and a configuration 
    obtained as a result of the transition
    """
    result = ""
    for i in range(start, idx):
        for j in local_list:
            rls = [r for r in rule_list if r["to"] == j]
            if len(rls) == 0:
                result += "(= 0 " + conf_symbol + str(i + 1) + "_" + str(j) + ")\n"
            elif len(rls) == 1:
                result += "(= " + trans_symbol + str(i) + "_" + str(rls[0]["idx"]) + " " + conf_symbol + str(i + 1) + "_" + str(j) + ")\n"
            else:
                rsum = "(+"
                for r in rls:
                    rsum += " " + trans_symbol + str(i) + "_" + str(r["idx"])
                rsum += ")"
                result += "(= " + rsum + " " + conf_symbol + str(i + 1) + "_" + str(j) + ")\n"
        result += "\n"
    return result