Zhicheng
Zhicheng
It's seems not related to E-ACSL, I can reproduce it with `owi c`
```c #include #include void primes(int *is_prime, int n) { for (int i = 0; i < n; ++i) is_prime[i] = 1; } int main(void) { int *is_prime; is_prime = malloc(2...
> Z3 sometimes segfault randomly when generating the model. We can see it in the CI sometimes. @Laplace-Demon, if you use `--debug` could you confirm the crash is happening around...
@zapashcanon Does it mean that the crash is happening around model generation? ```sh Assert failure: false Model: (model (symbol_0 (i32 2))) typechecking ... typechecking ... linking ... interpreting ... stack...
Ok, thanks! @zapashcanon @filipeom @krtab
I added the `pure` clause in function contract which indicates the function should pass certain syntactic check to be recognized as a pure function, and is therefore in the scope...
> Is this really needed? The way I understand this is : if a function is used in a contract, it must be pure. So we check it has the...
```wasm (module (@contract $plus_three (ensures (= result (+ (param 0) 3))) ) (func $plus_three (param $x i32) (result i32) (i32.add (i32.const 3) (local.get $x))) (func $f1) (func $f2) (func $start...
> I don't understand your `add --add-assert-to-assume option`, I believe this is something that should be done at the symbolic execution implementation level directly, you should not try to emulate...