From b4f7d057d3ff747a280f8bb0be6da0b203d755e4 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Thu, 26 Feb 2026 03:21:33 +0000
Subject: [PATCH] Add model_validate and invalid-check to fpa regression tests

Add (set-option :model_validate true) to each SMT-LIB2 spec in
src/test/fpa.cpp, and add ENSURE checks that the output does not
contain the string "invalid".

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/test/fpa.cpp | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/src/test/fpa.cpp b/src/test/fpa.cpp
index 589f43bdb..355c0a3e0 100644
--- a/src/test/fpa.cpp
+++ b/src/test/fpa.cpp
@@ -21,10 +21,12 @@ static void test_fp_to_real_denormal() {
     ctx = Z3_mk_context(nullptr);
     {
         const char * spec =
+            "(set-option :model_validate true)\n"
             "(assert (> (fp.to_real (fp #b0 #b00 #b00111011011111001011101)) 1.0))\n"
             "(check-sat)\n";
         const char * result = Z3_eval_smtlib2_string(ctx, spec);
         ENSURE(strstr(result, "unsat") != nullptr);
+        ENSURE(strstr(result, "invalid") == nullptr);
     }
     Z3_del_context(ctx);
 
@@ -33,11 +35,13 @@ static void test_fp_to_real_denormal() {
     ctx = Z3_mk_context(nullptr);
     {
         const char * spec =
+            "(set-option :model_validate true)\n"
             "(assert (= (fp.to_real (fp #b0 #b00 #b10000000000000000000000)) (/ 1.0 2.0)))\n"
             "(check-sat)\n";
         const char * result = Z3_eval_smtlib2_string(ctx, spec);
         ENSURE(strstr(result, "sat") != nullptr);
         ENSURE(strstr(result, "unsat") == nullptr);
+        ENSURE(strstr(result, "invalid") == nullptr);
     }
     Z3_del_context(ctx);
 
@@ -46,11 +50,13 @@ static void test_fp_to_real_denormal() {
     ctx = Z3_mk_context(nullptr);
     {
         const char * spec =
+            "(set-option :model_validate true)\n"
             "(assert (= (fp.to_real (fp #b0 #b00 #b00100000000000000000000)) (/ 1.0 8.0)))\n"
             "(check-sat)\n";
         const char * result = Z3_eval_smtlib2_string(ctx, spec);
         ENSURE(strstr(result, "sat") != nullptr);
         ENSURE(strstr(result, "unsat") == nullptr);
+        ENSURE(strstr(result, "invalid") == nullptr);
     }
     Z3_del_context(ctx);
 
@@ -59,11 +65,13 @@ static void test_fp_to_real_denormal() {
     ctx = Z3_mk_context(nullptr);
     {
         const char * spec =
+            "(set-option :model_validate true)\n"
             "(assert (> (fp.to_real (fp #b0 #b01 #b11111111111111111111111)) 1.0))\n"
             "(check-sat)\n";
         const char * result = Z3_eval_smtlib2_string(ctx, spec);
         ENSURE(strstr(result, "sat") != nullptr);
         ENSURE(strstr(result, "unsat") == nullptr);
+        ENSURE(strstr(result, "invalid") == nullptr);
     }
     Z3_del_context(ctx);
 }