From 05da2508bfecfdf6fdfb5bcac821b19a753df01c Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 22 Jan 2020 11:08:44 -0600
Subject: [PATCH] fix #2873

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/tactic/core/solve_eqs_tactic.cpp | 6 ++++--
 src/tactic/smtlogics/qfbv_tactic.cpp | 1 -
 src/util/lp/gomory.cpp               | 8 ++++----
 src/util/rational.h                  | 2 +-
 4 files changed, 9 insertions(+), 8 deletions(-)

diff --git a/src/tactic/core/solve_eqs_tactic.cpp b/src/tactic/core/solve_eqs_tactic.cpp
index 0978f3aa6f8..d474214c2ea 100644
--- a/src/tactic/core/solve_eqs_tactic.cpp
+++ b/src/tactic/core/solve_eqs_tactic.cpp
@@ -586,7 +586,9 @@ class solve_eqs_tactic : public tactic {
         bool check_eq_compat_rec(expr_mark& occ, svector<lbool>& cache, expr* f, expr* v, expr* eq, bool& all) {
             expr_ref_vector args(m());
             expr* f1 = nullptr;
-            if (!occ.is_marked(f)) {
+            // flattening may introduce fresh negations, 
+            // occ is not defined on these negations
+            if (!m().is_not(f) && !occ.is_marked(f)) {
                 all = false;
                 return true;
             }
@@ -682,7 +684,7 @@ class solve_eqs_tactic : public tactic {
             hoist_rewriter_star rw(m());
             th_rewriter thrw(m());
             expr_ref tmp(m()), tmp2(m());
-            TRACE("solve_eqs", g.display(tout););
+            // TRACE("solve_eqs", g.display(tout););
             for (unsigned idx = 0; idx < size; idx++) {
                 checkpoint();
                 if (g.is_decided_unsat()) break;
diff --git a/src/tactic/smtlogics/qfbv_tactic.cpp b/src/tactic/smtlogics/qfbv_tactic.cpp
index cd1cb7dec48..bef94427dde 100644
--- a/src/tactic/smtlogics/qfbv_tactic.cpp
+++ b/src/tactic/smtlogics/qfbv_tactic.cpp
@@ -124,7 +124,6 @@ tactic * mk_qfbv_tactic(ast_manager & m, params_ref const & p) {
     tactic * new_sat = cond(mk_produce_proofs_probe(),
                             and_then(mk_simplify_tactic(m), mk_smt_tactic(m)),
                             mk_psat_tactic(m, p));
-
     return mk_qfbv_tactic(m, p, new_sat, mk_smt_tactic(m, p));
 
 }
diff --git a/src/util/lp/gomory.cpp b/src/util/lp/gomory.cpp
index a86e5e50f85..ffcbd14c868 100644
--- a/src/util/lp/gomory.cpp
+++ b/src/util/lp/gomory.cpp
@@ -252,7 +252,6 @@ class gomory::imp {
         dump_term_le_k(out << "(assert (not ") << "))\n";
     }
 
-
     void dump_cut_and_constraints_as_smt_lemma(std::ostream& out) const {
         dump_declarations(out);
         dump_the_row(out);
@@ -260,15 +259,16 @@ class gomory::imp {
         dump_the_cut_assert(out);
         out << "(check-sat)\n";
     }
+
 public:
+
     lia_move create_cut() {
         TRACE("gomory_cut",
-              tout << "applying cut at:\n"; print_linear_combination_of_column_indices_only(m_row, tout); tout << std::endl;
+              print_linear_combination_of_column_indices_only(m_row, tout << "applying cut at:\n"); tout << std::endl;
               for (auto & p : m_row) {
                   m_int_solver.m_lar_solver->m_mpq_lar_core_solver.m_r_solver.print_column_info(p.var(), tout);
               }
-              tout << "inf_col = " << m_inf_col << std::endl;
-              );
+              tout << "inf_col = " << m_inf_col << std::endl;);
         
         // gomory will be   t <= k and the current solution has a property t > k
         m_k = 1;
diff --git a/src/util/rational.h b/src/util/rational.h
index a158639badf..751d395db75 100644
--- a/src/util/rational.h
+++ b/src/util/rational.h
@@ -107,7 +107,7 @@ class rational {
 
     int64_t get_int64() const { return m().get_int64(m_val); }
     
-    bool is_unsigned() const { return is_uint64() && (get_uint64() < (1ull << 32)); }
+    bool is_unsigned() const { return is_uint64() && (get_uint64() < (1ull << 32ull)); }
 
     unsigned get_unsigned() const {
         SASSERT(is_unsigned());