From 5d2f682f7a0730e87b631d2b97e102f5b82e9ff2 Mon Sep 17 00:00:00 2001
From: Arie Gurfinkel <arie.gurfinkel@uwaterloo.ca>
Date: Tue, 4 Sep 2018 15:29:14 -0400
Subject: [PATCH] Enable proof mode in add_cover

---
 src/muz/spacer/spacer_context.cpp | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp
index 617266779..dd6656954 100644
--- a/src/muz/spacer/spacer_context.cpp
+++ b/src/muz/spacer/spacer_context.cpp
@@ -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);