From 7c7c603270c4101b3361cd8a64128f8047b6318d Mon Sep 17 00:00:00 2001
From: Sergey Morozov <morozov.serg901@gmail.com>
Date: Wed, 6 Sep 2023 16:05:20 +0300
Subject: [PATCH] [fix] Fixed building of expressions with floats: added way to
 cast bool to fp.

---
 lib/Solver/Z3BitvectorBuilder.cpp       |  2 ++
 test/regression/2023-09-05-bool-to-fp.c | 35 +++++++++++++++++++++++++
 2 files changed, 37 insertions(+)
 create mode 100644 test/regression/2023-09-05-bool-to-fp.c

diff --git a/lib/Solver/Z3BitvectorBuilder.cpp b/lib/Solver/Z3BitvectorBuilder.cpp
index f673949618..82e2ba206f 100644
--- a/lib/Solver/Z3BitvectorBuilder.cpp
+++ b/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;
diff --git a/test/regression/2023-09-05-bool-to-fp.c b/test/regression/2023-09-05-bool-to-fp.c
new file mode 100644
index 0000000000..72eb891159
--- /dev/null
+++ b/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