From 9c4003d12e3f5c628f986d9896e3183660ab8da9 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 6 Jun 2023 11:06:13 -0700
Subject: [PATCH] fix to arithmetic internalize for multiplier

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/smt/euf_proof_checker.cpp |  5 +++++
 src/smt/smt_context_pp.cpp        |  4 ++--
 src/smt/theory_arith_core.h       |  1 +
 src/smt/theory_lra.cpp            | 14 ++++++++------
 4 files changed, 16 insertions(+), 8 deletions(-)

diff --git a/src/sat/smt/euf_proof_checker.cpp b/src/sat/smt/euf_proof_checker.cpp
index a538b2a80..e63297787 100644
--- a/src/sat/smt/euf_proof_checker.cpp
+++ b/src/sat/smt/euf_proof_checker.cpp
@@ -521,12 +521,17 @@ namespace euf {
         core_solver->assert_expr(m.mk_not(mk_or(clause)));
         lbool ch = core_solver->check_sat(assumptions);
         std::cout << "failed to verify\n" << clause << "\n";
+        std::cout << "check result: " << ch << "\n";
+
         if (ch == l_false) {
             core_solver->get_unsat_core(core);
             std::cout << "core\n";
             for (expr* f : core)
                 std::cout << mk_pp(f, m) << "\n";
         }
+
+        return;
+        
         SASSERT(false);
         
         exit(0);
diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp
index 0e72f2f93..c1d903631 100644
--- a/src/smt/smt_context_pp.cpp
+++ b/src/smt/smt_context_pp.cpp
@@ -241,7 +241,7 @@ namespace smt {
                 if (!is_relevant(lit)) out << " n ";
                 out << ": ";
                 display_verbose(out, m, 1, &lit, m_bool_var2expr.data());
-                if (level > 0) {
+                if (level > 0 || true) {
                     auto j = get_justification(lit.var());
                     display(out << " ", j);
                 }
@@ -635,7 +635,7 @@ namespace smt {
             literal_vector lits;
             const_cast<conflict_resolution&>(*m_conflict_resolution).justification2literals(j.get_justification(), lits);
             out << "justification " << j.get_justification()->get_from_theory() << ": ";
-            // display_literals_smt2(out, lits);
+            display_literals_smt2(out, lits);
             break;
         }
         default:
diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index 4b9684679..0c696fcbb 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -390,6 +390,7 @@ namespace smt {
         if (v == null_theory_var) {
             v = mk_var(e);
         }
+        
         return v;
     }
 
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 966f3922a..0271bcf44 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -378,7 +378,7 @@ class theory_lra::imp {
             if (a.is_extended_numeral(arg2, val)) 
                 std::swap(arg1, arg2);
             if (a.is_extended_numeral(arg1, val)) {
-                st.add(internalize_term_core(to_app(arg2)), val);
+                st.add(internalize_term_core(to_app(arg2)), sign * val);
                 if (reflect(arg)) {
                     internalize_term_core(to_app(arg1));
                     mk_enode(arg);
@@ -386,7 +386,8 @@ class theory_lra::imp {
                 return;
             }
         }
-        st.add(internalize_term_core(arg), sign);
+        else 
+            st.add(internalize_term_core(arg), sign);
     }
 
     theory_var internalize_numeral(app* n, rational const& val) {
@@ -1326,7 +1327,7 @@ public:
             n1->get_th_var(get_id()) != null_theory_var &&
             n2->get_th_var(get_id()) != null_theory_var && n1 != n2) {
             //            verbose_stream() << "ineq\n";
-            m_arith_eq_adapter.mk_axioms(n1, n2);
+            // m_arith_eq_adapter.mk_axioms(n1, n2);
         }
         //        else
         //    verbose_stream() << "skip\n";
@@ -2120,7 +2121,6 @@ public:
         result = final_check_core();
         TRACE("arith", tout << "result: " << result << "\n";);
         if (result == FC_DONE) {
-            verbose_stream() << "second round\n";
             validate_solution();
         }
         return result;
@@ -2247,7 +2247,7 @@ public:
             }
             if (st == FC_DONE) {
                 if (assume_eqs()) {
-                    verbose_stream() << "not done\n";
+                    // verbose_stream() << "not done\n";
                     return FC_CONTINUE;
                 }
 
@@ -2939,6 +2939,7 @@ public:
     literal_vector m_core2;
 
     void assign(literal lit, literal_vector const& core, svector<enode_pair> const& eqs, vector<parameter> const& params) {
+        TRACE("arith", tout << lit << " <- " << core << " #eqs " << eqs.size() << "\n");
         if (core.size() < small_lemma_size() && eqs.empty()) {
             m_core2.reset();
             for (auto const& c : core) {
@@ -3805,7 +3806,8 @@ public:
               for (auto const& p : m_params) tout << " " << p;
               tout << "\n";
               display_evidence(tout, m_explanation);
-              display(tout << "is-conflict: " << is_conflict << "\n"););
+              //display(tout << "is-conflict: " << is_conflict << "\n");
+              );
 
         TRACE("arith_conflict",
               display_evidence(tout, m_explanation);