[Symbolic Memory] Bug fixes

	* Different memories should generate different symbols.
	* During a merge, entries from the other memory should be
	  "deepcopied"

symbolic_execution/hardware/machines/btc_machine.py

@@ -313,7 +313,7 @@ class BTCMachine(IStackBasedMachine, IRAMBasedMachine, ISymbolicMachine):
             raise ValueError("A BTC machine must include 2 stacks.")
         self._stack_count = stack_count
         self._stacks = [
-            memory_constructor(word_size=word_size, mem_id=i)
+            memory_constructor(word_size=word_size, mem_id=f"stack{i}")
             for i in range(stack_count)
         ]
         self._word_size = word_size

symbolic_execution/hardware/memory/ram.py

 """Different mplementations of a random access memory."""
 from collections import namedtuple
+from copy import deepcopy
 from heapq import heappush
 from typing import Any, List, Tuple, Union
 
@@ -53,6 +54,8 @@ class FullySymbolicRAM(ISymbolicMemory):
         # Constrains on the current path
         self.constraints = And(True)
 
+        self.mem_id = mem_id
+
     def read(self, pos: Union[int, ExprRef] = None) -> Word:
         """Read the memory at pos {pos}.
 
@@ -69,7 +72,8 @@ class FullySymbolicRAM(ISymbolicMemory):
         if s.check() == sat:
             self.neg_t -= 1
             new_symbol = Word(
-                Int(f"n_{abs(self.neg_t)}"), Int(f"n_{abs(self.neg_t)}_size")
+                Int(f"{self.mem_id}_{abs(self.neg_t)}"),
+                Int(f"n_{abs(self.neg_t)}_size"),
             )
 
             heappush(
@@ -125,6 +129,7 @@ class FullySymbolicRAM(ISymbolicMemory):
                 entry.constraints = And(entry.constraints, self_constraints)
 
         for timer, entry in sorted(other.writes):
+            entry = deepcopy(entry)
             if timer < negative_timer or timer > positive_timer:
                 entry.constraints = And(entry.constraints, other_constraints)
                 heappush(self.writes, (timer, entry))

tests/language/bitcoin/testing_scenarii.py

@@ -279,7 +279,7 @@ TESTING_SCENARII = [
         "76010593",
         "OP_DUP 05 OP_ADD",
         "[0: StackAlterationOperator((['x1'], ['x1', 'x1'])), 1: PushDataOperator(05), 2: ArithmeticOperator(+), 3: UnconditionalJump(4), 4: UnconditionalJump(inf)]",
-        [["n_1", "5 + n_1"], []],
+        [["stack0_1", "5 + stack0_1"], []],
         None,
     ),
     TestScenario(
@@ -287,7 +287,7 @@ TESTING_SCENARII = [
         "93",
         "OP_ADD",
         "[0: ArithmeticOperator(+), 1: UnconditionalJump(2), 2: UnconditionalJump(inf)]",
-        [["n_2 + n_1"], []],
+        [["stack0_2 + stack0_1"], []],
         None,
     ),
     TestScenario(