Stack overflow in "src/lib/util/zarithNumbers.ml", line 65, when the CDCL solver is used

[hra687261]

co_2096_l.ae.txt

Running Alt-Ergo on the attached file with:

alt-ergo --sat-solver CDCL co_2096_l.ae

causes a stack overflow in the call to Zarith's gcd function.

The problem is probably in the Zarith library.

[Stevendeo]

It seems Alt-Ergo enters an infinite loop in update_monome (file intervalCalculus.ml, l726 recursively called at l741).

[hra687261]

I don't know if it is an infinite loop. It seems to me that when it instantiates the quantified formulas, it generates terms that contain high degree polynomials and the loop might just take so long that a stack overflow exception is raised.
Running the command with the following debugging options shows how big the generated terms are:

./alt-ergo ./co_2096.ae --sat-solver CDCL --dsat --verbose

[bclement-ocp]

SMT-LIB version:

(set-logic ALL)
(declare-const ui_0 Int)

(assert (exists ((ieqv0 Int)) (forall ((iuqv0 Int)) (= (* ieqv0 ieqv0) iuqv0))))
(assert (forall ((iuqv0 Int)) (>= ui_0 iuqv0)))

(check-sat)

Interestingly the manually skolemized version:

(set-logic ALL)
(declare-const ui_0 Int)

(declare-const ieqv0 Int)
(assert (forall ((iuqv0 Int)) (= (* ieqv0 ieqv0) iuqv0)))
(assert (forall ((iuqv0 Int)) (>= ui_0 iuqv0)))

(check-sat)

doesn't exhibit the behavior, whereas we should expect both to behave in the same way (the automatic skolemization is there for a reason!), but that is probably a different bug. Alt-Ergo responds "I don't know" in this case, even though the problem is unsat in two different ways (there is no constant ieqv0 whose square is equal to all integers, and there is no constant ui_0 that is greater than all integers), but we may not quite have the means to exploit any of these, unfortunately.

[bclement-ocp]

It looks like the runaway loop is due to wrong pattern inference on the first quantifier when under the existential: in the manually skolemized version, the trigger is iuqv0, while in the original version, the triggers are ieqv0 and (* ieqv0 ieqv0). Well, the triggers of the existentials are ieqv0 and (* ieqv0 ieqv0), which I am not entirely sure the meaning of…

In any case, the following completes quickly and does not go into the infinite loop (with an unknown result):

(set-logic ALL)
(declare-const ui_0 Int)

(assert (exists ((ieqv0 Int)) (forall ((iuqv0 Int)) (! (= (* ieqv0 ieqv0) iuqv0) :pattern (iuqv0)))))
(assert (forall ((iuqv0 Int)) (>= ui_0 iuqv0)))

(check-sat)

[bclement-ocp]

It looks like the issue is indeed related to the "triggers of the existential" thing. We do multiple rounds of instantiation. In the first round (where we don't allow inferring variables as triggers), we correctly use the triggers of the skolemized term (= iuqv0 (* !?___sko[]!1 !?___sko[]!1)). In a second round where we do allow inferring variables as triggers (this is needed here), we use the non-skolemized (<sko exists 'iuqv0~4':Int.> (not (= 'iuqv0~4' (* 'ieqv0~3' 'ieqv0~3')))) instead, which is wrong.

The manually skolemized version uses the skolem version everywhere.