boolector: Add API checks to fun/array models.

Boolector · Jan 9, 2020 · 4a3d82c · 4a3d82c
1 parent 4f3f93b
commit 4a3d82c
Showing 1 changed file with 4 additions and 2 deletions.
diff --git a/src/boolector.c b/src/boolector.c
@@ -4202,7 +4202,8 @@ boolector_free_array_assignment (Btor *btor,
 
   funass =
       btor_ass_get_fun ((const char **) indices, (const char **) values, size);
-  (void) funass;
+  BTOR_ABORT (size != funass->size,
+              "wrong size given, expected %u, but got %u", funass->size, size);
 #ifndef NDEBUG
   char **cindices, **cvalues;
   cindices = funass->cloned_indices;
@@ -4285,7 +4286,8 @@ boolector_free_uf_assignment (Btor *btor,
   BTOR_ABORT (!size && values, "non zero 'values' but 'size == 0'");
   funass =
       btor_ass_get_fun ((const char **) args, (const char **) values, size);
-  (void) funass;
+  BTOR_ABORT (size != funass->size,
+              "wrong size given, expected %u, but got %u", funass->size, size);
 #ifndef NDEBUG
   char **cargs, **cvalues;
   cargs   = funass->cloned_indices;