michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(library/blast/blast): make sure blast uses the given ios options for tracing

Browse source 
They might have been updated using the with_options tactic
This commit is contained in:
Leonardo de Moura 2015-12-09 07:21:18 -08:00
parent a3346e997b
commit 36f3549c44
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/library/blast/blast.cpp
View file

@ -1143,6 +1143,7 @@ optional<expr> blast_goal(environment const & env, io_state const & ios, list<na
blast::scope_blastenv scope2(b); blast::scope_blastenv scope2(b);
blast::scope_congruence_closure scope3; blast::scope_congruence_closure scope3;
blast::scope_config scope4(ios.get_options()); blast::scope_config scope4(ios.get_options());
scope_trace_env scope5(env, ios);
return b(g); return b(g);
} }
void initialize_blast() { void initialize_blast() {