Unexpected result when using transitive closure with quantifier #7602
Description
In the following example the intention is to exhaustively define the relation. The expected result of the assertion is thus UNSAT, since I does not connect to C.
(declare-datatypes () ((Ent A B C D E F H I J K L M)))
(declare-fun rel (Ent Ent) Bool)
(assert (forall ((_a Ent) (_b Ent))
(ite (or
(and (= _a I) (= _b M)) (and (= _a M) (= _b F)) (and (= _a M) (= _b A)) (and (= _a M) (= _b J))
(and (= _a J) (= _b A)) (and (= _a J) (= _b F)) (and (= _a J) (= _b B)) (and (= _a K) (= _b C)))
(rel _a _b)
(not (rel _a _b)))
))
(assert ((_ transitive-closure rel) I C))
(check-sat)
(assert ((_ transitive-closure rel) I C))
(check-sat)
The result, however is SAT for the first assertion and UNSAT for the following one, even though they are the same.
The model for SAT was as follows:
(
(define-fun rel ((x!0 Ent) (x!1 Ent)) Bool
(ite (and (= x!0 I) (= x!1 C)) false
(ite (and (= x!0 I) (= x!1 M)) true
(ite (and (= x!0 M) (= x!1 C)) false
(ite (and (= x!0 A) (= x!1 E)) false
(ite (and (= x!0 M) (= x!1 A)) true
(ite (and (= x!0 A) (= x!1 C)) false
(ite (and (= x!0 M) (= x!1 K)) false
(ite (and (= x!0 A) (= x!1 H)) false
(ite (and (= x!0 A) (= x!1 J)) false
(ite (and (= x!0 A) (= x!1 L)) false
(let ((a!1 (not (or (not (= x!0 I)) (not (= x!1 M)))))
(a!2 (not (or (not (= x!0 M)) (not (= x!1 F)))))
(a!3 (not (or (not (= x!0 M)) (not (= x!1 A)))))
(a!4 (not (or (not (= x!0 M)) (not (= x!1 J)))))
(a!5 (not (or (not (= x!0 J)) (not (= x!1 B)))))
(a!6 (not (or (not (= x!0 K)) (not (= x!1 C)))))
(a!7 (not (or (not (= x!0 J)) (not (= x!1 F)))))
(a!8 (not (or (not (= x!0 J)) (not (= x!1 A))))))
(or a!1 a!2 a!3 a!4 a!5 a!6 a!7 a!8)))))))))))))
(define-fun specrel.next!!0 ((x!0 Ent) (x!1 Ent)) Ent
(ite (and (= x!0 M) (= x!1 C)) A
(ite (and (= x!0 A) (= x!1 C)) B
(ite (and (= x!0 B) (= x!1 C)) E
M))))
)
Moreover, if any of the AND clauses are removed from the body of the quantifier, the result becomes UNSAT, UNSAT as expected. We have noted this behaviour in several examples but the above is the smallest we could extract.
The results have been obtained using Z3 version 4.14.1 - 64 bit