mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-20 11:22:04 +00:00
Code Activity

move in assumptions to loop

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-02-01 10:59:48 -08:00
parent 75fb25a06c
commit 7df8d17639
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/smt/smt_context.cpp
View file

@ -3449,14 +3449,15 @@ namespace smt {
if (!check_preamble(reset_cancel)) return l_undef; if (!check_preamble(reset_cancel)) return l_undef;
SASSERT(at_base_level()); SASSERT(at_base_level());
setup_context(false); setup_context(false);
expr_ref_vector asms(m, num_assumptions, assumptions);
if (m_fparams.m_threads > 1) { if (m_fparams.m_threads > 1) {
expr_ref_vector asms(m, num_assumptions, assumptions);
parallel p(*this); parallel p(*this);
return p(asms); return p(asms);
} }
lbool r; lbool r;
do { do {
pop_to_base_lvl(); pop_to_base_lvl();
expr_ref_vector asms(m, num_assumptions, assumptions);
internalize_assertions(); internalize_assertions();
add_theory_assumptions(asms); add_theory_assumptions(asms);
TRACE("unsat_core_bug", tout << asms << "\n";); TRACE("unsat_core_bug", tout << asms << "\n";);