From 1d83ecb9de1d31b148c34b29bcd904d2b57eed94 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 23 Jul 2026 09:39:21 -0700 Subject: [PATCH] Move SMTLIB2 verdict unit tests to z3test regressions These tests fed a fixed SMTLIB2 string to Z3_eval_smtlib2_string and checked a sat/unsat verdict. They are now data-driven regression files under z3test regressions/smt2 (with .expected.out ground truth), so remove them from the C++ test suite: - fpa.cpp: removed entirely (all tests transferred) - seq_rewriter.cpp: removed the two seq.foldl model-validation tests - simplifier.cpp: removed the sat.smt QF_UFBV predicate model-validation test - mod_factor.cpp: removed the const-array store-chain unsat test The API-constructed mod/idiv internalization-order tests remain in mod_factor.cpp. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 96a14756-2ffe-4cc3-87e7-49fda1b6113a --- src/test/CMakeLists.txt | 1 - src/test/fpa.cpp | 147 -------------------------------------- src/test/main.cpp | 1 - src/test/mod_factor.cpp | 25 ------- src/test/seq_rewriter.cpp | 72 ------------------- src/test/simplifier.cpp | 21 ------ 6 files changed, 267 deletions(-) delete mode 100644 src/test/fpa.cpp diff --git a/src/test/CMakeLists.txt b/src/test/CMakeLists.txt index 4563752812..21d089e85f 100644 --- a/src/test/CMakeLists.txt +++ b/src/test/CMakeLists.txt @@ -60,7 +60,6 @@ add_executable(test-z3 f2n.cpp finite_set.cpp finite_set_rewriter.cpp - fpa.cpp factor_rewriter.cpp finder.cpp fixed_bit_vector.cpp diff --git a/src/test/fpa.cpp b/src/test/fpa.cpp deleted file mode 100644 index 07fc86fb9f..0000000000 --- a/src/test/fpa.cpp +++ /dev/null @@ -1,147 +0,0 @@ -/*++ -Copyright (c) 2025 Microsoft Corporation - ---*/ - -// Regression tests for floating-point arithmetic encoding and model generation. - -#include "api/z3.h" -#include "util/debug.h" -#include - -static void run_fp_test(const char * assertion, bool expect_sat) { - Z3_context ctx = Z3_mk_context(nullptr); - const char * result = Z3_eval_smtlib2_string(ctx, assertion); - if (expect_sat) { - ENSURE(strstr(result, "sat") != nullptr); - ENSURE(strstr(result, "unsat") == nullptr); - } else { - ENSURE(strstr(result, "unsat") != nullptr); - } - ENSURE(strstr(result, "invalid") == nullptr); - Z3_del_context(ctx); -} - -// Test that fp.to_real produces correct values for denormal floating-point numbers. -// Regression test for: incorrect model with (_ FloatingPoint 2 24) and fp.to_real. -// Denormal numbers require subtracting the normalization shift (lz) from the exponent; -// without this fix, denormals in fp.to_real were ~2^lz times too large. -static void test_fp_to_real_denormal() { - // Test 1: the specific denormal from the bug report (fp #b0 #b00 #b00111011011111001011101) - // has fp.to_real ~= 0.232, which must NOT be > 1.0 - run_fp_test( - "(set-option :model_validate true)\n" - "(assert (> (fp.to_real (fp #b0 #b00 #b00111011011111001011101)) 1.0))\n" - "(check-sat)\n", - false); - - // Test 2: denormal with leading significand bit = 1, fp.to_real should be 0.5 - // (fp #b0 #b00 #b10000000000000000000000) in (_ FloatingPoint 2 24) - run_fp_test( - "(set-option :model_validate true)\n" - "(assert (= (fp.to_real (fp #b0 #b00 #b10000000000000000000000)) (/ 1.0 2.0)))\n" - "(check-sat)\n", - true); - - // Test 3: denormal with significand bit pattern giving fp.to_real = 0.125 - // (fp #b0 #b00 #b00100000000000000000000) in (_ FloatingPoint 2 24) - run_fp_test( - "(set-option :model_validate true)\n" - "(assert (= (fp.to_real (fp #b0 #b00 #b00100000000000000000000)) (/ 1.0 8.0)))\n" - "(check-sat)\n", - true); - - // Test 4: a normal value (fp #b0 #b01 #b11111111111111111111111) must be > 1.0 - // This is the maximum finite normal number in (_ FloatingPoint 2 24) - run_fp_test( - "(set-option :model_validate true)\n" - "(assert (> (fp.to_real (fp #b0 #b01 #b11111111111111111111111)) 1.0))\n" - "(check-sat)\n", - true); -} - -// Regression test for soundness bug in to_fp (from real) with symbolic real interval. -// When the rounding mode is RTZ and the real variable is constrained to an interval -// that includes the exact rational value of a float, Z3 should return SAT. -// This was broken because mk_to_real computed 2^(1/|exp|) instead of 1/(2^|exp|) -// for floats with negative exponents, causing a conflict in the NRA solver. -static void test_to_fp_from_real_interval() { - // The interval (-4127125/16777216, -16508499/67108864] contains -16508499/67108864 - // which is the exact rational value of fp #b1 #b01111100 #b11110111110011001010011. - // to_fp(RTZ, r) for r in this closed interval must equal that float. - run_fp_test( - "(set-logic QF_FPLRA)\n" - "(declare-const x Float32)\n" - "(assert (= x (fp #b1 #b01111100 #b11110111110011001010011)))\n" - "(declare-const r Real)\n" - "(assert (and (> r (- (/ 4127125.0 16777216.0))) (<= r (- (/ 16508499.0 67108864.0)))))\n" - "(declare-const w Float32)\n" - "(assert (= w ((_ to_fp 8 24) RTZ r)))\n" - "(assert (= x w))\n" - "(check-sat)\n", - true); -} - -// Preserve the signed value of the internal exponent when converting a symbolic -// unsigned bit-vector. In-range values must not take the overflow path. -static void test_to_fp_unsigned_exponent_width_boundary() { - run_fp_test( - "(set-logic QF_BVFP)\n" - "(set-option :model_validate true)\n" - "(declare-const high (_ BitVec 13))\n" - "(assert (or (= high #b1111111111110) (= high #b1111111111111)))\n" - "(assert (= ((_ to_fp_unsigned 2 11) RTN high) (fp #b0 #b10 #b1111111111)))\n" - "(assert (= ((_ to_fp_unsigned 2 11) RTZ high) (fp #b0 #b10 #b1111111111)))\n" - "(assert (= ((_ to_fp_unsigned 2 11) RTP high) (_ +oo 2 11)))\n" - "(assert (= ((_ to_fp_unsigned 2 11) RNE high) (_ +oo 2 11)))\n" - "(assert (= ((_ to_fp_unsigned 2 11) RNA high) (_ +oo 2 11)))\n" - "(declare-const small (_ BitVec 13))\n" - "(assert (or (= small #b0000000000001) (= small #b0000000000010)))\n" - "(assert (= ((_ to_fp_unsigned 2 11) RTN small)\n" - " (ite (= small #b0000000000001)\n" - " (fp #b0 #b01 #b0000000000)\n" - " (fp #b0 #b10 #b0000000000))))\n" - "(check-sat)\n", - true); -} - -static void test_to_fp_unsigned_common_widths() { - run_fp_test( - "(set-logic QF_BVFP)\n" - "(set-option :model_validate true)\n" - "(declare-const high (_ BitVec 32))\n" - "(assert (or (= high #xfffffffe) (= high #xffffffff)))\n" - "(assert (= ((_ to_fp_unsigned 8 24) RTN high)\n" - " (fp #b0 #b10011110 #b11111111111111111111111)))\n" - "(assert (= ((_ to_fp_unsigned 8 24) RTZ high)\n" - " (fp #b0 #b10011110 #b11111111111111111111111)))\n" - "(assert (= ((_ to_fp_unsigned 8 24) RTP high)\n" - " (fp #b0 #b10011111 #b00000000000000000000000)))\n" - "(assert (= ((_ to_fp_unsigned 8 24) RNE high)\n" - " (fp #b0 #b10011111 #b00000000000000000000000)))\n" - "(assert (= ((_ to_fp_unsigned 8 24) RNA high)\n" - " (fp #b0 #b10011111 #b00000000000000000000000)))\n" - "(check-sat)\n", - true); -} - -static void test_recfun_defined_function_soundness() { - run_fp_test( - "(set-option :model_validate true)\n" - "(declare-fun fixedAdd () Int)\n" - "(declare-fun variableAdd () Int)\n" - "(define-fun-rec $$add$$ ((a Int) (b Int)) Int\n" - " (ite (= 0 b) 2 (- a (+ 0 (- fixedAdd b)))))\n" - "(assert (= fixedAdd (* 9 fixedAdd)))\n" - "(assert (= 1 ($$add$$ 1 3)))\n" - "(check-sat)\n", - false); -} - -void tst_fpa() { - test_fp_to_real_denormal(); - test_to_fp_from_real_interval(); - test_to_fp_unsigned_exponent_width_boundary(); - test_to_fp_unsigned_common_widths(); - test_recfun_defined_function_soundness(); -} diff --git a/src/test/main.cpp b/src/test/main.cpp index 3a3cab41db..be1cb1f252 100644 --- a/src/test/main.cpp +++ b/src/test/main.cpp @@ -198,7 +198,6 @@ X(finite_set) \ X(finite_set_rewriter) \ X(seq_split) \ - X(fpa) \ X(seq_regex_bisim) \ X(term_enumeration) \ X(lcube) \ diff --git a/src/test/mod_factor.cpp b/src/test/mod_factor.cpp index 314537ca8d..069802522a 100644 --- a/src/test/mod_factor.cpp +++ b/src/test/mod_factor.cpp @@ -4,7 +4,6 @@ Copyright (c) 2025 Microsoft Corporation #include "api/z3.h" #include "util/util.h" -#include // x mod 7 = 0 & (x*y) mod 7 != 0 should be unsat // Exercises: mod internalization path (is_mod with numeric divisor) @@ -61,31 +60,7 @@ static void test_mod_factor_idiv_path() { Z3_del_context(ctx); } -static void test_const_array_store_chain_unsat() { - Z3_config cfg = Z3_mk_config(); - Z3_context ctx = Z3_mk_context(cfg); - const char* script = R"( -(set-logic QF_ABV) -(declare-const x (_ BitVec 8)) -(declare-const y (_ BitVec 8)) -(define-fun A0 () (Array (_ BitVec 2) (_ BitVec 8)) ((as const (Array (_ BitVec 2) (_ BitVec 8))) x)) -(define-fun A1 () (Array (_ BitVec 2) (_ BitVec 8)) ((as const (Array (_ BitVec 2) (_ BitVec 8))) y)) -(declare-const i0 (_ BitVec 2)) -(declare-const e0 (_ BitVec 8)) -(declare-const i1 (_ BitVec 2)) -(declare-const e1 (_ BitVec 8)) -(assert (distinct x y)) -(assert (= (store A0 i0 e0) (store A1 i1 e1))) -(check-sat) -)"; - std::string resp = Z3_eval_smtlib2_string(ctx, script); - ENSURE(resp.find("unsat") != std::string::npos); - Z3_del_config(cfg); - Z3_del_context(ctx); -} - void tst_mod_factor() { test_mod_factor_mod_path(); test_mod_factor_idiv_path(); - test_const_array_store_chain_unsat(); } diff --git a/src/test/seq_rewriter.cpp b/src/test/seq_rewriter.cpp index 84facb37e4..9557b9cfc6 100644 --- a/src/test/seq_rewriter.cpp +++ b/src/test/seq_rewriter.cpp @@ -23,11 +23,8 @@ Tests: #include "ast/reg_decl_plugins.h" #include "ast/rewriter/th_rewriter.h" #include "ast/seq_decl_plugin.h" -#include "api/z3.h" #include "smt/smt_context.h" -#include #include -#include #include // Build a single-char string literal expression. @@ -35,72 +32,6 @@ static expr_ref mk_str(ast_manager& m, seq_util& su, unsigned c) { return expr_ref(su.str.mk_string(zstring(c)), m); } -static void test_seq_foldl_nth_model_validation() { - Z3_context ctx = Z3_mk_context(nullptr); - char const* result = - Z3_eval_smtlib2_string(ctx, - "(set-option :model_validate true)\n" - "(declare-const initial Int)\n" - "(declare-const all (Seq Int))\n" - "(declare-const final Int)\n" - "(declare-const elements (Seq Int))\n" - "(define-fun all_sums ((prev_sums (Seq Int)) (elem Int)) (Seq Int)\n" - " (seq.++ (seq.unit (+ (seq.nth prev_sums 0) elem)) prev_sums))\n" - "(assert (= all (seq.foldl all_sums (seq.unit initial) elements)))\n" - "(assert (= final (seq.nth all 0)))\n" - "(assert (= initial 0))\n" - "(assert (= final 6))\n" - "(check-sat)\n" - "(get-model)\n"); - ENSURE(std::strstr(result, "sat") != nullptr); - ENSURE(std::strstr(result, "invalid model") == nullptr); - Z3_del_context(ctx); -} - -static void test_seq_foldl_foldli_scalar_model_validation() { - Z3_context ctx = Z3_mk_context(nullptr); - char const* result = - Z3_eval_smtlib2_string(ctx, - "(set-option :model_validate true)\n" - "(push)\n" - "(declare-fun f (Int Int) Int)\n" - "(declare-const il (Seq Int))\n" - "(assert (= (seq.foldl f 0 il) 5))\n" - "(check-sat)\n" - "(pop)\n" - "(push)\n" - "(declare-const il (Seq Int))\n" - "(declare-const F (Array Bool Int Bool))\n" - "(assert (= (seq.foldl F true il) true))\n" - "(assert (> (seq.len il) 0))\n" - "(assert (not (= F ((as const (Array Bool Int Bool)) true))))\n" - "(check-sat)\n" - "(pop)\n" - "(push)\n" - "(declare-fun f (Int Int Int) Int)\n" - "(declare-const il (Seq Int))\n" - "(assert (= (seq.foldli f 0 0 il) 5))\n" - "(check-sat)\n" - "(pop)\n" - "(push)\n" - "(declare-const il (Seq Int))\n" - "(declare-const F (Array Int Bool Int Bool))\n" - "(assert (= (seq.foldli F 5 true il) true))\n" - "(assert (> (seq.len il) 0))\n" - "(assert (not (= F ((as const (Array Int Bool Int Bool)) true))))\n" - "(check-sat)\n" - "(pop)\n"); - ENSURE(std::strstr(result, "unknown") == nullptr); - ENSURE(std::strstr(result, "invalid model") == nullptr); - unsigned sat_count = 0; - std::istringstream in{std::string(result)}; - for (std::string line; std::getline(in, line);) - if (line == "sat") - ++sat_count; - ENSURE(sat_count == 4); - Z3_del_context(ctx); -} - void tst_seq_rewriter() { ast_manager m; reg_decl_plugins(m); @@ -365,8 +296,5 @@ void tst_seq_rewriter() { } } - test_seq_foldl_nth_model_validation(); - test_seq_foldl_foldli_scalar_model_validation(); - std::cout << "tst_seq_rewriter: all tests passed\n"; } diff --git a/src/test/simplifier.cpp b/src/test/simplifier.cpp index 3b2abf7b25..660e881ee6 100644 --- a/src/test/simplifier.cpp +++ b/src/test/simplifier.cpp @@ -212,26 +212,6 @@ static void test_array() { Z3_del_context(ctx); } -static void test_sat_smt_ufbv_predicate_model_validation() { - Z3_context ctx = Z3_mk_context(nullptr); - const char* result = - Z3_eval_smtlib2_string(ctx, - "(set-logic QF_UFBV)\n" - "(set-option :sat.smt true)\n" - "(set-option :model_validate true)\n" - "(declare-fun p ((_ BitVec 4)) Bool)\n" - "(declare-const x (_ BitVec 4))\n" - "(declare-const y (_ BitVec 4))\n" - "(assert (xor (p x) (p y)))\n" - "(assert (bvuge x (_ bv1 4)))\n" - "(assert (bvult y (_ bv1 4)))\n" - "(check-sat)\n" - "(get-model)\n"); - ENSURE(std::strstr(result, "sat") != nullptr); - ENSURE(std::strstr(result, "invalid model") == nullptr); - Z3_del_context(ctx); -} - void tst_simplifier() { test_array(); @@ -239,5 +219,4 @@ void tst_simplifier() { test_datatypes(); test_bool(); test_skolemize_bug(); - test_sat_smt_ufbv_predicate_model_validation(); }