ISLa 2.0 features substantial changes to the language and the solver implementation.
Our current plan includes the following significant changes:

1. Removal of "semantic predicates" and the "exists int" / "forall int" quantifiers from the ISLa language. Motivation: Semantic predicates are replaced by higher-order and external functions; numeric quantifiers only glued semantic predicates to other formulas.
2. Addition of the higher-order functions/numeric comprehensions/generalized quantifiers "num" and "sum." In ISLa 2.0, you would write num(<byte> b; inside(b, <packet>)) < 40 instead of exists int num_bytes: (count(<packet>, "<byte>", num_bytes) and num_bytes < 40) in ISLa 1.x syntax. The solver will at least support expressions of the shape num(<T> v; inside(v, ...)) (basically the old count semantics). The syntax will be more liberal, though.
3. Addition of "external" functions to extend the ISLa language for specific purposes. Roughly comparable to the old semantic predicates, but as expressions.
4. Replacement of the Fibonacci queue/cost function approach by random choice guided by syntactic & semantic coverage with backtracking. Motivation: The cost function is highly problem-specific. Choosing a non-optimal cost function can lead to an explosion of elements in the solver queue that will never be touched again. The need for a notion of semantic coverage has become apparent in different case studies.