z3remote now wraps z3 on the server-side, which allows for a few optimisations:
* compress entire query at app level, rather than relying on ssh
* avoid needless round-trips: just one per query
also included the original shell script which prompted it (and works
just fine with Linux/mono -- the only reason for compiling the exe is
so that win32 Boogie can call CreateProcess on it!)
use with:
make -jN verified EXTRADAFNYFLAGS="/z3exe:tools/z3ssh/bin/z3ssh.exe /vcsCores:M"
... where N and M are adjusted to taste.
use with /z3exe:tools/z3remote.py /vcsCores:10 (or more)
in practice, this currently doesn't work very well, because the load
balancer doesn't react fast enough, and all the queries end up running
on the same overloaded server
* Dafny release v1.9.9
* Boogie master 9fbb097803c640922b71ae22141c93d0f57fcdd6 PLUS one cherry-picked commit:
a7260f1880
(attempting to make /restartProver behave more like /proc)
* Z3 master 169295c9ba74802e4e17b908982ba8a9f1c9f491
* fix verification in two places that broke as a result of the
new tools (this appears to be related to arithmetic that looks
non-linear due to the use of constants)
* bump vale version to pick up {:split_here}{:refined} assert syntax
* add some splits suggested by chris
* minor cleanup and a split in sha256_block_data_order_inner
* invoke dafny with /induction:1
The DLLs were grabbed from z3-4.5.0-x64-win.zip
Verification status ("make verified"):
(Aside from the last case, verification was continued by running touch
<FILENAME> for files that fail to build.)
- 1 timeout in ptebits.i.dfy
- Several "unresolved identifier" errors in exception_handlers.sdfy
- Unsupported expression in init_addrspace.sdfy (after which verification
could not be continued by touching init_addrspace.verified)
these binaries correspond to:
z3 release 4.5.0 x64 windows
dafny commit 28bf5d11ce1a8dc5663f1f9d04c721acae12403f
Author: qunyanm <qunyanm@hotmail.com>
Date: Fri Jan 27 21:02:58 2017 -0800
Fix incorrect translation of forallstmt
(experience suggests that trying keep track of support for multiple
versions of dafny or z3 is unproductive)
Andrew Baumann
Andrew Ferraiuolo