Error with derived axioms database in KeYmaera 5.0.2

[ytzemih]

Hi, I'm running KeYmaera X 5.0.2 on my Ubuntu 22.04 machine (plain, just using Z3). I've completely removed the ~/.keymaerax directory to also avoid clearing the cache. But the error remains, only the line about "Clearing your cache" is gone. It seems that my Java version is alright. Assuming that this type of error might be somewhat concerning despite its about derived axioms. I thank you for some help.

[launcher] Restarting KeYmaera X with sufficient stack space /usr/lib/jvm/java-17-openjdk-amd64/bin/java -Xss20M -da -jar keymaerax.jar -launch -ui WARNING: sun.reflect.Reflection.getCallerClass is not supported. This will impact performance. [launcher] Database version: 4.8.0 Clearing your cache because of an update. Error deriving axioms, KeYmaera X continues with restricted functionality; details: WARNING: Encountered 19 errors when trying to populate DerivedAxioms database. Unable to derive: timesDivInverse powNegOne powerLemma timesPowersBoth powerEven powerOdd divideNumber divideRat divideNeg normalizeCoeff0 powerDivideEven powerDivideOdd ratFormAdd ratFormMinus ratFormDivide ratFormTimes ratFormNeg taylorModelPowerEven taylorModelPowerOdd

[Garmelon]

As far as I know, Z3 is unable to prove all the derived axioms by itself. However, setting AXIOM_DERIVE_TIMEOUT to a higher value (for example 30 for 30 seconds) in your keymaerax.conf might allow Z3 to prove at least some more axioms.

Mathematica with a sufficiently high timeout is able to prove all derived axioms, though the default timeout is maybe a bit too short.

[ytzemih]

Thanks, @Garmelon . This is very helpful. Perhaps, a hint like this would also be useful in the error message.