mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-14 09:09:58 +00:00
Code Activity

Address PR review: add ENSURE checks, fix duplicate test, fix comment

Browse source 
- Add ENSURE(result == Z3_L_TRUE) for each BNH optimization call and
  ENSURE(num_sat == 7) at the end so CI catches regressions.
- Remove test_bnh_optimize() from tst_api() to avoid duplicate
  execution under /a; keep standalone tst_bnh_opt() entry point.
- Fix Test 2 comment: it tests same-size backup, not backup-longer.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
Lev Nachmanson 2026-03-10 16:58:24 -10:00
parent 6d890fb026
commit 274d64299e
2 changed files with 5 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/test/api.cpp
View file

@ -218,6 +218,7 @@ void test_bnh_optimize() {
Z3_optimize_minimize(ctx, opt, f1);
Z3_lbool result = Z3_optimize_check(ctx, opt, 0, nullptr);
std::cout << "BNH min f1: " << result_str(result) << std::endl;
ENSURE(result == Z3_L_TRUE);
if (result == Z3_L_TRUE) {
Z3_model m = Z3_optimize_get_model(ctx, opt);
Z3_model_inc_ref(ctx, m);
@ -235,6 +236,7 @@ void test_bnh_optimize() {
Z3_optimize_minimize(ctx, opt, f2);
Z3_lbool result = Z3_optimize_check(ctx, opt, 0, nullptr);
std::cout << "BNH min f2: " << result_str(result) << std::endl;
ENSURE(result == Z3_L_TRUE);
if (result == Z3_L_TRUE) {
Z3_model m = Z3_optimize_get_model(ctx, opt);
Z3_model_inc_ref(ctx, m);
@ -255,6 +257,7 @@ void test_bnh_optimize() {
Z3_lbool result = Z3_optimize_check(ctx, opt, 0, nullptr);
std::cout << "BNH weighted (w1=" << w[0] << "/5, w2=" << w[1] << "/5): "
<< result_str(result) << std::endl;
ENSURE(result == Z3_L_TRUE);
if (result == Z3_L_TRUE) {
Z3_model m = Z3_optimize_get_model(ctx, opt);
Z3_model_inc_ref(ctx, m);
@ -270,6 +273,7 @@ void test_bnh_optimize() {
}
std::cout << "BNH: " << num_sat << "/7 optimizations returned sat" << std::endl;
ENSURE(num_sat == 7);
Z3_del_context(ctx);
std::cout << "BNH optimization test done" << std::endl;
}
@ -279,7 +283,6 @@ void tst_api() {
test_bvneg();
test_mk_distinct();
test_optimize_translate();
test_bnh_optimize();
}
void tst_bnh_opt() {

2
src/test/lp/lp.cpp
View file

@ -1806,7 +1806,7 @@ void test_restore_x() {
std::cout << " test 1 (backup shorter): " << lp_status_to_string(status) << " - PASSED" << std::endl;
}
// Test 2: backup longer than current (columns removed after backup, or pop)
// Test 2: same-size backup (restore_x copies all elements directly)
{
lar_solver solver;
lpvar x = solver.add_var(0, false);