mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

call core::random()

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-04-12 15:39:11 -07:00
parent c7c2d81f53
commit c1ee4600d1
2 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/util/lp/factorization_factory_imp.h
View file

@ -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;

4
src/util/lp/nla_basics_lemmas.cpp
View file

@ -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]];