From 2560c9b739be55eb4534bee113649ac25fd7f60a Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 17 Jun 2019 20:48:29 -0700 Subject: [PATCH] randomize m_to_refine() init Signed-off-by: Lev Nachmanson --- src/math/lp/emonomials.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/math/lp/emonomials.h b/src/math/lp/emonomials.h index a97b7d92a..bbbbf4e0c 100644 --- a/src/math/lp/emonomials.h +++ b/src/math/lp/emonomials.h @@ -95,7 +95,6 @@ class emonomials { hashtable m_cg_table; // congruence (canonical) table. - unsigned number_of_monomials() const { return m_monomials.size(); } void inc_visited() const; void remove_cell(head_tail& v, unsigned mIndex); @@ -115,6 +114,7 @@ class emonomials { bool is_visited(monomial const& m) const; std::ostream& display_use(std::ostream& out) const; public: + unsigned number_of_monomials() const { return m_monomials.size(); } /** \brief emonomials builds on top of var_eqs. push and pop on emonomials calls push/pop on var_eqs, so no