mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-01 19:26:53 +00:00
Code Activity

Add model_validate and invalid-check to fpa regression tests

Browse source 
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>
This commit is contained in:
copilot-swe-agent[bot] 2026-02-26 03:21:33 +00:00
parent add65451fd
commit b4f7d057d3
1 changed files with 8 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/test/fpa.cpp
View file

@ -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);
}