From ad98594447753b3b8b9f7faabfcb218772894e47 Mon Sep 17 00:00:00 2001
From: Lev <levnach@hotmail.com>
Date: Thu, 13 Dec 2018 15:36:01 -1000
Subject: [PATCH] disable a check

Signed-off-by: Lev <levnach@hotmail.com>
---
 src/util/lp/nla_solver.cpp | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/util/lp/nla_solver.cpp b/src/util/lp/nla_solver.cpp
index 6a508d7b4..62949c318 100644
--- a/src/util/lp/nla_solver.cpp
+++ b/src/util/lp/nla_solver.cpp
@@ -849,7 +849,6 @@ struct solver::imp {
     
     // x is equivalent to y if x = +- y
     void init_vars_equivalence() {
-        SASSERT(abs_values_table_is_ok());
         TRACE("nla_solver",);
         SASSERT(m_vars_equivalence.empty());
         collect_equivs();
@@ -858,7 +857,7 @@ struct solver::imp {
             m_vars_equivalence.register_var(j, vvr(j));
         }
         
-        SASSERT(tables_are_ok());
+        SASSERT((m_lar_solver.settings().random_next() % 100) || tables_are_ok());
     }
 
     bool vars_table_is_ok() const {