From 7cb956a0e2370e00e6cc065dffbba01adebac5bb Mon Sep 17 00:00:00 2001
From: Arie Gurfinkel <arie.gurfinkel@uwaterloo.ca>
Date: Tue, 9 Jul 2019 13:29:42 -0400
Subject: [PATCH] Uses non-flattening rewriter in profos

---
 src/ast/proofs/proof_utils.h | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/ast/proofs/proof_utils.h b/src/ast/proofs/proof_utils.h
index e3ad8d06e..c7634250c 100644
--- a/src/ast/proofs/proof_utils.h
+++ b/src/ast/proofs/proof_utils.h
@@ -107,6 +107,7 @@ public:
     {
         ast_manager &m = args.get_manager();
         bool_rewriter brwr(m);
+        brwr.set_flat(false);
 
         if (m.is_or(decl))
         { mk_or_core(args, res); }