boolector: Fix model construction for constant arrays.

src/boolector.c

@@ -4070,23 +4070,37 @@ generate_fun_model_str (
 
     /* build assignment string for all arguments */
     t   = (BtorBitVectorTuple *) btor_iter_hashptr_next (&it);
-    len = t->arity;
-    for (j = 0; j < t->arity; j++) len += btor_bv_get_width (t->bv[j]);
-    BTOR_NEWN (btor->mm, arg, len);
-    tmp = arg;
-
-    bv = btor_bv_to_char (btor->mm, t->bv[0]);
-    strcpy (tmp, bv);
-    btor_mem_freestr (btor->mm, bv);
-
-    for (j = 1; j < t->arity; j++)
+    if (t->arity)
     {
-      bv = btor_bv_to_char (btor->mm, t->bv[j]);
-      strcat (tmp, " ");
-      strcat (tmp, bv);
+      len = t->arity;
+      for (j = 0; j < t->arity; j++) len += btor_bv_get_width (t->bv[j]);
+      BTOR_CNEWN (btor->mm, arg, len);
+      tmp = arg;
+
+      bv = btor_bv_to_char (btor->mm, t->bv[0]);
+      strncpy (tmp, bv, len);
+      len -= strlen (bv);
       btor_mem_freestr (btor->mm, bv);
+
+      for (j = 1; j < t->arity; j++)
+      {
+        bv = btor_bv_to_char (btor->mm, t->bv[j]);
+        strncat (tmp, " ", len);
+        len -= 1;
+        strncat (tmp, bv, len);
+        len -= strlen (bv);
+        btor_mem_freestr (btor->mm, bv);
+      }
+      len -= 1;
+      assert (len == 0);
+    }
+    /* If argument tuple has arity 0, value represents the default value for
+     * the function/array (constant arrays). */
+    else
+    {
+      BTOR_CNEWN (btor->mm, arg, 2);
+      arg[0] = '*';
     }
-    assert (strlen (arg) == len - 1);
 
     (*args)[i]   = arg;
     (*values)[i] = (char *) btor_bv_to_char (btor->mm, value);

src/boolector.h

@@ -2051,10 +2051,11 @@ void boolector_free_bv_assignment (Btor *btor, const char *assignment);
   expression. See our publication `Lemmas on Demand for Lambdas
   <http://fmv.jku.at/papers/PreinerNiemetzBiere-DIFTS13.pdf>`_ for details. At
   indices that do not occur in the model, it is assumed that the array stores a
-  globally unique default value, for example 0.  The bit-vector assignments to
-  the indices and values have to be freed by boolector_free_bv_assignment.
-  Furthermore, the user has to free the array of indices and the array of
-  values, respectively of size ``size``.
+  globally unique default value, for example 0. If the model of a constant array
+  is queried the default value of the constant array is indicated via index '*'.
+  The bit-vector assignments to the indices and values have to be freed by
+  boolector_free_bv_assignment. Furthermore, the user has to free the array of
+  indices and the array of values, respectively of size ``size``.
 
   :param btor: Boolector instance.
   :param n_array: Array operand for which the array model should be built.