mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 03:45:51 +00:00
Code Activity

throw from push #4425

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-06-04 01:05:23 -07:00
parent b013df9a9f
commit 9f8887cc2e
1 changed files with 4 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/smt/smt_context.cpp
View file

@ -2845,12 +2845,13 @@ namespace smt {
}
}
void context::push() {
TRACE("unit_subsumption_bug", display(tout << "context::push()\n"););
void context::push() {
pop_to_base_lvl();
setup_context(false);
bool was_consistent = !inconsistent();
internalize_assertions(); // internalize assertions before invoking m_asserted_formulas.push_scope
if (!m.inc())
throw default_exception("push canceled");
scoped_suspend_rlimit _suspend_cancel(m.limit());
propagate();
if (was_consistent && inconsistent() && !m_asserted_formulas.inconsistent()) {
@ -3084,6 +3085,7 @@ namespace smt {
TRACE("internalize_assertions", tout << "internalize_assertions()...\n";);
timeit tt(get_verbosity_level() >= 100, "smt.preprocessing");
reduce_assertions();
if (get_cancel_flag()) return;
if (!m_asserted_formulas.inconsistent()) {
unsigned sz = m_asserted_formulas.get_num_formulas();
unsigned qhead = m_asserted_formulas.get_qhead();