From f97dd3402880963fe5b19ccbf144c3cce4e07cd7 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 30 Oct 2023 14:54:04 -0700
Subject: [PATCH] tests

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/seq_rewriter.cpp |  2 +-
 src/math/lp/int_solver.cpp        | 26 ++++++++++++++++++++++----
 src/math/lp/nla_basics_lemmas.cpp |  2 +-
 src/math/lp/nla_grobner.cpp       |  2 --
 src/math/lp/nra_solver.cpp        |  2 --
 src/smt/theory_lra.cpp            |  2 +-
 6 files changed, 25 insertions(+), 11 deletions(-)

diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 4f94b89d2..12ab1cbb1 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -873,8 +873,8 @@ br_status seq_rewriter::mk_seq_length(expr* a, expr_ref& result) {
         m_autil.is_numeral(y, r) && r.is_zero() &&
         m_autil.is_numeral(z, r) && r >= 0) {
         expr* len_x = str().mk_length(x);
-        expr* zero = m_autil.mk_int(0);
         result = m().mk_ite(m_autil.mk_le(len_x, z), len_x, z);
+        // expr* zero = m_autil.mk_int(0);
         // result = m().mk_ite(m_autil.mk_le(z, zero), zero, result);
         return BR_REWRITE_FULL;
     }
diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp
index 6e0c90679..a16fdea4c 100644
--- a/src/math/lp/int_solver.cpp
+++ b/src/math/lp/int_solver.cpp
@@ -689,7 +689,8 @@ namespace lp {
 
     void int_solver::simplify(std::function<bool(unsigned)>& is_root) {
 
-#if 0
+        return;
+#if 1
 
         // in-processing simplification can go here, such as bounds improvements.
 
@@ -699,6 +700,20 @@ namespace lp {
                 return;
         }
 
+        
+#endif
+
+#if 1
+        lp::explanation exp;
+        m_ex = &exp;
+        m_t.clear();
+        m_k.reset();
+
+        if (has_inf_int()) 
+            local_gomory();            
+#endif
+
+#if 0
         stopwatch sw;
         explanation exp1, exp2;
 
@@ -919,8 +934,7 @@ namespace lp {
     }
 
     lia_move int_solver::local_gomory() {
-        for (unsigned i = 0; i < 4; ++i) {
-            
+        for (unsigned i = 0; i < 2 && has_inf_int() && !settings().get_cancel_flag(); ++i) {
             m_ex->clear();
             m_t.clear();
             m_k.reset();
@@ -939,11 +953,15 @@ namespace lp {
                 lra.get_infeasibility_explanation(*m_ex);
                 return lia_move::conflict;
             }
+            //r = m_patcher();
+            //if (r != lia_move::undef)
+            //    return r;
         }
         m_ex->clear();
         m_t.clear();
         m_k.reset();
-
+        if (!has_inf_int())
+            return lia_move::sat;
         return lia_move::undef;
     }
 
diff --git a/src/math/lp/nla_basics_lemmas.cpp b/src/math/lp/nla_basics_lemmas.cpp
index 191e59a79..705247aa1 100644
--- a/src/math/lp/nla_basics_lemmas.cpp
+++ b/src/math/lp/nla_basics_lemmas.cpp
@@ -331,7 +331,7 @@ bool basics::basic_lemma_for_mon_neutral_derived(const monic& rm, const factoriz
     for (auto fc : f) {
         lpvar j = var(fc);
         all_int &= c().var_is_int(j);        
-        if (j == null_lpvar && abs(val(j)) == abs_mv && 
+        if (u == null_lpvar && abs(val(j)) == abs_mv && 
             c().vars_are_equiv(j, mon_var) &&
             (mon_var_is_sep_from_zero ||  c().var_is_separated_from_zero(j))) 
             u = j;
diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp
index 21d46cccc..92c02ab80 100644
--- a/src/math/lp/nla_grobner.cpp
+++ b/src/math/lp/nla_grobner.cpp
@@ -100,7 +100,6 @@ namespace nla {
     }
 
     bool grobner::is_conflicting() {
-        bool is_conflict = false;
         for (auto eq : m_solver.equations()) {
             if (is_conflicting(*eq)) {
                 lp_settings().stats().m_grobner_conflicts++;
@@ -677,7 +676,6 @@ namespace nla {
         nex_creator& nc = m_nex_creator;
         nc.pop(0);
         nex_creator::sum_factory sum(nc);
-        unsigned row_index = 0;
         u_map<nex_var*> var2nex;
         for (auto v : eq.poly().free_vars()) 
             var2nex.insert(v, nc.mk_var(v));
diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp
index 5bf983f15..74d6f7187 100644
--- a/src/math/lp/nra_solver.cpp
+++ b/src/math/lp/nra_solver.cpp
@@ -286,11 +286,9 @@ struct solver::imp {
 
     bool check_constraint(unsigned idx) {
         auto& c = lra.constraints()[idx];
-        auto& pm = m_nlsat->pm();
         auto k = c.kind();
         auto offset = -c.rhs();
         auto lhs = c.coeffs();
-        auto sz = lhs.size();
         
         scoped_anum val(am()), mon(am());
         am().set(val, offset.to_mpq());
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 7856485d6..90e6ddce0 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1091,7 +1091,7 @@ public:
 
     void restart_eh() {
         m_arith_eq_adapter.restart_eh();
-#if 0
+#if 1
         // experiment
         if (m_lia) {
             std::function<bool(unsigned)> is_root = [&](unsigned j) {