mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-11 19:53:34 +00:00
Code Activity

bug fixes

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-12-23 14:41:16 -08:00
parent c199344bbf
commit 8198a8ce7b
3 changed files with 8 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/ast/ast_translation.cpp
View file

@ -196,7 +196,7 @@ ast * ast_translation::process(ast const * _n) {
SASSERT(m_extra_children_stack.empty());
++m_num_process;
if (m_num_process > (1 << 16)) {
if (m_num_process > (1 << 14)) {
reset_cache();
m_num_process = 0;
}

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

@ -915,7 +915,7 @@ void sat2goal::mc::flush_gmc() {
}
model_converter* sat2goal::mc::translate(ast_translation& translator) {
mc* result = alloc(mc, m);
mc* result = alloc(mc, translator.to());
result->m_smc.copy(m_smc);
result->m_gmc = m_gmc ? dynamic_cast<generic_model_converter*>(m_gmc->translate(translator)) : nullptr;
for (app* e : m_var2expr) {
@ -983,6 +983,10 @@ void sat2goal::mc::operator()(expr_ref& fml) {
}
void sat2goal::mc::insert(sat::bool_var v, app * atom, bool aux) {
if (m_var2expr.get(v, nullptr)) {
std::cout << mk_pp(atom, m) << "\n";
std::cout << mk_pp(m_var2expr.get(v, nullptr), m) << "\n";
}
VERIFY(!m_var2expr.get(v, nullptr));
m_var2expr.reserve(v + 1);
m_var2expr.set(v, atom);
@ -1038,7 +1042,7 @@ struct sat2goal::imp {
for (sat::bool_var v = 0; v < num_vars; v++) {
checkpoint();
sat::literal l(v, false);
if (m_lit2expr.get(l.index())) {
if (m_lit2expr.get(l.index()) && !mc->var2expr(v)) {
mc->insert(v, to_app(m_lit2expr.get(l.index())), false);
SASSERT(m_lit2expr.get((~l).index()));
}

2
src/util/resource_limit.h
View file

@ -1,7 +1,7 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
Modulre Name:
resource_limit.h