diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index ac1aa01c4..14ecd3904 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1623,10 +1623,8 @@ public: svector vars; theory_var sz = static_cast(th.get_num_vars()); for (theory_var v = 0; v < sz; ++v) { - if (th.is_relevant_and_shared(get_enode(v))) { - if (can_be_used_in_random_update(v)) - vars.push_back(get_lpvar(v)); - } + if (can_be_used_in_random_update(v)) + vars.push_back(get_lpvar(v)); } if (vars.empty()) { return false;