Hi Makarius,
Compared to „argo“ the „smt“ method is more powerful since it supports
quantifiers as well as linear natural and integer arithmetic. For the moment,
argo is not capable of proving problems that require both equality reasoning
and linear real arithmetic. This combination of theories is no problem for
„smt“.
I would mark „old-smt“ as legacy for the coming release and remove it right
after the release fork. Please also consider Jasmin’s opinion on this case.
Indeed, the names sound similar, but this is a coincidence as there is no
relation to „alt-ergo“.
Cheers,
Sascha
Von: Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
