mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-03 11:25:40 +00:00
Code Activity

Merge branch 'master' of https://github.com/Z3Prover/z3

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-11-17 16:36:44 +00:00
commit ad76e536b2
1 changed files with 14 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/rewriter/rewriter_def.h
View file

@ -596,6 +596,7 @@ template<typename Config>
template<bool ProofGen> template<bool ProofGen>
void rewriter_tpl<Config>::main_loop(expr * t, expr_ref & result, proof_ref & result_pr) { void rewriter_tpl<Config>::main_loop(expr * t, expr_ref & result, proof_ref & result_pr) {
if (m_cancel_check && m().canceled()) { if (m_cancel_check && m().canceled()) {
reset();
throw rewriter_exception(m().limit().get_cancel_msg()); throw rewriter_exception(m().limit().get_cancel_msg());
} }
SASSERT(!ProofGen || result_stack().size() == result_pr_stack().size()); SASSERT(!ProofGen || result_stack().size() == result_pr_stack().size());
@ -630,6 +631,7 @@ void rewriter_tpl<Config>::resume_core(expr_ref & result, proof_ref & result_pr)
SASSERT(!frame_stack().empty()); SASSERT(!frame_stack().empty());
while (!frame_stack().empty()) { while (!frame_stack().empty()) {
if (m_cancel_check && m().canceled()) { if (m_cancel_check && m().canceled()) {
reset();
throw rewriter_exception(m().limit().get_cancel_msg()); throw rewriter_exception(m().limit().get_cancel_msg());
} }
SASSERT(!ProofGen || result_stack().size() == result_pr_stack().size()); SASSERT(!ProofGen || result_stack().size() == result_pr_stack().size());