---

yaml --- r: 76563 b: refs/heads/type-of-boolean-ops c: acde1a8 h: refs/heads/develop i: 76561: bfaf0a3 76559: c002371
smowton · Apr 11, 2019 · ff7e7d5 · ff7e7d5
1 parent bc5eda5
commit ff7e7d5
Show file tree

Hide file tree

Showing 2 changed files with 22 additions and 22 deletions.
diff --git a/[refs] b/[refs]
@@ -123,7 +123,7 @@ refs/heads/symex-type-renaming4: 600ba5bdcc86dff4cf68099bb16fd8629dc12eec
 refs/heads/test-issue-3653: 379155721d0e6756000898d3d80f9d41aac0a95a
 refs/heads/type-cleanup2: f1980e47f0dc6dd1526d92d660fcea1428204be7
 refs/heads/type-equality: 7a744e6b50540ee9797618077651162a8581bc0e
-refs/heads/type-of-boolean-ops: 848e633b6770d96f7761a08c862b829cc2515384
+refs/heads/type-of-boolean-ops: acde1a83cba94e3ff655ea61bec286295e0f5709
 refs/heads/unwind-counters4: 57aedaa3fe3995b30ba69c96c9f04df79f8e8ff8
 "refs/heads/use_make_X5": e5f49319d259411f754c149ed371459f426ba855
 "refs/heads/use_object_size_for_heap": b0875f62cd33a7caf08fc5889cf660e24b069bf2

diff --git a/branches/type-of-boolean-ops/src/solvers/flattening/boolbv_typecast.cpp b/branches/type-of-boolean-ops/src/solvers/flattening/boolbv_typecast.cpp
@@ -415,31 +415,31 @@ bool boolbvt::type_conversion(
       }
       break;
 
-    case bvtypet::IS_BV:
-      INVARIANT(
-        src_width == dest_width,
-        "source bitvector with shall equal the destination bitvector width");
-      dest=src;
-      return false;
-
-    default:
-      if(src_type.id()==ID_bool)
-      {
-        // bool to integer
-
+      case bvtypet::IS_BV:
         INVARIANT(
-          src_width == 1, "bitvector of type boolean shall have width one");
+          src_width == dest_width,
+          "source bitvector with shall equal the destination bitvector width");
+        dest = src;
+        return false;
 
-        for(std::size_t i=0; i<dest_width; i++)
+      default:
+        if(src_type.id() == ID_bool)
         {
-          if(i==0)
-            dest.push_back(src[0]);
-          else
-            dest.push_back(const_literal(false));
-        }
+          // bool to integer
 
-        return false;
-      }
+          INVARIANT(
+            src_width == 1, "bitvector of type boolean shall have width one");
+
+          for(std::size_t i = 0; i < dest_width; i++)
+          {
+            if(i == 0)
+              dest.push_back(src[0]);
+            else
+              dest.push_back(const_literal(false));
+          }
+
+          return false;
+        }
     }
     break;