mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-05 21:53:23 +00:00
Code Activity

guarding bb_rewriter now that it gets reset

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-03-08 16:50:06 -08:00
parent d0de8fff62
commit 335a1dba6e
1 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/sat/sat_solver/inc_sat_solver.cpp
View file

@ -163,14 +163,14 @@ public:
m_fmls_lim.push_back(m_fmls.size()); m_fmls_lim.push_back(m_fmls.size());
m_asms_lim.push_back(m_asmsf.size()); m_asms_lim.push_back(m_asmsf.size());
m_fmls_head_lim.push_back(m_fmls_head); m_fmls_head_lim.push_back(m_fmls_head);
m_bb_rewriter->push(); if (m_bb_rewriter) m_bb_rewriter->push();
m_map.push(); m_map.push();
} }
virtual void pop(unsigned n) { virtual void pop(unsigned n) {
if (n > m_num_scopes) { // allow inc_sat_solver to if (n > m_num_scopes) { // allow inc_sat_solver to
n = m_num_scopes; // take over for another solver. n = m_num_scopes; // take over for another solver.
} }
m_bb_rewriter->pop(n); if (m_bb_rewriter) m_bb_rewriter->pop(n);
m_map.pop(n); m_map.pop(n);
SASSERT(n <= m_num_scopes); SASSERT(n <= m_num_scopes);
m_solver.user_pop(n); m_solver.user_pop(n);
@ -429,7 +429,7 @@ private:
} }
m_model = md; m_model = md;
if (!m_bb_rewriter->const2bits().empty()) { if (m_bb_rewriter.get() && !m_bb_rewriter->const2bits().empty()) {
m_mc0 = concat(m_mc0.get(), mk_bit_blaster_model_converter(m, m_bb_rewriter->const2bits())); m_mc0 = concat(m_mc0.get(), mk_bit_blaster_model_converter(m, m_bb_rewriter->const2bits()));
} }
if (m_mc0) { if (m_mc0) {