mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-16 22:01:44 +00:00
Code Activity

Improve test validation for mk_transitivity

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-02-16 01:52:20 +00:00
parent e627e60fe7
commit f3c4c57c58
1 changed files with 12 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/test/proof_checker.cpp
View file

@ -53,17 +53,23 @@ void tst_initializer_list_overloads() {
VERIFY(m.get_fact(p4.get()) == b.get());
// Test mk_transitivity with initializer_list
expr_ref c(m), eq_ab(m), eq_bc(m);
// Create a simple transitivity chain: a = b, b = c => a = c
expr_ref c(m);
c = m.mk_const(symbol("c"), m.mk_bool_sort());
eq_ab = m.mk_eq(a.get(), b.get());
eq_bc = m.mk_eq(b.get(), c.get());
proof_ref pr1(m.mk_reflexivity(eq_ab.get()), m);
proof_ref pr2(m.mk_reflexivity(eq_bc.get()), m);
// Create rewrite proofs for a = b and b = c
proof_ref pr_ab(m.mk_rewrite(a.get(), b.get()), m);
proof_ref pr_bc(m.mk_rewrite(b.get(), c.get()), m);
// Test the new initializer_list overload for transitivity
proof_ref p5(m.mk_transitivity({ pr1.get(), pr2.get() }), m);
// This should create a proof of a = c
proof_ref p5(m.mk_transitivity({ pr_ab.get(), pr_bc.get() }), m);
VERIFY(p5.get() != nullptr);
// Verify the result is a proof with the expected fact (a = c)
expr* trans_fact = m.get_fact(p5.get());
VERIFY(m.is_eq(trans_fact));
VERIFY(to_app(trans_fact)->get_arg(0) == a.get());
VERIFY(to_app(trans_fact)->get_arg(1) == c.get());
std::cout << "Initializer list overloads test passed!" << std::endl;
}