From 3d2fc57b82453631ab1f6e27202384ad69bfa15d Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Fri, 23 Aug 2019 16:36:17 -0700
Subject: [PATCH] fix the build

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/lp/cross_nested.h | 8 ++++++--
 src/math/lp/horner.cpp     | 5 +++--
 src/test/lp/lp.cpp         | 7 +++++--
 3 files changed, 14 insertions(+), 6 deletions(-)

diff --git a/src/math/lp/cross_nested.h b/src/math/lp/cross_nested.h
index f76a2434b..09d3706ee 100644
--- a/src/math/lp/cross_nested.h
+++ b/src/math/lp/cross_nested.h
@@ -38,6 +38,7 @@ class cross_nested {
     nex *                                 m_e;
     std::function<bool (const nex*)>      m_call_on_result;
     std::function<bool (unsigned)>        m_var_is_fixed;
+    std::function<unsigned ()>            m_random;    
     bool                                  m_done;
     std::unordered_map<lpvar, occ>        m_occurences_map;
     std::unordered_map<lpvar, unsigned>   m_powers;
@@ -45,6 +46,7 @@ class cross_nested {
     ptr_vector<nex>                       m_b_split_vec;
     int                                   m_reported;
     bool                                  m_random_bit;
+    
 #ifdef Z3DEBUG
     nex* m_e_clone;
 #endif
@@ -53,9 +55,11 @@ class cross_nested {
     }
 public:
     cross_nested(std::function<bool (const nex*)> call_on_result,
-                 std::function<bool (unsigned)> var_is_fixed):
+                 std::function<bool (unsigned)> var_is_fixed,
+                 std::function<unsigned ()> random):
         m_call_on_result(call_on_result),
         m_var_is_fixed(var_is_fixed),
+        m_random(random),
         m_done(false),
         m_reported(0)
     {}
@@ -363,7 +367,7 @@ public:
         for (auto & p : m_occurences_map)
             vars.push_back(p.first);
 
-        m_random_bit = random() % 2;
+        m_random_bit = m_random() % 2;
         TRACE("nla_cn", tout << "m_random_bit = " << m_random_bit << "\n";);
         std::sort(vars.begin(), vars.end(), [this](lpvar j, lpvar k)
                                             {
diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp
index 4f2ff2f33..e6c57b63c 100644
--- a/src/math/lp/horner.cpp
+++ b/src/math/lp/horner.cpp
@@ -91,8 +91,9 @@ template <typename T>
 bool horner::lemmas_on_row(const T& row) {
     cross_nested cn(
         [this](const nex* n) { return check_cross_nested_expr(n); },
-        [this](unsigned j)   { return c().var_is_fixed(j); }
-        );
+        [this](unsigned j)   { return c().var_is_fixed(j); },
+        [this]() { return c().random(); }
+                    );
 
     SASSERT (row_is_interesting(row));
     create_sum_from_row(row, cn);
diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp
index 0433232d5..13d37fb8a 100644
--- a/src/test/lp/lp.cpp
+++ b/src/test/lp/lp.cpp
@@ -74,11 +74,14 @@ void test_cn_on_expr(nex_sum *t, cross_nested& cn) {
 }
 
 void test_cn() {
-    cross_nested cn([](const nex* n) {
+    cross_nested cn(
+        [](const nex* n) {
                            TRACE("nla_cn_test", tout << *n << "\n";);
                            return false;
                        } ,
-        [](unsigned) { return false; });
+        [](unsigned) { return false; },
+        []{ return 1; }
+        );
     enable_trace("nla_cn");
     enable_trace("nla_cn_details");
     nex_var* a = cn.mk_var(0);