mirror of
https://github.com/Z3Prover/z3
synced 2025-04-12 12:08:18 +00:00
deal with warning for unused parameter
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
10c5ed6344
commit
92166eb5cb
|
@ -1274,7 +1274,7 @@ namespace pdr {
|
||||||
m_pm(m_fparams, params.max_num_contexts(), m),
|
m_pm(m_fparams, params.max_num_contexts(), m),
|
||||||
m_query_pred(m),
|
m_query_pred(m),
|
||||||
m_query(0),
|
m_query(0),
|
||||||
m_search(m_params.bfs_model_search(), m),
|
m_search(m_params.bfs_model_search()),
|
||||||
m_last_result(l_undef),
|
m_last_result(l_undef),
|
||||||
m_inductive_lvl(0),
|
m_inductive_lvl(0),
|
||||||
m_expanded_lvl(0),
|
m_expanded_lvl(0),
|
||||||
|
|
|
@ -245,7 +245,6 @@ namespace pdr {
|
||||||
|
|
||||||
class model_search {
|
class model_search {
|
||||||
typedef ptr_vector<model_node> model_nodes;
|
typedef ptr_vector<model_node> model_nodes;
|
||||||
ast_manager& m;
|
|
||||||
bool m_bfs;
|
bool m_bfs;
|
||||||
model_node* m_root;
|
model_node* m_root;
|
||||||
std::deque<model_node*> m_leaves;
|
std::deque<model_node*> m_leaves;
|
||||||
|
@ -258,7 +257,7 @@ namespace pdr {
|
||||||
void enqueue_leaf(model_node& n); // add leaf to priority queue.
|
void enqueue_leaf(model_node& n); // add leaf to priority queue.
|
||||||
void update_models();
|
void update_models();
|
||||||
public:
|
public:
|
||||||
model_search(bool bfs, ast_manager& m): m(m), m_bfs(bfs), m_root(0) {}
|
model_search(bool bfs): m_bfs(bfs), m_root(0) {}
|
||||||
~model_search();
|
~model_search();
|
||||||
|
|
||||||
void reset();
|
void reset();
|
||||||
|
|
Loading…
Reference in a new issue