Arshavir Ter-Gabrielyan

Here's an example of datatype usage from [F*](https://github.com/FStarLang/FStar), a software verification framework that works atop Z3: Declaration: ```SMT2 (declare-datatypes () ((Fuel (ZFuel) (SFuel (prec Fuel))))) ``` Examples: ```SMT2 (declare-fun MaxIFuel...

Here at ETH Zurich, we are working on a Visual Studio Code extension for a sound deductive verification tool Viper (viper.ethz.ch). The extension could be found here: https://marketplace.visualstudio.com/items?itemName=rukaelin.viper-advanced We use...

Is this the intended behaviour?

From the discussions about the termination plugin that we had, I concluded that the ```deactivated``` flag should be switched on if there are no decreases clauses in the program, but...

Yes, when caching is enabled, the transformations affect the information about which nodes have been cached. I files a separate issue for that one: #451

While installing the extension from this branch, I've experienced the following minor hick-ups: 1. Needed to run `npm install run-a --dev` (maybe repeating `npm install` would have sufficed) 2. Needed...

Also, one probably needs `code --force --install-extension `pwd`/vscode-motoko-0.5.3-viper.vsix`

Thanks for looking into this. Feel free to decide what to do with the ticket (I just wanted to somehow keep track of the incompletenesses we stumble upon to make...

Could you add instructions here on how to get the current version of the tool working with the motoko-san extension, please?