Unexpected output for universally quantified input

[alebugariu]

The command ddsmt input.smt2 output.smt2 <path_to_z3>, where input.smt2 is:

(set-option :smt.auto-config false)
(set-option :smt.mbqi true)
(set-option :sat.random_seed 488)
(set-option :smt.random_seed 599)
(set-option :nlsat.seed 611)
(set-option :memory_max_size 6000)
(declare-sort T@U 0)
(declare-sort T@T 0)
(declare-fun Ctor (T@T) Int)
(declare-const intType T@T)
(declare-const boolType T@T)
(declare-fun type (T@U) T@T)
(declare-const RefType T@T)
(declare-fun int_2_U (Int) T@U)
(declare-fun bool_2_U (Bool) T@U)
(declare-fun U_2_int (T@U) Int)
(declare-fun MapType1Type (T@T T@T) T@T)
(declare-fun MapType1TypeInv1 (T@T) T@T)
(declare-fun MapType1Select (T@U T@U T@U) T@U)
(declare-fun MapType1Store (T@U T@U T@U T@U) T@U)
(assert (= (Ctor intType) 1))
(assert (= (Ctor boolType) 2))
(assert (forall ((kt0 T@T) (vt0 T@T) ) (! (= (MapType1TypeInv1 (MapType1Type kt0 vt0)) vt0) :pattern ( (MapType1Type kt0 vt0)))))
(assert (forall ((m1 T@U) (k1 T@U) (v1 T@U) ) (! (let ((aVar1 (MapType1TypeInv1 (type m1)))) (= (type (MapType1Select m1 k1 v1)) aVar1)) :pattern ( (MapType1Select m1 k1 v1)))))
(assert (forall ((m2 T@U) (k2 T@U) (x2 T@U) (v2 T@U) ) (! (let ((aVar1@@0 (type v2))) (let ((aVar0@@0 (type k2))) (= (type (MapType1Store m2 k2 x2 v2)) (MapType1Type aVar0@@0 aVar1@@0)))) :pattern ( (MapType1Store m2 k2 x2 v2)))))
(assert (forall ((v3 T@U) (m3 T@U) (k3 T@U) (x3 T@U) (other_k3 T@U) (other_v3 T@U) ) (! (or (= k3 other_k3) (= (MapType1Select (MapType1Store m3 k3 x3 v3) other_k3 other_v3) (MapType1Select m3 other_k3 other_v3))) :pattern ( (MapType1Select (MapType1Store m3 k3 x3 v3) other_k3 other_v3)))))
(assert (forall ((arg4 Int) ) (! (= (type (int_2_U arg4)) intType) :pattern ( (int_2_U arg4)))))
(assert (forall ((arg5 Bool) ) (! (= (type (bool_2_U arg5)) boolType) :pattern ( (bool_2_U arg5)))))
(assert (forall ((arg6 Int) ) (! (= (U_2_int (int_2_U arg6)) arg6) :pattern ( (int_2_U arg6)))))
(check-sat-using smt)

produces the following output:

(assert (forall ((a Bool)) false))
(check-sat-using smt)

I got similar outputs for other (more complex) verification benchmarks and for different versions of Z3. Is this behaviour expected? From my understanding, ddsmt minimizes the input, so I expected to obtain a subset of the input assertions. Thank you very much for your time!

[aniemetz]

ddSMT minimizes the input not line by line, but while simplifying the input while preserving the behavior of the executable. So this is, generally speaking, not unexpected. What is the actual solver output on the original input?

[alebugariu]

The solver output is unsat, both on the original input and on the minimized one. Is it possible to disable the simplification?

[mpreiner]

In your case ddsmt does exactly what it is supposed to do: minimize the input file while preserving the original solver behavior. If the solver returns unsat for the original file, ddsmt minimizes the input file as much as possible, but there is no guarantee that it will preserve any of the original assertions.

If you want to extract an unsatisfiable core, it'd generally better to ask the solver via the SMT-LIB command (get-unsat-core). If you still want to do it with ddsmt (which would definitely be a lot slower), you could try options: --disable-all --erase-node, which still not guarantees to preserve the original assertions, but may get you closer to it. With these options you'd get something like this (last assertion omitted):

(declare-sort T@U)
(declare-sort T@T)
(declare-fun Ctor (T@T) Int)
(declare-const intType T@T)
(declare-const boolType T@T)
(declare-fun type (T@U) T@T)
(declare-fun int_2_U (Int) T@U)
(declare-fun bool_2_U (Bool) T@U)
(declare-fun MapType1Type (T@T T@T) T@T)
(declare-fun MapType1TypeInv1 (T@T) T@T)
(declare-fun MapType1Select (T@U T@U T@U) T@U)
(declare-fun MapType1Store (T@U T@U T@U T@U) T@U)
(assert (= (Ctor intType) 1))
(assert (= (Ctor boolType) 2))
(assert (forall ((kt0 T@T) (vt0 T@T)) (! (= (MapType1TypeInv1 (MapType1Type kt0 vt0)) vt0) :pattern ())))
(assert (forall ((m1 T@U) (k1 T@U) (v1 T@U)) (! (let ((aVar1 (MapType1TypeInv1 (type m1)))) (= (type (MapType1Select m1 k1 v1)) aVar1)) :pattern ())))
(assert (forall ((m2 T@U) (k2 T@U) (x2 T@U) (v2 T@U)) (! (let ((aVar1@@0 (type v2))) (let ((aVar0@@0 (type k2))) (= (type (MapType1Store m2 k2 x2 v2)) (MapType1Type aVar0@@0 aVar1@@0)))) :pattern ())))
(assert (forall ((v3 T@U) (m3 T@U) (k3 T@U) (x3 T@U) (other_k3 T@U) (other_v3 T@U)) (! (or (= (MapType1Select (MapType1Store m3 k3 x3 v3) other_k3 other_v3) (MapType1Select m3 other_k3 other_v3))) :pattern ())))
(assert (forall ((arg4 Int)) (! (= (type (int_2_U arg4)) intType) :pattern ())))
(assert (forall ((arg5 Bool)) (! (= (type (bool_2_U arg5)) boolType) :pattern ())))
(check-sat-using smt)

[alebugariu]

Ok, I will try, thank you very much for all the explanations!