 }
 
 
-
 void update_state_using_previous_layers(elina_manager_t* man, fppoly_t* fp, const size_t layerno)
 {
     fppoly_internal_t* pr = fppoly_init_from_manager(man, ELINA_FUNID_ASSIGN_LINEXPR_ARRAY);

        if(is_lower)
        {
            expr_t** expr_ptr = &expr;
            replace_input_poly_cons_in_lexpr(expr_ptr, fp->input_inf, fp->input_sup, fp->input_lexpr, fp->input_uexpr);
        }
        else
        {
            expr_t** expr_ptr = &expr;
            replace_input_poly_cons_in_uexpr(expr_ptr, fp->input_inf, fp->input_sup, fp->input_lexpr, fp->input_uexpr);
        }
    }


        {
            if(fp->layers[k]->activation == RELU)
            {
                lexpr_replace_relu_bounds(lexpr_array, aux_neurons, num_out_neurons);
                uexpr_replace_relu_bounds(uexpr_array, aux_neurons, num_out_neurons);
            }

            expr_from_previous_layer(lexpr_array, aux_neurons, num_out_neurons);
            expr_from_previous_layer(uexpr_array, aux_neurons, num_out_neurons);
        }
        else
        {
            lexpr_replace_maxpool_bounds(lexpr_array, aux_neurons, num_out_neurons);
            uexpr_replace_maxpool_bounds(uexpr_array, aux_neurons, num_out_neurons);
        }
    }

    if((fp->input_lexpr != nullptr) && (fp->input_uexpr != nullptr))
    {
        replace_input_poly_cons_in_lexpr(lexpr_array, fp->input_inf, fp->input_sup, fp->input_lexpr, fp->input_uexpr, num_out_neurons);
        replace_input_poly_cons_in_uexpr(uexpr_array, fp->input_inf, fp->input_sup, fp->input_lexpr, fp->input_uexpr, num_out_neurons);
    }

    double* lb_array = (double*) malloc(num_out_neurons*sizeof(double));
    double* ub_array = (double*) malloc(num_out_neurons*sizeof(double));

    compute_lb_from_expr(lb_array, lexpr_array, fp->input_inf, fp->input_sup, fp->input_lexpr, fp->input_uexpr, num_out_neurons);
    compute_ub_from_expr(ub_array, uexpr_array, fp->input_inf, fp->input_sup, fp->input_lexpr, fp->input_uexpr, num_out_neurons);

    for(size_t i = 0; i < num_out_neurons; i++)
    {
        out_neurons[i]->lb = lb_array[i];
        out_neurons[i]->ub = ub_array[i];
    }

    free(lb_array);
    free(ub_array);

    if(fp->out != nullptr)
    {
        //TODO: The (l/u)expr_array assigned here is not correct. The contents were changed in the replace_input_poly_cons_in_lexpr, but they should not have been changed there. Need to create another temporary array for the results of replace_input_poly_cons_in_lexpr. Maybe this is a feature, not a bug? Seems like this is exactly what the method get_expr_for_output_neuron is doing!
        fp->out->lexpr = lexpr_array;
        fp->out->uexpr = uexpr_array;
    }
    else
    {
        for(size_t i = 0; i < num_out_neurons; i++)
        {
            free_expr(lexpr_array[i]);
            free_expr(uexpr_array[i]);
        }

        free(lexpr_array);
        free(uexpr_array);
    }
}

