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

fix(library/blast/strategy): initialization

Browse source 
A strategy is supposed to solve the current branch.
This commit is contained in:
Leonardo de Moura 2015-11-18 10:20:02 -08:00
parent e580e6cdb1
commit 59e676e4fa
2 changed files with 6 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/library/blast/state.h
View file

@ -356,6 +356,11 @@ public:
return m_proof_depth;
}
void clear_proof_steps() {
m_proof_steps = list<proof_step>();
m_proof_depth = 0;
}
/************************
Assignment management
*************************/

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

@ -114,6 +114,7 @@ optional<expr> strategy::invoke_preprocess() {
optional<expr> strategy::search() {
scope_choice_points scope1;
curr_state().clear_proof_steps();
m_init_num_choices = get_num_choice_points();
curr_state().set_simp_rule_sets(get_simp_rule_sets(env()));
if (auto pr = invoke_preprocess())