From 93e6c3b1cf805e0b5d0f37f6c6fb7f7c0b3c1731 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Wed, 10 Dec 2025 14:55:08 -0800
Subject: [PATCH] Flattening backend: further cases for casts to range types

This adds further cases for casts to range types to the flattening backend
(casts from bool, casts from signed bit vectors, casts to ranges that do not
start at zero).
---
 src/solvers/flattening/boolbv_typecast.cpp | 57 ++++++++++++----------
 1 file changed, 32 insertions(+), 25 deletions(-)

diff --git a/src/solvers/flattening/boolbv_typecast.cpp b/src/solvers/flattening/boolbv_typecast.cpp
index 84d25cc8883..79607549568 100644
--- a/src/solvers/flattening/boolbv_typecast.cpp
+++ b/src/solvers/flattening/boolbv_typecast.cpp
@@ -124,40 +124,47 @@ bool boolbvt::type_conversion(
   {
   case bvtypet::IS_RANGE:
     if(
-      src_bvtype == bvtypet::IS_UNSIGNED || src_bvtype == bvtypet::IS_SIGNED ||
-      src_bvtype == bvtypet::IS_C_BOOL)
+      src_bvtype == bvtypet::IS_UNSIGNED ||
+      src_bvtype == bvtypet::IS_C_BOOL) // unsigned to range
     {
-      mp_integer dest_from = to_range_type(dest_type).get_from();
+      // need to do arithmetic: add -dest_from
+      mp_integer offset = -to_range_type(dest_type).get_from();
+      dest = bv_utils.add(
+        bv_utils.zero_extension(src, dest_width),
+        bv_utils.build_constant(offset, dest_width));
 
-      if(dest_from == 0)
-      {
-        // do zero extension
-        dest.resize(dest_width);
-        for(std::size_t i = 0; i < dest.size(); i++)
-          dest[i] = (i < src.size() ? src[i] : const_literal(false));
+      return false;
+    }
+    else if(src_bvtype == bvtypet::IS_SIGNED) // signed to range
+    {
+      // need to do arithmetic: add -dest_from
+      mp_integer offset = -to_range_type(dest_type).get_from();
+      dest = bv_utils.add(
+        bv_utils.sign_extension(src, dest_width),
+        bv_utils.build_constant(offset, dest_width));
 
-        return false;
-      }
+      return false;
     }
     else if(src_bvtype == bvtypet::IS_RANGE) // range to range
     {
       mp_integer src_from = to_range_type(src_type).get_from();
       mp_integer dest_from = to_range_type(dest_type).get_from();
 
-      if(dest_from == src_from)
-      {
-        // do zero extension, if needed
-        dest = bv_utils.zero_extension(src, dest_width);
-        return false;
-      }
-      else
-      {
-        // need to do arithmetic: add src_from-dest_from
-        mp_integer offset = src_from - dest_from;
-        dest = bv_utils.add(
-          bv_utils.zero_extension(src, dest_width),
-          bv_utils.build_constant(offset, dest_width));
-      }
+      // need to do arithmetic: add src_from-dest_from
+      mp_integer offset = src_from - dest_from;
+      dest = bv_utils.add(
+        bv_utils.zero_extension(src, dest_width),
+        bv_utils.build_constant(offset, dest_width));
+
+      return false;
+    }
+    else if(src_type.id() == ID_bool) // bool to range
+    {
+      // need to do arithmetic: add -dest_from
+      mp_integer offset = -to_range_type(dest_type).get_from();
+      dest = bv_utils.add(
+        bv_utils.zero_extension(src, dest_width),
+        bv_utils.build_constant(offset, dest_width));
 
       return false;
     }