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