From 601ba2a3616aecabeafcf93dd8b5556372d0f927 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 29 Oct 2020 12:10:00 -0700 Subject: [PATCH] #4765 Signed-off-by: Nikolaj Bjorner --- src/smt/smt_context_pp.cpp | 6 ++++-- src/smt/theory_arith_nl.h | 2 +- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp index 492346c90..3196fa417 100644 --- a/src/smt/smt_context_pp.cpp +++ b/src/smt/smt_context_pp.cpp @@ -432,7 +432,8 @@ namespace smt { unsigned context::display_lemma_as_smt_problem(unsigned num_antecedents, literal const * antecedents, literal consequent, symbol const& logic) const { std::stringstream strm; - strm << "lemma_" << (++m_lemma_id) << ".smt2"; + std::thread::id this_id = std::this_thread::get_id(); + strm << "lemma_" << this_id << "." << (++m_lemma_id) << ".smt2"; std::ofstream out(strm.str()); TRACE("lemma", tout << strm.str() << "\n";); display_lemma_as_smt_problem(out, num_antecedents, antecedents, consequent, logic); @@ -474,7 +475,8 @@ namespace smt { unsigned num_eq_antecedents, enode_pair const * eq_antecedents, literal consequent, symbol const& logic) const { std::stringstream strm; - strm << "lemma_" << (++m_lemma_id) << ".smt2"; + std::thread::id this_id = std::this_thread::get_id(); + strm << "lemma_" << this_id << "." << (++m_lemma_id) << ".smt2"; std::ofstream out(strm.str()); TRACE("lemma", tout << strm.str() << "\n"; display_lemma_as_smt_problem(tout, num_antecedents, antecedents, num_eq_antecedents, eq_antecedents, consequent, logic); diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h index 1d9584b2f..88e311f47 100644 --- a/src/smt/theory_arith_nl.h +++ b/src/smt/theory_arith_nl.h @@ -1136,7 +1136,7 @@ bool theory_arith::get_polynomial_info(buffer const & p, sbuffe if (m_util.is_numeral(m)) { continue; } - else if (m_util.is_add(m)) + else if (false && m_util.is_add(m)) // introduced by #4532, disabled for #4765 return false; else if (ctx.e_internalized(m) && !is_pure_monomial(m)) add_occ(m);