ArithLogic: Fix handling of minus operator with more than two arguments

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

regression/QF_LIA/issue_690.smt2

@@ -0,0 +1,4 @@
+(set-logic QF_LIA)
+(set-info :status sat)
+(assert (= 0 (- 3 2 1)))
+(check-sat)

regression/QF_LIA/issue_690.smt2.expected.out

@@ -0,0 +1 @@
+sat

src/logics/ArithLogic.cc

@@ -560,12 +560,9 @@ PTRef ArithLogic::mkMinus(vec<PTRef> && args)
     if (args.size() == 1) {
         return mkNeg(args[0]);
     }
-    assert(args.size() == 2);
-    if (args.size() > 2) { throw OsmtApiException("Too many terms provided to LALogic::mkNumMinus"); }
-
-    PTRef fact = mkNeg(args[1]);
-    assert(fact != PTRef_Undef);
-    args[1] = fact;
+    // Minus is left associative according to SMT-LIB
+    for (int i = 1; i < args.size(); ++i)
+        args[i] = mkNeg(args[i]);
     return mkPlus(std::move(args));
 }