From 3393fdab58187d1ad79ab1141392ed4381c27db6 Mon Sep 17 00:00:00 2001
From: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com>
Date: Tue, 16 Apr 2024 22:32:02 -0700
Subject: [PATCH] Fix Typo in initial var order (#508)

* fix typo

* add test
---
 src/mcsat/solver.c                   |  2 +-
 tests/api/test_mcsat_set_var_order.c | 72 +++++++++++++++++++++++++---
 2 files changed, 67 insertions(+), 7 deletions(-)

diff --git a/src/mcsat/solver.c b/src/mcsat/solver.c
index 51ba2fc98..795dbf494 100644
--- a/src/mcsat/solver.c
+++ b/src/mcsat/solver.c
@@ -2641,7 +2641,7 @@ void mcsat_set_initial_var_order(mcsat_solver_t* mcsat) {
   assert(vars != NULL);
 
   uint32_t i;
-  for (i = 0; i < n; ++n) {
+  for (i = 0; i < n; ++i) {
     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));
diff --git a/tests/api/test_mcsat_set_var_order.c b/tests/api/test_mcsat_set_var_order.c
index f906d5ce4..89c4b8818 100644
--- a/tests/api/test_mcsat_set_var_order.c
+++ b/tests/api/test_mcsat_set_var_order.c
@@ -8,13 +8,60 @@
 
 #include <yices.h>
 
-int main(void)
-{
-  if (! yices_has_mcsat()) {
-    return 1; // skipped
+void check_fixed_order(void) {
+  ctx_config_t* config = yices_new_config();
+  yices_default_config_for_logic(config, "QF_NIA");
+  context_t* ctx = yices_new_context(config);
+
+  term_t x = yices_new_uninterpreted_term(yices_int_type());
+  yices_set_term_name(x, "x");
+
+  term_t y = yices_new_uninterpreted_term(yices_int_type());
+  yices_set_term_name(y, "y");
+
+  assert(!yices_error_code());
+
+  // assertion
+  term_t a = yices_arith_gt_atom(x, yices_mul(y, y));
+  yices_assert_formula(ctx, a);
+
+  // variable order
+  term_t order_vars[2];
+  order_vars[0] = y;
+  order_vars[1] = x;
+  yices_mcsat_set_fixed_var_order(ctx, 2, order_vars);
+
+  // model hint
+  model_t* mdl = yices_new_model();
+  int32_t code;
+  code = yices_model_set_int32(mdl, y, 4);
+  if (code < 0) {
+    yices_print_error(stderr);
+    exit(1);
   }
-  yices_init();
 
+  term_t vars[2];
+  vars[0] = y;
+  vars[1] = x;
+  
+  smt_status_t status;
+  status = yices_check_context_with_model_and_hint(ctx, NULL,  mdl, 1, vars, 0);
+  assert(!yices_error_code());
+
+  assert(status == STATUS_SAT);
+
+  model_t* res_mdl = yices_get_model(ctx, 1);
+  // we should have decided y first and because of the hint its value should be 4
+  assert(yices_formula_true_in_model(res_mdl, yices_arith_eq_atom(y, yices_int32(4))));
+  // x value should be greater than 16 (because x > y*y and y is assigned 4)
+  assert(yices_formula_true_in_model(res_mdl, yices_arith_gt_atom(x, yices_int32(16))));
+  
+  yices_free_model(mdl);
+  yices_free_context(ctx);
+
+}
+
+void check_initial_order(void) {
   ctx_config_t* config = yices_new_config();
   yices_default_config_for_logic(config, "QF_NIA");
   context_t* ctx = yices_new_context(config);
@@ -35,7 +82,7 @@ int main(void)
   term_t order_vars[2];
   order_vars[0] = y;
   order_vars[1] = x;
-  yices_mcsat_set_fixed_var_order(ctx, 2, order_vars);
+  yices_mcsat_set_initial_var_order(ctx, 2, order_vars);
 
   // model hint
   model_t* mdl = yices_new_model();
@@ -64,6 +111,19 @@ int main(void)
   
   yices_free_model(mdl);
   yices_free_context(ctx);
+
+}
+
+int main(void)
+{
+  if (! yices_has_mcsat()) {
+    return 1; // skipped
+  }
+  yices_init();
+
+  check_fixed_order();
+  check_initial_order();
+
   yices_exit();
 
   return 0;