diff --git a/src/test/resources/regressions/issues/000659.gobra b/src/test/resources/regressions/issues/000659.gobra new file mode 100644 index 000000000..7c6ecb2d9 --- /dev/null +++ b/src/test/resources/regressions/issues/000659.gobra @@ -0,0 +1,33 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +package issue659 + +type Node struct { + ok bool +} + +pred (s *Set)mem(){ + acc(s) && + acc(s.nodes) && + forall i int:: i in domain(s.nodes) ==> acc(s.nodes[i]) +} + +type Set struct { + nodes map[int]*Node +} + +requires s.mem() +requires acc(n) +requires !(k in unfolding s.mem() in domain(s.nodes)) +func (s *Set) add2(n *Node, k int){ + unfold s.mem() + _,ok := s.nodes[0]; + if ok { + s.nodes[k] = n + fold s.mem() + //:: ExpectedOutput(assert_error:assertion_error) + assert false // should fail + return + } +} diff --git a/viperserver b/viperserver index a474657fa..8ac486e32 160000 --- a/viperserver +++ b/viperserver @@ -1 +1 @@ -Subproject commit a474657fa402c6c88da590525be790d3e16aadd8 +Subproject commit 8ac486e32dc2b45d82c345dfbf9602468b3b6682