mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity

Enable proof mode in add_cover

Browse source
This commit is contained in:
Arie Gurfinkel 2018-09-04 15:29:14 -04:00
parent 7bff74dec0
commit 5d2f682f7a
1 changed files with 2 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/muz/spacer/spacer_context.cpp
View file

@ -2489,6 +2489,8 @@ expr_ref context::get_cover_delta(int level, func_decl* p_orig, func_decl* p)
void context::add_cover(int level, func_decl* p, expr* property, bool bg)
{
scoped_proof _pf_(m);
pred_transformer* pt = nullptr;
if (!m_rels.find(p, pt)) {
pt = alloc(pred_transformer, *this, get_manager(), p);