Add TaskSolver as abstraction layer over ModelChecker

[ThomasHaas]

This PR adds a new abstraction layer before the ModelChecker. For now, this layer does not do much apart from choosing the appropriate ModelChecker and managing timeouts.
However, the intend is to make this layer more powerful in the future and enable more interesting solving approaches such as:

• Automatic bound unrolling without external script
• Running SMC for some time and if SMC solves the task in, say, < 1000 explored executions, then we are done. Otherwise, fall back to BMC but exploit information gathered from SMC (loop bounds, indirect call targets, aliasing information, summary of sequential prefix, etc.).
• Parallel solving via decomposition?
• "Proof mode" that first unrolls loops until completion and only then checks the properties of interest. This can be a lot more efficient if the program is likely to be correct.
• State-space exploration mode for compilation correctness.

TODO: Update reflection metadata for native build.

EDIT: I also added a TaskResultAnalyzer class that is now responsible for generating the ResultSummary and witness files. Basically, I moved all output generation from Dartagnan.java to TaskResultAnalyzer

EDIT 2: I took the freedom to clean up Dartagnan.java. I think it is a lot easier to follow the logic of Dartagnan now.

[xeren]

You should capture timeout and modelChecker in the lambda's closure, or join timeoutThread in run(). The accesses here are potentially racy, e.g. with modelChecker = null in close().

[ThomasHaas]

I guess we could add a join() after the interrupt(). The join should then return more or less instantly.

The case you have in mind seems to be an extreme edge-case where the model checker returns right before the timeout, the interrupt gets send but doesn't arrive quickly enough (though the target thread is sleeping and therefore listens to interrupts) before the task solver gets closed and the timeout thread reaches its timeout.