         output_print<<<1, 1>>>(fp->out->output_inf, fp->out->output_sup, output_size);
     }
 }
-
-
-/*
-elina_interval_t * box_for_neuron(elina_abstract0_t * abs, size_t layerno, size_t neuron_no){
-    fppoly_t *fp = fppoly_of_abstract0(abs);
-    if(layerno >= fp->numlayers){
-        fprintf(stdout,"the layer does not exist\n");
-        return nullptr;
-    }
-    layer_t * layer = fp->layers[layerno];
-    size_t dims = layer->dims;
-    if(neuron_no >= dims){
-        fprintf(stdout,"the neuron does not exist\n");
-        return nullptr;
-    }
-    neuron_t * neuron = layer->neurons[neuron_no];
-    elina_interval_t * res = elina_interval_alloc();
-    elina_interval_set_double(res,-neuron->lb,neuron->ub);
-    return res;
-}
-
-elina_interval_t ** box_for_layer(elina_abstract0_t * abs, size_t layerno){
-    fppoly_t *fp = fppoly_of_abstract0(abs);
-    if(layerno >= fp->numlayers){
-        fprintf(stdout,"the layer does not exist\n");
-        return nullptr;
-    }
-    layer_t * layer = fp->layers[layerno];
-    size_t dims = layer->dims;
-    elina_interval_t ** itv_arr = (elina_interval_t **)malloc(dims*sizeof(elina_interval_t *));
-    size_t i;
-    for(i=0; i< dims; i++){
-        itv_arr[i] = box_for_neuron(abs, layerno, i);
-    }
-    return itv_arr;
-}
-*/
-
-
-/*
-elina_linexpr0_t* get_expr_for_output_neuron(elina_manager_t* man, elina_abstract0_t* abs, const size_t i, const bool is_lower)
-{
-    fppoly_internal_t* pr = fppoly_init_from_manager(man, ELINA_FUNID_ASSIGN_LINEXPR_ARRAY);
-    fppoly_t* fp = fppoly_of_abstract0(abs);
-
-    const size_t output_size = fp->layers[fp->numlayers - 1]->dims;
-
-    if(i >= output_size)
-    {
-        return nullptr;
-    }
-
-    expr_t* expr = nullptr;
-
-    if(is_lower)
-    {
-        expr = fp->out->lexpr[i];
-    }
-    else
-    {
-        expr = fp->out->uexpr[i];
-    }
-
-    elina_linexpr0_t* res = nullptr;
-
-    if((fp->input_lexpr != nullptr) && (fp->input_uexpr != nullptr))
-    {
-        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, 1);
-        }
-        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, 1);
-        }
-    }
-
-    size_t expr_size = expr->size;
-
-    if(expr->type == SPARSE)
-    {
-        sort_sparse_expr(expr);
-        res = elina_linexpr0_alloc(ELINA_LINEXPR_SPARSE, expr_size);
-    }
-    else
-    {
-        res = elina_linexpr0_alloc(ELINA_LINEXPR_DENSE, expr_size);
-    }
-
-    elina_linexpr0_set_cst_interval_double(res, -expr->inf_cst, expr->sup_cst);
-
-    size_t k;
-
-    for(size_t j = 0; j < expr_size; j++)
-    {
-        if(expr->type == DENSE)
-        {
-            k = j;
-        }
-        else
-        {
-            k = expr->dim[j];
-        }
-
-        elina_linexpr0_set_coeff_interval_double(res, k, -expr->inf_coeff[j], expr->sup_coeff[j]);
-    }
-
-    if((fp->input_lexpr != nullptr) && (fp->input_uexpr != nullptr))
-    {
-        free_expr(expr);
-    }
-
-    return res;
-}
-
-elina_linexpr0_t* get_lexpr_for_output_neuron(elina_manager_t* man, elina_abstract0_t* abs, const size_t i)
-{
-    return get_expr_for_output_neuron(man, abs, i, true);
-}
-
-elina_linexpr0_t* get_uexpr_for_output_neuron(elina_manager_t* man, elina_abstract0_t* abs, const size_t i)
-{
-    return get_expr_for_output_neuron(man, abs, i, false);
-}
-*/

        std::cout << "num_threads" << num_threads << " num_blocks_relu " << num_blocks_relu.y << " num_blocks_linear " << num_blocks_linear.y << std::endl;

        expr_t** aux_expr_array = fp->layers[k]->expr_array;
        expr_t** aux_maxpool_lexpr_array = fp->layers[k]->maxpool_lexpr_array;
        expr_t** aux_maxpool_uexpr_array = fp->layers[k]->maxpool_uexpr_array;

        double* aux_lb_array = fp->layers[k]->lb_array;
        double* aux_ub_array = fp->layers[k]->ub_array;

        if(fp->layers[k]->type != MAXPOOL)
        {
            if(fp->layers[k]->activation == RELU)
            {
                lexpr_replace_relu_bounds_specialized<<<num_blocks_relu, num_threads>>>(lexpr_array, aux_lb_array, aux_ub_array, num_out_neurons_last_layer, num_out_neurons_current_layer);
                uexpr_replace_relu_bounds_specialized<<<num_blocks_relu, num_threads>>>(uexpr_array, aux_lb_array, aux_ub_array, num_out_neurons_last_layer, num_out_neurons_current_layer);
            }

            layer_allocate_exprs<<<num_out_neurons_last_layer, 1>>>(lexpr_array_tmp, num_out_neurons_last_layer, num_in_neurons_current_layer);
            layer_allocate_exprs<<<num_out_neurons_last_layer, 1>>>(uexpr_array_tmp, num_out_neurons_last_layer, num_in_neurons_current_layer);

            expr_from_previous_layer_specialized<<<num_blocks_linear, num_threads>>>(lexpr_array, lexpr_array_tmp, aux_expr_array, num_out_neurons_last_layer, num_out_neurons_current_layer, num_in_neurons_current_layer);
            expr_from_previous_layer_specialized<<<num_blocks_linear, num_threads>>>(uexpr_array, uexpr_array_tmp, aux_expr_array, num_out_neurons_last_layer, num_out_neurons_current_layer, num_in_neurons_current_layer);

            std::swap(lexpr_array, lexpr_array_tmp);
            std::swap(uexpr_array, uexpr_array_tmp);

            free_expr_array<<<num_out_neurons_last_layer, 1>>>(lexpr_array_tmp, num_out_neurons_current_layer);
            free_expr_array<<<num_out_neurons_last_layer, 1>>>(uexpr_array_tmp, num_out_neurons_current_layer);
        }
        else
        {
            lexpr_replace_maxpool_bounds<<<num_out_neurons_last_layer, 1>>>(lexpr_array, aux_maxpool_lexpr_array, aux_maxpool_uexpr_array, aux_lb_array, aux_ub_array, num_out_neurons_last_layer);
            uexpr_replace_maxpool_bounds<<<num_out_neurons_last_layer, 1>>>(uexpr_array, aux_maxpool_lexpr_array, aux_maxpool_uexpr_array, aux_lb_array, aux_ub_array, num_out_neurons_last_layer);
        }
    }

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

    compute_lb_from_expr<<<num_out_neurons_last_layer, 1>>>(lb_array, lexpr_array, fp->input_inf, fp->input_sup, num_out_neurons_last_layer);

    }
}


__global__
void expr_from_previous_layer(expr_t** expr_array, expr_t** res_array, expr_t** aux_expr_array, const size_t num_out_neurons_last_layer, const size_t num_out_neurons_current_layer, const size_t num_in_neurons_current_layer)
{
    size_t n = blockIdx.x;
    size_t j = blockIdx.y*blockDim.x + threadIdx.x;
