henriman

The spaces specified in the `Position` of `ptz.GetStatus` are not recognized (for some reason), changing them to an empty string fixes this. Also, I changed the loop in `if __name__...

Search behavior changed

3

It seems that the behavior of the search in the app list has changed. Now, after entering a character, all apps that contain that character are listed, _in alphabetical order_...

I am working on verifying SIF for the VerifiedSCION router (using hyperGobra) with @jcp19. ```go requires forall i int :: { b[i] } 0 low(b[i]) func test2(b [2]int) { assert...

I am working on verifying SIF for the VerifiedSCION router (using hyperGobra) with @jcp19. ```go type Struct struct { length int } requires acc(s) requires low(s.length) func test(s *Struct) {...

hyperGobra: incorrect encoding of `forall` with `--hyperMode=on`

1

I am working on verifying SIF for the VerifiedSCION router (using hyperGobra) with @jcp19. ```go requires low(b) func test1(b [2]int) { assert low(b[0]) assert low(b[1]) // Fails: assert forall i...

Low sensitivity doesn't transfer when creating a slice from low values under specific circumstances

2

I am working on verifying SIF for the VerifiedSCION router (using **hyperGobra**) with @jcp19. The circumstance under which this bug occurs can be seen in the below code. Crucially, we...

I am working on verifying SIF for the VerifiedSCION router (using hyperGobra) with @jcp19, however this bug is unrelated to hyperGobra and also occurs using "normal" Gobra. I believe these...

The result of `low` is not properly assigned to `ghost` variables

2

I am working on verifying SIF for the VerifiedSCION router (using hyperGobra) with @jcp19. When assigning the result of a `low` assertion to a `ghost` variable (or returning it in...

```go type Struct1 struct { x int } decreases pure func f1(Struct1) bool requires f1(x) func test1(x Struct1) { assert f1(x) xAddr@ := x assert x == xAddr assert f1(xAddr)...

hyperGobra doesn't translate `unfolding` correctly when predicate or assertion contains `low`

1

I am working on verifying SIF for the VerifiedSCION router (using hyperGobra) with @jcp19. This issue describes two slightly different bugs, but I grouped them together for now, as I...