Fix mcsat-initial-var-order (#507)

* Update solver.c

* 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

@@ -2643,8 +2643,10 @@ void mcsat_set_initial_var_order(mcsat_solver_t* mcsat) {
   uint32_t i;
   for (i = 0; i < n; ++n) {
     term_t x = vars->data[i];
+    assert(term_kind(mcsat->terms, x) == UNINTERPRETED_TERM || term_kind(mcsat->terms, x) == VARIABLE);
     variable_t v = variable_db_get_variable(mcsat->var_db, unsigned_term(x));
     int_queue_push(&mcsat->hinted_decision_vars, v);
+    mcsat_process_registration_queue(mcsat);
   }
 }