diff --git a/src/mcsat/value.c b/src/mcsat/value.c index 03053fd1b..25b1a440a 100644 --- a/src/mcsat/value.c +++ b/src/mcsat/value.c @@ -23,6 +23,8 @@ #include "utils/memalloc.h" #include "utils/hash_functions.h" +#include "api/yices_api_lock_free.h" + const mcsat_value_t mcsat_value_none = { VALUE_NONE, { true } }; const mcsat_value_t mcsat_value_true = { VALUE_BOOLEAN, { true } }; const mcsat_value_t mcsat_value_false = { VALUE_BOOLEAN, { false } }; @@ -118,8 +120,19 @@ void mcsat_value_construct_from_constant_term(mcsat_value_t* t_value, term_table break; } case CONSTANT_TERM: { - assert(t == true_term || t == false_term); - mcsat_value_construct_bool(t_value, t == true_term); + // Boolean terms case + if (t == true_term || t == false_term) { + mcsat_value_construct_bool(t_value, t == true_term); + } else { + // scalar case + int32_t int_value; + _o_yices_scalar_const_value(t, &int_value); + rational_t q; + q_init(&q); + q_set32(&q, int_value); + mcsat_value_construct_rational(t_value, &q); + q_clear(&q); + } break; } case ARITH_CONSTANT: { diff --git a/tests/api/issue_486.c b/tests/api/issue_486.c new file mode 100644 index 000000000..f6588a9b0 --- /dev/null +++ b/tests/api/issue_486.c @@ -0,0 +1,65 @@ +#include + +#include "yices.h" + +#include "assert.h" + +/* + * Create an MCSAT context + */ +static context_t *make_mcsat_context(void) { + ctx_config_t *config; + context_t *context; + int32_t code; + + config = yices_new_config(); + code = yices_set_config(config, "solver-type", "mcsat"); + if (code < 0) goto error; + context = yices_new_context(config); + if (context == NULL) goto error; + yices_free_config(config); + return context; + + error: + yices_print_error(stderr); + yices_free_config(config); + return NULL; +} + +int +main(void) +{ + context_t *ctx; + + yices_init(); + ctx = make_mcsat_context(); + + type_t p = yices_new_uninterpreted_type(); + type_t r = yices_real_type(); + + //type_t a = yices_function_type1(p, r); + //type_t f = yices_function_type1(p, a); + type_t f = yices_function_type1(p, r); + //type_t g = yices_function_type2(p, a, r); + + term_t f1 = yices_new_uninterpreted_term(f); + //term_t g1 = yices_new_uninterpreted_term(g); + + term_t c1 = yices_constant(p, 1); + + term_t t1 = yices_application1(f1, c1); + //term_t t2 = yices_application2(g1, c1, t1); + term_t zero = yices_zero(); + + yices_assert_formula(ctx, yices_eq(zero, t1)); + + smt_status_t status; + status = yices_check_context(ctx, NULL); + if (status != STATUS_SAT) { + assert(false); + } + + //model_t *model = yices_get_model(ctx, 1); + + return 0; +}