There is no bug.
The problem is the following line of code:

       expressions.add(context.MkForall(sorts, symbols, body, 0, null, null, null, null));

This MkForall is building a quantifier by binding in body the free variables: var 0 and var 1. It binds two variables because sorts and symbols have size 2. Moreover, it associates the names in symbols with these variables. Since body does not have free variables, the quantifier is equivalent to body.

In Z3, the free variables are created using the function mkBound (MkBound in previous versions). This function takes two arguments: int index, Sort ty. The index is the de Bruijn index for the variable.

In the past, several users complained that de Bruijn indices were not "user friendly" and were hard to use.
Then, we included a new mkForall API that takes a vector of "constants" that should be transformed into variables. In this API, Z3 automatically converts these constants into free variables and invokes the old API.

If we replace the line of code above with:

        expressions.add(context.MkForall(new Expr[]{obconst, pconst}, body, 0, null, null, null, null));

We get the expected quantifier. This version reflects your true intention, since you created the constants obconst and pconst and used them to create body.

We may ask, why Z3 displayed the following output when we executed your program?

(solver
(forall ((ob SimpleObject) (p Int))

(let ((a!1 (= (var (target (ptr p))) ob)))
(let ((a!2 (and a!1 (= (shift (ptr p)) 0))))
  (=> a!2 (= (dereffrom p) (value ob))))))

(= (var Va10) objVa10)
(= (value (var Va10)) 123)
(and (= (target objVp10) Va10) (= (shift objVp10) 0) (= (ptr Vp10) objVp10))
(= (dereffrom Vp10) 124))

The pretty printer missed a name clash between the constants ob and p and the variables named ob and p. The pretty printer should have renamed the variables ob and p when displaying the formula to avoid the clash and all this confusion.

Thanks to Leo for identifying the problem and proposing a fix. I would just like to add that the testcases that were submitted for this issue are based on an old version of the Java API. Most function calls have since been renamed to comply with the usual Java naming conventions and the version that will be released with the next Z3 release will use this new naming scheme.

Thank you very much for resolving this so fast!
This string representation was a bit confusing.
You saved lots of time to me.