Program Analysis on a Wargame Binary

Question

I've recently took it upon myself to research more about reverse engineering, I'm currently testing my intermediate skills on various CTF hosting sites. Interestingly enough I have come across a challenge on this particular site:

0x0539.net

Now the challenge I'm focused on at this moment in time is Very_Malicious

So far what I've gathered about this challenge is that it has some form of program obfuscation, in this case the obfuscation I've identified is a VM (Virtual Machine) which fetches and decodes a large set of opcodes. The opcodes are stored within the same function as the entry point of the program.

Now I have identified each of the custom VM instructions and have created a very short IDA Python script to extract the bytecode. It isn't ideal but it does what it is suppose to do.

dism_addr = list(FuncItems(0x1b4c))
for addr in dism_addr:
    if "mov     byte ptr [rax]," in GetDisasm(addr):
        print(GetDisasm(addr))

After creating a disassembler for the challenge, I'm curious if there is a better way to solve this challenge rather than spending a couple of hours (2/3) reverse engineering. I've read about Symbolic Execution and my question is:

How would a reverse engineer solve a challenge like this using Symbolic Execution?

Please refrain from posting flags, I just want a thorough explanation on what I could do to solve this more efficiently and quickly.

Any help is appreciated, thank you for taking the time to read my question!