Merge pull request #502 from SRI-CSL/486-assertion-failure-in-srcmcsa…

…tvaluec-could-be-a-duplicate-of-451

#486 fix

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: {

tests/api/issue_486.c

@@ -0,0 +1,65 @@
+#include <stdbool.h>
+
+#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;
+}