search

dafny-lang / dafny

Dafny is a verification-aware programming language
https://dafny.org
Other
2.9k stars 260 forks source link

Guarantee same diagnostics between `verify` and `server` commands #3109

Open keyboardDrummer opened 1 year ago

keyboardDrummer commented 1 year ago

Add a test that verifies dafny server produces the same SMTLib as dafny verify

robin-aws commented 1 year ago

Lots of things

LOL

Is making verification consistent in scope?

keyboardDrummer commented 12 months ago

Lots of things

LOL

Fixed 😅

Is making verification consistent in scope?

Was not but is now :)

keyboardDrummer commented 8 months ago

This has mostly been resolved by https://github.com/dafny-lang/dafny/pull/4798 and https://github.com/dafny-lang/dafny/pull/5008

I wonder what we can further do to guarantee same generated SMT between server and CLI