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

   1 ; COMMAND-LINE:
   2 ; EXPECT: sat
   3 ; EXPECT: ((pos_int (/ 3 1)) (pos_rat (/ 1 3)) (zero (/ 0 1)) (neg_rat (/ (- 2) 3)) (neg_int (/ (- 2) 1)))
   4 (set-info :smt-lib-version 2.0)
   5 (set-option :produce-models true)
   6 (set-logic QF_LRA)
   7
   8 ; This output changes if the smt2 printer output for Reals changes.
   9 (declare-fun pos_int () Real)
  10 (declare-fun pos_rat () Real)
  11 (declare-fun zero () Real)
  12 (declare-fun neg_rat () Real)
  13 (declare-fun neg_int () Real)
  14
  15 (assert (= pos_int 3))
  16 (assert (= pos_rat (/ 1 3)))
  17 (assert (= zero 0))
  18 (assert (= neg_rat (/ (- 2) 3)))
  19 (assert (= neg_int (- 2)))
  20
  21 (check-sat)
  22 (get-value (pos_int pos_rat zero neg_rat neg_int))