* We (probably) need to instrument the SUT with angelixOutput. Then compile it beforehand with dependency
(classpath) including the jangelix.jar. For example, with the distance test, we compile test (from test folder) by:
javac -cp ../main/:/home/dxble/workspace/jangelix/out/artifacts/jangelix_jar/jangelix.jar  Distance1Test.java
where ../main is path to the SUT (Distance.java)

* Test files of SUT must end with Test, etc, see TestCase.isTestFile in testrunner package

* now working examples: field, for-loop, distance, if-condition

* Handling PC generated from JPF-Symbc:
    - PC is generated by the CustomUnitTestCaller (if nothing wrong happens e.g., array out of bound),
      otherwise it is generated by MySymbolicListener in propertyViolated() method
    - if PC is generated by CustomUnitTestCaller, it is concatenated and written to file. This is because
      we may have many paths to explore and lead to expected output. For example, see Distance test with test value
      4 5 6 7 as in evaluateDistance3() in Distance1Test.java

* BE CAREFUL with Junit assert method. Use them correctly so that symbolic execution can also run correctly.
 I encountered an odd error before, where I incorrectly used assertEquals(true, some method),
 which should correctly be assertTrue(some method). This oddly leads to error saying symbolic string analysis,
 not handle ObjectEquals, etc.

* BE CAREFUL with assert file. If expected output is double, write in double format, e.g., 1.0 instead of 1
This is because we parse output and convert it into according form, e.g., 1 => integer, 1.0 => double

* This is how we handle method call:
    - WriteFault2SMT: name mangling
    - InstrumentUtils#createChooseNode:
    - InstrumentUtils.createdMethodCalls
    - MethodCallRunTime
    - BackendInstrument