dafny icon indicating copy to clipboard operation
dafny copied to clipboard

Published 20 hours ago • verified publisher icon dafny-lang

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

Open keyboardDrummer opened this issue 2 years ago • 3 comments

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

keyboardDrummer avatar Nov 24 '22 10:11 keyboardDrummer

Lots of things

LOL

Is making verification consistent in scope?

robin-aws avatar Oct 17 '23 15:10 robin-aws

Lots of things

LOL

Fixed 😅

Is making verification consistent in scope?

Was not but is now :)

keyboardDrummer avatar Oct 17 '23 21:10 keyboardDrummer

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

keyboardDrummer avatar Jan 30 '24 11:01 keyboardDrummer