mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

fix location of research

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-10-18 18:15:35 -07:00
parent 2d4a5e0a5e
commit 936312cfd2
1 changed files with 16 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

30
src/smt/smt_context.cpp
View file

@ -3423,15 +3423,16 @@ namespace smt {
if (!check_preamble(reset_cancel)) return l_undef;
SASSERT(at_base_level());
setup_context(false);
expr_ref_vector asms(m_manager, num_assumptions, assumptions);
add_theory_assumptions(asms);
// introducing proxies: if (!validate_assumptions(asms)) return l_undef;
TRACE("unsat_core_bug", tout << asms << "\n";);
internalize_assertions();
init_assumptions(asms);
TRACE("before_search", display(tout););
lbool r;
do {
pop_to_base_lvl();
expr_ref_vector asms(m_manager, num_assumptions, assumptions);
add_theory_assumptions(asms);
// introducing proxies: if (!validate_assumptions(asms)) return l_undef;
TRACE("unsat_core_bug", tout << asms << "\n";);
internalize_assertions();
init_assumptions(asms);
TRACE("before_search", display(tout););
r = search();
r = mk_unsat_core(r);
}
@ -3444,15 +3445,16 @@ namespace smt {
if (!check_preamble(true)) return l_undef;
TRACE("before_search", display(tout););
setup_context(false);
expr_ref_vector asms(cube);
add_theory_assumptions(asms);
// introducing proxies: if (!validate_assumptions(asms)) return l_undef;
for (auto const& clause : clauses) if (!validate_assumptions(clause)) return l_undef;
internalize_assertions();
init_assumptions(asms);
for (auto const& clause : clauses) init_clause(clause);
lbool r;
do {
pop_to_base_lvl();
expr_ref_vector asms(cube);
add_theory_assumptions(asms);
// introducing proxies: if (!validate_assumptions(asms)) return l_undef;
for (auto const& clause : clauses) if (!validate_assumptions(clause)) return l_undef;
internalize_assertions();
init_assumptions(asms);
for (auto const& clause : clauses) init_clause(clause);
r = search();
r = mk_unsat_core(r);
}