Here is a demonstration involving two decision problems (where evalf is applied to the output for better readability):
As you can see, the
SMTLIB:-Satisfy command fails to work in Maple 2023, and I have to install the Visual Studio 2013 (VC++ 12.0) manually. But unfortunately, even if I have installed the vcredist_x64.exe beforehand, the computation still cannot be done in 1000 seconds! (Please note that I just require one real instance rather than all solutions.) Does anyone know why?
By the way, since the default SMT solver (in Maple 2023) is Z3, will another SMT solver (like cvc5) be supported in future Maple releases?