From f5565d1d92fec9e09dde3685fa4cffb774d2d390 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Sat, 10 Oct 2020 12:35:07 +0200
Subject: [PATCH] fix: mark a few more things as persistent

---
 src/kernel/declaration.cpp | 2 ++
 src/kernel/local_ctx.cpp   | 1 +
 2 files changed, 3 insertions(+)

diff --git a/src/kernel/declaration.cpp b/src/kernel/declaration.cpp
index ae65a3ac02..e01ecb450c 100644
--- a/src/kernel/declaration.cpp
+++ b/src/kernel/declaration.cpp
@@ -312,7 +312,9 @@ bool constant_info::is_unsafe() const {
 
 void initialize_declaration() {
     g_opaque = new reducibility_hints(reducibility_hints::mk_opaque());
+    mark_persistent(g_opaque->raw());
     g_dummy  = new declaration(mk_axiom(name(), names(), expr()));
+    mark_persistent(g_dummy->raw());
 }
 
 void finalize_declaration() {
diff --git a/src/kernel/local_ctx.cpp b/src/kernel/local_ctx.cpp
index 1de07eeb11..10c651c7d6 100644
--- a/src/kernel/local_ctx.cpp
+++ b/src/kernel/local_ctx.cpp
@@ -130,6 +130,7 @@ void initialize_local_ctx() {
     g_dummy_decl   = new local_decl(std::numeric_limits<unsigned>::max(),
                                     name("__local_decl_for_default_constructor"), name("__local_decl_for_default_constructor"),
                                     mk_Prop(), mk_binder_info());
+    mark_persistent(g_dummy_decl->raw());
 }
 
 void finalize_local_ctx() {