From 2ac2badd582c33fcbd2f82b201a21f04fef1a399 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 13 Sep 2016 08:46:20 -0700
Subject: [PATCH] fix(library/compiler/preprocess): do not unfold proofs

---
 src/library/compiler/preprocess.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/library/compiler/preprocess.cpp b/src/library/compiler/preprocess.cpp
index 4ff379d2c9..dfdd300a90 100644
--- a/src/library/compiler/preprocess.cpp
+++ b/src/library/compiler/preprocess.cpp
@@ -91,7 +91,7 @@ class expand_aux_fn : public compiler_step_visitor {
     virtual expr visit_app(expr const & e) override {
         switch (get_recursor_app_kind(e)) {
         case recursor_kind::NotRecursor: {
-            if (is_not_vm_function(e)) {
+            if (is_not_vm_function(e) && !ctx().is_proof(e)) {
                 if (auto r = unfold_term(env(), e)) {
                     return visit(*r);
                 }