From 7a74b099baa40326f5f954f3e42af1f517c5d3e6 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 20 Sep 2023 15:04:24 -0700
Subject: [PATCH] remove experimental code

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/theory_arith_nl.h | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h
index 77e2b25f3..f44516cad 100644
--- a/src/smt/theory_arith_nl.h
+++ b/src/smt/theory_arith_nl.h
@@ -511,7 +511,6 @@ bool theory_arith<Ext>::propagate_nl_downward(expr * n, var_power_pair const& p)
 */
 template<typename Ext>
 bool theory_arith<Ext>::propagate_nl_bounds(expr * m) {
-    return false;
     TRACE("non_linear", tout << "propagate several bounds using:\n"; display_monomial(tout, m); tout << "\n";);
     bool result = propagate_nl_upward(m);
     buffer<var_power_pair> vp;
@@ -531,7 +530,6 @@ bool theory_arith<Ext>::propagate_nl_bounds(expr * m) {
 */
 template<typename Ext>
 bool theory_arith<Ext>::propagate_nl_bounds() {
-    return false;
     m_dep_manager.reset();
     bool propagated = false;
     for (unsigned i = 0; i < m_nl_monomials.size(); i++) {
@@ -1634,7 +1632,6 @@ bool theory_arith<Ext>::is_cross_nested_consistent(row const & r) {
 */
 template<typename Ext>
 bool theory_arith<Ext>::is_cross_nested_consistent(svector<theory_var> const & nl_cluster) {
-    return true;
     for (theory_var v : nl_cluster) {
         if (!is_base(v))
             continue;