Dear Maude Abusers, There are issues with the Linux builds for Alpha121. They were reported by Santiago Escobar . The less serious problem is that they crash with an "Illegal Instruction" error almost immediately when run on pre-Haswell CPUs. This is because the recent version of GMP that I used for this build configured itself to use the newest instructions available on my machine - a Haswell CPU. The much more serious problem is memory corruption that only shows up in long runs that make heavy use of unification. Valgrind points the finger of suspicion at the garbage-collector in the BuDDy BDD library. BDDs are used in three algorithms in Maude: (1) Manipulation of Boolean formula during Buchi automaton construction for anything using LTL. (2) Sort computations for order-sorted unification. (3) Diophantine basis element selection for ACU unification. The reason it has shown up now is that previously the Maude binaries were built with: gcc (Ubuntu 4.8.4-2ubuntu1~14.04.4) 4.8.4 Copyright (C) 2013 Free Software Foundation, Inc. and now that my machine is running a new version of Linux, Alpha121 was built with: gcc (Ubuntu 7.4.0-1ubuntu1~18.04.1) 7.4.0 Copyright (C) 2017 Free Software Foundation, Inc. I've tried a couple of other versions of GCC, 5.2.0 and 8.3.1, and both result in memory corruption when the BuDDy garbage-collector runs. Perhaps this is to be expected - BuDDy is an old library dating from the turn of the century when x86 machines were 32-bit and it doesn't seem to have been actively maintained since about 2002. In the meantime C and C++ standards have gotten progressively stricter with respect to pointer manipulations in the interests of better optimization, to the point where it is challenging to write a standards conforming memory-manager/garbage-collector at all. GCC is noted for being ruthless about breaking code with "Undefined Behavior" wrt the standards in order the generate faster binaries. The short term fix is to use Clang for Maude and all its dependencies - this is already the standard C/C++ compiler on Darwin as well Android, FreeBSD and OpenBSD. To this end I've added two new files to the Alpha121 release directory: -rwxrwxr-x 1 eker eker 17927416 Jun 24 19:48 maude-CVC4.linux64.clang -rwxrwxr-x 1 eker eker 4979936 Jun 24 16:57 maude-Yices2.linux64.clang which are Clang compiled replacements for the buggy Linux builds. Steven