From bd9326134c0bc6abe78d8ea272e6f0bd48f64b9e Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Thu, 14 May 2026 04:19:37 -0400 Subject: [PATCH] Fix `sat.smt=true` model reconstruction for QF_UFBV with Bool-valued UF predicates (#9519) `sat.smt=true` could return `sat` with an invalid model for QF_UFBV formulas combining Bool-valued UFs and BV range constraints. The failure came from broken model-trail reconstruction in `elim_unconstrained`, where `ADD` entries were effectively turned into identity substitutions. - **Root-cause fix: restore model-trail substitution composition** - In `elim_unconstrained::update_model_trail`, `generic_model_converter::ADD` entries now use `entry.m_def` (rewritten through accumulated substitutions) instead of creating self-referential const-to-const mappings. - This re-enables correct back-substitution for eliminated unconstrained terms during witness reconstruction. - **Regression coverage: QF_UFBV + `sat.smt=true` + model validation** - Added a focused unit test in `src/test/simplifier.cpp` for: - Bool-valued UF predicate over BV vars - split BV range constraints (`bvuge` / `bvult`) - `:sat.smt true` and `:model_validate true` - The test asserts the solver returns `sat` without emitting an invalid-model error. ```cpp // before (effectively no-op back-mapping) new_def = m.mk_const(entry.m_f); sub->insert(new_def, new_def, nullptr, nullptr); // after (compose and apply recorded definition) new_def = entry.m_def; (*rp)(new_def); sub->insert(m.mk_const(entry.m_f), new_def, nullptr, nullptr); ``` --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/ast/simplifiers/elim_unconstrained.cpp | 7 +++---- src/test/simplifier.cpp | 22 ++++++++++++++++++++++ 2 files changed, 25 insertions(+), 4 deletions(-) diff --git a/src/ast/simplifiers/elim_unconstrained.cpp b/src/ast/simplifiers/elim_unconstrained.cpp index cb52a9c85..6b53882cd 100644 --- a/src/ast/simplifiers/elim_unconstrained.cpp +++ b/src/ast/simplifiers/elim_unconstrained.cpp @@ -413,10 +413,9 @@ void elim_unconstrained::update_model_trail(generic_model_converter& mc, vector< case generic_model_converter::instruction::HIDE: break; case generic_model_converter::instruction::ADD: - // new_def = entry.m_def; - // (*rp)(new_def); - new_def = m.mk_const(entry.m_f); - sub->insert(new_def, new_def, nullptr, nullptr); + new_def = entry.m_def; + (*rp)(new_def); + sub->insert(m.mk_const(entry.m_f), new_def, nullptr, nullptr); break; } } diff --git a/src/test/simplifier.cpp b/src/test/simplifier.cpp index a4da49861..3b2abf7b2 100644 --- a/src/test/simplifier.cpp +++ b/src/test/simplifier.cpp @@ -6,6 +6,7 @@ Copyright (c) 2015 Microsoft Corporation #include "api/z3.h" #include "api/z3_private.h" +#include #include #include "util/util.h" #include "util/trace.h" @@ -211,6 +212,26 @@ static void test_array() { Z3_del_context(ctx); } +static void test_sat_smt_ufbv_predicate_model_validation() { + Z3_context ctx = Z3_mk_context(nullptr); + const char* result = + Z3_eval_smtlib2_string(ctx, + "(set-logic QF_UFBV)\n" + "(set-option :sat.smt true)\n" + "(set-option :model_validate true)\n" + "(declare-fun p ((_ BitVec 4)) Bool)\n" + "(declare-const x (_ BitVec 4))\n" + "(declare-const y (_ BitVec 4))\n" + "(assert (xor (p x) (p y)))\n" + "(assert (bvuge x (_ bv1 4)))\n" + "(assert (bvult y (_ bv1 4)))\n" + "(check-sat)\n" + "(get-model)\n"); + ENSURE(std::strstr(result, "sat") != nullptr); + ENSURE(std::strstr(result, "invalid model") == nullptr); + Z3_del_context(ctx); +} + void tst_simplifier() { test_array(); @@ -218,4 +239,5 @@ void tst_simplifier() { test_datatypes(); test_bool(); test_skolemize_bug(); + test_sat_smt_ufbv_predicate_model_validation(); }