diff --git a/ci/matrix.py b/ci/matrix.py
index cbf5db29a..1f509812f 100644
--- a/ci/matrix.py
+++ b/ci/matrix.py
@@ -108,11 +108,7 @@ def listify(s: str | Sequence[str]) -> Sequence[str]:
             "odroidc4",
             "maaxboard",
         ],
-        # Disable until https://github.com/au-ts/libvmm/issues/233 is resolved.
-        "tests_exclude": [
-            { "config": "smp-debug" },
-            { "config": "smp-release" },
-        ],
+        "tests_exclude": [],
     },
     "virtio": {
         "configs": ["debug", "release"],
diff --git a/examples/smp/board/maaxboard/smp.system b/examples/smp/board/maaxboard/smp.system
index 7b8bc2f12..6a09be715 100644
--- a/examples/smp/board/maaxboard/smp.system
+++ b/examples/smp/board/maaxboard/smp.system
@@ -24,14 +24,10 @@
         <program_image path="vmm.elf" />
         <map mr="guest_ram" vaddr="0x40000000" perms="rw" setvar_vaddr="guest_ram_vaddr" />
         <virtual_machine name="linux" >
-            <!-- Due to https://github.com/seL4/seL4/issues/1645 we are placing all 4 VCPUs on
-                 1 physical CPU, this should be changed to 1 VCPU per core once the issue is fixed
-                 for true SMP.
-            -->
             <vcpu id="0" cpu="0" />
-            <vcpu id="1" cpu="0" />
-            <vcpu id="2" cpu="0" />
-            <vcpu id="3" cpu="0" />
+            <vcpu id="1" cpu="1" />
+            <vcpu id="2" cpu="2" />
+            <vcpu id="3" cpu="3" />
             <map mr="guest_ram" vaddr="0x40000000" perms="rwx" />
             <map mr="uart" vaddr="0x30860000" perms="rw" cached="false" />
             <!-- The guest needs to view what is actually the vCPU interface as the CPU interface. -->
diff --git a/examples/smp/board/odroidc4/smp.system b/examples/smp/board/odroidc4/smp.system
index aa3afaa02..956f26d89 100644
--- a/examples/smp/board/odroidc4/smp.system
+++ b/examples/smp/board/odroidc4/smp.system
@@ -23,14 +23,10 @@
         <program_image path="vmm.elf" />
         <map mr="guest_ram" vaddr="0x20000000" perms="rw" setvar_vaddr="guest_ram_vaddr" />
         <virtual_machine name="linux" >
-            <!-- Due to https://github.com/seL4/seL4/issues/1645 we are placing all 4 VCPUs on
-                 1 physical CPU, this should be changed to 1 VCPU per core once the issue is fixed
-                 for true SMP.
-            -->
             <vcpu id="0" cpu="0" />
-            <vcpu id="1" cpu="0" />
-            <vcpu id="2" cpu="0" />
-            <vcpu id="3" cpu="0" />
+            <vcpu id="1" cpu="1" />
+            <vcpu id="2" cpu="2" />
+            <vcpu id="3" cpu="3" />
             <map mr="guest_ram" vaddr="0x20000000" perms="rwx" />
             <map mr="bus1" vaddr="0xff600000" perms="rw" cached="false" />
             <map mr="bus2" vaddr="0xff800000" perms="rw" cached="false" />
diff --git a/examples/smp/board/qemu_virt_aarch64/smp.system b/examples/smp/board/qemu_virt_aarch64/smp.system
index d7c30ac18..ea038c058 100644
--- a/examples/smp/board/qemu_virt_aarch64/smp.system
+++ b/examples/smp/board/qemu_virt_aarch64/smp.system
@@ -37,14 +37,10 @@
         -->
         <map mr="guest_ram" vaddr="0x40000000" perms="rw" setvar_vaddr="guest_ram_vaddr" />
         <virtual_machine name="linux" >
-            <!-- Due to https://github.com/seL4/seL4/issues/1645 we are placing all 4 VCPUs on
-                 1 physical CPU, this should be changed to 1 VCPU per core once the issue is fixed
-                 for true SMP.
-            -->
             <vcpu id="0" cpu="0" />
-            <vcpu id="1" cpu="0" />
-            <vcpu id="2" cpu="0" />
-            <vcpu id="3" cpu="0" />
+            <vcpu id="1" cpu="1" />
+            <vcpu id="2" cpu="2" />
+            <vcpu id="3" cpu="3" />
             <!--
              The device tree given to Linux specifies that RAM will start
              at 0x40000000.