Arithmetic Operator:

	All operands are passed at once to the constraint function.
	It allows to create different conditions based on the order
	of the operands.

	Example: for the division, only the second operand
	must be != 0

symbolic_execution/language/bitcoin/op_codes.py

@@ -28,7 +28,7 @@ nSequence = Int("nSequence")
 version = Int("version")
 
 
-def arithmetic_constraint_on_operands_size(op: BTCVector):
+def arithmetic_constraint_on_operands_size(ops: List[BTCVector]):
     """Return a constraint on an arithmetic operand to enforce its minimal encoding.
 
     An operand is minimally encoded if it is represented with the least amount of bytes.
@@ -37,10 +37,11 @@ def arithmetic_constraint_on_operands_size(op: BTCVector):
         01 is the minimal hex representation of 1.
         0100 is not a minimal hex representation of 1.
     """
-    return op.size == BTCVector._min_bytes_needed(op.val)
+    constraints = [op.size == BTCVector._min_bytes_needed(op.val) for op in ops]
+    return constraints
 
 
-def locktime_constraint(op: BTCVector):
+def locktime_constraint(ops: List[BTCVector]):
     """Return a constraint to mimic OP_CHECKLOCKTIMEVERIFY specification.
 
     The conditions are:
@@ -53,6 +54,12 @@ def locktime_constraint(op: BTCVector):
     """
     LOCKTIME_THRESHOLD = 500000000
 
+    if len(ops) != 1:
+        raise ValueError("Sequence operator should take one arg.")
+
+    op = ops[0]
+
+
     condition = And(
         op.size <= 5,
         op.val <= nLockTime,
@@ -64,10 +71,10 @@ def locktime_constraint(op: BTCVector):
         nSequence != 0xFFFFFFFF,
     )
 
-    return condition
+    return [condition]
 
 
-def sequence_constraint(op: BTCVector):
+def sequence_constraint(ops: List[BTCVector]):
     """Return a constraint to mimic OP_CHECKSEQUENCEVERIFY specification.
 
     The conditions are:
@@ -94,6 +101,11 @@ def sequence_constraint(op: BTCVector):
         """Return the 23th bit of the vector."""
         return (val % (2 ** 23)) / (2 ** 22)
 
+    if len(ops) != 1:
+        raise ValueError("Sequence operator should take one arg.")
+
+    op = ops[0]
+
     condition = And(
         op.size <= 5,
         op.val >= 0,
@@ -107,7 +119,8 @@ def sequence_constraint(op: BTCVector):
         ),
     )
 
-    return condition
+    return [condition]
+
 
 
 class OpCode:

symbolic_execution/program/instruction/stack_based.py

@@ -57,7 +57,7 @@ class ArithmeticOperator(IInstruction):
         machine.push_onto_stack(self._operator(*ops))
 
         if self._constraint_on_operands and isinstance(machine, ISymbolicMachine):
-            constraints = [self._constraint_on_operands(op) for op in ops]
+            constraints = self._constraint_on_operands(ops)
             machine.add_constraints(constraints)
 
     def __repr__(self) -> str: