From 1f71d530f7c5555d84ffe14896f2317509f3d2b3 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Sun, 12 Jul 2026 23:49:50 +0000 Subject: [PATCH] Refine QE regression test assertions per review feedback --- src/test/quant_solve.cpp | 11 ----------- 1 file changed, 11 deletions(-) diff --git a/src/test/quant_solve.cpp b/src/test/quant_solve.cpp index 8bf0818a30..9f5dc90696 100644 --- a/src/test/quant_solve.cpp +++ b/src/test/quant_solve.cpp @@ -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 } -