test/regress/regress0/print_model.cvc.smt2


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20

; COMMAND-LINE: --produce-models
; EXPECT: sat
; EXPECT: (
; EXPECT: (define-fun s1 () Int 2)
; EXPECT: (define-fun s2 () Int 1)
; EXPECT: )
(set-logic ALL)
(set-option :incremental true)
(set-option :produce-models true)
(declare-fun s1 () Int)
(declare-fun s2 () Int)
(assert (= s1 2))
(push 1)

(assert (and (> s2 0) (< s2 s1)))

(check-sat)
(get-model)

(pop 1)