produce-unsat-cores affects convergence

[mtzguido]

The following file reliably returns unsat in the current HEAD. Removing the line to enable production of unsat cores makes this reliably return unknown (incomplete quantifiers). Not sure if this is expected behavior or not.

Also I noticed that trying to disable produce-unsat-cores (e.g. by uncommenting the 2nd line) is a no-op, so it will return unsat in this example and we can get an unsat core out. Probably a warning (or even error) would be useful here-- if that makes sense to you I could take a stab at writing a patch.

(set-option :produce-unsat-cores true)
; (set-option :produce-unsat-cores false)
(set-option :smt.mbqi false)
(declare-sort T)
(declare-datatypes () ((F (Z))))
(declare-fun M () F)
(declare-fun V (T) Bool)
(declare-fun H (F T T) Bool)
(declare-fun A (T T) T)
(declare-fun T () T)
(declare-fun S (T T) T)
(declare-fun FS () T)
(push)
(declare-fun F (T T) T)
(declare-fun F (T T T T) T)
(declare-fun S (T T T T) T)
(assert (forall ((x T)) (= (F T T) (A (A FS T) x))))
(assert (forall ((@ T) (x T) (x2 T) (@x T)) (! (and (implies (and (V (F x x x x2))) (V (S x2 x2 x2 x2)))) :pattern ((S @ x x2 @x)) :qid equation_FStar.PCM.frame_preserving)))
(assert (forall ((x T) (x2 T)) (= (S T T) (F x2 x x2 T))))
(assert (forall ((x T) (x2 T)) (= (V (S x x x2 x)) (exists ((@ T)) (= x2 (F @ x @ x2))))))
(declare-fun Tm (T T T) T)
(assert (forall ((x T) (x2 T)) (iff (H M x (Tm x2 x2 x)) (and (V (A x2 (A (F x2 x2) x2)))))))
(declare-fun m (T T T) T)
(assert (forall ((x T) (x2 T)) (iff (and (V (S x x))) (H M x2 (m x2 x2 x)))))
(assert (! (exists ((x T) (x2 T)) (not (implies true (and (implies (and (H M x2 (m x2 x2 T))) (or (V (S x2 x2 T x2)))) (implies (and (V (S x2 x2)) (V (S x2 x)) (H M x2 (Tm T T x2))) (or (V (A T (A (A (A FS T) (S x2 x2)) T))))))))) :named @query))
(check-sat)
(get-info :reason-unknown)