./verified/remove.vad(76,56): Error: assertion violation

[xiexiewww]

when I make verified,there is a error in remove.vad,line 76
line76: assert extractPageDbEntry(this.m, as_page) ==
extractPageDbEntry(old(this.m), as_page);
I do not kown why?
who can help me?
Thank you very much!

[xiexiewww]

Anyone here?
Emm.............

[0xabu]

This definitely worked for us, but unfortunately the verification tools can be unstable on different machines/environments. Are you using the same versions of the dafny, Z3 and boogie binaries included in the repository? Can you copy and paste the exact error message and the steps you used to recreate it?

[xiexiewww]

We used boogie binaries and dafny in the repository.But,we can not make verified (because it can only find z3.exe,but it can not work, and it suggested us to install z3) until we installed Z3(linux distribution for ubuntu 16.04), it may cause this problem,we run this project on ubuntu17.so,which z3 should I Iinstall?
Thanks very much！

[0xabu]

The Windows x64 Z3 binary in our repo is built from commit 169295c9ba74802e4e17b908982ba8a9f1c9f491, so if you wanted to be sure you could build Z3 for Linux at that specific commit. For a near guess, try the next Z3 release which would be 4.6.0, but I can't guarantee it will work.

[xiexiewww]

It can not work,because we used z3(4.6.0)....haha😂😂

[xiexiewww]

I will try it next day,thanks very much!Good night!

[Davidleeh]

Encountered the same issue here...

Same as @xiexiewww , cannot use z3.exe in the repo since:

Under Ubuntu 18.04, the SConscript (line 171-184) in tools/vale/tools/Vale cannot locate z3.exe since the path "/proc/sys/fs/binfmt_misc/WSLInterop" is not existed. Therefore it has to find "z3", instead of "z3.exe". Hacked the script to search for "z3.exe", then there was "FATAL UNHANDLED EXCEPTION: System.AggregateException: One or more errors occurred. ---> System.IO.IOException: Write fault on path" error.

Natively building z3 4.7.1 solved the above issue, but encountered the same error:
"
Verifying Impl$$_module.__default.va__lemma__kom__smc__remove__non__addr__success ...
[16.844 s, 456 proof obligations] error
./verified/remove.vad(76,56): Error: assertion violation
"

Seems related to pagedb.*... Any hints? Thanks!

[Davidleeh]

Update:

As @0xabu mentioned, natively built z3 with the specific commit solved the issue.

Z3 version 4.5.1 - 64 bit

Might be able to close this issue. :)