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 

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“.


Von: Makarius
isabelle-dev mailing list

Reply via email to