mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-16 07:05:35 +00:00
Code Activity

Fix elim_unconstrained model trail substitution for sat.smt UFBV models

Browse source 
Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/099b4307-a085-4e7d-a5ae-3d9ab23c5588

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-05-13 02:01:48 +00:00 • committed by GitHub
parent 0bd911c70d
commit cfb62479d1
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 25 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/ast/simplifiers/elim_unconstrained.cpp
View file

@ -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;
}
}

22
src/test/simplifier.cpp
View file

@ -6,6 +6,7 @@ Copyright (c) 2015 Microsoft Corporation
#include "api/z3.h"
#include "api/z3_private.h"
#include <cstring>
#include <iostream>
#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();
}