Simple ADT test with different behavior with or without push

[Stevendeo]

The following test have a different behavior given if the push instruction is here or not:

File test_adt.smt2

(set-logic ALL)
(declare-datatype t ((A) (B) (C (i Int))))

(declare-const e t)

(push 1)
(assert (not ((_ is A) e)))
(assert (not ((_ is B) e)))
(assert (not (exists ((n Int)) (= e (C n)))))
(check-sat)

Command: alt-ergo test_adt.smt2 --enable-assertions --output smtlib2 --sat-solver CDCL --no-minimal-bj

Without the push, alt-ergo returns unsat (as expected); with the push, it never returns.

The culplrit may be the presence of the existential quantifier and --no-minimal-bj; remove the option and everything works fine. This test is a translation of goal g_valid_5_1 of tests/adts/simple_1.ae.

[bclement-ocp]

The following test have a different behavior given if the push instruction is here or not:

Can you clarify what behavior is different and if either behavior is incorrect/unsound?

[Stevendeo]

Oh you're right I forgot about it: with the push it does not return, while without it returns unsat (as expected). So it's not an unsoundness issue.

[bclement-ocp]

Interesting. I actually don't understand how we prove this in the first place…

Here is a simpler example that we are able to prove:

(set-logic ALL)
(declare-datatype t ((A) (B (i Int))))

(declare-const e t)

(assert ((_ is B) e))
(assert (forall ((n Int)) (distinct e (B n))))
(check-sat)

Here is an even simpler example that we are not able to prove anymore, because the type gets converted to a record:

(set-logic ALL)
(declare-datatype t ((B (i Int))))

(declare-const e t)

(assert ((_ is B) e))
(assert (forall ((n Int)) (distinct e (B n))))
(check-sat)

So the ADT theory must be doing something weird… Pinging @Halbaroth who has been looking at ADTs.