Dear Maude Abusers,

A new alpha release can be accessed at SRI-CSL in:

~eker/public_html/Maude/Alpha89d/

or downloaded from:

http://www.csl.sri.com/~eker/Maude/Alpha89d/

Alpha release site authentication:

User Name: maudeabuser
Password: bughunter

These is bug fix release to fix a critical problem in unification sort
computations exposed by the following example from Santiago:

fmod TEST is
   sort Msg .
   sort Fresh .
   sort FreshSet .
   subsort Fresh < FreshSet . *** Uncomment this and it crashes

   --- Sort Information
   sorts Name Nonce Key Enc .
   subsort Name Nonce Enc Key < Msg .

   --- Encoding operators for public/private encryption
   op pk : Key Msg -> Enc [frozen] .

   --- Nonce operator
   op n : Name Fresh -> Nonce [frozen] .

   --- Principals
   op i : -> Name . --- Intruder

--- Associativity operator
   op _;_ : Msg  Msg  -> Msg [gather (e E) frozen] .

endfm

red in META-LEVEL :
metaUnify(
upModule('TEST,true),
'_;_['#3:Nonce,'n['#4:Name,'#5:Fresh]]
=?
'#1:Msg,
6, 0) .

What is happening is that on certain branches through the sort
computation code, new BDD variables are not being allocated. Whether
this causes a problem or not depends on whether there are enough BDD
variables lying around from previous sort computations.

Steven