Possible inflation of ownerships by alias

[aigarashi]

Found a bug in Consort. Consider the following program:

{
  let pa = mkref 0 in
  let pb = pa in
  {
     alias(pa = pa);
     pa := 1;
     assert(*pb = 0)
  }
}

The program is unsafe, but Consort returns "VERIFIED" (at least in my environment).
The problem is in the treatment of alias(pa=pa) mentioned above.
Consort generates the following constraint:

(assert (= ovar-4 1.0))
(assert (= (+ ovar-1 ovar-1) (+ ovar-3 ovar-4)))
...

where over-1 represents the ownership of pa before the alias statement and ovar-4 is that of pa after the statement.
This allows us to inflate the ownership of pa:
if ovar-1 is 0.5, then ovar-4 can be 1.0.
In this way, we can assign
0.5 to pb; and
1.0 to pa
after the alias statement.
We should actually generate the constraint like:

ovar-1 >= ovar-10 + ovar-11
ovar-10+ovar-11 >= ovar_3 + ovar_4

instead of

ovar-1+ovar-1 = ovar-3+ovar-4.