fix #2873

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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;

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));
 
 }

src/util/lp/gomory.cpp

@@ -252,23 +252,23 @@ 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);
         dump_explanations(out);
         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;

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());