mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-22 05:43:39 +00:00
Code Activity

unused variables

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-10-13 10:58:42 -07:00
parent 5b6472f022
commit f79cd8f0bc
1 changed files with 2 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/muz/spacer/spacer_qe_project.cpp
View file

@ -66,7 +66,6 @@ class peq {
app_ref m_peq; // partial equality application app_ref m_peq; // partial equality application
app_ref m_eq; // equivalent std equality using def. of partial eq app_ref m_eq; // equivalent std equality using def. of partial eq
array_util m_arr_u; array_util m_arr_u;
ast_eq_proc m_eq_proc; // for checking if two asts are equal
public: public:
static const char* PARTIAL_EQ; static const char* PARTIAL_EQ;
@ -102,7 +101,7 @@ peq::peq (app* p, ast_manager& m):
VERIFY (is_partial_eq (p)); VERIFY (is_partial_eq (p));
SASSERT (m_arr_u.is_array (m_lhs) && SASSERT (m_arr_u.is_array (m_lhs) &&
m_arr_u.is_array (m_rhs) && m_arr_u.is_array (m_rhs) &&
m_eq_proc (m.get_sort (m_lhs), m.get_sort (m_rhs))); ast_eq_proc() (m.get_sort (m_lhs), m.get_sort (m_rhs)));
for (unsigned i = 2; i < p->get_num_args (); i++) { for (unsigned i = 2; i < p->get_num_args (); i++) {
m_diff_indices.push_back (p->get_arg (i)); m_diff_indices.push_back (p->get_arg (i));
} }
@ -121,7 +120,7 @@ peq::peq (expr* lhs, expr* rhs, unsigned num_indices, expr * const * diff_indice
{ {
SASSERT (m_arr_u.is_array (lhs) && SASSERT (m_arr_u.is_array (lhs) &&
m_arr_u.is_array (rhs) && m_arr_u.is_array (rhs) &&
m_eq_proc (m.get_sort (lhs), m.get_sort (rhs))); ast_eq_proc() (m.get_sort (lhs), m.get_sort (rhs)));
ptr_vector<sort> sorts; ptr_vector<sort> sorts;
sorts.push_back (m.get_sort (m_lhs)); sorts.push_back (m.get_sort (m_lhs));
sorts.push_back (m.get_sort (m_rhs)); sorts.push_back (m.get_sort (m_rhs));