mirror of
https://github.com/Z3Prover/z3
synced 2025-04-23 17:15:31 +00:00
unused variable warnings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
320d6640b1
commit
b371592c0d
2 changed files with 1 additions and 3 deletions
|
@ -3215,7 +3215,6 @@ bool theory_seq::branch_nqs() {
|
|||
}
|
||||
|
||||
void theory_seq::branch_nq(ne const& n) {
|
||||
context& ctx = get_context();
|
||||
literal eq = mk_eq(n.l(), n.r(), false);
|
||||
literal eq_len = mk_eq(mk_len(n.l()), mk_len(n.r()), false);
|
||||
literal len_gt = mk_literal(m_autil.mk_ge(mk_len(n.l()), m_autil.mk_int(1)));
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue