From 7399f78dfd2c38fc50170f3560811bc54b917859 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 3 Mar 2019 12:40:59 -0800
Subject: [PATCH] disable model compression for regressions

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/parsers/smt2/smt2parser.cpp | 2 +-
 src/qe/qe_lite.cpp              | 1 -
 src/sat/sat_solver.cpp          | 2 +-
 src/util/lp/int_solver.cpp      | 4 +++-
 4 files changed, 5 insertions(+), 4 deletions(-)

diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp
index b3b8082fe..e09ea0f3c 100644
--- a/src/parsers/smt2/smt2parser.cpp
+++ b/src/parsers/smt2/smt2parser.cpp
@@ -2677,7 +2677,7 @@ namespace smt2 {
             m_ctx.regular_stream() << "(";
             expr ** expr_it  = expr_stack().c_ptr() + spos;
             expr ** expr_end = expr_it + m_cached_strings.size();
-            md->compress();
+            // md->compress();
             for (unsigned i = 0; expr_it < expr_end; expr_it++, i++) {
                 model::scoped_model_completion _scm(md, true);
                 expr_ref v = (*md)(*expr_it);
diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp
index 1f8f78aaa..4e2d8413a 100644
--- a/src/qe/qe_lite.cpp
+++ b/src/qe/qe_lite.cpp
@@ -2430,7 +2430,6 @@ class qe_lite_tactic : public tactic {
             tactic_report report("qe-lite", *g);
             proof_ref new_pr(m);
             expr_ref new_f(m);
-            bool produce_proofs = g->proofs_enabled();
 
             unsigned sz = g->size();
             for (unsigned i = 0; i < sz; i++) {
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index c6b04cfd8..427077804 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -42,8 +42,8 @@ namespace sat {
         m_checkpoint_enabled(true),
         m_config(p),
         m_par(nullptr),
-        m_cls_allocator_idx(false),
         m_drat(*this),
+        m_cls_allocator_idx(false),
         m_cleaner(*this),
         m_simplifier(*this, p),
         m_scc(*this, p),
diff --git a/src/util/lp/int_solver.cpp b/src/util/lp/int_solver.cpp
index 0967c6cc6..6af668506 100644
--- a/src/util/lp/int_solver.cpp
+++ b/src/util/lp/int_solver.cpp
@@ -282,6 +282,7 @@ void int_solver::find_feasible_solution() {
 lia_move int_solver::run_gcd_test() {
     if (settings().m_int_run_gcd_test) {
         settings().st().m_gcd_calls++;
+        TRACE("int_solver", tout << "gcd-test " << settings().st().m_gcd_calls << "\n";);
         if (!gcd_test()) {
             settings().st().m_gcd_conflicts++;
             return lia_move::conflict;
@@ -291,6 +292,7 @@ lia_move int_solver::run_gcd_test() {
 }
 
 lia_move int_solver::gomory_cut() {
+    TRACE("int_solver", tout << "gomory " << m_number_of_calls << "\n";);
     if ((m_number_of_calls) % settings().m_int_gomory_cut_period != 0)
         return lia_move::undef;
 
@@ -1052,7 +1054,7 @@ lia_move int_solver::create_branch_on_column(int j) {
         m_k = m_upper? floor(get_value(j)) : ceil(get_value(j));        
     }
 
-    TRACE("arith_int", tout << "branching v" << j << " = " << get_value(j) << "\n";
+    TRACE("int_solver", tout << "branching v" << j << " = " << get_value(j) << "\n";
           display_column(tout, j);
           tout << "k = " << m_k << std::endl;
           );