From e2e7e2b95ce8013699f97b351a84cdeb6d40cb50 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sat, 4 Jul 2026 12:28:59 -0700 Subject: [PATCH 1/5] Add KNOWNBUG regression test for #9101 The SMT2 export path aborts with an invariant violation when flatten2bv encounters a non-constant FPA-encoded float (e.g. a nondet float stored in a union and read back as unsigned). Add a minimal reproducer that exercises this code path via the classic union-based float-to-int type-punning idiom. The test is marked KNOWNBUG because the export currently aborts (SIGABRT) instead of producing a complete SMT2 formula. --- .../smt2-fpa-nonconst-union-flatten2bv/main.c | 24 +++++++++++++++++++ .../test.desc | 20 ++++++++++++++++ 2 files changed, 44 insertions(+) create mode 100644 regression/cbmc/smt2-fpa-nonconst-union-flatten2bv/main.c create mode 100644 regression/cbmc/smt2-fpa-nonconst-union-flatten2bv/test.desc diff --git a/regression/cbmc/smt2-fpa-nonconst-union-flatten2bv/main.c b/regression/cbmc/smt2-fpa-nonconst-union-flatten2bv/main.c new file mode 100644 index 00000000000..1edaa1285cd --- /dev/null +++ b/regression/cbmc/smt2-fpa-nonconst-union-flatten2bv/main.c @@ -0,0 +1,24 @@ +// Reproducer for #9101: flatten2bv aborts on non-constant FPA-encoded float +// when exporting to SMT2 with --fpa. +// +// The classic union-based float-to-int type-punning idiom (used pervasively +// in bit-exact libm code) triggers an invariant violation in the SMT2 export +// path because flatten2bv does not handle non-constant floatbv expressions +// under FPA theory. The native (SAT) back-end solves this without issue. + +extern void reach_error(void); +extern float __VERIFIER_nondet_float(void); + +int main(void) +{ + float f = __VERIFIER_nondet_float(); + union + { + float f; + unsigned u; + } pun; + pun.f = f; + if((pun.u & 0x7fffffffu) > 0x7f800000u) + reach_error(); + return 0; +} diff --git a/regression/cbmc/smt2-fpa-nonconst-union-flatten2bv/test.desc b/regression/cbmc/smt2-fpa-nonconst-union-flatten2bv/test.desc new file mode 100644 index 00000000000..ed5b9a0ed6f --- /dev/null +++ b/regression/cbmc/smt2-fpa-nonconst-union-flatten2bv/test.desc @@ -0,0 +1,20 @@ +KNOWNBUG +main.c +--smt2 --fpa --outfile - +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- +Issue #9101: `--smt2 --fpa --outfile` aborts with an invariant violation +("flatten2bv of a non-constant FPA-encoded float is unsupported") when the +program reinterprets the bits of a non-constant float through a union. + +The SMT-LIB FloatingPoint theory deliberately has no fp-to-bitvector +operator (NaN bit patterns are ambiguous), so the export path must emit a +fresh BV variable constrained via to_fp round-trip — as it already does for +explicit typecast_exprt(floatbv→bv). The union/with path bypasses that +mechanism and calls flatten2bv directly on the float symbol, hitting the +invariant. + +The native SAT back-end solves the identical program without issue. From 369320979b55ee7611212e451651093e2ba66cf7 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sat, 4 Jul 2026 12:35:36 -0700 Subject: [PATCH 2/5] Fix flatten2bv abort on non-constant FPA float [#9101] MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit When flatten2bv encounters a non-constant floatbv expression under FPA theory (e.g. a nondet float stored in a union), it now emits the same bvfromfloat round-trip that find_symbols already uses for explicit typecast(floatbv→bv): declare a fresh BV variable and assert that ((_ to_fp E S) bv) equals the float expression. Previously this hit an UNEXPECTEDCASE invariant violation, aborting the SMT2 export mid-write and leaving a truncated output file. The regression test is promoted from KNOWNBUG to CORE. --- .../test.desc | 19 +++------ src/solvers/smt2/smt2_conv.cpp | 41 +++++++++++++++---- 2 files changed, 39 insertions(+), 21 deletions(-) diff --git a/regression/cbmc/smt2-fpa-nonconst-union-flatten2bv/test.desc b/regression/cbmc/smt2-fpa-nonconst-union-flatten2bv/test.desc index ed5b9a0ed6f..2d98b50c323 100644 --- a/regression/cbmc/smt2-fpa-nonconst-union-flatten2bv/test.desc +++ b/regression/cbmc/smt2-fpa-nonconst-union-flatten2bv/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.c --smt2 --fpa --outfile - ^EXIT=0$ @@ -6,15 +6,8 @@ main.c -- ^warning: ignoring -- -Issue #9101: `--smt2 --fpa --outfile` aborts with an invariant violation -("flatten2bv of a non-constant FPA-encoded float is unsupported") when the -program reinterprets the bits of a non-constant float through a union. - -The SMT-LIB FloatingPoint theory deliberately has no fp-to-bitvector -operator (NaN bit patterns are ambiguous), so the export path must emit a -fresh BV variable constrained via to_fp round-trip — as it already does for -explicit typecast_exprt(floatbv→bv). The union/with path bypasses that -mechanism and calls flatten2bv directly on the float symbol, hitting the -invariant. - -The native SAT back-end solves the identical program without issue. +Issue #9101: `--smt2 --fpa --outfile` previously aborted with an invariant +violation ("flatten2bv of a non-constant FPA-encoded float is unsupported") +when the program reinterprets the bits of a non-constant float through a +union. The fix emits the same bvfromfloat round-trip (declare a fresh BV, +assert to_fp(bv) == float) that find_symbols uses for explicit typecasts. diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index 8ee689aabec..2981ab4497e 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -5252,14 +5252,10 @@ void smt2_convt::flatten2bv(const exprt &expr) { if(use_FPA_theory) { - // A floatbv constant's IEEE-754 interchange bit pattern is exactly its - // bit-vector representation, so it is emitted as a literal bit-vector. - // This is the only shape that reaches flatten2bv under FPA: a - // non-constant float whose bits are read is lowered by - // lower_byte_operators into a float typecast, which is handled by the - // bvfromfloat round-trip in find_symbols and never reaches here. if(expr.is_constant()) { + // A floatbv constant's IEEE-754 interchange bit pattern is exactly + // its bit-vector representation, so emit it as a literal BV. const ieee_float_spect spec(to_floatbv_type(type)); const mp_integer value = bvrep2integer( to_constant_expr(expr).get_value(), spec.width(), false); @@ -5267,8 +5263,37 @@ void smt2_convt::flatten2bv(const exprt &expr) } else { - UNEXPECTEDCASE( - "flatten2bv of a non-constant FPA-encoded float is unsupported"); + // Non-constant float under FPA theory: the SMT-LIB FP theory has + // no fp-to-bitvector operator (NaN bit patterns are ambiguous), so + // we declare a fresh BV variable and assert that converting it back + // to FP equals the original float value. This is the same + // round-trip that find_symbols uses for typecast(floatbv → bv). + const auto &floatbv_type = to_floatbv_type(type); + const typecast_exprt tc{expr, bv_typet{floatbv_type.width()}}; + + auto it = defined_expressions.find(tc); + if(it == defined_expressions.end()) + { + const irep_idt id = + "bvfromfloat." + std::to_string(defined_expressions.size()); + out << "(declare-fun " << id << " () "; + convert_type(tc.type()); + out << ')' << '\n'; + + out << "(assert (= "; + out << "((_ to_fp " << floatbv_type.get_e() << " " + << floatbv_type.get_f() + 1 << ") " << id << ')'; + convert_expr(expr); + out << ')'; // = + out << ')' << '\n'; + + defined_expressions[tc] = id; + out << id; + } + else + { + out << it->second; + } } } else From 71a33b98adb7022832429853d17dcb67f76c010b Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sat, 4 Jul 2026 13:09:40 -0700 Subject: [PATCH 3/5] Tag regression test to exclude from SMT-backend re-runs The test explicitly controls the output format (--smt2 --fpa --outfile -) and must not be re-run with a different solver backend appended. Add broken-smt-backend and no-new-smt tags, matching the convention used by other --outfile tests (e.g. array_of_bool_as_bitvec/test-smt2-outfile.desc). --- .../cbmc/smt2-fpa-nonconst-union-flatten2bv/test.desc | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/regression/cbmc/smt2-fpa-nonconst-union-flatten2bv/test.desc b/regression/cbmc/smt2-fpa-nonconst-union-flatten2bv/test.desc index 2d98b50c323..3127f059b75 100644 --- a/regression/cbmc/smt2-fpa-nonconst-union-flatten2bv/test.desc +++ b/regression/cbmc/smt2-fpa-nonconst-union-flatten2bv/test.desc @@ -1,4 +1,4 @@ -CORE +CORE broken-smt-backend no-new-smt main.c --smt2 --fpa --outfile - ^EXIT=0$ @@ -11,3 +11,7 @@ violation ("flatten2bv of a non-constant FPA-encoded float is unsupported") when the program reinterprets the bits of a non-constant float through a union. The fix emits the same bvfromfloat round-trip (declare a fresh BV, assert to_fp(bv) == float) that find_symbols uses for explicit typecasts. + +Tagged broken-smt-backend/no-new-smt because this test explicitly controls +the output format (--smt2 --fpa --outfile -) and must not be re-run with a +different solver backend. From 813ca9814333e1e647af59c17f794c1428029a66 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sat, 4 Jul 2026 15:27:26 -0700 Subject: [PATCH 4/5] Exclude --outfile test from XML trace validation Tests using --outfile - dump raw SMT2 to stdout, which is not valid XML. Add the new test to the exclusion list in validate-trace-xml-schema/check.py, matching the existing exclusions for array_of_bool_as_bitvec and others. --- regression/validate-trace-xml-schema/check.py | 1 + 1 file changed, 1 insertion(+) diff --git a/regression/validate-trace-xml-schema/check.py b/regression/validate-trace-xml-schema/check.py index 8ede2e47dd3..91c1af33880 100644 --- a/regression/validate-trace-xml-schema/check.py +++ b/regression/validate-trace-xml-schema/check.py @@ -16,6 +16,7 @@ ['array_of_bool_as_bitvec', 'test-smt2-outfile.desc'], ['deterministic-smt-output', 'test.desc'], ['z3-lambda-unflatten', 'test.desc'], + ['smt2-fpa-nonconst-union-flatten2bv', 'test.desc'], # these tests expect input from stdin ['json-interface1', 'test_wrong_option.desc'], ['json-interface1', 'test.desc'], From 48ddabe0c1fc154ead4d18b2fd847bd8c1527b9b Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sat, 4 Jul 2026 17:48:05 -0700 Subject: [PATCH 5/5] Move bvfromfloat declaration to find_symbols The bvfromfloat auxiliary (declare-fun + assert) must be emitted at the SMT-LIB top level, not inline during expression conversion. Move the declaration logic into find_symbols, which runs before any expression output. find_symbols now pre-creates a bvfromfloat entry for every non-constant floatbv-typed expression it visits under FPA theory. flatten2bv then simply looks up the existing entry by its defined_expressions key (a synthetic typecast_exprt from floatbv to bv). --- src/solvers/smt2/smt2_conv.cpp | 64 ++++++++++++++++++++-------------- 1 file changed, 37 insertions(+), 27 deletions(-) diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index 2981ab4497e..14e6f3ddff8 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -5263,37 +5263,16 @@ void smt2_convt::flatten2bv(const exprt &expr) } else { - // Non-constant float under FPA theory: the SMT-LIB FP theory has - // no fp-to-bitvector operator (NaN bit patterns are ambiguous), so - // we declare a fresh BV variable and assert that converting it back - // to FP equals the original float value. This is the same - // round-trip that find_symbols uses for typecast(floatbv → bv). + // Non-constant float under FPA theory: look up the bvfromfloat + // auxiliary that find_symbols pre-created for this expression. const auto &floatbv_type = to_floatbv_type(type); const typecast_exprt tc{expr, bv_typet{floatbv_type.width()}}; auto it = defined_expressions.find(tc); - if(it == defined_expressions.end()) - { - const irep_idt id = - "bvfromfloat." + std::to_string(defined_expressions.size()); - out << "(declare-fun " << id << " () "; - convert_type(tc.type()); - out << ')' << '\n'; - - out << "(assert (= "; - out << "((_ to_fp " << floatbv_type.get_e() << " " - << floatbv_type.get_f() + 1 << ") " << id << ')'; - convert_expr(expr); - out << ')'; // = - out << ')' << '\n'; - - defined_expressions[tc] = id; - out << id; - } - else - { - out << it->second; - } + CHECK_RETURN_WITH_DIAGNOSTICS( + it != defined_expressions.end(), + "flatten2bv: bvfromfloat entry missing for non-constant float"); + out << it->second; } } else @@ -6071,6 +6050,37 @@ void smt2_convt::find_symbols(const exprt &expr) defined_expressions[expr] = id; } } + else if( + use_FPA_theory && !expr.is_constant() && + expr.type().id() == ID_floatbv) + { + // Pre-create a bvfromfloat auxiliary for non-constant floatbv + // expressions that may be passed to flatten2bv (e.g. when stored + // into a union or flattened as part of a struct). The SMT-LIB FP + // theory has no fp-to-bitvector operator, so the round-trip + // (declare fresh BV, assert to_fp(BV) == float) must be emitted at + // the top level, before flatten2bv is called mid-expression. + const auto &floatbv_type = to_floatbv_type(expr.type()); + const typecast_exprt tc{expr, bv_typet{floatbv_type.width()}}; + + if(defined_expressions.find(tc) == defined_expressions.end()) + { + const irep_idt id = + "bvfromfloat." + std::to_string(defined_expressions.size()); + out << "(declare-fun " << id << " () "; + convert_type(tc.type()); + out << ')' << '\n'; + + out << "(assert (= "; + out << "((_ to_fp " << floatbv_type.get_e() << " " + << floatbv_type.get_f() + 1 << ") " << id << ')'; + convert_expr(expr); + out << ')'; // = + out << ')' << '\n'; + + defined_expressions[tc] = id; + } + } else if(expr.id() == ID_initial_state) { irep_idt function = "initial-state";