From bd2daab658c1c3ac86cfb724245b7ab3c86890d2 Mon Sep 17 00:00:00 2001 From: Thomas Hader Date: Tue, 5 Mar 2024 20:46:15 -0800 Subject: [PATCH] avoid dupplication in top_decision_queue --- src/mcsat/solver.c | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/mcsat/solver.c b/src/mcsat/solver.c index e2fb8e11e..69195671b 100644 --- a/src/mcsat/solver.c +++ b/src/mcsat/solver.c @@ -632,6 +632,11 @@ void mcsat_plugin_context_gc(plugin_context_t* self) { static inline void mcsat_add_top_decision(mcsat_solver_t* mcsat, variable_t x) { + for (int i = 0; i < mcsat->top_decision_vars.size; ++i) { + if (mcsat->top_decision_vars.data[i] == x) { + return; + } + } ivector_push(&mcsat->top_decision_vars, x); }