mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-14 19:15:41 +00:00
Code Activity

Refine QE regression test assertions per review feedback

Browse source
This commit is contained in:
copilot-swe-agent[bot] 2026-07-12 23:49:50 +00:00 • committed by GitHub
parent bcee5ef4d4
commit 1f71d530f7
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 0 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/test/quant_solve.cpp
View file

@ -182,16 +182,6 @@ static void test_qe_regression_4175() {
expr_ref r1(m.mk_const(symbol("r1"), a.mk_real()), m);
expr_ref zero(a.mk_numeral(rational(0), false), m);
{
smt::kernel solver(m, params);
solver.assert_expr(fml);
VERIFY(l_true == solver.check());
}
{
smt::kernel solver(m, params);
solver.assert_expr(result);
VERIFY(l_true == solver.check());
}
{
smt::kernel solver(m, params);
solver.assert_expr(result);
@ -301,4 +291,3 @@ void tst_quant_solve() {
exit(0);
#endif
}