asserts

SRI-CSL · Nov 1, 2023 · bdd5e40 · bdd5e40
1 parent eb52eef
commit bdd5e40
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 0 deletions.
diff --git a/src/api/yices_api.c b/src/api/yices_api.c
@@ -9267,6 +9267,8 @@ EXPORTED smt_status_t yices_check_context_with_model_and_hint(context_t *ctx, co
     return STATUS_ERROR;
   }
 
+  assert(m <= n);
+
   // cleanup
   switch (context_status(ctx)) {
   case STATUS_UNKNOWN:

diff --git a/src/context/context_solver.c b/src/context/context_solver.c
@@ -638,6 +638,8 @@ smt_status_t check_context_with_model(context_t *ctx, const param_t *params, mod
  * - set the model hint and call check_context_with_model
  */
 smt_status_t check_context_with_model_and_hint(context_t *ctx, const param_t *params, model_t* mdl, uint32_t n, const term_t t[], uint32_t m) {
+  assert(m <= n);
+
   mcsat_set_model_hint(ctx->mcsat, mdl, n, t);
 
   return check_context_with_model(ctx, params, mdl, m, t);