"Simple" bug in Attributed Variables (2)

Here is a bug in attributed variables that seems to
indicate some strange compiler interaction. The
offending program was distilled from one where I
initially suspected indexing instructions, so the
underlying problem may be more general. The results
also differ whether we have trace on or off.

I hope finding the problem would be relatively easy.
Please let me know when you fix this.

Happy hunting!
- CR

:- import put_atts/2, get_atts/2 from atts.
:- import attv_unify/2 from machine.

:- attribute skolem/1.

%% Check if Var can be unified to Value,
%% where Var is a skolem constant
%% Value may be another skolem constant or a term
%% A skolem constant unifies only with another
identical constant.
verify_attributes(Var, Value) :-
get_atts(Var, skolem(X)), % Get the attribute
of Var
var(Value), % Value must be another skolem
constant
get_atts(Value, skolem(Y)), % Get the other
constant
X == Y. % Var and Value unify only if their
% "constant" fields are identical.

%% Generate a new skolem constant
newvar(Var) :-
(is_attv(Var) % is Var already known to be a
skolem constant?
-> true % then no need to do anything
now
; put_atts(Var, skolem(_)) % generate
a "fresh" variable as the
% attribute of Var
).

same(X, Y) :- X=Y, nop.
nop.

/** Example trace illustrating the bug:
% same/2 differs from =/2 due to a trailing (fact) nop.
% So we'd expect not(same(X,Y)) and not(X=Y) to give
identical results.
| ?- [bug2].
[Compiling ./bug2]
[bug2 compiled, cpu time used: 0.0500 seconds]
[bug2 loaded]

yes
| ?- newvar(X), not(same(X, a)).

X = _h191;

no
| ?- newvar(X), not(X=a).

no
| ?-

*/