From d906a0cc2d27ac16de754150dc377b3237a0251b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 27 Feb 2026 12:02:49 -0800 Subject: [PATCH] fix bug reported by Maria Novoszel Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/finite_set_axioms.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/rewriter/finite_set_axioms.cpp b/src/ast/rewriter/finite_set_axioms.cpp index 025040be0..5392ba742 100644 --- a/src/ast/rewriter/finite_set_axioms.cpp +++ b/src/ast/rewriter/finite_set_axioms.cpp @@ -272,7 +272,7 @@ void finite_set_axioms::in_map_axiom(expr *x, expr *a) { expr_ref f1(u.mk_in(x, a), m); expr_ref f2(u.mk_in(inv, b), m); add_binary("map-inverse", x, a, m.mk_not(f1), f2); - add_binary("map-inverse", x, b, f1, m.mk_not(f2)); + add_binary("map-inverse", x, a, f1, m.mk_not(f2)); } // a := set.map(f, b)