I'm confused by the lifetime of variables bound by Twelf's %solve, and documentation does not seem to help.

Reduced.elf

% (Possible) bug report or confusing behavior.

% The code is in three parts, Part 1 is boring and 3 are boring, the interaction
% between 2 and 3 is confusing. How long is the result of a %solve directive
% supposed to persist?

% I have an Agda background and I've read some papers on Twelf.

% I've seen this bug in Emacs, but I imagine this only requires keeping the
% Twelf server alive throughout.
%
% 1. Typecheck this file - it works here, as expected.
% 2. Comment in the %solve directive in Part 2.
% 3. Now typechecking will fail, because D is know declared by %solve, while the
%    clauses of plus-z-r expect it to be free.
% 4. So comment back out the %solve directive (reverting step 2).
% 5. Typecheck again, with the same server used for 3. It will fail again, with
%    a slightly different error message!
% 6. Restart the server. Everything will be fine again!

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Part 1: a standard signature of naturals.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% (Unrelatedly, Emacs only highlights as comment the last char of the above
% %%% ... line, which seems wrong).
% also, %%% ... without a space ensures the file content is ignored. Apparently I don't get the comment syntax, nor does Emacs.

% Following a Twelf tutorial:
% http://twelf.org/wiki/Proving_metatheorems_with_Twelf

nat : type.
z : nat.
s : nat -> nat.

0 = z.
1 = s 0.
2 = s 1.

even : nat -> type.
even-z : even z.
even-s : even N -> even (s (s N)).
v = even-s (even-z).

plus : nat -> nat -> nat -> type.
plus-z : plus z N N.
plus-s : plus (s M) N (s R) <- plus M N R.
%mode plus +N1 +N2 -N3.
%worlds () (plus _ _ _).

%total N (plus N _ _).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Part 2: a solve directive triggering strange behavior
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%
% %solve D : plus (s z) (s z) N.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Part 3: a proof
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

plus-z-r : {N : nat} plus N z N -> type.
plus-z-r-z : plus-z-r z plus-z.
plus-z-r-s : plus-z-r _ (plus-s D) <- plus-z-r _ D.

%mode plus-z-r +N -D.
%worlds () (plus-z-r _ _).
%total N (plus-z-r N _).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Part 4: errors
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Error during second typechecking:

% plus-z-r-z : plus-z-r z plus-z.
% Reduced.elf:66.50-66.51 Error:
% Type mismatch
% Expected: plus X1 z X1
% Inferred: plus (s z) (s z) (s (s z))
% Constant clash
% Argument type did not match function domain type
% (Index object(s) did not match)
% Reduced.elf:66.26-66.34 Error:
% Type mismatch
% Expected: plus X2 z X2
% Inferred: plus (s (s z)) (s z) (s (s (s z)))
% Constant clash
% Argument type did not match function domain type
% (Index object(s) did not match)
% [Closing file Reduced.elf]
% Reduced.elf:66.1-66.52 Error:
%  2 errors found
% %% ABORT %%

% Error during third typechecking:

% plus-z-r-z : plus-z-r z plus-z.
% Reduced.elf:66.50-66.51 Error:
% Type mismatch
% Expected: plus X1 z X1
% Inferred: %plus% (%s% %z%) (%s% %z%) (%s% (%s% %z%))
% Type/kind constant clash
% Argument type did not match function domain type
% Reduced.elf:66.33-66.34 Error:
% Type mismatch
% Expected: plus X2 z X2
% Inferred: %plus% (%s% %z%) (%s% %z%) (%s% (%s% %z%))
% Type/kind constant clash
% Argument type did not match function domain type
% [Closing file Reduced.elf]
% Reduced.elf:66.1-66.52 Error:
%  2 errors found
% %% ABORT %%