Rebase master onto Scala 2.13

[sankalpgambhir]

Don't merge, yet.

Bringing the Scala 2.13 branch up to speed with recent fixes and improvements.

The CI will fail. There is one issue in the horn-adt tests. On the file de-bruijn-bug.smt2, the model generated is different from the expected answer.

107c107
<     (define-fun p ((A f) (B d1) (C f)) Bool (or (or (and (and (= (_size A) (_size C)) (= (_size B) 1)) (>= (_size C) 1)) (and (and (and (is-b B) (= (_size B) 3)) (and (>= (_size A) 1) (>= (_size C) 1))) (is-b B))) (and (and (and (is-b B) (and (and (and (and (or (and (is-g A) (>= (_size B) 4)) (and (is-h A) (>= (+ (- 1) (_size B)) 4))) (or (and (is-g A) (>= (_size B) 5)) (and (is-h A) (>= (+ 1 (_size B)) 5)))) (>= (+ (_size A) (_size B)) 6)) (>= (_size A) 1)) (>= (_size C) 1))) (is-b B)) (= (mod (+ 1 (_size B)) 2) 0))))
---
>     (define-fun p ((A f) (B d1) (C f)) Bool (or (or (and (and (= (_size A) (_size C)) (= (_size B) 1)) (>= (_size C) 1)) (and (and (and (is-b B) (= (_size B) 3)) (and (>= (_size A) 1) (>= (_size C) 1))) (is-b B))) (and (and (and (is-b B) (and (and (and (or (and (is-g A) (>= (_size B) 4)) (and (is-h A) (>= (+ (- 1) (_size B)) 4))) (or (and (is-g A) (>= (_size B) 5)) (and (is-h A) (>= (+ 1 (_size B)) 5)))) (>= (_size A) 1)) (>= (_size C) 1))) (is-b B)) (= (mod (+ 1 (_size B)) 2) 0))))

Notably, if the test is run without -assert, it matches the answer, but as the tests are run with -assert, the model is a bit different.

I have had eldarica test that both models satisfy the clauses by inserting the defs into the smt2 file.

I have no problem with replacing this modified model as the new expected answer, other than that I don't understand why running under -assert would affect the model at all. I have had a quick look at the usage of the -assert option internally with little success.

I have additionally requested that CI be run for the Scala 2.13 branch, since I do want it to be stable and depend on it.