Daniel Nezamabadi

Strange output when reporting quantifier instantiations using newer Z3 versions

1

When using Z3 version 4.8.12-31 (Debian) or 4.12.4 (current upstream), running ```sh ./silicon.sh --numberOfParallelVerifiers 1 --z3Args "smt.qi.profile=true smt.qi.profile_freq=1" prog.vpr ``` prints ``` Invalid quantifier instances line from prover: [quantifier_instances] $Set[Int]_prog.equality_definition...

Use named axioms instead of anonymous axioms

2

At the moment, it seems that Gobra uses [anonymous quantified axioms](https://github.com/search?q=repo%3Aviperproject%2Fgobra+anonymous+forall&type=code). This makes measuring the quantifier instantiations as described in this [Silicon PR](https://github.com/viperproject/silicon/pull/587) harder for those axioms. If possible, it...

`dafny run` crashes on `print @"\";`

1

### Dafny version 4.7.0+769d1572fdd799c7bf76b78a3bc9cb94d18aac59 ### Code to produce this issue ```dafny method Main() { print @"\"; } ``` ### Command to run and resulting output ```code dafny run crash.dfy Dafny...

Dafny IR does not generate modules in dependency order anymore

1

### Dafny version 4.8.0 ### Code to produce this issue _No response_ ### Command to run and resulting output _No response_ ### What happened? Previously, the Dafny IR generated modules...

### What change in documentation do you suggest? The [INSTALL page on the Wiki](https://github.com/dafny-lang/dafny/wiki/INSTALL) mentions ``` `make z3-ubuntu` ``` for installing from source under Linux. While this command seems to...

Dafny IR contains singleton tuples when compiling pair with ghost

3

### Dafny version 4.7.0 ### Code to produce this issue ```dafny method Main() { print ("ab", ghost "ab"), "\n"; } ``` ### Command to run and resulting output ```code [Module...

### Dafny version 4.8.0+5faf876b2c768c61044b8f87825385682b6e772d ### Code to produce this issue ```dafny method Main() { print "hello from main"; } method foo() { Main(); } ``` ### Command to run and...

Improvement suggestions for the Dafny AST (AST.dfy)

3

### Summary Various suggestions to change the [Dafny AST](https://github.com/dafny-lang/dafny/blob/master/Source/DafnyCore/Backends/Dafny/AST.dfy) to make it, and using it for compilation easier. ### Background and Motivation I am currently working on a [project](https://github.com/CakeML/cakeml/tree/dafny) to...

Make "modern" Definition syntax extensible

5

Currently, the attributes for the "modern" Definition syntax seem to be fixed. This means that in some cases one has to fall back on using the "old" style `Define`. For...

As suggested by @myreen on Discord, the definitions in `libScript.sml` should be removed if unused, moved to `miscScript.sml`, or upstreamed to HOL4 (where it makes sense).