Markus Alexander Kuppe
Markus Alexander Kuppe
This change seems to make the difference: https://github.com/JohnnyTheTank/apiNG-plugin-rss/commit/df22fe39319ae021dfe33d35dcab86fdb8e0880e @jlengrand Thanks for digging into this.
Fundamentally, I don't care where z3 is coming from. ```shell root@sv-c2-large-arm-01:~/# uname -a Linux sv-c2-large-arm-01 5.4.0-40-generic #44-Ubuntu SMP Mon Jun 22 23:59:48 UTC 2020 aarch64 aarch64 aarch64 GNU/Linux root@sv-c2-large-arm-01:~# free...
The z3 loader doesn't know about `aarch64` but seems to [just copy the libraries](https://github.com/tudo-aqua/z3-turnkey/blob/master/src/main/java/com/microsoft/z3/Z3Loader.java) to some location from where Java picks it up. For those that run into this problem:...
@konnov https://github.com/informalsystems/apalache/issues/130#issuecomment-743165594 :-)
Is this issue perhaps related https://github.com/tlaplus/tlaplus/issues/471 ?
```tla Spec == Init /\ [][TRUE]_x ``` also not accepted.
```tla ------- MODULE Foo ------- EXTENDS Integers CONSTANT \* @type: Set(Int); S ConstInit == LET ss == SUBSET {1,2} sss == ss \ {{}} IN S \in sss VARIABLE \*...
> The main reason for keeping `CHOOSE` non-deterministic was to reduce complexity of recursive operators that heavily depend on `CHOOSE`. Once we support the fold operator, this should be less...
See the warning in 14.6 of Specifying Systems (p. 262). In practice, the given example is too simple, though: ```tla Welcome to the TLA+ REPL! TLC2 Version 2.16 of Day...
(Leslie agreed to make the aforementioned discussion public) @xxyzz: > I presume you're talking about the weakening of the semantics of CHOOSE on page 262 of "Specifying Systems". The weakening...