test/regress/regress0/bug421b.smt2

   1 ; same as bug421.smt2 but adds --check-models on command line:
   2 ; this actually caused the same bug for a different reason, so
   3 ; we check them both independently in regressions
   4 ;
   5 ; COMMAND-LINE: --incremental --abstract-values --check-models
   6 ; EXPECT: sat
   7 ; EXPECT: ((a (as @1 (Array Int Int))) (b (as @2 (Array Int Int))))
   8 (set-logic QF_AUFLIA)
   9 (set-option :produce-models true)
  10 (declare-fun a () (Array Int Int))
  11 (declare-fun b () (Array Int Int))
  12 (assert (not (= a b)))
  13 (check-sat)
  14 (get-value (a b))