Possible incorrectness in backend solver for formula with disjunction below separating conjunction

[TDacik]

When experimenting with grasshopper's backend solver, I found a possible incorrectness for formulae containing boolean connectives nested below separating conjunctions. I was able to shrink my problem to the following input:

struct Node { 
  var next: Node; 
}
 
predicate lseg(x: Node, y: Node) {
 acc({ z: Node :: Btwn(next, x, z, y) && z != y }) &*& Reach(next, x, y)
}
 

procedure query(x1 : Node, x2 : Node, x4 : Node, x5 : Node, x6 : Node)
  requires (x2.next |-> x6 &*& ((lseg (x5, x6) || x4.next |-> x6) && x6.next |-> x1))
  ensures (false)
{}

Grasshopper verifies the program which should be the case iff the formula x2 -> x6 * ((lseg(x5, x6) \/ x4 -> x6) /\ x6 -> x1) is unsatisfiable. However, if I get the semantics of used SL correctly, the formula should be satisfiable in the following model:

When one removes the subformula lseg(x5, x6), the results of grasshopper is correct, so I assume that the disjunction can be the cause of the problem.