3 ; EXPECT: ((pos_int 5) (pos_real_int_value (/ 3 1)) (pos_rat (/ 1 3)) (zero (/ 0 1)) (neg_rat (/ (- 2) 3)) (neg_real_int_value (/ (- 2) 1)) (neg_int (- 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 Reals_Ints changes.
10 (declare-fun pos_int () Int)
11 (declare-fun pos_real_int_value () Real)
12 (declare-fun pos_rat () Real)
13 (declare-fun zero () Real)
14 (declare-fun neg_rat () Real)
15 (declare-fun neg_real_int_value () Real)
16 (declare-fun neg_int () Int)
18 (assert (= pos_int 5))
19 (assert (= pos_real_int_value 3))
20 (assert (= pos_rat (/ 1 3)))
22 (assert (= neg_rat (/ (- 2) 3)))
23 (assert (= neg_real_int_value (- 2)))
24 (assert (= neg_int (- 6)))
27 (get-value (pos_int pos_real_int_value pos_rat zero neg_rat neg_real_int_value neg_int))