Please apply 'ant format-diff' before commiting,
or the extended version 'ant format-source'.

Scala is not upwards and not downwards compatible.
The upcoming Ostrich library is only available for Scala 2.12,
so we downgrade Scala for Princess.

This is an initial step and the usage is still unclear. This is not tested.

…erbose.

…ntation.

… theory and arrays.

Princess intenally converts all real-arrays to int-arrays
and thus there is some casting and quantification in SMT.

Princess needs non-rational UF arguments to be explicitly casted to rational.

…rms.

# Conflicts:
#	.idea/JavaSMT.iml
#	.idea/copyright/JavaSMT.xml
#	lib/ivy.xml
#	src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java

…t should be removed once Ostrich has been updated in our own repository. The new version is needed as it fixes a bug (uuverifiers/princess#9) that affected two of our tests in StringFormulaManagerTest

…eout for Princess

…n 2 arguments

…incess does seem to support unicode characters as part of its Strings and we may just want to remove the escape sequence

…irectly

…nd an issue in Princess/Ostrich

…oid CI complaints

… See uuverifiers/princess#7 and uuverifiers/princess#8

… test uses rational numbers as indices/elements for an array, which is not supported by Princess.

…st. These were added by accident: Ostrich 1.3.5 only requires 13 arguments, while the new version 1.4-pre requires 15

…bers as array elements. See c89c6ac

…Prover from intSymbols` to `theorySymbols` as it may not only contain integer variables.

…s. Extending the partial model does not seem to work in this case, so we need to (temporarily) add the formula to the assertion stack and then re-run the sat-check to get the value. This should work around the issues in uuverifiers/princess#7 and uuverifiers/princess#8

…-singleton strings as their arguments. Ostrich does not support such operations yet, although the feature will likely be added later. See uuverifiers/ostrich#88 for some details.

…est. This one was disabled by accident in the last commit.

… This bug has been fixed in uuverifiers/ostrich#87

… constant symbols. Princess will generate terms like (Rat_int(-1 * Rat_frac(0, 10)) that would have to be rewritten first before they can be evaluated to a rational number.

…o crash when non-linear terms are used

…se are only needed for Ostrich 1.4 and later.

…n was not reflexive and returned `false` if both arguments are the same. This has reported in uuverifiers/ostrich#89 and is now fixed

…ls (f.ex "1/3 <= y"). This extends the workaround we already use for terms to equations as Princess seems to have a bug when it comes to evaluating rational terms

…or-princess

… rationals (f.ex "1/3 <= y"). This extends the workaround we already use for terms to equations as Princess seems to have a bug when it comes to evaluating rational terms"

This reverts commit 3b7229a

…eger terms

…ager

…variable by zero returns an integer term

…ese were temporarily disabled due to a bug that has now been fixed. See uuverifiers/princess#11

…. The problem here is that Princess introduces quantifiers when rationals are used, not that arrays can't be combined with rational numbers.

…upport division by zero, but it currently seems to be broken for rationals (at least with the way we're using them)

…incess to crash when non-linear terms are used"

This reverts commit 3bc04a8.

…trich to the latest release

…FormulaManager, rather than an AssertionError