Nevertheless I think you should do a comprehensive list what your tool can detect and what not, instead of some examples. From the sample programs i learned that it can check two programs for semantical equivalence and can detect undefined behavior. I did not get the example with the memory violation, as symbolica.h is not included in the code. Additionally, your tool could create test cases that trigger the error, afaik.
Regarding the feedback for the user, as multiple others have mentioned, the running time is very long and thus a simple timer may not be sufficient. But I do not have an idea how to improve that.
I am not sure if you are working on the target program directly, or on the compiled binary. In the example with the division by zero, there is a print statement in order to stop the compiler from removing dead code. But I do not understand where you need a compiler, if you are working directly on C. On the other hand, when you are working on the compiled binary, then your tool is very similar to other symbolic execution engines, such as angr.