[fix] Fixed building of expressions with floats

lib/Solver/Z3BitvectorBuilder.cpp

@@ -1059,6 +1059,8 @@ Z3ASTHandle Z3BitvectorBuilder::castToBitVector(const Z3ASTHandle &e) {
   Z3SortHandle currentSort = Z3SortHandle(Z3_get_sort(ctx, e), ctx);
   Z3_sort_kind kind = Z3_get_sort_kind(ctx, currentSort);
   switch (kind) {
+  case Z3_BOOL_SORT:
+    return Z3ASTHandle(Z3_mk_ite(ctx, e, bvOne(1), bvZero(1)), ctx);
   case Z3_BV_SORT:
     // Already a bitvector
     return e;

test/regression/2023-09-05-bool-to-fp.c

@@ -0,0 +1,35 @@
+// RUN: %clang %s -g -emit-llvm %O0opt -c -o %t1.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --optimize --output-dir=%t.klee-out %t1.bc 2>&1 | FileCheck %s
+
+#include "klee/klee.h"
+
+extern void abort(void);
+extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__((__nothrow__, __leaf__)) __attribute__((__noreturn__));
+void reach_error() { __assert_fail("0", "float3.c", 3, "reach_error"); }
+
+double d = 0.0;
+
+void f1() {
+  d = 1.0;
+}
+
+int main() {
+  int x = 2;
+
+  if (klee_int("a"))
+    x = 4;
+
+  (void)f1();
+
+  d += (x == 2);
+
+  d += (x > 3);
+
+  if (!(d == 2.0)) {
+    reach_error();
+    abort();
+  }
+}
+
+// CHECK: KLEE: done: generated tests = 1