Philipp Ruemmer

Sure, I can create another release here. You can get the latest nightly build from our local Maven repository as well, but there should be a proper release on Maven...

I now published a version of OSTRICH through Maven, an example of how to use OSTRICH as a library is here: http://www.philipp.ruemmer.org/princess/ostrich-example.zip

Good point, I can update our Scala 2.13 branch. We don't want to lose compatibility with Scala 2.11, which is still producing the fastest bytecode by some margin; in our...

In case you want to switch back, I also just published a Scala 2.13 build of Ostrich 1.1 on Maven.

That exception indicates an occurrence of str.replace in which the second argument is symbolic, and not a concrete string. For which test case or input does this occur? Note that...

|Rationals.ring2int| is the right function, it represents the floor operation. However, since we currently don't have a decision procedure for the combined theory of ints and rationals, you might well...

The encoding of such operations combining ints and rationals should be correct, you should not see any wrong answers, but you might see cases of non-termination due to incompleteness of...

There are two ways to solve this: either we add explicit clauses defining multiplication, division, etc.; or we rely on the Horn solver to provide according operations. I'm inclined to...

That makes sense for real numbers, but for integers (which are more important for Java of course) we can actually choose a complete encoding of multiplication. Something along the following...

I have been trying to hunt this down, but not able to get any further right now. The problem is that the Java expression `UnsatInstOf.class` is translated to a CFG...