Federico Poli

I observe that this message is printed to stdout. Is there a way to avoid that? It pollutes Prusti's output.

> Since the [message is a logger warning](https://github.com/viperproject/silicon/blob/master/src/main/scala/supporters/functions/HeapAccessReplacingExpressionTranslator.scala#L154), you could set Silicon's log level to error (`--logLevel ERROR`), which should suppress any message of lower severity. Thanks!

The recent Windows CI failures seem related to this issue. After the test suite successfully terminates, `prusti-server-driver.exe` is still running while `prusti-server.exe` is not. The proper solution used in cargo...

> To keep things simple for the verification tool, the specification language should be completely pure, so the borrow-checker would not need to run on the specs (the lifetime should...

The error message is reporting that the string used in the `println!` is not supported. At the moment, there is not much that we do to veryify I/O or string...

Wow, thanks! I'm not sure why the CI is not running. Even if it's a draft, I was wondering if you considered moving `native_verifier` *outside* `viper`, because the API of...

* Use `git rebase -i master` to remove 4b055b7b4edb49a03141732dc1a64285129b9dcc and 5484ca74c2d742325f4933a61d4c0e20fc5c403c. * Remove `.DS_Store` (from the history of the PR, not in a new commit) and add it to `.gitignore`.

Is there a clear advantage in splitting `backend-common` out of `viper`? All its current content (java exceptions, verification results, silicon counterexamples) can still be seen as part of Viper, and...

I notice that the PR runs `cargo fmt` on `prusti-viper`, but from the diff it's difficult to see if you made more changes in there. Could you try to reformat...

Could you describe how to reproduce this issue? Do you run `cargo prusti` or something different?