3 ; EXPECT: ((pos 1) (zero 0) (neg (- 6)))
4 (set-info :smt-lib-version 2.0)
5 (set-option :produce-models true)
8 ; This output changes if the smt2 printer output for Ints changes.
10 (declare-fun pos () Int)
11 (declare-fun zero () Int)
12 (declare-fun neg () Int)
16 (assert (= neg (- 6)))
19 (get-value (pos zero neg))