The documentation on (==) says the following:

e1 == e2 tests for physical equality of e1 and e2. On mutable types such as references, arrays, byte sequences, records with mutable fields and objects with mutable instance variables, e1 == e2 is true if and only if physical modification of e1 also affects e2. On non-mutable types, the behavior of ( == ) is implementation-dependent; however, it is guaranteed that e1 == e2 implies compare e1 e2 = 0. Left-associative operator, see Ocaml_operators for more information.

And in fact there are cases where behavior differs between bytecode and native OCaml compilers. That depends on how much sharing is done. For example, in utop "foo" == "foo" evaluates to false.
The important point is that the implication between (==) and (=) is only one way. So physical non-equality does not imply structural non-equality.

In this PR I went though physical equality usage in Goblint and changed those which happen on immutable types. On int-like types this shouldn't actually make a difference in practice, but it's just better to not rely on implementation-defined behavior unnecessarily.
Most of these are probably typos from writing == like in other languages.