From 36f3549c44b0c757fb765c1c565b39752856966c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 9 Dec 2015 07:21:18 -0800
Subject: [PATCH] fix(library/blast/blast): make sure blast uses the given ios
 options for tracing

They might have been updated using the with_options tactic
---
 src/library/blast/blast.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/library/blast/blast.cpp b/src/library/blast/blast.cpp
index ff788df06..da66348d2 100644
--- a/src/library/blast/blast.cpp
+++ b/src/library/blast/blast.cpp
@@ -1143,6 +1143,7 @@ optional<expr> blast_goal(environment const & env, io_state const & ios, list<na
     blast::scope_blastenv           scope2(b);
     blast::scope_congruence_closure scope3;
     blast::scope_config             scope4(ios.get_options());
+    scope_trace_env                 scope5(env, ios);
     return b(g);
 }
 void initialize_blast() {