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.
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 filede-bruijn-bug.smt2
, the model generated is different from the expected answer.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.