Fix soundness bug in SdHoareTripleChecker

[maul-esel]

This change fixes an unsoundness bug in SdHoareTripleChecker, shown by the failing test HoareTripleCheckerTests::sdHtcTest02.

(It's probably best to review the two commits separately.)

[maul-esel]

After discussion with @Heizmann, we have decided to spend a little more time on this and make sure all soundness issues surrounding constants in the SdHoareTripleChecker are fixed (e.g. also for call / return), and to add missing support for axioms.

[schuessf]

Compared the latest nightly build #53 with the reference build #302 of the reference branch.

The following tests failed:

• I_programs_regression_c_NutzTransformation02.c S_programs_regression_c_BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf T_programs_regression_c_BlockEncodingV2AutomizerC.xml (de.uni_freiburg.informatik.ultimate.regressiontest.generic.RegressionTestSuite)
• I_programs_regression_c_TestIntegerDivision01.c S_programs_regression_c_AutomizerC-BitvectorTranslation.epf T_programs_regression_c_AutomizerC.xml (de.uni_freiburg.informatik.ultimate.regressiontest.generic.RegressionTestSuite)

Please check these tests before merging this PR.

[maul-esel]

In its current form, the PR

• fixes a known bug with constants in internal statements
• refactors and simplifies the code (though more could be done, especially for calls and returns, in the future)
• adds a number of additional unit tests for Hoare triple checkers, including one test that reveals an existing bug in the handling of calls

Things left to do in the future:

• further refactor and simplify the code
• document the assumptions made about call and return statements, including in the case of interprocedural compositions
• make fewer assumptions
• implement IAbstractPredicate::getConsts and fix the bug with calls
• ensure support for function symbols and axioms

As discussed, I'll merge this PR now.