fix

src/context/context.c

@@ -5830,6 +5830,9 @@ void reset_context(context_t *ctx) {
 
   reset_gate_manager(&ctx->gate_manager);
 
+  ivector_reset(&ctx->mcsat_var_order);
+  ivector_reset(&ctx->mcsat_initial_var_order);
+
   reset_intern_tbl(&ctx->intern);
   ivector_reset(&ctx->top_eqs);
   ivector_reset(&ctx->top_atoms);
@@ -6691,3 +6694,4 @@ void context_gc_mark(context_t *ctx) {
     mcsat_gc_mark(ctx->mcsat);
   }
 }
+

src/context/context.h

@@ -494,5 +494,4 @@ extern bval_t context_bool_term_value(context_t *ctx, term_t t);
 extern void context_gc_mark(context_t *ctx);
 
 
-
 #endif /* __CONTEXT_H */

src/mcsat/solver.c

@@ -2632,7 +2632,7 @@ void mcsat_set_model_hint(mcsat_solver_t* mcsat, model_t* mdl, uint32_t n_mdl_fi
 
 static
 void mcsat_set_initial_var_order(mcsat_solver_t* mcsat) {
-  ivector_t* vars = &mcsat->ctx->mcsat_initial_var_order;
+  const ivector_t* vars = &mcsat->ctx->mcsat_initial_var_order;
   uint32_t n = vars->size;
   if (n == 0) {
     return;
@@ -2648,8 +2648,6 @@ void mcsat_set_initial_var_order(mcsat_solver_t* mcsat) {
     int_queue_push(&mcsat->hinted_decision_vars, v);
     mcsat_process_registration_queue(mcsat);
   }
-
-  ivector_reset(vars);
 }
 
 void mcsat_solve(mcsat_solver_t* mcsat, const param_t *params, model_t* mdl, uint32_t n_assumptions, const term_t assumptions[]) {