From 62dd0b223af2f3bb27d0aae9d87ae7f7061d0b24 Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Thu, 28 May 2026 05:45:50 +0000 Subject: [PATCH] simplify: align choice axiom naming and inline literal in theory_array_full - Rename 'ax' to 'body' in instantiate_choice_axiom to match the parallel implementation in sat/smt/array_axioms.cpp (assert_choice_axiom), where the same variable is already called 'body' - Inline redundant 'literal l' variable: assert_axiom(mk_literal(q)) - Remove trailing whitespace in array_decl_plugin.h Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/ast/array_decl_plugin.h | 2 +- src/smt/theory_array_full.cpp | 7 +++---- 2 files changed, 4 insertions(+), 5 deletions(-) diff --git a/src/ast/array_decl_plugin.h b/src/ast/array_decl_plugin.h index 4411ed3d2e..092b457d8a 100644 --- a/src/ast/array_decl_plugin.h +++ b/src/ast/array_decl_plugin.h @@ -107,7 +107,7 @@ class array_decl_plugin : public decl_plugin { func_decl * mk_set_subset(unsigned arity, sort * const * domain); func_decl * mk_as_array(func_decl * f); - + func_decl * mk_choice(unsigned arity, sort* const* domain); bool is_array_sort(sort* s) const; diff --git a/src/smt/theory_array_full.cpp b/src/smt/theory_array_full.cpp index 736e447d32..7834dae900 100644 --- a/src/smt/theory_array_full.cpp +++ b/src/smt/theory_array_full.cpp @@ -619,12 +619,11 @@ namespace smt { expr_ref px(mk_select(2, args1), m); expr* args2[2] = { pred, choice_term }; expr_ref pc(mk_select(2, args2), m); - expr_ref ax(m.mk_implies(px, pc), m); + expr_ref body(m.mk_implies(px, pc), m); symbol x_name("x"); - expr_ref q(m.mk_forall(1, &x_sort, &x_name, ax), m); + expr_ref q(m.mk_forall(1, &x_sort, &x_name, body), m); ctx.get_rewriter()(q); - literal l = mk_literal(q); - assert_axiom(l); + assert_axiom(mk_literal(q)); return true; }