From 69c89426da6e5a69ef657f646fd83bf096df90d5 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Sun, 3 Nov 2019 14:28:38 -0800
Subject: [PATCH] port Grobner

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/lp/nla_grobner.cpp | 2 +-
 src/smt/theory_arith_nl.h   | 1 +
 2 files changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp
index fbcaf2e98..f3df0270b 100644
--- a/src/math/lp/nla_grobner.cpp
+++ b/src/math/lp/nla_grobner.cpp
@@ -756,7 +756,7 @@ bool nla_grobner::push_calculation_forward(ptr_vector<equation>& eqs, unsigned &
 }
 
 bool nla_grobner::try_to_modify_eqs(ptr_vector<equation>& eqs, unsigned& next_weight) {
-    NOT_IMPLEMENTED_YET();
+    //    NOT_IMPLEMENTED_YET();
     return false;
 }
 
diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h
index 903968cb8..cd8e389b4 100644
--- a/src/smt/theory_arith_nl.h
+++ b/src/smt/theory_arith_nl.h
@@ -2293,6 +2293,7 @@ template<typename Ext>
 bool theory_arith<Ext>::scan_for_linear(ptr_vector<grobner::equation>& eqs, grobner& gb) {
     bool result = false;
     if (m_params.m_nl_arith_gb_eqs) { // m_nl_arith_gb_eqs is false by default
+        SASSERT(false);
         for (grobner::equation* eq : eqs) {
             if (!eq->is_linear_combination()) {
                     TRACE("non_linear", tout << "processing new equality:\n"; gb.display_equation(tout, *eq););