diff --git a/src/util/lp/factorization_factory_imp.h b/src/util/lp/factorization_factory_imp.h
index 810be8096..f6d1bcba2 100644
--- a/src/util/lp/factorization_factory_imp.h
+++ b/src/util/lp/factorization_factory_imp.h
@@ -21,7 +21,7 @@
 #include "util/lp/factorization.h"
 namespace nla {
 struct core;
-class rooted_mon;
+struct rooted_mon;
 struct factorization_factory_imp: factorization_factory {
     const core&  m_core;
     const monomial *m_mon;
diff --git a/src/util/lp/nla_basics_lemmas.cpp b/src/util/lp/nla_basics_lemmas.cpp
index c03f37ed8..1e18b71f9 100644
--- a/src/util/lp/nla_basics_lemmas.cpp
+++ b/src/util/lp/nla_basics_lemmas.cpp
@@ -101,7 +101,7 @@ void basics::basic_sign_lemma_model_based_one_mon(const monomial& m, int product
 }
     
 bool basics::basic_sign_lemma_model_based() {
-    unsigned i = random() % c().m_to_refine.size();
+    unsigned i = c().random() % c().m_to_refine.size();
     unsigned ii = i;
     do {
         const monomial& m = c().m_monomials[c().m_to_refine[i]];
@@ -267,7 +267,7 @@ bool basics::basic_lemma(bool derived) {
     c().init_rm_to_refine();
     const auto& rm_ref = c().m_rm_table.to_refine();
     TRACE("nla_solver", tout << "rm_ref = "; print_vector(rm_ref, tout););
-    unsigned start = random() % rm_ref.size();
+    unsigned start = c().random() % rm_ref.size();
     unsigned i = start;
     do {
         const rooted_mon& r = c().m_rm_table.rms()[rm_ref[i]];