From 002546d83f5dbe721f1ef5a51cb14f164a72b83d Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Sun, 12 Jul 2026 23:50:14 +0000
Subject: [PATCH] Add sanity assertions in QE regression test setup

---
 src/test/quant_solve.cpp | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/test/quant_solve.cpp b/src/test/quant_solve.cpp
index 9f5dc90696..59e35d927e 100644
--- a/src/test/quant_solve.cpp
+++ b/src/test/quant_solve.cpp
@@ -175,9 +175,11 @@ static void test_qe_regression_4175() {
     arith_util a(m);
 
     expr_ref fml = parse_fml(m, "(forall ((b Real)) (= (= r1 b) (= b 0)))");
+    VERIFY(fml);
     expr_ref result(m);
     qe::expr_quant_elim qe(m, params);
     qe(m.mk_true(), fml, result);
+    VERIFY(result);
 
     expr_ref r1(m.mk_const(symbol("r1"), a.mk_real()), m);
     expr_ref zero(a.mk_numeral(rational(0), false), m);