From e8930c23ca32bcec63838ad9744323f66cf87857 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 3 Jun 2026 11:15:55 +0000 Subject: [PATCH] smt2: add missing separator in bvfromfloat equality assertion The `bvfromfloat` mechanism in smt2_convt::find_symbols emits, for a bit-wise `typecast` from an FPA-encoded float to a bit-vector, an assertion of the form (assert (= ((_ to_fp e f) ))) with no whitespace between the closing parenthesis of the `to_fp` application and the second operand of the equality. Most SMT-LIB tokenizers treat `)` as a token boundary, but CPROVER's own smt2 tokenizer does not, so it reads `)|float|` as a single (invalid) token and rejects the assertion. This path is only reached when reading the raw bytes of an FPA-encoded float (e.g. a union-based bit access under --cprover-smt2 or an FPA solver), which is itself subject to other backend limitations, so the bug was latent. Emit the missing space. Co-authored-by: Kiro --- src/solvers/smt2/smt2_conv.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index d118a55ef32..71d3a3a86b7 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -5726,7 +5726,7 @@ void smt2_convt::find_symbols(const exprt &expr) const auto &floatbv_type = to_floatbv_type(tc.op().type()); out << "(assert (= "; out << "((_ to_fp " << floatbv_type.get_e() << " " - << floatbv_type.get_f() + 1 << ") " << id << ')'; + << floatbv_type.get_f() + 1 << ") " << id << ") "; convert_expr(tc.op()); out << ')'; // = out << ')' << '\n';