From 3b93035e0f3e3e34986117806226a6cd016adba9 Mon Sep 17 00:00:00 2001
From: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com>
Date: Thu, 11 Apr 2024 01:50:06 -0700
Subject: [PATCH] Fix mcsat-initial-var-order (#507)

* Update solver.c

* fix
---
 src/context/context.c | 4 ++++
 src/context/context.h | 1 -
 src/mcsat/solver.c    | 2 ++
 3 files changed, 6 insertions(+), 1 deletion(-)

diff --git a/src/context/context.c b/src/context/context.c
index 74dc490be..f36c7eb82 100644
--- a/src/context/context.c
+++ b/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);
   }
 }
+
diff --git a/src/context/context.h b/src/context/context.h
index 3b2cc12db..3d97600c2 100644
--- a/src/context/context.h
+++ b/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 */
diff --git a/src/mcsat/solver.c b/src/mcsat/solver.c
index 143dcfe4c..51ba2fc98 100644
--- a/src/mcsat/solver.c
+++ b/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);
   }
 }