Improve visualization of conditions for correctness witnesses

[vmordan]

Currently conditions are the main elements, which are shown for the correctness witnesses visualization. Before visualization all conditions are combined for the same triplets <source file, line number, thread id>, and after that we can highlight conditions, for which some branches were not covered and thus should be explored by the users. But in order to do it, we need to understand, whether the given conditions cover all branches or not.

Currently only simple conditions (such as a and !a, a == b and a != b) are supported. Here are some simple ideas for improvements:

• [x] support more complex boolean operations in conditions (OR, AND, arithmetic operations, etc.);
• [ ] support different branches in switch operator (such conditions may have different line number);
• [x] support more complex conditions (such as x || y == VAR).

[kateya]

Switches are currently too hard to support. Need to understand how verifier works with them.

[vmordan]

Merged in commit 118c3af