According to the SMT-LIB definition of theory of Ints, operator minus is left associative. This means that it is allowed to create a function application of minus to more than two arguments. This is then a syntactic sugar that applies the operator recursively first to all the arguments except the last one and then apply the operator to the result and the last argument.
As @aehyvari pointed out, we can treat expression (- t1 t2 t3 ... tn) as (+ t1 (- t2) (- t3) ... (- tn)).
According to the SMT-LIB definition of theory of Ints, operator minus is left associative. This means that it is allowed to create a function application of minus to more than two arguments. This is then a syntactic sugar that applies the operator recursively first to all the arguments except the last one and then apply the operator to the result and the last argument.
As @aehyvari pointed out, we can treat expression
(- t1 t2 t3 ... tn)as(+ t1 (- t2) (- t3) ... (- tn)).Fixes #690.