test/regress/regress0/get-value-ints.smt2

   1 ; COMMAND-LINE:
   2 ; EXPECT: sat
   3 ; EXPECT: ((pos 1) (zero 0) (neg (- 6)))
   4 (set-info :smt-lib-version 2.0)
   5 (set-option :produce-models true)
   6 (set-logic QF_LIA)
   7
   8 ; This output changes if the smt2 printer output for Ints changes.
   9
  10 (declare-fun pos () Int)
  11 (declare-fun zero () Int)
  12 (declare-fun neg () Int)
  13
  14 (assert (= pos 1))
  15 (assert (= zero 0))
  16 (assert (= neg (- 6)))
  17
  18 (check-sat)
  19 (get-value (pos zero neg))