Update nra_plugin.c (#543)

SRI-CSL · Dec 11, 2024 · 1ae6ec6 · 1ae6ec6
1 parent f4f5978
commit 1ae6ec6
Showing 1 changed file with 1 addition and 8 deletions.
diff --git a/src/mcsat/nra/nra_plugin.c b/src/mcsat/nra/nra_plugin.c
@@ -802,7 +802,7 @@ void nra_plugin_process_unit_constraint(nra_plugin_t* nra, trail_token_t* prop,
 
     // We don't do any hinting for complicated algebraic values
     if (lp_value_is_rational(&x_value)) {
-      if (lp_feasibility_set_is_point(feasible_set)) {
+      if (lp_feasibility_set_is_point(feasible_set) || (x_is_int_var && lp_feasibility_set_is_point_int(feasible_set))) {
         if (trail_is_at_base_level(nra->ctx->trail) && !nra->ctx->options->model_interpolation) {
           mcsat_value_t value;
           mcsat_value_construct_lp_value(&value, &x_value);
@@ -814,13 +814,6 @@ void nra_plugin_process_unit_constraint(nra_plugin_t* nra, trail_token_t* prop,
           }
           nra->ctx->hint_next_decision(nra->ctx, x);
         }
-      } else if (x_is_int_var && lp_feasibility_set_is_point_int(feasible_set)) {
-        // hint integer variable;
-        // a good candidate for next decision as the feasibility set contains a single integer solution
-        if (ctx_trace_enabled(nra->ctx, "nra::propagate")) {
-          ctx_trace_printf(nra->ctx, "nra: hinting variable = %d\n", x);
-        }
-        nra->ctx->hint_next_decision(nra->ctx, x);
       } else if (!lp_feasibility_set_is_full(feasible_set)) {
         lp_interval_t x_interval;
         lp_interval_construct_full(&x_interval); // [-inf, +inf]