mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

Merge branch 'opt' of https://github.com/nikolajbjorner/z3 into opt

Browse source
This commit is contained in:
Nikolaj Bjorner 2018-01-19 21:36:24 -08:00
commit 7fc1b75cb8
38 changed files with 143 additions and 123 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -899,7 +899,7 @@ void sat2goal::mc::flush_gmc() {
sat::literal_vector updates;
m_smc.expand(updates);
m_smc.reset();
if (!m_gmc) m_gmc = alloc(generic_model_converter, m);
if (!m_gmc) m_gmc = alloc(generic_model_converter, m, "sat2goal");
// now gmc owns the model converter
sat::literal_vector clause;
expr_ref_vector tail(m);
@ -1017,7 +1017,7 @@ void sat2goal::mc::insert(sat::bool_var v, app * atom, bool aux) {
if (aux) {
SASSERT(is_uninterp_const(atom));
SASSERT(m.is_bool(atom));
if (!m_gmc) m_gmc = alloc(generic_model_converter, m);
if (!m_gmc) m_gmc = alloc(generic_model_converter, m, "sat2goal");
m_gmc->hide(atom->get_decl());
}
}