Input {48, MemoryConstrained[...]} cannot be evaluated, cause: {HoldForm[MessageName[ForAll, "msgs"]]} about keymaerax-release HOT 2 OPEN

The error message means that there is a warning generated by Mathematica/Wolfram Engine, but KeYmaera X couldn't retrieve it for display on the UI. Instead, we display the attempted query. When copying that attempted query and evaluating it in Mathematica or Wolfram Engine directly, the message usually appears on their debug output.

There can be several reasons for warnings in Mathematica, but in this particular case there is a division by zero in some of the "irrelevant" other assumptions.

Once the assumptions that use division by zero are hidden, the QE call on this particular proof obligation succeeds. However, unless the assumptions are completely irrelevant for the entire proof, or you are branching on a quantity (0 vs. !=0) where on the 0 branch the affected assumptions are irrelevant, sooner or later there will be a proof obligation that cannot be proved because of the division by zero.

from keymaerax-release.

Great, thank you very much! That helps a lot. I apparently tried to simplify a model a bit too much.

Would it be possible to add the suggestion of entering the query directly in Mathematica/Wolfram Engine to the error message when the warning retrieval fails? Now I know what to do, but I imagine it could be helpful to others.

from keymaerax-release.