mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fix missing conversions

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-11-28 14:12:05 -08:00
parent b5ff4602e9
commit a57628fbcc
2 changed files with 3 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -436,9 +436,9 @@ public:
virtual model_converter_ref get_model_converter() const { virtual model_converter_ref get_model_converter() const {
const_cast<inc_sat_solver*>(this)->convert_internalized(); const_cast<inc_sat_solver*>(this)->convert_internalized();
if (m_cached_mc)
return m_cached_mc;
if (m_internalized && m_internalized_converted) { if (m_internalized && m_internalized_converted) {
if (m_cached_mc)
return m_cached_mc;
m_cached_mc = concat(m_mc0.get(), mk_bit_blaster_model_converter(m, m_bb_rewriter->const2bits())); m_cached_mc = concat(m_mc0.get(), mk_bit_blaster_model_converter(m, m_bb_rewriter->const2bits()));
m_cached_mc = concat(solver::get_model_converter().get(), m_cached_mc.get()); m_cached_mc = concat(solver::get_model_converter().get(), m_cached_mc.get());
m_cached_mc = concat(m_cached_mc.get(), m_sat_mc.get()); m_cached_mc = concat(m_cached_mc.get(), m_sat_mc.get());
@ -452,7 +452,6 @@ public:
void convert_internalized() { void convert_internalized() {
if (!m_internalized || m_internalized_converted) return; if (!m_internalized || m_internalized_converted) return;
sat2goal s2g; sat2goal s2g;
m_sat_mc = nullptr;
m_cached_mc = nullptr; m_cached_mc = nullptr;
goal g(m, false, true, false); goal g(m, false, true, false);
s2g(m_solver, m_map, m_params, g, m_sat_mc); s2g(m_solver, m_map, m_params, g, m_sat_mc);

2
src/sat/tactic/goal2sat.cpp
View file

@ -1183,8 +1183,8 @@ struct sat2goal::imp {
ref<sat_model_converter> _mc; ref<sat_model_converter> _mc;
if (r.models_enabled()) { if (r.models_enabled()) {
_mc = alloc(sat_model_converter, m, s); _mc = alloc(sat_model_converter, m, s);
mc = _mc.get();
} }
mc = _mc.get();
init_lit2expr(s, map, _mc); init_lit2expr(s, map, _mc);
// collect units // collect units
unsigned num_vars = s.num_vars(); unsigned num_vars = s.num_vars();