blob: 53337c5d39c84e5813fa4fc8d7e311d11bb17450 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
|
; COMMAND-LINE:
; EXPECT: sat
; EXPECT: ((pos_int 5) (pos_real_int_value 3.0) (pos_rat (/ 1 3)) (zero 0.0) (neg_rat (- (/ 2 3))) (neg_real_int_value (- 2.0)) (neg_int (- 6)))
(set-info :smt-lib-version 2.0)
(set-option :produce-models true)
(set-logic QF_LIRA)
; This output changes if the smt2 printer output for Reals_Ints changes.
(declare-fun pos_int () Int)
(declare-fun pos_real_int_value () Real)
(declare-fun pos_rat () Real)
(declare-fun zero () Real)
(declare-fun neg_rat () Real)
(declare-fun neg_real_int_value () Real)
(declare-fun neg_int () Int)
(assert (= pos_int 5))
(assert (= pos_real_int_value 3))
(assert (= pos_rat (/ 1 3)))
(assert (= zero 0))
(assert (= neg_rat (/ (- 2) 3)))
(assert (= neg_real_int_value (- 2)))
(assert (= neg_int (- 6)))
(check-sat)
(get-value (pos_int pos_real_int_value pos_rat zero neg_rat neg_real_int_value neg_int))
|
