karthikbhargavan

Needs Design: Allow &mut and raw pointer returning functions in interfaces

1

We currently do not support code that returns `&mut` or `*mut` and more generally we ban these patterns from appearing in many places in the AST. However, it may be...

Deep updates in F* blows up memory.

2

We do not have a small reproducer, but deep updates in F* are causing a memory blow up. Two of these patterns are: * `a.coefficients[i] += 3` * `a[i][j] +=...

Debug Asserts with arguments throw an error in F*.

1

```rust fn f(x:u8) { debug_assert!(x > 0, "x is {}", x) } ``` [Open this code snippet in the playground](https://hax-playground.cryspen.com/#fstar/d3313f9a7f/gist=bf912db17ba18ea5632cca38322f4c77)

change z3 version to 4.13.3

8

I am sure there may be a better place to put the `--z3version` but with this change, KaRaMeL works with the latest F* and Z3 4.13.3

The following snippet works on the F* command-line but fails in emacs. ``` [@@ "opaque_to_smt"] let f (_: Prims.unit) : Prims.unit = () ```