mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-11 05:30:51 +00:00
Code Activity

fix warning messages for unused variables

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-03-18 21:37:44 -07:00
parent b8598225bf
commit d1ffeb36b0
5 changed files with 32 additions and 70 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/muz_qe/dl_mk_karr_invariants.cpp
View file

@ -325,7 +325,6 @@ namespace datalog {
TRACE("dl", m_hb.display(tout););
SASSERT(is_sat == l_true);
unsigned basis_size = m_hb.get_basis_size();
bool first_initial = true;
for (unsigned i = 0; i < basis_size; ++i) {
bool is_initial;
vector<rational> soln;
@ -378,7 +377,6 @@ namespace datalog {
}
void mk_karr_invariants::update_body(rule_set& rules, rule& r){
func_decl* p = r.get_decl();
unsigned utsz = r.get_uninterpreted_tail_size();
unsigned tsz = r.get_tail_size();
app_ref_vector tail(m);