3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00

Fix unused variable warnings. (#5760)

This commit fixes a few cases of unused variables in release builds.
The commit uses the (void)xxx; syntax which is used in other parts of
the code.
This commit is contained in:
Nadav Rotem 2022-01-08 18:18:30 -08:00 committed by GitHub
parent 174889ad5e
commit 9f9543ef69
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
3 changed files with 5 additions and 1 deletions

View file

@ -1081,6 +1081,7 @@ namespace seq {
sort* domain[4] = { srt, srt, srt, srt };
auto d = plugin.ensure_def(symbol("ra"), 4, domain, m.mk_bool_sort(), true);
func_decl* ra = d.get_def()->get_decl();
(void)ra;
sort* isrt = a.mk_int();
var_ref vi(m.mk_var(5, isrt), m);
var_ref vj(m.mk_var(4, isrt), m);
@ -1089,6 +1090,7 @@ namespace seq {
var_ref vt(m.mk_var(1, srt), m);
var_ref vr(m.mk_var(0, srt), m);
var* vars[6] = { vi, vj, vs, vp, vt, vr };
(void)vars;
expr_ref len_s(seq.str.mk_length(vs), m);
expr_ref len_r(seq.str.mk_length(vr), m);
expr_ref test1(m.mk_eq(len_s, vi), m);

View file

@ -268,6 +268,7 @@ namespace qe {
ap.set_check_purified(false);
vector<mbp::def> defs;
bool ok = ap.project(*mdl.get(), avars, lits, defs);
(void)ok;
CTRACE("qe", !ok, tout << "projection failure ignored!!!!\n");
return defs;
}

View file

@ -77,7 +77,8 @@ namespace array {
bool solver::post_visit(expr* e, bool sign, bool root) {
euf::enode* n = expr2enode(e);
app* a = to_app(e);
app *a = to_app(e);
(void)a;
SASSERT(!n || !n->is_attached_to(get_id()));
if (!n)
n = mk_enode(e, false);