Fix regression tests

[schuessf]

On the Nightly build 405 we had 320 failed regression tests. To improve our workflow we should avoid failures of regression tests in the future.

Issues with test-suites/verdicts:

• QvasrAbstractionJoinTest: Flaky test, sometimes works and sometimes not.
• FastUprTest: Some tests because the result is not equivalent to the expected verdict or we fail to show the equivalence.
• MonniauxMapEliminatorTest: Expected verdict broken?
• AuxVarInCall.bpl and Overapproximation.bpl contain overapproximation flags and therefore the expected result cannot be safe.

Tests that succeed locally, but fail in Jenkins-Build:

• ParallelCompositionGeneratorTest: JAXBException expected:<...2) === (); {} ===> ([4), (2) === (); {} ===> (3])]> but was:<...2) === (); {} ===> ([3), (2) === (); {} ===> (4])]>
• RundefinitionTest: JAXBException
• Tests with toolchain MonniauxAutomizerBpl.xml: Did not find plugin with id "de.uni_freiburg.informatik.ultimate.plugins.icfgtransformation"
• MonitoredProcessTest.testProcessToolchainTimeout: Process is still running (works sometimes locally)
• SystemTest (from SmtInterpol): Currently not working because of some path issues, was fixed on this branch, this reveals some real issues (ArrayIndexOutOfBoundsException).

Issues with AutomataLibraryRegressionTestSuite:

• MixedAcceptingStates*.ats (NWA DelayedSimulation): Result of operation minimizeNwaPmaxSatDelayedBi is wrong (according to its checkResult method)
• MinimizeNwaPmaxSat_TestSuiteUsage05.ats: Operand contains transition twice
• MinimzeNwaPmaxSatDelayedTest_simpleExamples.ats: Missing variable
• ConceptualProblemDelayed02-NiceMountain.ats: Assertion failed
• BothSyncMethods.ats (petri net): Assertion failed
• BugBlackAndWhiteProduct.ats and difference-Egypt.ats (petri net): Wrong difference
• GlobalWeekForFuture01.ats (petri net): Dummy action is synchronized and therefore leads to a NullPointerException
• Kerala-TwoThreadOneRessource-difference.ats (petri net): "Must not add place twice". It looks like it is not handled correctly in the difference, if one place occurs in the minuend and the subtrahend.
• minimize_hopcroft_01.ats (tree automata): Result of operation minimizeNftaHopcroft is wrong

Issues with ReqCheckerRegressionTestSuite:

• rtinconsistency_test5.req: SmtInterpol ignored the timeout there
• rtinconsistency_test112.req: Timeout during simplification with SmtInterpol
• bug_465_ex03.req: Rt-inconsistent requirements different
• ex-527-ex01.req, ex_527_ex02.req, ex-530-ex01.req, ex-rtinconsistent-04.req: Vacuous requirements different
• vacuity_test14.req, vacuity_test25.req, vacuity_test30.req: Timeout with Z3 on simplification

Other Issues:

• PdrAutomizer: SIMPLIFY_QUICK does not support simplification with respect to context, should we use another simplification technique?
• PdrAutomizer: UnsupportedOperationException: Solver returned unknown
• recursive-CallABAB_incorrect.bpl (abstract interpretation): Looks like an actual unsoundness.
• overflow.c: We currently do not add any in-range-assumptions for parameters. This can be unsound, if we are in library mode (i.e. the entry-method is not declared). Should we adapt this or is the library mode not important enough for us? An easy fix would be to always assume that the arguments are in range, but not sure, if this is desired.
• Enum03-Unsafe.c: ClassCastException: class CEnum cannot be cast to class CPrimitive in TypeSizes.extractIntegerValue
• Some Float tests with MathSAT (e.g. this): SMTLIBException: The CNF conversion does not support quantifiers
• ctrans-float-round.c: unknown symbol: roundNearestTiesToAway (with two strategies); Problem with MathSAT?
• float22_simplified.c, ctrans-float-union.c: Sort Array not declared
• ctrans-float-union.c: The translation of unions is unsound.
• SubwordAccess.c: Looks like an actual unsoundness, how should we proceed with that?
• Bug_ProcedureDNF.c (LTL): Assertion error in "old" map elimination
• Some tests of ChcRegressionTestSuite fail because of issues in TreeAutomizer or because external solvers (like Z3) time out.
• LTLAutomizer: AssertionError: No corresponding entry node for exit node with procedure main
• UpAndDownGlobalReals.bpl: AssertionError in SMTInterpol (Interpolator$MixedLAInterpolator::convert)
• builtin_ffs.c (with bitvector settings): IllegalArgumentException: incompatible types LONG INT
• structFlexibleArray01.c: NumberFormatException: For input string: "18446744073708317049"
• flexible_array.c: Unsoundness with bitvector translation

Unsupported features:

• SyntaxSupportMixedIntReal2.bpl: PolynomialRelation does not support mixed sorts. The problem is that we do not really support ranking functions for real variables, since most constants and variables created in the termination analysis have the sort int. Therefore we often create terms with inconsistent sorts.
• multipleCallSuccessors-01.bpl: State has more than one call successor
• C2BoogieRegressionTestSuite: All the failing tests are currently unsupported cases, do we want to keep those as regression tests?
• Some tests of the RegressionTestSuite (e.g this) also fail, because we don't support a specific feature.
• ConstArray.bpl: SMTLIBException: Const is only supported for infinite index sort (with three settings)
• InParamRenaming.c: Issue with renaming parameters that are used in ACSL
• NonterminatingForLoopSafe.c: Some settings don't support non-linear arithmetic, we could however just simplify this example, the intention would remain the same.

Tests fail with unknown/timeout:

• Several SMT tests are too hard for the underlying solver and should not run in regression tests.
• Most of the other tests (e.g. from RegressionTestSuite) simply always fail, because we say unknown or have a timeout (at least for some of the settings/toolchains). We should try to fix them and otherwise find a way to ignore these failures in the test result.