[BTC Language] Bug fix

	* False is encoded over 0 byte. The operators were returning
	  a value encoded over 1 byte.

symbolic_execution/hardware/machines/btc_machine.py

@@ -143,49 +143,53 @@ class BTCVector:
                 self.BTC_TRUE,
                 self.BTC_FALSE,
             ),
-            IntVal(1),  # True and False are always encoded on 1 byte.
+            If(
+                And(self.val == other.val, self.size == other.size),
+                IntVal(1),
+                IntVal(0),
+            ),
         )
 
     def __le__(self, other):
         """Return the BTC vector `True` if `self.val <= other.val`."""
         return BTCVector(
             If(self.val <= other.val, self.BTC_TRUE, self.BTC_FALSE),
-            IntVal(1),  # True and False are always encoded on 1 byte.
+            If(self.val <= other.val, IntVal(1), IntVal(0)),
         )
 
     def __lt__(self, other):
         """Return the BTC vector `True` if `self.val < other.val`."""
         return BTCVector(
             If(self.val < other.val, self.BTC_TRUE, self.BTC_FALSE),
-            IntVal(1),  # True and False are always encoded on 1 byte.
+            If(self.val < other.val, IntVal(1), IntVal(0)),
         )
 
     def __gt__(self, other):
         """Return the BTC vector `True` if `self.val > other.val`."""
         return BTCVector(
             If(self.val > other.val, self.BTC_TRUE, self.BTC_FALSE),
-            IntVal(1),  # True and False are always encoded on 1 byte.
+            If(self.val > other.val, IntVal(1), IntVal(0)),
         )
 
     def __ge__(self, other):
         """Return the BTC vector `True` if `self.val >= other.val`."""
         return BTCVector(
             If(self.val >= other.val, self.BTC_TRUE, self.BTC_FALSE),
-            IntVal(1),  # True and False are always encoded on 1 byte.
+            If(self.val >= other.val, IntVal(1), IntVal(0)),
         )
 
     def __and__(self, other):
         """Return the BTC vector `True` if `self.val != 0 and other.val != 0`."""
         return BTCVector(
             If(And(self.val != 0, other.val != 0), self.BTC_TRUE, self.BTC_FALSE),
-            IntVal(1),  # True and False are always encoded on 1 byte.
+            If(And(self.val != 0, other.val != 0), IntVal(1), IntVal(0)),
         )
 
     def __or__(self, other):
         """Return the BTC vector `True` if `self.val != 0 or other.val != 0`."""
         return BTCVector(
             If(Or(self.val != 0, other.val != 0), self.BTC_TRUE, self.BTC_FALSE),
-            IntVal(1),  # True and False are always encoded on 1 byte.
+            If(Or(self.val != 0, other.val != 0), IntVal(1), IntVal(0)),
         )
 
     def __min__(self, other):
@@ -206,7 +210,7 @@ class BTCVector:
         """Return the BTC vector `True` if `a.val <= self.val < b.val`."""
         return BTCVector(
             If(And(self.val < b.val, self.val >= a.val), self.BTC_TRUE, self.BTC_FALSE),
-            IntVal(1),  # True and False are always encoded on 1 byte.
+            If(And(self.val < b.val, self.val >= a.val), IntVal(1), IntVal(0)),
         )
 
     def __inc__(self):
@@ -221,14 +225,14 @@ class BTCVector:
         """If the input is 0 or 1, it is flipped. Otherwise the output will be 0."""
         return BTCVector(
             If(self.val == 0, self.BTC_TRUE, self.BTC_FALSE),
-            IntVal(1),  # True and False are always encoded on 1 byte.
+            If(self.val == 0, IntVal(1), IntVal(0)),
         )
 
     def __num_eq__(self, other):
         """Return the BTC vector `True` if `self.val == other.val`."""
         return BTCVector(
             If(self.val == other.val, self.BTC_TRUE, self.BTC_FALSE),
-            IntVal(1),  # True and False are always encoded on 1 byte.
+            If(self.val == other.val, IntVal(1), IntVal(0)),
         )
 
     def __size__(self):