From ca0a8441771856f204e5212b3a3326be436ea52a Mon Sep 17 00:00:00 2001
From: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com>
Date: Tue, 10 Sep 2024 23:46:36 -0700
Subject: [PATCH] remove duplicated code about hints in mcsat

---
 src/mcsat/solver.c | 16 ++--------------
 1 file changed, 2 insertions(+), 14 deletions(-)

diff --git a/src/mcsat/solver.c b/src/mcsat/solver.c
index 3a775a2d8..038a685e8 100644
--- a/src/mcsat/solver.c
+++ b/src/mcsat/solver.c
@@ -2451,19 +2451,6 @@ bool mcsat_decide(mcsat_solver_t* mcsat) {
       var = variable_null;
     }
 
-    // then try the variables a plugin requested
-    if (var == variable_null) {
-      while (!int_queue_is_empty(&mcsat->hinted_decision_vars)) {
-        var = int_queue_pop(&mcsat->hinted_decision_vars);
-        assert(var != variable_null);
-        if (!trail_has_value(mcsat->trail, var)) {
-          force_decision = true;
-          break;
-        }
-        var = variable_null;
-      }
-    }
-
     // If there is a fixed order that was passed in, try that
     if (var == variable_null) {
       const ivector_t* order = &mcsat->ctx->mcsat_var_order;
@@ -2489,12 +2476,13 @@ bool mcsat_decide(mcsat_solver_t* mcsat) {
       }
     }
 
-    // try the variables a plugin requested
+    // then try the variables a plugin requested
     if (var == variable_null) {
       while (!int_queue_is_empty(&mcsat->hinted_decision_vars)) {
         var = int_queue_pop(&mcsat->hinted_decision_vars);
         assert(var != variable_null);
         if (!trail_has_value(mcsat->trail, var)) {
+          force_decision = true;
           break;
         }
         var = variable_null;