mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-01 11:16:54 +00:00
Code Activity

fix build warnings

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-11-26 09:43:52 -08:00
parent 8298302358
commit 233184944c
6 changed files with 4 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/ast/euf/euf_arith_plugin.cpp
View file

@ -59,7 +59,6 @@ namespace euf {
expr* e = n->get_expr(), * x, * y;
// x - y = x + (* -1 y)
if (a.is_sub(e, x, y)) {
auto& m = g.get_manager();
auto e1 = a.mk_numeral(rational(-1), a.is_int(x));
auto n1 = g.find(e1) ? g.find(e1) : g.mk(e1, 0, 0, nullptr);
auto e2 = a.mk_mul(e1, y);

3
src/ast/euf/ho_matcher.cpp
View file

@ -293,8 +293,7 @@ namespace euf {
// v - offset |-> t
if (is_meta_var(p, wi.pat_offset()) && is_closed(t, 0, wi.term_offset())) {
auto v = to_var(p);
auto idx = v->get_idx() - wi.pat_offset();
SASSERT(!m_subst.get(idx)); // reduce ensures meta variables are not in substitutions
SASSERT(!m_subst.get(v->get_idx() - wi.pat_offset())); // reduce ensures meta variables are not in substitutions
add_binding(v, wi.pat_offset(), t);
wi.set_done();
return true;