MCSAT crashes when generating models for curried functions

[daniel-raffler]

Hello,

We notices some crashes in mcsat when using curried functions:

#include <cassert>
#include <iostream>

#include <yices.h>

context_t *newContext(const char *solver) {
    auto cfg = yices_new_config();
    yices_set_config(cfg, "solver-type", solver);
    yices_set_config(cfg, "mode", "interactive");
    yices_set_config(cfg, "model-interpolation", "true");
    auto context = yices_new_context(cfg);
    yices_free_config(cfg);
    return context;
}

int main() {
    yices_init();
    auto integer = yices_int_type();

    auto array = yices_new_uninterpreted_term(yices_function_type1(integer, yices_function_type1(integer, integer)));
    yices_set_term_name(array, "array");

    // array[1][7] = 10
    auto f = yices_eq(
        yices_application(yices_application(array, 1, (int[]){yices_int32(1)}), 1, (int[]){yices_int32(7)}),
        yices_int32(10));

    auto ctx = newContext("mcsat");
    yices_assert_formula(ctx, f);

    auto r = yices_check_context(ctx, nullptr);
    assert(r == YICES_STATUS_SAT);

    std::cout << "SAT" << std::endl;
    auto model = yices_get_model(ctx, true);
    std::cout << yices_model_to_string(model, 100, 80, 0) << std::endl;

    yices_free_context(ctx);
    yices_exit();
    return 0;
}

There are no crashes when using dpllt as solver, and a correct model is printed:

(function array
 (type (-> int (-> int int)))
 (= (array 1) fun!6)
 (default fun!9))
(function fun!6
 (type (-> int int))
 (= (fun!6 7) 10)
 (default 0))
(function fun!9
 (type (-> int int))
 (default 2))

We're using functions in Yices to handle Smtlib Arrays. Most of the time only one index is needed, and that case works just fine with MCSAT. However, if MCSAT fails we'd prefer to get a proper error result, instead of a segfault