Incomplete encoding of && in for loops

[HSMF]

In the following snippet, gobra is unable to verify the assertion inside the loop body

package main

func something() bool { return true }

func foo(a, b int) {
	for a < b && something() {
		assert a < b // Assert might fail
	}
}